noncomputable def Deformation.pullbackproduct {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : ArtinResAlg Λ

Equations

• Deformation.pullbackproduct X Y = pullbackinC X.toResidueField Y.toResidueField

noncomputable def Deformation.productcone {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : CategoryTheory.Limits.BinaryFan X Y

Equations

• Deformation.productcone X Y = CategoryTheory.Limits.BinaryFan.mk (fstinC X.toResidueField Y.toResidueField) (sndinC X.toResidueField Y.toResidueField)

noncomputable def Deformation.islimitproduct {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : CategoryTheory.Limits.IsLimit (productcone X Y)

Equations

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

noncomputable def Deformation.productlift {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {W X Y : ArtinResAlg Λ} (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ pullbackproduct X Y

Equations

• Deformation.productlift f g = (Deformation.islimitproduct X Y).lift (CategoryTheory.Limits.BinaryFan.mk f g)

@[simp]

theorem Deformation.productlift_fst (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {W X Y : ArtinResAlg Λ} (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (productlift f g) (productcone X Y).fst = f

@[simp]

theorem Deformation.productlift_snd (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {W X Y : ArtinResAlg Λ} (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (productlift f g) (productcone X Y).snd = g

@[simp]

theorem Deformation.productlift_fstinC (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {W X Y : ArtinResAlg Λ} (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (productlift f g) (fstinC X.toResidueField Y.toResidueField) = f

@[simp]

theorem Deformation.productlift_sndinC (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {W X Y : ArtinResAlg Λ} (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (productlift f g) (sndinC X.toResidueField Y.toResidueField) = g

@[simp]

theorem Deformation.productcone_fst (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {X Y : ArtinResAlg Λ} : (productcone X Y).fst = fstinC X.toResidueField Y.toResidueField

@[simp]

theorem Deformation.productcone_snd (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {X Y : ArtinResAlg Λ} : (productcone X Y).snd = sndinC X.toResidueField Y.toResidueField

@[simp]

theorem Deformation.productlift_fstinC_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {W X Y : ArtinResAlg Λ} (f : W ⟶ X) (g : W ⟶ Y) (x : ↑W) : (↑((productlift f g).hom x)).1 = f.hom x

@[simp]

theorem Deformation.productlift_sndinC_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] {W X Y : ArtinResAlg Λ} (f : W ⟶ X) (g : W ⟶ Y) (x : ↑W) : (↑((productlift f g).hom x)).2 = g.hom x

noncomputable def Deformation.prodiso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : X ⨯ Y ≅ pullbackproduct X Y

Equations

• Deformation.prodiso X Y = CategoryTheory.Limits.limit.isoLimitCone { cone := Deformation.productcone X Y, isLimit := Deformation.islimitproduct X Y }

@[simp]

theorem Deformation.prodiso_hom_fst (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : CategoryTheory.CategoryStruct.comp (prodiso X Y).hom (fstinC X.toResidueField Y.toResidueField) = CategoryTheory.Limits.prod.fst

@[simp]

theorem Deformation.prodiso_hom_snd (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : CategoryTheory.CategoryStruct.comp (prodiso X Y).hom (sndinC X.toResidueField Y.toResidueField) = CategoryTheory.Limits.prod.snd

@[simp]

theorem Deformation.prodiso_inv_fst (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : CategoryTheory.CategoryStruct.comp (prodiso X Y).inv CategoryTheory.Limits.prod.fst = fstinC X.toResidueField Y.toResidueField

@[simp]

theorem Deformation.prodiso_inv_snd (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : CategoryTheory.CategoryStruct.comp (prodiso X Y).inv CategoryTheory.Limits.prod.snd = sndinC X.toResidueField Y.toResidueField

theorem Deformation.product_toResidueField {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : CategoryTheory.CategoryStruct.comp (fstinC X.toResidueField Y.toResidueField) X.toResidueField = CategoryTheory.CategoryStruct.comp (sndinC X.toResidueField Y.toResidueField) Y.toResidueField

theorem Deformation.product_residue {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y : ArtinResAlg Λ} (x : ↑(pullbackproduct X Y)) : X.toResidueField.hom (↑x).1 = Y.toResidueField.hom (↑x).2

theorem Deformation.product_toResidueField1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (X Y : ArtinResAlg Λ) : (pullbackproduct X Y).toResidueField = CategoryTheory.CategoryStruct.comp (fstinC X.toResidueField Y.toResidueField) X.toResidueField

theorem Deformation.product_residue1 {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X Y : ArtinResAlg Λ} (x : ↑(pullbackproduct X Y)) : (pullbackproduct X Y).toResidueField.hom x = X.toResidueField.hom (↑x).1

noncomputable def Deformation.instModuleCarrierResidueField_schlessinger (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : Module Λ ↑M

Equations

• Deformation.instModuleCarrierResidueField_schlessinger Λ M = RestrictScalars.module Λ (IsLocalRing.ResidueField Λ) ↑M

theorem Deformation.instIsScalarTowerResidueFieldCarrier_schlessinger (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : IsScalarTower Λ (IsLocalRing.ResidueField Λ) ↑M

noncomputable def Deformation.instModuleMulOppositeResidueFieldCarrier_schlessinger (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : Module (IsLocalRing.ResidueField Λ)ᵐᵒᵖ ↑M

Equations

• Deformation.instModuleMulOppositeResidueFieldCarrier_schlessinger Λ M = Commutative.RightModule.instModuleMulOpposite_schlessinger (IsLocalRing.ResidueField Λ) ↑M

theorem Deformation.instIsCentralScalarResidueFieldCarrier_schlessinger (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : IsCentralScalar (IsLocalRing.ResidueField Λ) ↑M

noncomputable def Deformation.tsze_C (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : ArtinResAlg Λ

Equations

• Deformation.tsze_C Λ M = Deformation.ArtinResAlg.of Λ (TrivSqZeroExt (IsLocalRing.ResidueField Λ) ↑M)

theorem Deformation.eq_tsze_C (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : ArtinResAlg.of Λ (TrivSqZeroExt (IsLocalRing.ResidueField Λ) ↑M) = tsze_C Λ M

noncomputable def Deformation.tsze_C_fst (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : tsze_C Λ M ⟶ ArtinResAlg.residueField

Equations

• Deformation.tsze_C_fst Λ M = Deformation.ArtinResAlg.ofHom (TrivSqZeroExt.fstHom Λ (IsLocalRing.ResidueField Λ) ↑M)

@[simp]

theorem Deformation.tsze_C_fst_hom_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (x : TrivSqZeroExt (IsLocalRing.ResidueField Λ) ↑M) : (tsze_C_fst Λ M).hom x = x.fst

theorem Deformation.tsze_C_fst_hom (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : tsze_C_fst Λ M = (tsze_C Λ M).toResidueField

noncomputable def Deformation.tsze_C_inl (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : ArtinResAlg.residueField ⟶ tsze_C Λ M

Equations

• Deformation.tsze_C_inl Λ M = Deformation.ArtinResAlg.ofHom (AlgHom.restrictScalars Λ (Algebra.ofId (IsLocalRing.ResidueField Λ) (TrivSqZeroExt (IsLocalRing.ResidueField Λ) ↑M)))

@[simp]

theorem Deformation.tsze_C_inl_hom_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (a✝ : IsLocalRing.ResidueField Λ) : (tsze_C_inl Λ M).hom a✝ = (Algebra.ofId (IsLocalRing.ResidueField Λ) (TrivSqZeroExt (IsLocalRing.ResidueField Λ) ↑M)) a✝

theorem Deformation.tsze_C_inl_hom (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (x : IsLocalRing.ResidueField Λ) : (tsze_C_inl Λ M).hom x = TrivSqZeroExt.inl x

theorem Deformation.tsze_fst_eq_residue (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (x : ↑(tsze_C Λ M)) : TrivSqZeroExt.fst x = (tsze_C Λ M).toResidueField.hom x

theorem Deformation.lem1' (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (f : tsze_C Λ M ⟶ tsze_C Λ N) (x : ↑(tsze_C Λ M)) : TrivSqZeroExt.fst x = TrivSqZeroExt.fst (f.hom x)

theorem Deformation.lem1 (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (f : tsze_C Λ M ⟶ tsze_C Λ N) (x : IsLocalRing.ResidueField Λ) : x = TrivSqZeroExt.fst (f.hom (TrivSqZeroExt.inl x))

theorem Deformation.lem2 (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (f : tsze_C Λ M ⟶ tsze_C Λ N) (x : IsLocalRing.ResidueField Λ) : 0 = TrivSqZeroExt.snd (f.hom (TrivSqZeroExt.inl x))

theorem Deformation.lem3 (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (f : tsze_C Λ M ⟶ tsze_C Λ N) (x : ↑M) : 0 = TrivSqZeroExt.fst (f.hom (TrivSqZeroExt.inr x))

noncomputable def Deformation.tsze_C_map {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {M N : FGModuleCat (IsLocalRing.ResidueField Λ)} (f : ↑M →ₗ[IsLocalRing.ResidueField Λ] ↑N) : tsze_C Λ M ⟶ tsze_C Λ N

Equations

• Deformation.tsze_C_map f = Deformation.ArtinResAlg.ofHom (AlgHom.restrictScalars Λ (TrivSqZeroExt.map f))

@[simp]

theorem Deformation.tsze_C_map_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (f : ↑M →ₗ[IsLocalRing.ResidueField Λ] ↑N) (x : ↑(tsze_C Λ M)) : (tsze_C_map f).hom x = (TrivSqZeroExt.map f) x

noncomputable def Deformation.tsze_functor {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] : CategoryTheory.Functor (FGModuleCat (IsLocalRing.ResidueField Λ)) (ArtinResAlg Λ)

Equations

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

@[simp]

theorem Deformation.tsze_functor_map {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X✝ Y✝ : FGModuleCat (IsLocalRing.ResidueField Λ)} (f : X✝ ⟶ Y✝) : tsze_functor.map f = tsze_C_map (ModuleCat.Hom.hom f)

@[simp]

theorem Deformation.tsze_functor_obj {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : tsze_functor.obj M = tsze_C Λ M

noncomputable def Deformation.fstHom_C (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : tsze_C Λ M ⟶ ArtinResAlg.of Λ (IsLocalRing.ResidueField Λ)

Equations

• Deformation.fstHom_C Λ M = Deformation.ArtinResAlg.ofHom (TrivSqZeroExt.fstHom Λ (IsLocalRing.ResidueField Λ) ↑M)

theorem Deformation.hom_comp_fst_eq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {M N : FGModuleCat (IsLocalRing.ResidueField Λ)} {A : ArtinResAlg Λ} (f : A ⟶ tsze_C Λ M) (g : A ⟶ tsze_C Λ N) : CategoryTheory.CategoryStruct.comp f (fstHom_C Λ M) = CategoryTheory.CategoryStruct.comp g (fstHom_C Λ N)

theorem Deformation.fst_eq {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {M N : FGModuleCat (IsLocalRing.ResidueField Λ)} {A : ArtinResAlg Λ} (f : A ⟶ tsze_C Λ M) (g : A ⟶ tsze_C Λ N) (x : ↑A) : TrivSqZeroExt.fst (f.hom x) = TrivSqZeroExt.fst (g.hom x)

noncomputable def Deformation.prodfst (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (N : FGModuleCat (IsLocalRing.ResidueField Λ)) : FGModuleCat.of (IsLocalRing.ResidueField Λ) (↑M × ↑N) ⟶ FGModuleCat.of (IsLocalRing.ResidueField Λ) ↑M

Equations

• Deformation.prodfst Λ M N = FGModuleCat.ofHom (LinearMap.fst (IsLocalRing.ResidueField Λ) ↑M ↑N)

noncomputable def Deformation.prodsnd (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (N : FGModuleCat (IsLocalRing.ResidueField Λ)) : FGModuleCat.of (IsLocalRing.ResidueField Λ) (↑M × ↑N) ⟶ FGModuleCat.of (IsLocalRing.ResidueField Λ) ↑N

Equations

• Deformation.prodsnd Λ M N = FGModuleCat.ofHom (LinearMap.snd (IsLocalRing.ResidueField Λ) ↑M ↑N)

noncomputable def Deformation.tsze_prod_cone (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) : CategoryTheory.Limits.BinaryFan (tsze_C Λ M) (tsze_C Λ N)

Equations

• Deformation.tsze_prod_cone Λ M N = CategoryTheory.Limits.BinaryFan.mk (Deformation.tsze_functor.map (Deformation.prodfst Λ M N)) (Deformation.tsze_functor.map (Deformation.prodsnd Λ M N))

@[simp]

theorem Deformation.tsze_prod_cone_π_app (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (x✝ : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (tsze_prod_cone Λ M N).π.app x✝ = match x✝.as with | CategoryTheory.Limits.WalkingPair.left => tsze_C_map (LinearMap.fst (IsLocalRing.ResidueField Λ) ↑M ↑N) | CategoryTheory.Limits.WalkingPair.right => tsze_C_map (LinearMap.snd (IsLocalRing.ResidueField Λ) ↑M ↑N)

@[simp]

theorem Deformation.tsze_prod_cone_pt_carrier (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) : ↑(tsze_prod_cone Λ M N).pt = TrivSqZeroExt (IsLocalRing.ResidueField Λ) (↑M × ↑N)

noncomputable def Deformation.tsze_prod_lift (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (s : CategoryTheory.Limits.BinaryFan (tsze_C Λ M) (tsze_C Λ N)) : ↑s.pt →ₐ[Λ] TrivSqZeroExt (IsLocalRing.ResidueField Λ) (↑M × ↑N)

Equations

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

@[simp]

theorem Deformation.tsze_prod_lift_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (s : CategoryTheory.Limits.BinaryFan (tsze_C Λ M) (tsze_C Λ N)) (x : ↑s.pt) : (tsze_prod_lift Λ M N s) x = TrivSqZeroExt.inl (TrivSqZeroExt.fst (s.fst.hom x)) + TrivSqZeroExt.inr (TrivSqZeroExt.snd (s.fst.hom x), TrivSqZeroExt.snd (s.snd.hom x))

noncomputable def Deformation.tsze_prod_lift_hom (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) (s : CategoryTheory.Limits.BinaryFan (tsze_C Λ M) (tsze_C Λ N)) : s.pt ⟶ tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) (↑M × ↑N))

Equations

• Deformation.tsze_prod_lift_hom Λ M N s = Deformation.ArtinResAlg.ofHom (Deformation.tsze_prod_lift Λ M N s)

noncomputable def Deformation.tsze_prod_limit (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) : CategoryTheory.Limits.IsLimit (tsze_prod_cone Λ M N)

Equations

• Deformation.tsze_prod_limit Λ M N = CategoryTheory.Limits.BinaryFan.isLimitMk (Deformation.tsze_prod_lift_hom Λ M N) ⋯ ⋯ ⋯

noncomputable def Deformation.prodcone_iso (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) : tsze_functor.mapCone (vs.cone M N).cone ≅ (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Limits.pairComp M N tsze_functor).inv).obj (tsze_prod_cone Λ M N)

Equations

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

instance Deformation.instPreservesLimitFGModuleCatResidueFieldArtinResAlgDiscreteWalkingPairPairTsze_functor (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair M N) tsze_functor

instance Deformation.instPreservesLimitsOfShapeFGModuleCatResidueFieldArtinResAlgDiscreteWalkingPairTsze_functor (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) tsze_functor

noncomputable def Deformation.iso_punit_zero (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] : tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) PUnit.{u + 1}) ≅ tsze_C Λ 0

Equations

• Deformation.iso_punit_zero Λ = Deformation.tsze_functor.mapIso (⋯.iso ⋯)

noncomputable def Deformation.iso_terminal (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] : tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) PUnit.{u + 1}) ≅ ArtinResAlg.residueField

Equations

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

instance Deformation.instPreservesLimitFGModuleCatResidueFieldArtinResAlgDiscretePEmptyEmptyTsze_functor (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (FGModuleCat (IsLocalRing.ResidueField Λ))) tsze_functor

instance Deformation.instPreservesLimitsOfShapeFGModuleCatResidueFieldArtinResAlgDiscretePEmptyTsze_functor (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) tsze_functor

instance Deformation.instPreservesLimitsOfShapeArtinResAlgDiscretePEmpty (Λ : Type u) [CommRing Λ] (F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F

instance Deformation.instPreservesLimitsOfShapeFGModuleCatResidueFieldDiscretePEmptyCompArtinResAlgTsze_functor (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (tsze_functor.comp F)

instance Deformation.instPreservesFiniteProductsFGModuleCatResidueFieldArtinResAlgTsze_functor (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] : CategoryTheory.Limits.PreservesFiniteProducts tsze_functor

instance Deformation.instPreservesFiniteProductsFGModuleCatResidueFieldCompArtinResAlgTsze_functor (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (tsze_functor.comp F)] : CategoryTheory.Limits.PreservesFiniteProducts (tsze_functor.comp F)

noncomputable instance Deformation.instAddCommGroupObjArtinResAlgTsze_C (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (tsze_functor.comp F)] : AddCommGroup (F.obj (tsze_C Λ M))

Equations

• Deformation.instAddCommGroupObjArtinResAlgTsze_C Λ M F = inferInstanceAs (AddCommGroup ((Deformation.tsze_functor.comp F).obj M))

noncomputable instance Deformation.instModuleResidueFieldObjArtinResAlgTsze_C (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (tsze_functor.comp F)] : Module (IsLocalRing.ResidueField Λ) (F.obj (tsze_C Λ M))

Equations

• Deformation.instModuleResidueFieldObjArtinResAlgTsze_C Λ M F = inferInstanceAs (Module (IsLocalRing.ResidueField Λ) ((Deformation.tsze_functor.comp F).obj M))

noncomputable instance Deformation.instUniqueObjArtinResAlgTsze_COfNatFGModuleCatResidueField (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (tsze_functor.comp F)] : Unique (F.obj (tsze_C Λ 0))

Equations

• Deformation.instUniqueObjArtinResAlgTsze_COfNatFGModuleCatResidueField Λ F = inferInstanceAs (Unique ((Deformation.tsze_functor.comp F).obj 0))

noncomputable def Deformation.zero_map {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (B : ArtinResAlg Λ) : B ⟶ tsze_C Λ 0

Equations

• Deformation.zero_map B = (isTerminal_residueField_artin.ofIso ((Deformation.iso_terminal Λ).symm ≪≫ Deformation.iso_punit_zero Λ)).from B

noncomputable def Deformation.zero_map' {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (B : ArtinResAlg Λ) : B ⟶ tsze_C Λ M

Equations

• Deformation.zero_map' M B = CategoryTheory.CategoryStruct.comp (Deformation.zero_map B) (Deformation.tsze_functor.map (vs.zero_hom 0 M))

@[simp]

theorem Deformation.zero_map_F {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (tsze_functor.comp F)] (B : ArtinResAlg Λ) (x : F.obj B) : F.map (zero_map' M B) x = 0

@[simp]

theorem Deformation.zero_map'_apply {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) (B : ArtinResAlg Λ) (x : ↑B) : (zero_map' M B).hom x = (B.toResidueField.hom x, 0)

theorem Deformation.nattrans_isLinear {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {F : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (tsze_functor.comp F)] {G : CategoryTheory.Functor (ArtinResAlg Λ) (Type u)} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (ArtinResAlg Λ)) G] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (tsze_functor.comp G)] (η : G ⟶ F) (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : IsLinearMap (IsLocalRing.ResidueField Λ) (η.app (tsze_C Λ M))