@[reducible, inline]

noncomputable abbrev dualNumber_C {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] : Deformation.ArtinResAlg Λ

Equations

• dualNumber_C = Deformation.tsze_C Λ (FGModuleCat.of (IsLocalRing.ResidueField Λ) (IsLocalRing.ResidueField Λ))

@[reducible, inline]

abbrev tangentSpace {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] : Type u

the tangent space of a functor F is F(k[ε]) where k[ε] is the ring of dual numbers over the residue field k of Λ (i.e. ε² = 0). If F = h_R, then it is Hom(R, k[ε]), which is the usual tangent space of R.

Equations

• tangentSpace F = F.obj dualNumber_C

@[reducible, inline]

abbrev finmodule (R : Type u) [CommRing R] (r : ℕ) : FGModuleCat R

Equations

• finmodule R r = FGModuleCat.of R (Fin r → R)

def fintsze {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) : Deformation.ArtinResAlg Λ

Equations

• fintsze r = Deformation.tsze_C Λ (finmodule (IsLocalRing.ResidueField Λ) r)

def isofinzero (R : Type u) [CommRing R] : finmodule R 0 ≅ FGModuleCat.of R PUnit.{u + 1}

Equations

• isofinzero R = (LinearEquiv.ofSubsingleton PUnit.{?u.24 + 1} (Fin 0 → R)).symm.toFGModuleCatIso

def isterminalfinmodulezero (R : Type u) [CommRing R] : CategoryTheory.Limits.IsTerminal (finmodule R 0)

Equations

• isterminalfinmodulezero R = ⋯.isTerminal.ofIso (isofinzero R).symm

def isofinonek (R : Type u) [CommRing R] : finmodule R 1 ≅ FGModuleCat.of R R

Equations

• isofinonek R = (LinearEquiv.funUnique (Fin 1) R R).toFGModuleCatIso

def isofinsucc (R : Type u) [CommRing R] (r : ℕ) : finmodule R (r + 1) ≅ vs.prod (FGModuleCat.of R R) (finmodule R r)

Equations

• isofinsucc R r = (Fin.consLinearEquiv R fun (x : Fin r.succ) => R).symm.toFGModuleCatIso

def vs.finrR {R : Type u} [CommRing R] (r : ℕ) : Fin r → FGModuleCat R

Equations

• vs.finrR r x✝ = FGModuleCat.of R R

def vs.productCone {R : Type u} [CommRing R] {ι : Type v} [Finite ι] (Z : ι → FGModuleCat R) : CategoryTheory.Limits.Fan Z

The product cone induced by the concrete product.

Equations

• vs.productCone Z = CategoryTheory.Limits.Fan.mk (FGModuleCat.of R ((i : ι) → ↑(Z i))) fun (i : ι) => FGModuleCat.ofHom (LinearMap.proj i)

def vs.productConeIsLimit {R : Type u} [CommRing R] {ι : Type v} [Finite ι] (Z : ι → FGModuleCat R) : CategoryTheory.Limits.IsLimit (productCone Z)

The concrete product cone is limiting.

Equations

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

noncomputable def vs.piIsoPi {R : Type u} [CommRing R] {ι : Type v} [Finite ι] (Z : ι → FGModuleCat R) [CategoryTheory.Limits.HasProduct Z] : ∏ᶜ Z ≅ FGModuleCat.of R ((i : ι) → ↑(Z i))

The categorical product of a family of objects in ModuleCat agrees with the usual module-theoretical product.

Equations

• vs.piIsoPi Z = CategoryTheory.Limits.limit.isoLimitCone { cone := vs.productCone Z, isLimit := vs.productConeIsLimit Z }

@[simp]

theorem vs.piIsoPi_inv_kernel_ι {R : Type u} [CommRing R] {ι : Type v} [Finite ι] (Z : ι → FGModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (piIsoPi Z).inv (CategoryTheory.Limits.Pi.π Z i) = FGModuleCat.ofHom (LinearMap.proj i)

@[simp]

theorem vs.piIsoPi_hom_ker_subtype {R : Type u} [CommRing R] {ι : Type v} [Finite ι] (Z : ι → FGModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (piIsoPi Z).hom (FGModuleCat.ofHom (LinearMap.proj i)) = CategoryTheory.Limits.Pi.π Z i

def residuefield_in_C {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] : Deformation.ArtinResAlg Λ

Equations

• residuefield_in_C = Deformation.ArtinResAlg.of Λ (IsLocalRing.ResidueField Λ)

class H2 {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] : Prop

• cond (A' : Deformation.ArtinResAlg Λ) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A' dualNumber_C) F

instance instIsIsoProdObjArtinResAlgFintszeOfNatNatFst {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (A' : Deformation.ArtinResAlg Λ) : CategoryTheory.IsIso CategoryTheory.Limits.prod.fst

instance instIsIsoArtinResAlgFst {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (A' : Deformation.ArtinResAlg Λ) : CategoryTheory.IsIso CategoryTheory.Limits.prod.fst

theorem prodcomparisoneqzero {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (A' : Deformation.ArtinResAlg Λ) : CategoryTheory.Limits.prodComparison F A' (fintsze 0) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) (CategoryTheory.inv CategoryTheory.Limits.prod.fst)

instance instIsIsoObjArtinResAlgProdFintszeOfNatNatProdComparison {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (A' : Deformation.ArtinResAlg Λ) : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' (fintsze 0))

instance instPreservesLimitArtinResAlgDiscreteWalkingPairPairDualNumber_C {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [H2 F] (A' : Deformation.ArtinResAlg Λ) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A' dualNumber_C) F

instance instPreservesLimitArtinResAlgDiscreteWalkingPairPairFintszeOfNatNat {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [H2 F] (A' : Deformation.ArtinResAlg Λ) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A' (fintsze 1)) F

noncomputable def goodiso {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (r : ℕ) : fintsze (r + 1) ≅ fintsze 1 ⨯ fintsze r

Equations

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

noncomputable def auxisosucc {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [H2 F] (r : ℕ) (A' : Deformation.ArtinResAlg Λ) [∀ (A'' : Deformation.ArtinResAlg Λ), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A'' (fintsze r)) F] : F.obj (A' ⨯ fintsze (r + 1)) ≅ F.obj A' ⨯ F.obj (fintsze (r + 1))

Equations

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

theorem auxisosucc_eq_prodcomparison {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [H2 F] (r : ℕ) (A' : Deformation.ArtinResAlg Λ) [∀ (A'' : Deformation.ArtinResAlg Λ), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A'' (fintsze r)) F] : (auxisosucc F r A').hom = CategoryTheory.Limits.prodComparison F A' (fintsze (r + 1))

instance instPreservesLimitArtinResAlgDiscreteWalkingPairPairFintszeOfH2 {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (r : ℕ) (A' : Deformation.ArtinResAlg Λ) [H2 F] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A' (fintsze r)) F

instance instPreservesLimitArtinResAlgDiscreteWalkingPairPairObjFGModuleCatResidueFieldTsze_functorOfH2 {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] (A' : Deformation.ArtinResAlg Λ) [H2 F] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A' (Deformation.tsze_functor.obj M)) F

instance instPreservesLimitArtinResAlgDiscreteWalkingPairCompFGModuleCatResidueFieldPairTsze_functor {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] (M N : FGModuleCat (IsLocalRing.ResidueField Λ)) : CategoryTheory.Limits.PreservesLimit ((CategoryTheory.Limits.pair M N).comp Deformation.tsze_functor) F

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