def rk215.instModuleResidueFieldSubtypeCarrierMemIdealKerAlgHomHom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : Module (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)

Equations

• rk215.instModuleResidueFieldSubtypeCarrierMemIdealKerAlgHomHom p = ⋯.module

theorem rk215.instIsScalarTowerResidueFieldSubtypeCarrierMemIdealKerAlgHomHom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : IsScalarTower Λ (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)

theorem rk215.residueField_smul {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (r : Λ) (x : ↥(RingHom.ker p.hom)) : (IsLocalRing.residue Λ) r • x = r • x

@[simp]

theorem rk215.preimage_smul {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (r : ↑B) (x : ↥(RingHom.ker p.hom)) : IsResidueAlgebra.preimage Λ r • x = r • x

instance rk215.instFiniteSubtypeCarrierMemIdealKerAlgHomHom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) : Module.Finite Λ ↥(RingHom.ker p.hom)

instance rk215.instFiniteResidueFieldSubtypeCarrierMemIdealKerAlgHomHom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : Module.Finite (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)

def rk215.hom1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) : pullbackinC p p ⟶ B

Equations

• rk215.hom1 p = fstinC p p

theorem rk215.mem_kerp {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) (x : ↑(pullbackinC p p)) : (↑x).2 - (↑x).1 ∈ RingHom.ker p.hom

@[simp]

theorem rk215.subtype_zero (R : Type u_1) [Ring R] (J : Ideal R) (h : 0 ∈ J) : ⟨0, h⟩ = 0

noncomputable def rk215.hom2_alghom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : ↑(pullbackinC p p) →ₐ[Λ] ↑(Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))

Equations

• One or more equations did not get rendered due to their size.

noncomputable def rk215.hom2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : pullbackinC p p ⟶ Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))

Equations

• rk215.hom2 p = Deformation.ArtinResAlg.ofHom (rk215.hom2_alghom p)

noncomputable def rk215.hom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : pullbackinC p p ⟶ Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))

Equations

• rk215.hom p = Deformation.productlift (rk215.hom1 p) (rk215.hom2 p)

noncomputable def rk215.inv1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) ⟶ B

Equations

• rk215.inv1 p = (Deformation.productcone B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))).fst

@[simp]

theorem rk215.inv1_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (x : ↑(Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))))) : (inv1 p).hom x = (↑x).1

theorem Module.IsTorsionBySet.zero_of_mem (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set R) (h : IsTorsionBySet R M s) (r : R) (x : M) (hr : r ∈ s) : r • x = 0

noncomputable def rk215.inv2_alghom {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : ↑(Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) →ₐ[Λ] ↑B

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem rk215.inv2_alghom_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (x : ↑(Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))))) : (inv2_alghom p) x = (fstinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField).hom x + ↑((TrivSqZeroExt.sndHom (IsLocalRing.ResidueField Λ) ↑(FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) ((sndinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField).hom x))

noncomputable def rk215.inv2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) ⟶ B

Equations

• rk215.inv2 p = Deformation.ArtinResAlg.ofHom (rk215.inv2_alghom p)

@[simp]

theorem rk215.inv2_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (x : ↑(Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))))) : (inv2 p).hom x = (↑x).1 + ↑(↑x).2.2

theorem rk215.inv2_zero {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : CategoryTheory.CategoryStruct.comp (Deformation.productlift (CategoryTheory.CategoryStruct.id B) (Deformation.zero_map' (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)) B)) (inv2 p) = CategoryTheory.CategoryStruct.id B

theorem rk215.inv12comm {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : CategoryTheory.CategoryStruct.comp (inv1 p) p = CategoryTheory.CategoryStruct.comp (inv2 p) p

noncomputable def rk215.inv {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) ⟶ pullbackinC p p

Equations

• rk215.inv p = pullbackinC_lift (CategoryTheory.Limits.PullbackCone.mk (rk215.inv1 p) (rk215.inv2 p) ⋯)

theorem rk215.trivsqfst_eq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : Deformation.ArtinResAlg.ofHom (TrivSqZeroExt.fstHom Λ (IsLocalRing.ResidueField Λ) ↑(FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) = (Deformation.ArtinResAlg.of Λ (TrivSqZeroExt (IsLocalRing.ResidueField Λ) ↑(FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))).toResidueField

theorem rk215.trivsqfst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (x : ↑(Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : TrivSqZeroExt.fst x = (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField.hom x

noncomputable def rk215.iso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : pullbackinC p p ≅ Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))

Equations

• rk215.iso p = { hom := rk215.hom p, inv := rk215.inv p, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem rk215.iso_hom_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : CategoryTheory.CategoryStruct.comp (iso p).hom (fstinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField) = fstinC p p

@[simp]

theorem rk215.iso_inv_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : CategoryTheory.CategoryStruct.comp (iso p).inv (fstinC p p) = fstinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField

@[simp]

theorem rk215.iso_hom_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : CategoryTheory.CategoryStruct.comp (iso p).hom (sndinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField) = hom2 p

@[simp]

theorem rk215.iso_inv_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] : CategoryTheory.CategoryStruct.comp (iso p).inv (sndinC p p) = inv2 p

def rk215.auxiso1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] : F.obj (Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) ≅ F.obj B × F.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem rk215.auxiso1_hom_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : CategoryTheory.CategoryStruct.comp (auxiso1 p F).hom Prod.fst = F.map (fstinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField)

@[simp]

theorem rk215.auxiso1_hom_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : CategoryTheory.CategoryStruct.comp (auxiso1 p F).hom Prod.snd = F.map (sndinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField)

@[simp]

theorem rk215.auxiso1_inv_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : CategoryTheory.CategoryStruct.comp (auxiso1 p F).inv (F.map (fstinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField)) = Prod.fst

@[simp]

theorem rk215.auxiso1_inv_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : CategoryTheory.CategoryStruct.comp (auxiso1 p F).inv (F.map (sndinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField)) = Prod.snd

@[simp]

theorem rk215.auxiso1_hom_fst_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (x : F.obj (Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))))) : ((auxiso1 p F).hom x).1 = F.map (fstinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField) x

@[simp]

theorem rk215.auxiso1_hom_snd_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (x : F.obj (Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))))) : ((auxiso1 p F).hom x).2 = F.map (sndinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField) x

@[simp]

theorem rk215.auxiso1_inv_fst_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (x : F.obj B × F.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : F.map (fstinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField) ((auxiso1 p F).inv x) = x.1

@[simp]

theorem rk215.auxiso1_inv_snd_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (x : F.obj B × F.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : F.map (sndinC B.toResidueField (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))).toResidueField) ((auxiso1 p F).inv x) = x.2

def rk215.auxmap2 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) : F.obj (pullbackinC p p) ⟶ CategoryTheory.Limits.Types.PullbackObj (F.map p) (F.map p)

Equations

• One or more equations did not get rendered due to their size.

def rk215.action {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : F.obj B × F.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) → CategoryTheory.Limits.Types.PullbackObj (F.map p) (F.map p)

Equations

• rk215.action p F = CategoryTheory.CategoryStruct.comp (rk215.auxiso1 p F).inv (CategoryTheory.CategoryStruct.comp (F.map (rk215.iso p).inv) (rk215.auxmap2 p F))

theorem rk215.action_fst' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : CategoryTheory.CategoryStruct.comp (action p F) (CategoryTheory.Limits.Types.pullbackCone (F.map p) (F.map p)).fst = Prod.fst

@[simp]

theorem rk215.action_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (x : F.obj B × F.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : (↑(action p F x)).1 = x.1

@[simp]

theorem rk215.action_snd' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : CategoryTheory.CategoryStruct.comp (action p F) (CategoryTheory.Limits.Types.pullbackCone (F.map p) (F.map p)).snd = CategoryTheory.CategoryStruct.comp (auxiso1 p F).inv (F.map (inv2 p))

@[simp]

theorem rk215.action_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (x : F.obj B × F.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : (↑(action p F x)).2 = F.map (inv2 p) ((auxiso1 p F).inv x)

theorem rk215.action_surj {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) (h : Function.Surjective ⇑p.hom) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H1 F] : Function.Surjective (action p F)

theorem rk215.action_bij {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H4 F] : Function.Bijective (action p F)

def rk215.app1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : G ⟶ F) : G.obj B × G.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) → F.obj B × F.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))

Equations

• rk215.app1 p η x = (η.app B x.1, η.app (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) x.2)

@[simp]

theorem rk215.app1_snd {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : G ⟶ F) (a✝ : G.obj B × G.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : (app1 p η a✝).2 = η.app (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) a✝.2

@[simp]

theorem rk215.app1_fst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : G ⟶ F) (a✝ : G.obj B × G.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : (app1 p η a✝).1 = η.app B a✝.1

theorem rk215.app1_def {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : G ⟶ F) (x : G.obj B × G.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : app1 p η x = (η.app B x.1, η.app (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))) x.2)

def rk215.app2 {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : G ⟶ F) : CategoryTheory.Limits.Types.PullbackObj (G.map p) (G.map p) → CategoryTheory.Limits.Types.PullbackObj (F.map p) (F.map p)

Equations

• rk215.app2 p η x = ⟨(η.app B (↑x).1, η.app B (↑x).2), ⋯⟩

@[simp]

theorem rk215.app2_coe {Λ : Type u} [CommRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : G ⟶ F) (a✝ : CategoryTheory.Limits.Types.PullbackObj (G.map p) (G.map p)) : ↑(app2 p η a✝) = (η.app B (↑a✝).1, η.app B (↑a✝).2)

theorem rk215.appcomm_aux {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] {G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 G] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) G] (η : G ⟶ F) : CategoryTheory.CategoryStruct.comp (app1 p η) (auxiso1 p F).inv = CategoryTheory.CategoryStruct.comp (auxiso1 p G).inv (η.app (Deformation.pullbackproduct B (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))))

theorem rk215.appcomm {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] {G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 G] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) G] (η : G ⟶ F) (x : G.obj B × G.obj (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom)))) : action p F (app1 p η x) = app2 p η (action p G x)

theorem rk215.exist_of_surj {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) (h : Function.Surjective ⇑p.hom) [IsSmallExtension p] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] {G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 G] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) G] (η : G ⟶ F) [H1 F] (h' : Function.Surjective (η.app (Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) ↥(RingHom.ker p.hom))))) (x1 : G.obj B) (x2 : F.obj B) (h12 : F.map p (η.app B x1) = F.map p x2) : ∃ (y : G.obj B), G.map p y = G.map p x1 ∧ η.app B y = x2

theorem rk215.action_zero {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {A B : Deformation.ArtinResAlg Λ} (p : B ⟶ A) [IsSmallExtension p] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (x : F.obj B) : (↑(action p F (x, 0))).2 = x