def hR {Λ : Type u} [CommRing Λ] (R : Deformation.ProArtinResAlg Λ) : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)

functor sending A : ArtinResAlg Λ to Hom(R, A)

Equations

• hR R = Deformation.inclusionFunctor.comp (CategoryTheory.coyoneda.obj (Opposite.op R))

@[reducible, inline]

abbrev Procouple {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) : Type (u + 1)

a procouple is a pair (A, a) with a : Fhat A (the projective limit of the F (A/m^n))

Equations

• Procouple F = ((R : Deformation.ProArtinResAlg Λ) × F.completion.obj R)

structure Procouple.Hom {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (A B : Procouple F) : Type u

• hom : A.fst ⟶ B.fst
• comp : F.completion.map self.hom A.snd = B.snd

noncomputable def nattrans_of {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {R : Deformation.ProArtinResAlg Λ} (x : F.completion.obj R) : hR R ⟶ F

nattrans_of is the canonical (iso)morphism from F.completion.obj R to natural transformations (hR R) ⟶ F

Equations

• nattrans_of F x = CategoryTheory.CategoryStruct.comp (Deformation.inclusionFunctor.whiskerLeft (CategoryTheory.coyonedaEquiv.symm x)) (natiso_completion F).inv

@[simp]

theorem nattrans_of_comp_artinhom {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} {R : Deformation.ProArtinResAlg Λ} (x : F.completion.obj R) {A B : Deformation.ArtinResAlg Λ} (u : R ⟶ Deformation.inclusionFunctor.obj A) (u' : A ⟶ B) : (nattrans_of F x).app B (CategoryTheory.CategoryStruct.comp u (Deformation.inclusionFunctor.map u')) = F.map u' ((nattrans_of F x).app A u)

theorem completion_map_quot_mk_eq_pi {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {A : Deformation.ProArtinResAlg Λ} (n : ℕ) : CategoryTheory.CategoryStruct.comp (F.completion.map (proartin_quot_mk (IsLocalRing.maximalIdeal ↑A ^ n.succ))) (completion_iso F (quot_C Λ (IsLocalRing.maximalIdeal ↑A ^ n.succ))).hom = CategoryTheory.Limits.limit.π ((inversediagram A).comp F) (Opposite.op n)

theorem nattrans_of_proartin_quot_mk {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {R : Deformation.ProArtinResAlg Λ} (x : F.completion.obj R) (n : ℕ) : (nattrans_of F x).app (quot_C Λ (IsLocalRing.maximalIdeal ↑R ^ (n + 1))) (proartin_quot_mk (IsLocalRing.maximalIdeal ↑R ^ (n + 1))) = CategoryTheory.Limits.limit.π ((inversediagram R).comp F) (Opposite.op n) x

theorem nattrans_of_fac {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) {R : Deformation.ProArtinResAlg Λ} (x : F.completion.obj R) (A : Deformation.ArtinResAlg Λ) (n : ℕ) (u' : quot_C Λ (IsLocalRing.maximalIdeal ↑R ^ n.succ) ⟶ A) : (nattrans_of F x).app A (CategoryTheory.CategoryStruct.comp (proartin_quot_mk (IsLocalRing.maximalIdeal ↑R ^ n.succ)) (Deformation.inclusionFunctor.map u')) = F.map u' (CategoryTheory.Limits.limit.π ((inversediagram R).comp F) (Opposite.op n) x)

@[reducible, inline]

abbrev Prorepresents {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) (x : Procouple F) : Prop

a procouple (R, r) for a functor F pro-represents F if the morphism hR ⟶ F induced by r is an isomorphism

Equations

• Prorepresents F x = CategoryTheory.IsIso (nattrans_of F x.snd)

def IsHull {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] (x : Procouple F) : Prop

a procouple is a hull of F if it induces a smooth natural transformation, which is an isomorphism of the tangent spaces.

Equations

• IsHull F x = (IsSmooth (nattrans_of F x.snd) ∧ CategoryTheory.IsIso ((nattrans_of F x.snd).app dualNumber_C))

theorem hull_of_prorepresents {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] (x : Procouple F) (h : Prorepresents F x) : IsHull F x

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

• cond {A A' A'' : Deformation.ArtinResAlg Λ} (f : A' ⟶ A) (g : A'' ⟶ A) : Function.Surjective ⇑g.hom → IsSmallExtension g → Function.Surjective (CategoryTheory.Limits.pullbackComparison F f g)

@[reducible, inline]

abbrev H3 {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] : Prop

Equations

• H3 F = Module.Finite (IsLocalRing.ResidueField Λ) (tangentSpace F)

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

• cond {A A' : Deformation.ArtinResAlg Λ} (f : A' ⟶ A) [IsSmallExtension f] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f f) F

noncomputable def pullbackComparison_spec {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) : F.obj (pullbackinC f g) ⟶ CategoryTheory.Limits.Types.PullbackObj (F.map f) (F.map g)

Equations

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

theorem pullbackComparison_spec_surj_iff {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) : Function.Surjective (pullbackComparison_spec F f g) ↔ Function.Surjective (CategoryTheory.Limits.pullbackComparison F f g)

theorem pullbackComparison_spec_fst {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) (x : F.obj (pullbackinC f g)) : (↑(pullbackComparison_spec F f g x)).1 = F.map (fstinC f g) x

theorem pullbackComparison_spec_snd {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) (x : F.obj (pullbackinC f g)) : (↑(pullbackComparison_spec F f g x)).2 = F.map (sndinC f g) x

theorem pullbackComparison_spec_surj_of_small {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) [H1 F] (surj : Function.Surjective ⇑g.hom) [small : IsSmallExtension g] : Function.Surjective (pullbackComparison_spec F f g)

theorem pullbackComparison_comp {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) {W : Deformation.ArtinResAlg Λ} (h : W ⟶ Y) : CategoryTheory.Limits.pullbackComparison F f (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g h).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison F (CategoryTheory.Limits.pullback.snd f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (F.map (CategoryTheory.Limits.pullback.snd f g)) (F.map h) (CategoryTheory.Limits.pullback.snd (F.map f) (F.map g)) (F.map h) (CategoryTheory.Limits.pullbackComparison F f g) (CategoryTheory.CategoryStruct.id (F.obj W)) (CategoryTheory.CategoryStruct.id (F.obj Y)) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso (F.map f) (F.map g) (F.map h)).hom (CategoryTheory.Limits.pullback.congrHom ⋯ ⋯).inv)))

theorem pullbackComparison_surj_of_surj {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) [H1 F] (surj : Function.Surjective ⇑g.hom) : Function.Surjective (CategoryTheory.Limits.pullbackComparison F f g)

theorem pullbackComparison_spec_surj_of_surj {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) [H1 F] (surj : Function.Surjective ⇑g.hom) : Function.Surjective (pullbackComparison_spec F f g)

theorem preservesterminal_iff {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F ↔ Nonempty (Unique (F.obj Deformation.ArtinResAlg.residueField))

noncomputable instance instUniqueObjArtinResAlgResidueFieldOfPreservesLimitDiscretePEmptyEmpty {Λ : Type u} [CommRing Λ] (F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)) [IsLocalRing Λ] [h : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] : Unique (F.obj Deformation.ArtinResAlg.residueField)

Equations

• instUniqueObjArtinResAlgResidueFieldOfPreservesLimitDiscretePEmptyEmpty F = Classical.choice ⋯

instance instPreservesLimitArtinResAlgDiscretePEmptyEmptyHR {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : Deformation.ProArtinResAlg Λ) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) (hR R)

instance instPreservesLimitArtinResAlgWalkingCospanCospanHR {Λ : Type u} [CommRing Λ] (R : Deformation.ProArtinResAlg Λ) {X Y Z : Deformation.ArtinResAlg Λ} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (hR R)

instance instPreservesLimitsOfShapeArtinResAlgWalkingCospanHR {Λ : Type u} [CommRing Λ] (R : Deformation.ProArtinResAlg Λ) : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (hR R)

instance instPreservesLimitsOfShapeArtinResAlgDiscreteWalkingPairHR {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : Deformation.ProArtinResAlg Λ) : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (hR R)

instance instH1HR {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : Deformation.ProArtinResAlg Λ) : H1 (hR R)

instance instH2HR {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : Deformation.ProArtinResAlg Λ) : H2 (hR R)

instance instH3HR {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] (R : Deformation.ProArtinResAlg Λ) : H3 (hR R)

instance instH4HR {Λ : Type u} [CommRing Λ] (R : Deformation.ProArtinResAlg Λ) : H4 (hR R)

theorem H1.congr {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H1 F] (i : F ≅ G) : H1 G

theorem H2.congr {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H2 F] (i : F ≅ G) : H2 G

theorem H3.congr {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F] [H2 F] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) G] [H2 G] [H3 F] (i : F ≅ G) : H3 G

theorem H4.congr {Λ : Type u} [CommRing Λ] {F G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [H4 F] (i : F ≅ G) : H4 G

instance instIsIsoObjArtinResAlgTsze_CAppOfDualNumber_C {Λ : Type u} [CommRing Λ] {F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} [IsLocalRing Λ] {G : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)} (η : G ⟶ F) [CategoryTheory.Limits.PreservesFiniteProducts (Deformation.tsze_functor.comp F)] [CategoryTheory.Limits.PreservesFiniteProducts (Deformation.tsze_functor.comp G)] [h : CategoryTheory.IsIso (η.app dualNumber_C)] (M : FGModuleCat (IsLocalRing.ResidueField Λ)) : CategoryTheory.IsIso (η.app (Deformation.tsze_C Λ M))

instance instQuotInCDenom_idealOfIsLocalHomRingHomAlgebraMap {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] {X : Type u} [CommRing X] [IsLocalRing X] [Algebra Λ X] [IsLocalHom (algebraMap Λ X)] : QuotInC (denom_ideal Λ X)