theorem
Schlessinger1
{Λ : Type u}
[CommRing Λ]
[IsNoetherianRing Λ]
[IsLocalRing Λ]
[Deformation.IsComplete Λ]
(F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u))
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F]
[H1 F]
[H2 F]
[H3 F]
:
theorem
Schlessinger2_H1
{Λ : Type u}
[CommRing Λ]
[IsNoetherianRing Λ]
[IsLocalRing Λ]
[Deformation.IsComplete Λ]
{F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)}
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F]
(h : ∃ (x : Procouple F), IsHull F x)
:
H1 F
theorem
h2_from_h1
{Λ : Type u}
[CommRing Λ]
[IsNoetherianRing Λ]
[IsLocalRing Λ]
[Deformation.IsComplete Λ]
{F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)}
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F]
[H1 F]
:
(∀ (A : Deformation.ArtinResAlg Λ),
Function.Injective (pullbackComparison_spec F A.toResidueField dualNumber_C.toResidueField)) →
H2 F
theorem
Schlessinger2
{Λ : Type u}
[CommRing Λ]
[IsNoetherianRing Λ]
[IsLocalRing Λ]
[Deformation.IsComplete Λ]
{F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)}
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F]
(h : ∃ (x : Procouple F), IsHull F x)
:
theorem
Schlessinger3
{Λ : Type u}
[CommRing Λ]
[IsNoetherianRing Λ]
[IsLocalRing Λ]
[Deformation.IsComplete Λ]
(F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u))
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F]
[H1 F]
[H2 F]
[H3 F]
[H4 F]
:
∃ (x : Procouple F), Prorepresents F x
theorem
Schlessinger4
{Λ : Type u}
[CommRing Λ]
[IsLocalRing Λ]
{F : CategoryTheory.Functor (Deformation.ArtinResAlg Λ) (Type u)}
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (Deformation.ArtinResAlg Λ)) F]
(h : ∃ (x : Procouple F), Prorepresents F x)
: