90.3 The base category to 90.15 Miniversal formal objects…

Section90.3 The base category #

Section 90.3 of the Stacks Project, Tag 06GB. 15 tags here are carried by 37 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06GC, a definition

Tag 06GC in the Stacks Project.

Deformation.ArtinianLocalAlgCat, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 170. The attribute's comment: “objects”. References: SGA 7 VI (1.15), “objects, K a field”.

An Artinian local Λ-algebra together with a specified Λ-algebra isomorphism from its residue field to k. These are the objects of the category 𝒞_Λ of Stacks Project, Tag 06GC.

structure ArtinianLocalAlgCat (Λ : Type u) (k : Type w) [CommRing Λ] [Field k]
    [Algebra Λ k]

Deformation.ArtinianLocalAlgCat.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 196. The attribute's comment: “morphisms”. References: SGA 7 VI (1.15), “morphisms, K a field”.

A morphism of Artinian local Λ-algebras with fixed residue field is a local Λ-algebra homomorphism whose induced map on residue fields respects the specified identifications with k.

structure Hom (A B : ArtinianLocalAlgCat.{u, v, w} Λ k)

Deformation.ArtinianLocalAlgCat.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 218. The attribute's comment: “category structure”.

The category structure on Artinian local Λ-algebras with the fixed residue field k. Composition is composition of the underlying local algebra homomorphisms.

instance instCategory : Category (ArtinianLocalAlgCat.{u, v, w} Λ k)

Deformation.IsClassical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 275. The attribute's comment: “classical case”.

The classical case of 𝒞_Λ: Λ is a Noetherian complete local ring and the given Λ-algebra k is its residue field.

def IsClassical (Λ : Type u) (k : Type w) [CommRing Λ] [Field k] [Algebra Λ k] : Prop

Tag 06GD, a definition

Tag 06GD in the Stacks Project.

Declarations registered for the tag:

InfinitesimalLifting.IsSmallExtension, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/Basic.lean, line 286 (StacksFrontier).

Tag 06GE, a lemma

Tag 06GE in the Stacks Project.

Deformation.surjective_factors_into_smallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 535.

A surjective morphism in \mathcal{C}_\Lambda is a finite composite of small extensions.

theorem surjective_factors_into_smallExtensions
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A)
    (hf : Function.Surjective f.hom) :
    ∃ (n : ℕ) (F : ComposableArrows (ArtinianLocalAlgCat.{u, v, w} Λ k) n)
      (hB : F.left = B) (e : F.right ≅ A),
      eqToHom hB.symm ≫ F.hom ≫ e.hom = f ∧
        ∀ (i : ℕ) (hi : i < n),
          InfinitesimalLifting.IsSmallExtension
            (CommRingCat.ofHom (F.map' i (i + 1)).hom.toRingHom)

Tag 06S2, an equation

Tag 06S2 in the Stacks Project.

Deformation.residueImageField_eq_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 831. The attribute's comment: “the image is a field”.

For a finite map to a field, the subfield generated by its image has underlying set equal to the image itself.

theorem residueImageField_eq_range (Λ : Type u) (k : Type v) [CommRing Λ]
    [IsNoetherianRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k] :
    (residueImageField Λ k : Set k) = Set.range (algebraMap Λ k)

Deformation.finrank_residueImageField_eq_quotient_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 847. The attribute's comment: “the equality of degrees”.

The degrees of k over the image field and over the quotient of Λ by the kernel of its structural map agree.

theorem finrank_residueImageField_eq_quotient_ker
    (Λ : Type u) (k : Type v) [CommRing Λ] [IsNoetherianRing Λ]
    [Field k] [Algebra Λ k] [Module.Finite Λ k] :
    let f : Λ →+* k := algebraMap Λ k
    let e : Λ ⧸ RingHom.ker f ≃+* RingHom.range f :=
      RingHom.quotientKerEquivRange f
    letI : Field f.range := (range_isField Λ k).toField
    letI : Field (Λ ⧸ RingHom.ker f) :=
      ((e.toMulEquiv.isField_congr).mpr (Field.toIsField f.range)).toField
    let q : Λ ⧸ RingHom.ker f →+* k :=
      (Subring.subtype (RingHom.range f)).comp e.toRingHom
    letI : Algebra (Λ ⧸ RingHom.ker f) k := q.toAlgebra
    Module.finrank (residueImageField Λ k) k =
      Module.finrank (Λ ⧸ RingHom.ker f) k

Deformation.residueImageField_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 887. The attribute's comment: “finiteness of the degree”.

Stacks Project, Tag 06S2. The extension of k over the image field of a finite ring map is finite.

theorem residueImageField_finite
    (Λ : Type u) (k : Type v) [CommRing Λ] [IsNoetherianRing Λ]
    [Field k] [Algebra Λ k] [Module.Finite Λ k] :
    Module.Finite (residueImageField Λ k) k

Tag 06GG, a lemma

Tag 06GG in the Stacks Project.

Deformation.finrank_residueImageField_mul_length_eq_length, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 959. The attribute's comment: “general case”.

Stacks Project, Tag 06GG. Restricting scalars from a local Λ-algebra with residue field k to Λ multiplies module length by the degree of k over the image field of Λ.

theorem finrank_residueImageField_mul_length_eq_length
    (Λ : Type u) (k : Type w) (A : Type v) (M : Type x)
    [CommRing Λ] [IsNoetherianRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    [CommRing A] [Algebra Λ A] [IsLocalRing A]
    [AddCommGroup M] [Module A M]
    (_ : ResidueField A ≃ₐ[Λ] k) :
    letI : Module Λ M := Module.compHom M (algebraMap Λ A)
    (Module.finrank (residueImageField Λ k) k : ℕ∞) * Module.length A M =
      Module.length Λ M

Deformation.length_eq_length_of_isClassical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 995. The attribute's comment: “classical case”.

Stacks Project, Tag 06GG. In the classical case, module length is unchanged by restriction of scalars from a local Λ-algebra with residue field k to Λ.

theorem length_eq_length_of_isClassical
    (Λ : Type u) (k : Type w) (A : Type v) (M : Type x)
    [CommRing Λ] [IsNoetherianRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    [CommRing A] [Algebra Λ A] [IsLocalRing A]
    [AddCommGroup M] [Module A M]
    (_ : ResidueField A ≃ₐ[Λ] k) (h : IsClassical Λ k) :
    letI : Module Λ M := Module.compHom M (algebraMap Λ A)
    Module.length A M = Module.length Λ M

Tag 06S3, a lemma

Tag 06S3 in the Stacks Project.

Deformation.ArtinianLocalAlgCat.surjective_hom_iff_surjective_cotangentMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjectionDifferential.lean, line 296. The attribute's comment: “conditions (1) and (2), on the conormal module of a presentation”.

The criterion of [Stacks, Tag 06S3] for surjectivity, read on the conormal modules of the presentations residueExt B and residueExt A: a morphism of 𝒞_Λ is surjective exactly when the map it induces on 𝔪/𝔪² is surjective.

theorem surjective_hom_iff_surjective_cotangentMap (f : B ⟶ A) :
    Function.Surjective f.hom ↔
      Function.Surjective (Algebra.Extension.Cotangent.map (residueExtHom f))

Deformation.ArtinianLocalAlgCat.surjective_iff_cotangentSpaceMap_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 1140. The attribute's comment: “conditions (1) and (2)”.

A morphism of Artinian local algebras is surjective exactly when its canonical map m_A / m_A² → m_B / m_B² is surjective.

public theorem surjective_iff_cotangentSpaceMap_surjective
    {A B : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : A ⟶ B) :
    Function.Surjective f.hom ↔
      Function.Surjective
        (Ideal.mapCotangent (maximalIdeal A) (maximalIdeal B) f.hom
          (by
            let _ : IsLocalHom f.hom.toRingHom := f.isLocal
            intro x hx
            change x ∈ (maximalIdeal B).comap f.hom.toRingHom
            simpa only [maximalIdeal_comap] using hx))

Deformation.ArtinianLocalAlgCat.cotangentSpaceMap_surjective_iff_relativeCotangentSpaceMap_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 1187. The attribute's comment: “conditions (2) and (3)”.

Surjectivity on m / m² is equivalent to surjectivity after also quotienting by the extension of the maximal ideal of the base.

public theorem cotangentSpaceMap_surjective_iff_relativeCotangentSpaceMap_surjective
    {A B : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : A ⟶ B) :
    Function.Surjective
        (Ideal.mapCotangent (maximalIdeal A) (maximalIdeal B) f.hom
          (by
            let _ : IsLocalHom f.hom.toRingHom := f.isLocal
            intro x hx
            change x ∈ (maximalIdeal B).comap f.hom.toRingHom
            simpa only [maximalIdeal_comap] using hx)) ↔
      Function.Surjective (relativeCotangentSpaceMap f)

Tag 06GY, a definition

Tag 06GY in the Stacks Project.

Deformation.relativeCotangentSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 776. References: SGA 1 III (2.2).

The relative cotangent space of a local homomorphism f : R → S, namely m_S / (m_R S + m_S²).

abbrev relativeCotangentSpace
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] : Type v

Tag 06GH, a lemma

Tag 06GH in the Stacks Project.

Deformation.ArtinianLocalAlgCat.hasPullback_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/FibreProduct.lean, line 431. The attribute's comment: “surjective_fiber_product_in_clambda”.

If either morphism is surjective, the ring of compatible pairs is a pullback in 𝒞_Λ; in particular the pullback exists.

theorem hasPullback_of_surjective (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A)
    (h : Function.Surjective f₁.hom ∨ Function.Surjective f₂.hom) :
    IsConcretePullback f₁ f₂ ∧ HasPullback f₁ f₂

Deformation.ArtinianLocalAlgCat.isConcretePullback_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/FibreProductSeparable.lean, line 173. The attribute's comment: “separable_fiber_product_in_clambda”.

The algebraic fibre product has its canonical object structure in 𝒞_Λ when k is separable over the image field of Λ.

theorem isConcretePullback_of_isSeparable
    [Algebra.IsSeparable (residueImageField Λ k) k]
    {A₁ A₂ A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A) :
    IsConcretePullback f₁ f₂

Deformation.ArtinianLocalAlgCat.isSmallExtension_pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/SmallExtensionPullback.lean, line 167. The attribute's comment: “pullback_small_extension”.

The first projection from the pullback of a small extension in 𝒞_Λ is a small extension.

theorem isSmallExtension_pullback_fst
    {A₁ A₂ A : ArtinianLocalAlgCat.{u, v, w} Λ k}
    (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A) [Limits.HasPullback f₁ f₂]
    (h₂ : IsSmallExtension (CommRingCat.ofHom f₂.hom.toRingHom)) :
    IsSmallExtension
      (CommRingCat.ofHom (Limits.pullback.fst f₁ f₂).hom.toRingHom)

Tag 06GF, a definition

Tag 06GF in the Stacks Project.

Deformation.IsEssentialSurjection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 301.

A surjective morphism in 𝒞_Λ is essential if, whenever its composite with a morphism into its source is surjective, that morphism is already surjective.

abbrev IsEssentialSurjection
    {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A) : Prop

Tag 06S5, a lemma

Tag 06S5 in the Stacks Project.

Deformation.ArtinianLocalAlgCat.essentialSurjection_iff_mod_maximalIdeal_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjection.lean, line 265. The attribute's comment: “conditions (1) and (2)”.

Essential surjectivity is detected modulo the maximal-ideal squares.

theorem essentialSurjection_iff_mod_maximalIdeal_sq
    {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A) :
    let IB := maximalIdeal B ^ 2
    let IA := maximalIdeal A ^ 2
    let hB : IB ≤ maximalIdeal B := Ideal.pow_le_self (by omega : 2 ≠ 0)
    let hA : IA ≤ maximalIdeal A := Ideal.pow_le_self (by omega : 2 ≠ 0)
    let hmap : IB ≤ IA.comap f.hom := by
      let _ : IsLocalHom f.hom.toRingHom := f.isLocal
      rw [← Ideal.map_le_iff_le_comap, Ideal.map_pow]
      exact Ideal.pow_right_mono (map_maximalIdeal_le f.hom.toRingHom) _
    IsEssentialSurjection f ↔
    IsEssentialSurjection (idealQuotientMap f IB IA hB hA hmap)

Deformation.ArtinianLocalAlgCat.essentialSurjection_iff_mod_relative_maximalIdeal_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjection.lean, line 285. The attribute's comment: “conditions (1) and (3)”.

Essential surjectivity is detected on the relative cotangent quotient.

theorem essentialSurjection_iff_mod_relative_maximalIdeal_sq
    {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A) :
    IsEssentialSurjection f ↔
      IsEssentialSurjection
        (idealQuotientMap f
          ((RingHom.ker (algebraMap Λ k)).map (algebraMap Λ B) + maximalIdeal B ^ 2)
          ((RingHom.ker (algebraMap Λ k)).map (algebraMap Λ A) + maximalIdeal A ^ 2)
          (relativeCotangentIdeal_le_maximalIdeal B)
          (relativeCotangentIdeal_le_maximalIdeal A)
          (relativeCotangentIdeal_le_comap f))

Tag 06S6, an equation

Tag 06S6 in the Stacks Project.

Declarations registered for the tag:

KaehlerDifferential.kerCotangentToTensor registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch90.lean, line 21 (StacksFrontier): “the map m_A/m_A² → k ⊗_A Ω_{A/Λ}”. References: EGA 0 (20.5.11); EGA 0 (20.5.12); EGA 0 (22.2.9); EGA 0 (22.6.4), “partial”; EGA IV (17.15.9); SGA 1 II (5.9).
KaehlerDifferential.mapBaseChange registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch90.lean, line 22 (StacksFrontier): “the map k ⊗_A Ω_{A/Λ} → Ω_{k/Λ}”. References: EGA 0 (20.5.2); EGA 0 (20.5.4), “special case”; EGA 0 (20.5.7); EGA 0 (20.6.5), “differential K₁ → K₀”.
KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch90.lean, line 23 (StacksFrontier): “exactness at k ⊗_A Ω_{A/Λ}”. References: EGA 0 (20.5.12), “partial”; EGA 0 (20.6.23), “partial”; EGA 0 (22.4.8), “partial”; EGA IV (16.4.21), “special case”; EGA IV (17.2.5), “affine middle exactness”.
KaehlerDifferential.mapBaseChange_surjective registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch90.lean, line 25 (StacksFrontier): “exactness at Ω_{k/Λ} (→ 0)”. References: EGA IV (17.13.1), “special case”.

Tag 06S7, an equation

Tag 06S7 in the Stacks Project.

Deformation.exact_cotangentSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/CotangentSequence.lean, line 142. References: EGA 0 (20.6.22), “last three terms”.

Stacks 06S7. Let Λ be a ring, k a field and A a Λ-algebra with a Λ-algebra surjection A → k with kernel 𝔪_A. Then the four-term sequence
H₁(L_{k/Λ}) ⟶ 𝔪_A/𝔪_A² ⟶ Ω_{A/Λ} ⊗_A k ⟶ Ω_{k/Λ} ⟶ 0
is exact: exact at 𝔪_A/𝔪_A², exact at Ω_{A/Λ} ⊗_A k, and surjective onto Ω_{k/Λ}.

public theorem exact_cotangentSequence (h : Function.Surjective (algebraMap A k)) :
    Function.Exact (h1CotangentToCotangent Λ h)
        (KaehlerDifferential.kerCotangentToTensor Λ A k) ∧
      Function.Exact (KaehlerDifferential.kerCotangentToTensor Λ A k)
        (KaehlerDifferential.mapBaseChange Λ A k) ∧
      Function.Surjective (KaehlerDifferential.mapBaseChange Λ A k)

Tag 06S8, an equation

Tag 06S8 in the Stacks Project.

Deformation.cotangentMap_comp_h1CotangentToConormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/JacobiZariskiFunctoriality.lean, line 144. The attribute's comment: “left square, for the canonical map through the universal presentation”.

Stacks 06S8, left square. The two arrows out of H₁(L_{k/Λ}) agree: pushing a class into 𝔪_B/𝔪_B² and then along B → A gives its image in 𝔪_A/𝔪_A².

The source leaves this horizontal arrow unlabelled. It is realized here as Deformation.h1CotangentToConormal, the canonical map through the universal presentation of k over Λ. The square for the other realization of that arrow, the one used in the four-term exact sequence of [Stacks, Tag 06S7], is Deformation.mapCotangent_h1CotangentToCotangent; the two realizations are not compared to each other, which is why the scope label names this one.

public theorem cotangentMap_comp_h1CotangentToConormal :
    Algebra.Extension.Cotangent.map (residueExtensionHom (Λ := Λ) hB hA) ∘ₗ
        h1CotangentToConormal (residueExtension Λ hB) =
      h1CotangentToConormal (residueExtension Λ hA)

Deformation.cotangentSpaceMap_comp_cotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/JacobiZariskiFunctoriality.lean, line 163. The attribute's comment: “middle square”.

Stacks 06S8, middle square. The differentials d_B : 𝔪_B/𝔪_B² → k ⊗_B Ω_{B/Λ} and d_A : 𝔪_A/𝔪_A² → k ⊗_A Ω_{A/Λ} are compatible with the maps induced by B → A.

public theorem cotangentSpaceMap_comp_cotangentComplex :
    Algebra.Extension.CotangentSpace.map (residueExtensionHom (Λ := Λ) hB hA) ∘ₗ
        (residueExtension Λ hB).cotangentComplex =
      (residueExtension Λ hA).cotangentComplex ∘ₗ
        Algebra.Extension.Cotangent.map (residueExtensionHom (Λ := Λ) hB hA)

Deformation.toKaehler_comp_cotangentSpaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/JacobiZariskiFunctoriality.lean, line 174. The attribute's comment: “right square”.

Stacks 06S8, right square. The two arrows into Ω_{k/Λ} agree: the projection of k ⊗_B Ω_{B/Λ} onto Ω_{k/Λ} factors through k ⊗_A Ω_{A/Λ} along B → A.

public theorem toKaehler_comp_cotangentSpaceMap :
    (residueExtension Λ hA).toKaehler ∘ₗ
        Algebra.Extension.CotangentSpace.map (residueExtensionHom (Λ := Λ) hB hA) =
      (residueExtension Λ hB).toKaehler

Deformation.mapCotangent_h1CotangentToCotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/JacobiZariskiFunctoriality.lean, line 239. The attribute's comment: “left square, for the arrow of the four-term sequence of 06S7”.

Stacks 06S8, left square, for the arrow H₁(L_{k/Λ}) → 𝔪/𝔪² of the four-term exact sequence of [Stacks, Tag 06S7]: pushing a class of H₁(L_{k/Λ}) into 𝔪_B/𝔪_B² and then along 𝔪_B → 𝔪_A gives its image in 𝔪_A/𝔪_A².

public theorem mapCotangent_h1CotangentToCotangent (x : Algebra.H1Cotangent Λ k) :
    Ideal.mapCotangent (RingHom.ker (algebraMap B k)) (RingHom.ker (algebraMap A k))
        (Algebra.ofId B A)
        (ker_algebraMap_le_comap_ker (Λ := B) (S := k) (k := k) (A := A))
        (h1CotangentToCotangent Λ hB x) =
      h1CotangentToCotangent Λ hA x

Tag 06S9, a lemma

Tag 06S9 in the Stacks Project.

Deformation.conormalToH1Cotangent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/CotangentHomology.lean, line 230. The attribute's comment: “canonical map”.

Stacks 06S9. The canonical map 𝔪_Λ/𝔪_Λ² → H₁(L_{k/Λ}), for k' the subfield of k generated by the image of Λ, presented as a field S with Λ → S surjective and S → k an extension: the conormal module of Λ → S maps to H₁(L_{S/Λ}) and then to H₁(L_{k/Λ}).

public noncomputable def conormalToH1Cotangent
    (h : Function.Surjective (algebraMap Λ S)) :
    (RingHom.ker (algebraMap Λ S)).Cotangent →ₗ[Λ] Algebra.H1Cotangent Λ k

Deformation.conormalToH1Cotangent_baseChange_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/CotangentHomology.lean, line 325. The attribute's comment: “separable case”.

Stacks 06S9. When k is separable over the image field S = k', the canonical map induces an isomorphism 𝔪_Λ/𝔪_Λ² ⊗_{k'} k = H₁(L_{k/Λ}). The base change is written over Λ, which is the same thing: the conormal module of Λ → S is annihilated by its kernel, hence is a module over Λ/𝔪_Λ = k'.

public theorem conormalToH1Cotangent_baseChange_bijective
    (h : Function.Surjective (algebraMap Λ S))
    [Algebra.IsSeparable S k] :
    Function.Bijective
      ((conormalToH1Cotangent (Λ := Λ) (S := S) (k := k) h).liftBaseChange k)

Deformation.conormalToH1Cotangent_bijective_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/CotangentHomology.lean, line 353. The attribute's comment: “classical case”.

Stacks 06S9. In the classical case k = k', that is Λ → k surjective, the canonical map 𝔪_Λ/𝔪_Λ² → H₁(L_{k/Λ}) is itself an isomorphism.

public theorem conormalToH1Cotangent_bijective_of_surjective
    (h : Function.Surjective (algebraMap Λ k)) :
    Function.Bijective
      (conormalToH1Cotangent (Λ := Λ) (S := k) (k := k) h)

Deformation.conormalToH1Cotangent_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/CotangentHomology.lean, line 390. The attribute's comment: “compatibility with the conormal map”.

Stacks 06S9. The composite 𝔪_Λ/𝔪_Λ² → H₁(L_{k/Λ}) → H₁(L_{k/A}) is the map induced by the structural map 𝔪_Λ → 𝔪_A: for A with Λ → A → k and A → k surjective, pushing a class of 𝔪_Λ/𝔪_Λ² forward to H₁(L_{k/A}) agrees with taking its image in 𝔪_A/𝔪_A² and applying the canonical map of A → k. Since the canonical map of A → k is an isomorphism by conormalToH1Cotangent_bijective_of_surjective, this identifies the composite 𝔪_Λ/𝔪_Λ² → H₁(L_{k/Λ}) → 𝔪_A/𝔪_A² of the source.

public theorem conormalToH1Cotangent_comp
    {A : Type*} [CommRing A] [Algebra Λ A] [Algebra A k]
    [IsScalarTower Λ A k]
    (h : Function.Surjective (algebraMap Λ S))
    (hg : Function.Surjective (algebraMap A k))
    (x : (RingHom.ker (algebraMap Λ S)).Cotangent) :
    Algebra.H1Cotangent.map Λ A k k
        (conormalToH1Cotangent (Λ := Λ) (S := S) (k := k) h x) =
      conormalToH1Cotangent (Λ := A) (S := k) (k := k) hg
        (Ideal.mapCotangent (RingHom.ker (algebraMap Λ S))
          (RingHom.ker (algebraMap A k)) (Algebra.ofId Λ A)
          (ker_algebraMap_le_comap_ker (Λ := Λ) (S := S) (k := k) (A := A)) x)

Tag 06H0, a lemma

Tag 06H0 in the Stacks Project.

Deformation.ArtinianLocalAlgCat.isEssentialSurjection_iff_bijective_differentialsBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityEssentialSurjection.lean, line 187. The attribute's comment: “part (2), conditions (a) and (c), through the base-change map of differentials”.

Stacks 06H0, part (2), conditions (a) and (c), with the cotangent space written as the base-change map of differentials. A morphism f : B ⟶ A of 𝒞_Λ is an essential surjection exactly when the canonical map k ⊗_B Ω_{B/Λ} ⟶ k ⊗_A Ω_{A/Λ} is bijective.

This is Deformation.ArtinianLocalAlgCat.isEssentialSurjection_iff_cotangentSpaceMap_bijective composed with Deformation.Artin.differentialsBaseChangeMap_eq_cotangentSpaceMap. It is the form in which the criterion meets Stacks 07YL, which produces its square-zero extension together with the bijectivity of exactly this map.

public theorem isEssentialSurjection_iff_bijective_differentialsBaseChangeMap
    {B A : ArtinianLocalAlgCat.{u, u, u} Λ k} (f : B ⟶ A) :
    letI : Algebra (B : Type u) (A : Type u) := f.hom.toRingHom.toAlgebra
    letI : IsScalarTower Λ (B : Type u) (A : Type u) :=
      .of_algebraMap_eq fun x => (f.hom.commutes x).symm
    letI : IsScalarTower (B : Type u) (A : Type u) k :=
      .of_algebraMap_eq fun b => (f.residue_comm b).symm
    (IsEssentialSurjection f ↔
      Function.Bijective
        (Deformation.Artin.differentialsBaseChangeMap Λ (B : Type u) (A : Type u) k))

Deformation.ArtinianLocalAlgCat.surjective_iff_imageDMap_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjectionDifferential.lean, line 723. The attribute's comment: “part (1)(a), the image of the differential”.

Stacks 06H0, part (1)(a). A morphism f : B ⟶ A of 𝒞_Λ is surjective — equivalently, satisfies the conditions of [Stacks, Tag 06S3] — exactly when Im(d_B) → Im(d_A) is surjective.

theorem surjective_iff_imageDMap_surjective (f : B ⟶ A) :
    Function.Surjective f.hom ↔ Function.Surjective (imageDMap f)

Deformation.ArtinianLocalAlgCat.surjective_iff_cotangentSpaceMap_residueExtHom_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjectionDifferential.lean, line 751. The attribute's comment: “part (1)(b), the cotangent space”.

Stacks 06H0, part (1)(b). A morphism f : B ⟶ A of 𝒞_Λ is surjective — equivalently, satisfies the conditions of [Stacks, Tag 06S3] — exactly when Ω_{B/Λ} ⊗_B k → Ω_{A/Λ} ⊗_A k is surjective.

theorem surjective_iff_cotangentSpaceMap_residueExtHom_surjective (f : B ⟶ A) :
    Function.Surjective f.hom ↔
      Function.Surjective (Algebra.Extension.CotangentSpace.map (residueExtHom f))

Deformation.ArtinianLocalAlgCat.imageDMap_bijective_iff_cotangentSpaceMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjectionDifferential.lean, line 761. The attribute's comment: “part (2), conditions (b) and (c)”.

Stacks 06H0, part (2), equivalence of conditions (b) and (c). For a morphism of 𝒞_Λ the map Im(d_B) → Im(d_A) is an isomorphism exactly when Ω_{B/Λ} ⊗_B k → Ω_{A/Λ} ⊗_A k is one.

theorem imageDMap_bijective_iff_cotangentSpaceMap_bijective (f : B ⟶ A) :
    Function.Bijective (imageDMap f) ↔
      Function.Bijective (Algebra.Extension.CotangentSpace.map (residueExtHom f))

Deformation.ArtinianLocalAlgCat.isEssentialSurjection_iff_cotangentSpaceMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjectionDifferential.lean, line 832. The attribute's comment: “part (2), conditions (a) and (c)”.

Stacks 06H0, part (2), equivalence of conditions (a) and (c). A morphism of 𝒞_Λ is an essential surjection exactly when Ω_{B/Λ} ⊗_B k → Ω_{A/Λ} ⊗_A k is an isomorphism.

theorem isEssentialSurjection_iff_cotangentSpaceMap_bijective (f : B ⟶ A) :
    IsEssentialSurjection f ↔
      Function.Bijective (Algebra.Extension.CotangentSpace.map (residueExtHom f))

Deformation.ArtinianLocalAlgCat.isEssentialSurjection_iff_imageDMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjectionDifferential.lean, line 841. The attribute's comment: “part (2), conditions (a) and (b)”.

Stacks 06H0, part (2), equivalence of conditions (a) and (b). A morphism of 𝒞_Λ is an essential surjection exactly when Im(d_B) → Im(d_A) is an isomorphism.

theorem isEssentialSurjection_iff_imageDMap_bijective (f : B ⟶ A) :
    IsEssentialSurjection f ↔ Function.Bijective (imageDMap f)

Deformation.ArtinianLocalAlgCat.isEssentialSurjection_iff_relativeCotangentSpaceMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/EssentialSurjectionDifferential.lean, line 1012. The attribute's comment: “part (3), separable case”.

Stacks 06H0, part (3). If k is separable over the image field k' — presented as a field S with Λ → S surjective and S → k separable — then a morphism f : B ⟶ A of 𝒞_Λ is an essential surjection exactly when 𝔪_B/(𝔪_Λ B + 𝔪_B²) → 𝔪_A/(𝔪_Λ A + 𝔪_A²) is an isomorphism.

In that case Im(d_A) = 𝔪_A/(𝔪_Λ A + 𝔪_A²) for every object A, by cotangentComplex_mk_eq_zero_of_mem_relative and mem_relative_of_cotangentComplex_mk_eq_zero, and the statement follows from part (2). Only the forward implication uses separability: the converse is isEssentialSurjection_of_relativeCotangentSpaceMap_bijective.

theorem isEssentialSurjection_iff_relativeCotangentSpaceMap_bijective
    {S : Type*} [Field S] [Algebra Λ S] [Algebra S k] [IsScalarTower Λ S k]
    (hS : Function.Surjective (algebraMap Λ S)) [Algebra.IsSeparable S k] (f : B ⟶ A) :
    IsEssentialSurjection f ↔ Function.Bijective (relativeCotangentSpaceMap f)

Deformation.not_isEssentialSurjection_iff_exists_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Basic.lean, line 639. The attribute's comment: “small_extension_section”.

A small extension in 𝒞_Λ is nonessential if and only if it has a section in 𝒞_Λ.

theorem not_isEssentialSurjection_iff_exists_section
    {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A)
    (hf : InfinitesimalLifting.IsSmallExtension
      (CommRingCat.ofHom f.hom.toRingHom)) :
    ¬ IsEssentialSurjection f ↔ ∃ s : A ⟶ B, s ≫ f = 𝟙 A

Sources

LeanDeformation.ArtinianLocalAlgCat · Deformation.ArtinianLocalAlgCat.Hom · Deformation.ArtinianLocalAlgCat.instCategory · Deformation.IsClassical · InfinitesimalLifting.IsSmallExtension · Deformation.surjective_factors_into_smallExtensions · Deformation.residueImageField_eq_range · Deformation.finrank_residueImageField_eq_quotient_ker

Section90.4 The completed base category #

Section 90.4 of the Stacks Project, Tag 06GV. 9 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06GW, a definition

Tag 06GW in the Stacks Project.

Deformation.CompleteLocalAlgCat, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Basic.lean, line 104. The attribute's comment: “objects”. References: SGA 7 VI (1.15), “objects, K a field”.

A Noetherian complete local Λ-algebra together with a specified Λ-algebra isomorphism from its residue field to k. These are the objects of \widehat{\mathcal C}_Λ in Stacks Project, Tag 06GW.

structure CompleteLocalAlgCat (Λ : Type u) (k : Type w) [CommRing Λ] [Field k]
    [Algebra Λ k]

Deformation.CompleteLocalAlgCat.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Basic.lean, line 142. The attribute's comment: “morphisms”. References: SGA 7 VI (1.15), “morphisms, K a field”.

A morphism of Noetherian complete local Λ-algebras with fixed residue field is a local Λ-algebra homomorphism whose induced map on residue fields respects the specified identifications with k.

structure Hom (A B : CompleteLocalAlgCat.{u, v, w} Λ k)

Deformation.CompleteLocalAlgCat.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Basic.lean, line 171. The attribute's comment: “category structure”.

The category structure on Noetherian complete local Λ-algebras with fixed residue field. Composition is composition of the underlying local algebra homomorphisms.

instance instCategory : Category (CompleteLocalAlgCat.{u, v, w} Λ k)

Tag 06GZ, a lemma

Tag 06GZ in the Stacks Project.

Deformation.surjective_iff_surjective_cotangentSpaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Basic.lean, line 519. The attribute's comment: “conditions (1) and (2)”.

A morphism of Noetherian complete local algebras is surjective if and only if its canonical map m_R / m_R² → m_S / m_S² is surjective.

theorem surjective_iff_surjective_cotangentSpaceMap
    {R S : CompleteLocalAlgCat.{u, v, w} Λ k} (f : R ⟶ S) :
    Function.Surjective f.hom ↔
      Function.Surjective
        (Ideal.mapCotangent (maximalIdeal R) (maximalIdeal S) f.hom
          (by
            let _ : IsLocalHom f.hom.toRingHom := f.isLocal
            intro x hx
            change x ∈ (maximalIdeal S).comap f.hom.toRingHom
            simpa only [maximalIdeal_comap] using hx))

Deformation.surjective_iff_surjective_relativeCotangentSpaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Basic.lean, line 541. The attribute's comment: “conditions (1) and (3)”.

A morphism of Noetherian complete local algebras is surjective if and only if its map m_R / (m_Λ R + m_R²) → m_S / (m_Λ S + m_S²) is surjective.

theorem surjective_iff_surjective_relativeCotangentSpaceMap
    {R S : CompleteLocalAlgCat.{u, v, w} Λ k} (f : R ⟶ S) :
    Function.Surjective f.hom ↔ Function.Surjective (relativeCotangentSpaceMap f)

Tag 06SB, a lemma

Tag 06SB in the Stacks Project.

Deformation.CompleteLocalAlgCat.hasPushouts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Pushout.lean, line 972.

The category of Noetherian complete local Λ-algebras with residue field identified with k admits pushouts.

public instance hasPushouts :
    HasPushouts (CompleteLocalAlgCat.{u, v, w} Λ k)

Tag 06H1, a lemma

Tag 06H1 in the Stacks Project.

Deformation.instHasBinaryCoproducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Coproduct.lean, line 558.

The category of Noetherian complete local Λ-algebras with residue field k admits coproducts of pairs of objects.

instance instHasBinaryCoproducts {Λ : Type u} {k : Type w}
    [CommRing Λ] [Field k] [Algebra Λ k] [Algebra.FiniteType Λ k] :
    HasBinaryCoproducts (CompleteLocalAlgCat.{u, v, w} Λ k)

Tag 06SC, a lemma

Tag 06SC in the Stacks Project.

Deformation.derivation_module_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Basic.lean, line 222.

Stacks Project, Tag 06SC. The k-vector space of Λ-derivations from a Noetherian local Λ-algebra with residue field k to k is finite-dimensional.

theorem derivation_module_finite
    {Λ : Type u} {S : Type v} {k : Type w} [CommRing Λ] [CommRing S]
    [IsLocalRing S] [IsNoetherianRing S] [Field k] [Algebra Λ S] [Algebra Λ k]
    [Module.Finite Λ k] (e : ResidueField S ≃ₐ[Λ] k) :
    letI : Algebra S k :=
      (e.toAlgHom.comp (IsScalarTower.toAlgHom Λ S (ResidueField S))).toRingHom.toAlgebra
    Module.Finite k (Derivation Λ S k)

Tag 06SD, a lemma

Tag 06SD in the Stacks Project.

Deformation.surjective_of_residueDerivation_comap_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/Basic.lean, line 650.

A morphism of Noetherian complete local algebras with fixed residue field is surjective if restriction of residue-field-valued derivations along it is injective.

public theorem surjective_of_residueDerivation_comap_injective
    {R S : CompleteLocalAlgCat.{u, v, w} Λ k} (f : R ⟶ S)
    (h : Function.Injective (ResidueDerivation.comap f)) :
    Function.Surjective f.hom

Tag 06SE, a lemma

Tag 06SE in the Stacks Project.

Deformation.quotient_filtration_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/InverseLimit.lean, line 191.

Let A be a Noetherian complete local algebra and let J n be a decreasing sequence of ideals containing the n-th power of the maximal ideal. In the quotient by ⋂ n, J n, the images of the J n form an adic filtration for the image of the maximal ideal.

theorem quotient_filtration_isAdic
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (A : CompleteLocalAlgCat.{u, v, w} Λ k) (J : ℕ → Ideal A)
    (hJ : Antitone J) (hpow : ∀ n, maximalIdeal A ^ n ≤ J n) :
    Ideal.IsAdicFiltration
      (Ideal.map (Ideal.Quotient.mk (⨅ n, J n)) (maximalIdeal A))
      (fun n ↦ Ideal.map (Ideal.Quotient.mk (⨅ n, J n)) (J n))

Tag 06SF, a lemma

Tag 06SF in the Stacks Project.

Deformation.inverseLimit_isObjectOfCompleteLocalAlgCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/InverseLimit.lean, line 1068. The attribute's comment: “complete local inverse limit”.

Stacks Project, Tag 06SF (first assertion). If the transition maps in a tower of Artinian local Λ-algebras are surjective and the dimensions of the cotangent spaces are bounded, then its inverse limit is a Noetherian complete local algebra whose residue field is the specified field k.

theorem inverseLimit_isObjectOfCompleteLocalAlgCat
    (A : ℕ → ArtinianLocalAlgCat.{u, v, w} Λ k)
    (f : ∀ n, A (n + 1) ⟶ A n)
    (hsurj : ∀ n, Function.Surjective (f n).hom)
    (hbounded : ∃ d : ℕ,
      ∀ n, Module.finrank (ResidueField (A n)) (CotangentSpace (A n)) ≤ d) :
    ∃ h : IsNoetherianCompleteLocalRing (inverseLimit A f),
      letI : IsLocalRing (inverseLimit A f) := h.isLocal
      Nonempty (ResidueField (inverseLimit A f) ≃ₐ[Λ] k)

Deformation.kernel_projections_define_maximalIdeal_adicTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/InverseLimit.lean, line 1095. The attribute's comment: “projection kernels define the adic topology”.

Stacks Project, Tag 06SF (second assertion). Under the same hypotheses, the kernels of the projections from the inverse limit are cofinal with the powers of its maximal ideal, and hence define its maximal-ideal-adic topology.

theorem kernel_projections_define_maximalIdeal_adicTopology
    (A : ℕ → ArtinianLocalAlgCat.{u, v, w} Λ k)
    (f : ∀ n, A (n + 1) ⟶ A n)
    (hsurj : ∀ n, Function.Surjective (f n).hom)
    (h : IsNoetherianCompleteLocalRing (inverseLimit A f)) :
    letI : IsLocalRing (inverseLimit A f) := h.isLocal
    Ideal.IsAdicFiltration (maximalIdeal (inverseLimit A f))
      (fun n ↦ RingHom.ker (inverseLimitProj A f n))

Tag 06SG, a lemma

Tag 06SG in the Stacks Project.

Deformation.mvPowerSeries_bijective_of_eventually_quotient_retract, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/PowerSeries.lean, line 249.

Suppose R is the additive direct sum of the image of R' and an ideal I, and x : Fin r → I is a basis of I / 𝔪_R I. The power-series map which sends X i to x i is bijective if, in all sufficiently high degrees, its maps modulo powers of the maximal ideals have local Λ-algebra retractions.

public theorem mvPowerSeries_bijective_of_eventually_quotient_retract
    {R' R : CompleteLocalAlgCat.{u, v, w} Λ k} (f : R' ⟶ R) (I : Ideal R)
    (hdecomp : ∀ z : R, ∃! p : R' × I, z = f.hom p.1 + p.2.1)
    {r : ℕ} (x : Fin r → I)
    (hspan : ∀ y : I, ∃ a : Fin r → R,
      y.1 - ∑ i, a i * (x i).1 ∈ maximalIdeal R * I)
    (hindep : ∀ a : Fin r → R,
      (∑ i, a i * (x i).1 ∈ maximalIdeal R * I) →
        ∀ i, a i ∈ maximalIdeal R)
    (F : MvPowerSeries (Fin r) R' →+* R)
    (hF_C : ∀ a : R', F (MvPowerSeries.C a) = f.hom a)
    (hF_X : ∀ i, F (MvPowerSeries.X i) = (x i).1)
    (hretract : ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      Ideal.map F (maximalIdeal (MvPowerSeries (Fin r) R') ^ n) ≤
          maximalIdeal R ^ n ∧
        ∃ h : (R ⧸ maximalIdeal R ^ n) →+*
            (MvPowerSeries (Fin r) R' ⧸ maximalIdeal (MvPowerSeries (Fin r) R') ^ n),
          IsLocalHom h ∧
          (∀ s : MvPowerSeries (Fin r) R',
            h (Ideal.Quotient.mk (maximalIdeal R ^ n) (F s)) =
              Ideal.Quotient.mk (maximalIdeal (MvPowerSeries (Fin r) R') ^ n) s) ∧
      (∀ a : Λ,
            h (Ideal.Quotient.mk (maximalIdeal R ^ n) (algebraMap Λ R a)) =
              Ideal.Quotient.mk (maximalIdeal (MvPowerSeries (Fin r) R') ^ n)
                (MvPowerSeries.C (algebraMap Λ R' a)))) :
    Function.Bijective F

Sources

LeanDeformation.CompleteLocalAlgCat · Deformation.CompleteLocalAlgCat.Hom · Deformation.CompleteLocalAlgCat.instCategory · Deformation.surjective_iff_surjective_cotangentSpaceMap · Deformation.surjective_iff_surjective_relativeCotangentSpaceMap · Deformation.CompleteLocalAlgCat.hasPushouts · Deformation.instHasBinaryCoproducts · Deformation.derivation_module_finite

Section90.5 Categories cofibered in groupoids #

Section 90.5 of the Stacks Project, Tag 06GA. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06GJ, a definition

Tag 06GJ in the Stacks Project.

Deformation.IsCofiberedInGroupoids, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Cofibered.lean, line 60.

A functor p : F ⥤ C is cofibered in groupoids when the opposite functor p.op : Fᵒᵖ ⥤ Cᵒᵖ is fibered in groupoids.

public abbrev IsCofiberedInGroupoids {F : Type u₁} [Category.{v₁} F]
    {C : Type u₂} [Category.{v₂} C] (p : F ⥤ C) : Prop

Tag 06GK, remarks

Tag 06GK in the Stacks Project.

Deformation.isCofiberedInGroupoids_twoFibreProductBasedCategory, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductBaseChangeSmooth.lean, line 93. The attribute's comment: “(13) the 2-fibre product of categories cofibered in groupoids over 𝒞_Λ is given by the construction of their 2-fibre product as categories over 𝒞_Λ”.

A 2-fibre product of categories cofibered in groupoids over 𝒞_Λ is cofibered in groupoids: the construction of the 2-fibre product as categories over 𝒞_Λ serves as the 2-fibre product in the (2, 1)-category of categories cofibered in groupoids over 𝒞_Λ.

public lemma isCofiberedInGroupoids_twoFibreProductBasedCategory
    (p₁ : BasedFunctor 𝓗₁ 𝓖) (p₂ : BasedFunctor 𝓗₂ 𝓖)
    (h𝓗₁ : IsCofiberedInGroupoids 𝓗₁.p) (h𝓗₂ : IsCofiberedInGroupoids 𝓗₂.p)
    (h𝓖 : IsCofiberedInGroupoids 𝓖.p) :
    IsCofiberedInGroupoids (twoFibreProductBasedCategory p₁ p₂).p

Deformation.cofiberedProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Cofibered/Product.lean, line 81. The attribute's comment: “(14) products of categories cofibered in groupoids”.

The product of two categories cofibered in groupoids 𝓕 and 𝓖 over 𝒞_Λ is their 2-fibre product 𝓕 ×_{𝒞_Λ} 𝓖, taken over 𝒞_Λ itself: the 2-fibre product of the two structure morphisms of 𝓕 and 𝓖 into the base category read through the identity functor as a category cofibered in groupoids over itself.

public def cofiberedProduct (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, w, w} Λ k)) :
    BasedCategory (ArtinianLocalAlgCat.{u, w, w} Λ k)

Deformation.isCofiberedInGroupoids_cofiberedProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Cofibered/Product.lean, line 217. The attribute's comment: “(14) the product is again a category cofibered in groupoids”.

The product of two categories cofibered in groupoids over 𝒞_Λ is again cofibered in groupoids.

public theorem isCofiberedInGroupoids_cofiberedProduct
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p) (h𝓖 : IsCofiberedInGroupoids 𝓖.p) :
    IsCofiberedInGroupoids (cofiberedProduct 𝓕 𝓖).p

Tag 07W5, an item

Tag 07W5 in the Stacks Project.

Deformation.isomorphismClasses, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/IsomorphismClasses.lean, line 475.

The associated covariant functor of fibrewise isomorphism classes.

noncomputable abbrev isomorphismClasses : C ⥤ Type u₁

Tag 0DZJ, an item

Tag 0DZJ in the Stacks Project.

Deformation.cofiberedProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Cofibered/Product.lean, line 81. The attribute's comment: “the product of two categories cofibered in groupoids over 𝒞_Λ is their 2-fibre product over 𝒞_Λ”.

The product of two categories cofibered in groupoids 𝓕 and 𝓖 over 𝒞_Λ is their 2-fibre product 𝓕 ×_{𝒞_Λ} 𝓖, taken over 𝒞_Λ itself: the 2-fibre product of the two structure morphisms of 𝓕 and 𝓖 into the base category read through the identity functor as a category cofibered in groupoids over itself.

public def cofiberedProduct (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, w, w} Λ k)) :
    BasedCategory (ArtinianLocalAlgCat.{u, w, w} Λ k)

Deformation.isCofiberedInGroupoids_cofiberedProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Cofibered/Product.lean, line 217. The attribute's comment: “the product of two categories cofibered in groupoids is cofibered in groupoids”.

The product of two categories cofibered in groupoids over 𝒞_Λ is again cofibered in groupoids.

public theorem isCofiberedInGroupoids_cofiberedProduct
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p) (h𝓖 : IsCofiberedInGroupoids 𝓖.p) :
    IsCofiberedInGroupoids (cofiberedProduct 𝓕 𝓖).p

Deformation.twoFibreProductBasedCategory_comp_baseProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Cofibered/Product.lean, line 233. The attribute's comment: “the 2-fibre product over 𝒞_Λ along the structure morphisms is the product”.

Given morphisms p₁ : 𝓗 → 𝓕 and p₂ : 𝓖 → 𝓕 of categories cofibered in groupoids over 𝒞_Λ, the 2-fibre product of 𝓗 and 𝓖 formed over 𝒞_Λ — that is, over the two composites of p₁ and p₂ with the structure morphism of 𝓕 — is the product 𝓗 ×_{𝒞_Λ} 𝓖.

public theorem twoFibreProductBasedCategory_comp_baseProjection
    (p₁ : BasedFunctor 𝓗 𝓕) (p₂ : BasedFunctor 𝓖 𝓕) :
    twoFibreProductBasedCategory (BasedFunctor.comp p₁ (baseProjection 𝓕.p))
        (BasedFunctor.comp p₂ (baseProjection 𝓕.p)) = cofiberedProduct 𝓗 𝓖

Sources

LeanDeformation.IsCofiberedInGroupoids · Deformation.isCofiberedInGroupoids_twoFibreProductBasedCategory · Deformation.cofiberedProduct · Deformation.isCofiberedInGroupoids_cofiberedProduct · Deformation.isomorphismClasses · Deformation.twoFibreProductBasedCategory_comp_baseProjection

Section90.6 Prorepresentable functors and predeformation categories #

Section 90.6 of the Stacks Project, Tag 06GI. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06GX, a definition

Tag 06GX in the Stacks Project.

Deformation.IsProrepresentable, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/Basic.lean, line 717.

A functor on Artinian local Λ-algebras is prorepresentable if it is naturally isomorphic to the restriction of the covariant representable functor of some Noetherian complete local Λ-algebra.

abbrev IsProrepresentable {Λ : Type u} {k : Type w} [CommRing Λ] [Field k]
    [Algebra Λ k] (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type v) : Prop

Tag 06GS, a definition

Tag 06GS in the Stacks Project.

Deformation.IsPredeformationCategory, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/Basic.lean, line 139. The attribute's comment: “objects”.

A functor to 𝒞_Λ presents a predeformation category when it is cofibered in groupoids and its fibre over the residue field k is equivalent to the category with one object and one morphism.

structure IsPredeformationCategory {Λ : Type u} {k : Type w} [CommRing Λ]
  [Field k] [Algebra Λ k] {F : Type u₁} [Category.{v₁} F] (p : F ⥤ ArtinianLocalAlgCat.{u, max v w,
    w} Λ k) : Prop

Declarations registered for the tag:

BasedFunctor registered with add_to_stacks in StacksFrontier/Deformation/Predeformation/Basic.lean, line 147 (StacksFrontier): “morphisms”.

Tag 06GT, a remark

Tag 06GT in the Stacks Project.

Deformation.isPredeformationFunctor_isomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/Associated.lean, line 37.

The associated functor of isomorphism classes of a predeformation category is a predeformation functor.

public theorem isPredeformationFunctor_isomorphismClasses
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{v₁, u₁}
      (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (h𝓕 : IsPredeformationCategory 𝓕.p) :
    IsPredeformationFunctor
      (isomorphismClasses 𝓕 h𝓕.cofibered)

Deformation.IsPredeformationFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/Basic.lean, line 611. The attribute's comment: “predeformation_functor”.

A set-valued functor on 𝒞_Λ is a predeformation functor when its value at the residue field k is a one-element set.

public abbrev IsPredeformationFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t) : Prop

Deformation.isPredeformationCategory_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/Basic.lean, line 619. The attribute's comment: “predeformation_functor”.

A functor is a predeformation functor exactly when its associated cofibered set, the category of elements, is a predeformation category.

public theorem isPredeformationCategory_iff
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t) :
    IsPredeformationCategory (Functor.Elements.π F) ↔
      IsPredeformationFunctor F

Tag 06GU, a remark

Tag 06GU in the Stacks Project.

Deformation.objectsOverFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/Basic.lean, line 251. The attribute's comment: “category_of_objects_over_x”.

The structure functor on the category of arrows in F with target x, obtained by forgetting the arrow to x and then applying p.

def objectsOverFunctor (p : F ⥤ C)
  (x : F) : Over x ⥤ C

Deformation.isPredeformationCategory_objectsOverFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/Basic.lean, line 403.

Localizing a category cofibered in groupoids at an object of its special fibre gives a predeformation category.

public theorem isPredeformationCategory_objectsOverFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    IsPredeformationCategory
      (objectsOverFunctor p x.1)

Declarations registered for the tag:

CategoryTheory.Over registered with add_to_stacks in StacksFrontier/Deformation/Predeformation/Basic.lean, line 229 (StacksFrontier): “category_of_objects_over_x”. References: EGA I (10.4.7); EGA I (2.5.1); EGA I (3.3.1); EGA IV (14.5.8); SGA 1 V (6.13); SGA 1 VIII (5.2), “fiber over S”; SGA 3 I (1.3); SGA 3 VIIA (4.0), “more general”; SGA 3 VIII (1.0.3); SGA 4 III (5.1), “special case”; SGA 4 IV (5.1); SGA 4 IV (7.1.8), “more general”; SGA 4 VI (4.1), “partial”; SGA 4½ Arcata (1.6.4), “partial”; SGA 7 VI (3.1(a)), “partial”.

Sources

LeanDeformation.IsProrepresentable · Deformation.IsPredeformationCategory · BasedFunctor · Deformation.isPredeformationFunctor_isomorphismClasses · Deformation.IsPredeformationFunctor · Deformation.isPredeformationCategory_iff · Deformation.objectsOverFunctor · Deformation.isPredeformationCategory_objectsOverFunctor

Section90.7 Formal objects and completion categories #

Section 90.7 of the Stacks Project, Tag 06H2. 14 tags here are carried by 46 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06H3, a definition

Tag 06H3 in the Stacks Project.

Deformation.FormalObject, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 312. The attribute's comment: “objects”. References: SGA 7 VI (1.15).

A formal object of a category F over 𝒞_Λ consists of a complete local algebra R, an object of F over each positive adic truncation of R, and transition maps lying over the quotient projections.

structure FormalObject {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)

Deformation.FormalObject.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 334. The attribute's comment: “morphisms”.

A morphism of formal objects is a morphism of their complete local bases together with a compatible family of morphisms over its maps on all adic truncations.

structure Hom (X Y : FormalObject p)

Deformation.FormalObject.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 397. The attribute's comment: “category structure”.

Formal objects and their compatible families of morphisms form a category.

instance instCategory : Category (FormalObject p)

Tag 06H4, a lemma

Tag 06H4 in the Stacks Project.

Deformation.formalObjectProjection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 476. References: SGA 7 VI (1.15), “Â is cofibered over Ĉ_{Λ”.

Stacks Project, Tag 06H4. The projection from the category of formal objects of a category cofibered in groupoids to the category of complete local algebras is cofibered in groupoids.

public theorem formalObjectProjection_isCofiberedInGroupoids
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p) :
    IsCofiberedInGroupoids (FormalObject.projection (p := p))

Tag 06H5, a definition

Tag 06H5 in the Stacks Project.

Deformation.FormalObject.projection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 410. The attribute's comment: “the completion of a category cofibered in groupoids”.

The canonical functor from formal objects to their underlying complete local algebras.

def projection : FormalObject p ⥤ CompleteLocalAlgCat.{u, v, w} Λ k

Tag 06H6, a lemma

Tag 06H6 in the Stacks Project.

Deformation.filteredFormalObjectsEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Filtration/Equivalence.lean, line 655.

A cofinal ideal filtration gives the same category of formal objects over R as the maximal-ideal filtration.

theorem filteredFormalObjectsEquivalence {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (R : CompleteLocalAlgCat.{u, v, w} Λ k) (I : IdealFiltration R)
    (hp : IsCofiberedInGroupoids p) :
    Nonempty
      (FilteredFormalObject p R I ≌
        (FormalObject.projection (p := p)).Fiber R)

Tag 06H8, a remark

Tag 06H8 in the Stacks Project.

Deformation.cofiberedCompletion_obj_equiv_formalObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/CofiberedCompletion.lean, line 721. The attribute's comment: “the completion of a set-valued functor is the limit over the adic truncations”.

A section of the completed cofibered set at S is a formal object of the category of elements of F whose base is S.

public noncomputable def cofiberedCompletion_obj_equiv_formalObject
    (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type (max v z))
    (S : CompleteLocalAlgCat.{u, v, w} Λ k) :
    (cofiberedCompletion.obj F).obj S ≃
      {X : FormalObject (CategoryOfElements.π F) // X.base = S}

Tag 06SJ, a remark

Tag 06SJ in the Stacks Project.

Deformation.restrictionCompletionEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/RestrictionEquivalence/Equivalence.lean, line 436. References: SGA 7 VI (1.15), “special case”.

Restricting the category of formal objects of a category cofibered in groupoids back to Artinian local algebras gives a canonical equivalence with the original category.

public noncomputable def restrictionCompletionEquivalence
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p) : RestrictionCompletionEquivalence p

Tag 06H9, a remark

Tag 06H9 in the Stacks Project.

Deformation.completionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 703. The attribute's comment: “completion_morphism”.

Stacks Project, Tag 06H9. A functor over the category of Artinian local algebras induces a functor on formal objects by application at every level.

public def completionMap
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q)) :
    BasedFunctor
      (BasedCategory.ofFunctor (FormalObject.projection (p := p)))
      (BasedCategory.ofFunctor (FormalObject.projection (p := q)))

Deformation.completionMap_obj_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 742. The attribute's comment: “completion_morphism”.

The induced functor does not change the complete local algebra underlying a formal object.

public theorem completionMap_obj_base
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (X : FormalObject p) :
    ((completionMap φ).obj X).base = X.base

Deformation.completionMap_obj_level, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 749. The attribute's comment: “completion_morphism”.

On objects, the induced completion functor applies the original functor at every level.

public theorem completionMap_obj_level
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (X : FormalObject p) (n : ℕ) :
    ((completionMap φ).obj X).level n = φ.obj (X.level n)

Deformation.completionMap_obj_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 757. The attribute's comment: “completion_morphism”.

On objects, the induced completion functor applies the original functor to every transition map.

public theorem completionMap_obj_transition
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (X : FormalObject p) (n : ℕ) :
    ((completionMap φ).obj X).transition n =
      eqToHom (completionMap_obj_level φ X (n + 1)) ≫ φ.map (X.transition n) ≫
        eqToHom (completionMap_obj_level φ X n).symm

Deformation.completionMap_map_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 769. The attribute's comment: “completion_morphism”.

The induced functor does not change the morphism of complete local algebras underlying a morphism of formal objects.

public theorem completionMap_map_base
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    {X Y : FormalObject p} (f : X ⟶ Y) :
    ((completionMap φ).map f).base =
      eqToHom (completionMap_obj_base φ X) ≫ f.base ≫
        eqToHom (completionMap_obj_base φ Y).symm

Deformation.completionMap_map_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 780. The attribute's comment: “completion_morphism”.

On morphisms, the induced completion functor applies the original functor to every level map.

public theorem completionMap_map_app
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    {X Y : FormalObject p} (f : X ⟶ Y) (n : ℕ) :
    ((completionMap φ).map f).app n =
      eqToHom (completionMap_obj_level φ X n) ≫ φ.map (f.app n) ≫
        eqToHom (completionMap_obj_level φ Y n).symm

Deformation.completionMap_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 804. The attribute's comment: “completion_two_functor”.

Stacks Project, Tag 06H9. Completion takes the identity morphism of a category cofibered in groupoids to the identity morphism of its completion. Together with completionMap_comp, completionNatTrans_id and completionNatTrans_comp this is the statement that completion is a functor of two-categories; the equality is strict, not merely up to isomorphism.

public theorem completionMap_id :
    completionMap (BasedFunctor.id (BasedCategory.ofFunctor p)) =
      BasedFunctor.id (BasedCategory.ofFunctor (FormalObject.projection (p := p)))

Deformation.completionMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 814. The attribute's comment: “completion_two_functor”.

Stacks Project, Tag 06H9. Completion takes a composite of morphisms of categories cofibered in groupoids to the composite of the completions. Together with completionMap_id, completionNatTrans_id and completionNatTrans_comp this is the statement that completion is a functor of two-categories; the equality is strict, not merely up to isomorphism.

public theorem completionMap_comp {H : Type uH} [Category.{vH} H]
    {r : H ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (ψ : BasedFunctor (BasedCategory.ofFunctor q) (BasedCategory.ofFunctor r)) :
    completionMap (φ.comp ψ) = (completionMap φ).comp (completionMap ψ)

Deformation.completionNatTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 839. The attribute's comment: “completion_two_morphism”.

Stacks Project, Tag 06H9. The natural transformation induced levelwise on formal objects by a two-morphism over the Artinian base.

public def completionNatTrans
    {φ ψ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q)}
    (t : BasedNatTrans φ ψ) :
    BasedNatTrans (completionMap φ) (completionMap ψ)

Deformation.completionNatTrans_app_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 963. The attribute's comment: “completion_two_morphism”.

The induced component is the identity on the complete local algebra.

public theorem completionNatTrans_app_base
    {φ ψ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q)}
    (t : BasedNatTrans φ ψ) (X : FormalObject p) :
    ((completionNatTrans t).toNatTrans.app X).base =
      eqToHom (completionMap_obj_base φ X) ≫
        eqToHom (completionMap_obj_base ψ X).symm

Deformation.completionNatTrans_app_level, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 973. The attribute's comment: “completion_two_morphism”.

At every Artinian quotient, the induced component is the original two-morphism.

public theorem completionNatTrans_app_level
    {φ ψ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q)}
    (t : BasedNatTrans φ ψ) (X : FormalObject p) (n : ℕ) :
    ((completionNatTrans t).toNatTrans.app X).app n =
      eqToHom (completionMap_obj_level φ X n) ≫
        t.toNatTrans.app (X.level n) ≫
          eqToHom (completionMap_obj_level ψ X n).symm

Deformation.completionNatTrans_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 986. The attribute's comment: “completion_two_functor”.

Stacks Project, Tag 06H9. Levelwise completion takes an identity two-morphism to an identity. This is half of the statement that completion is a functor of two-categories on two-morphisms.

public theorem completionNatTrans_id
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q)) :
    completionNatTrans (𝟙 φ) = 𝟙 (completionMap φ)

Deformation.completionNatTrans_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Basic.lean, line 1003. The attribute's comment: “completion_two_functor”.

Stacks Project, Tag 06H9. Levelwise completion is compatible with composition of two-morphisms. This is the other half of the statement that completion is a functor of two-categories on two-morphisms.

public theorem completionNatTrans_comp
    {φ ψ χ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q)}
    (t : φ ⟶ ψ) (s : ψ ⟶ χ) :
    completionNatTrans (t ≫ s) =
      BasedNatTrans.comp (completionNatTrans t) (completionNatTrans s)

Tag 06HA, a remark

Tag 06HA in the Stacks Project.

Deformation.completionHomEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/HomEquivalenceMain.lean, line 45. The attribute's comment: “hom_equivalence”.

Stacks Project, Tag 06HA (hom equivalence). Completion and restriction induce quasi-inverse equivalences on hom categories, with the forward and backward formulas specified above.

public noncomputable def completionHomEquivalence
    (hp : IsCofiberedInGroupoids p)
    (hq : IsCofiberedInGroupoids q) :
    CompletionHomEquivalence p q hp hq

Deformation.completionUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Unit.lean, line 512. The attribute's comment: “unit”.

Stacks Project, Tag 06HA (unit). Chosen pushforwards along all adic quotient maps assemble canonically into a morphism from a category cofibered in groupoids to the category of formal objects of its restriction. It sends an object to its tower of chosen pushforwards, with the induced transition maps.

public noncomputable def completionUnit
    {G : Type uG} [Category.{vG} G]
    (p : G ⥤ CompleteLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p) :
    CompletionUnit p (adicPushforwardChoice p hp)

Tag 06HB, a remark

Tag 06HB in the Stacks Project.

Deformation.cofiberedCompletion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/CofiberedCompletion.lean, line 78. The attribute's comment: “completion functor”.

Completion of a cofibered set, viewed as a covariant set-valued functor. Its sections over a complete local algebra are the compatible families of values on the Artinian truncations.

public noncomputable def cofiberedCompletion :
    (ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type (max v z)) ⥤
      (CompleteLocalAlgCat.{u, v, w} Λ k ⥤ Type (max v z))

Deformation.cofiberedCompletionAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/CofiberedCompletion.lean, line 616. The attribute's comment: “functorial hom bijection”.

Completion is right adjoint to restriction; its hom equivalence is the functorial bijection from maps out of a restriction to maps into a completion.

public noncomputable def cofiberedCompletionAdjunction :
    (Functor.whiskeringLeft
      (ArtinianLocalAlgCat.{u, v, w} Λ k)
      (CompleteLocalAlgCat.{u, v, w} Λ k)
      (Type (max v z))).obj
      (artinianToComplete (Λ := Λ) (k := k)) ⊣
      cofiberedCompletion (Λ := Λ) (k := k)

Deformation.cofiberedCompletion_isRightKanExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/CofiberedCompletion.lean, line 686. The attribute's comment: “canonical completion”.

Completion is the right Kan extension of a set-valued functor along the inclusion of Artinian local algebras, with the comparison supplied by the adjunction counit.

public theorem cofiberedCompletion_isRightKanExtension
    (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type (max v z)) :
    (cofiberedCompletion (Λ := Λ) (k := k) |>.obj F).IsRightKanExtension
      ((cofiberedCompletionAdjunction (Λ := Λ) (k := k)).counit.app F)

Deformation.cofiberedCompletion_obj_equiv_formalObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/CofiberedCompletion.lean, line 721. The attribute's comment: “formal-object description”.

A section of the completed cofibered set at S is a formal object of the category of elements of F whose base is S.

public noncomputable def cofiberedCompletion_obj_equiv_formalObject
    (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type (max v z))
    (S : CompleteLocalAlgCat.{u, v, w} Λ k) :
    (cofiberedCompletion.obj F).obj S ≃
      {X : FormalObject (CategoryOfElements.π F) // X.base = S}

Deformation.cofiberedCompletion_restriction_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/CofiberedCompletion.lean, line 731. The attribute's comment: “counit isomorphism”.

The canonical map from the restriction of a completion to the original cofibered set is an isomorphism.

public theorem cofiberedCompletion_restriction_isIso
    (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type (max v z)) :
    IsIso ((cofiberedCompletionAdjunction (Λ := Λ) (k := k)).counit.app F)

Tag 06HE, a remark

Tag 06HE in the Stacks Project.

Deformation.coyonedaIsoAdicCompletion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Completion.lean, line 380. The attribute's comment: “representable_completion”. References: SGA 3 XI (3.3), “representable, affine”.

The covariant functor represented by R is canonically the adic completion of its restriction to Artinian local algebras.

public noncomputable def coyonedaIsoAdicCompletion
    (R : CompleteLocalAlgCat.{u, v, w} Λ k) :
    coyoneda.obj (Opposite.op R) ≅
      adicCompletion (artinianToComplete ⋙
        coyoneda.obj (Opposite.op R))

Deformation.coyonedaIsoAdicCompletion_hom_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Completion.lean, line 399. The attribute's comment: “representable_completion”.

At level n, the canonical isomorphism sends f : R ⟶ S to the composite of f with the quotient homomorphism S → S / m_S ^ (n + 1).

public theorem coyonedaIsoAdicCompletion_hom_apply
    (R S : CompleteLocalAlgCat.{u, v, w} Λ k) (f : R ⟶ S) (n : ℕ) :
    (((coyonedaIsoAdicCompletion R).hom.app S f).value n).hom =
      (Ideal.Quotient.mkₐ Λ (AdicTruncation.ideal S n)).comp f.hom

Deformation.adicCompletionRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Completion.lean, line 814. The attribute's comment: “continuous_functor_completion”.

A limit-preserving functor on complete local algebras is canonically the completion of its restriction to Artinian local algebras.

public noncomputable def adicCompletionRestrictionIso
    (G : CompleteLocalAlgCat.{u, v, w} Λ k ⥤ Type v)
    [PreservesLimits G] :
    G ≅ adicCompletion (artinianToComplete ⋙ G)

Deformation.adicCompletionRestrictionIso_hom_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Completion.lean, line 843. The attribute's comment: “continuous_functor_completion”.

The canonical isomorphism sends a value to its image on each adic quotient. The formula is independent of the chosen morphism representing that quotient.

public theorem adicCompletionRestrictionIso_hom_apply
    (G : CompleteLocalAlgCat.{u, v, w} Λ k ⥤ Type v)
    [PreservesLimits G]
    (S : CompleteLocalAlgCat.{u, v, w} Λ k) (x : G.obj S) (n : ℕ)
    (q : S ⟶ artinianToComplete.obj (AdicTruncation.obj S n))
    (hq : q.hom = Ideal.Quotient.mkₐ Λ (AdicTruncation.ideal S n)) :
    ((adicCompletionRestrictionIso G).hom.app S x).value n = G.map q x

Tag 06HC, a remark

Tag 06HC in the Stacks Project.

Deformation.associatedMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/Associated.lean, line 358. The attribute's comment: “associated_morphism_of_formal_object”. References: SGA 7 VI (2.2(d)), “construction of ξ^#”.

Stacks Project, Tag 06HC. After choosing pushforwards, a formal object ξ over R determines a morphism from the restriction of the cofibered set represented by R to F. On an Artinian point α : R → A, it is the pushforward of the level indexed by the least nilpotence exponent of the maximal ideal of A, minus one.

public noncomputable def associatedMorphism
    (hp : IsCofiberedInGroupoids p) (ξ : FormalObject p)
    (pushforwards : ChosenPushforwards p) : AssociatedMorphism ξ pushforwards

Deformation.formalObjectsYonedaEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/YonedaEquivalence.lean, line 385. The attribute's comment: “formal_objects_yoneda_equivalence”.

Morphisms over the Artinian base from the restriction of the functor represented by R to a category cofibered in groupoids form a category equivalent to the category of formal objects over R, with the quasi-inverse Ψ ∘ ι. The forward direction is the equivalence constructed in Tag 06SK by representableMorphismFormalObjectEquivalence, so it carries that construction's explicit description at the Artinian quotient points of R and its factorization through Φ followed by 2-Yoneda evaluation.

public noncomputable def formalObjectsYonedaEquivalence
    (hp : IsCofiberedInGroupoids p)
    (R : CompleteLocalAlgCat.{u, v, w} Λ k)
    (P : ChosenCompletePushforwards (FormalObject.projection (p := p))) :
    BasedFunctor
        (BasedCategory.ofFunctor (Functor.Elements.π (restrictedCoyoneda R)))
        (BasedCategory.ofFunctor p) ≌
      (FormalObject.projection (p := p)).Fiber R

Deformation.formalObjectsYonedaEquivalence_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/YonedaEquivalence.lean, line 401. The attribute's comment: “formal_objects_yoneda_equivalence”.

The forward direction of the Yoneda equivalence is the equivalence constructed in Tag 06SK. Its levelIso and transition_comm give the explicit description sending φ to the formal object (R, φ(R → R/𝔪_R^n), φ(f_n)), and its completionComparison exhibits it as Φ followed by 2-Yoneda evaluation.

public theorem formalObjectsYonedaEquivalence_functor
    (hp : IsCofiberedInGroupoids p)
    (R : CompleteLocalAlgCat.{u, v, w} Λ k)
    (P : ChosenCompletePushforwards (FormalObject.projection (p := p))) :
    (formalObjectsYonedaEquivalence hp R P).functor =
      (representableMorphismFormalObjectEquivalence p hp R).equivalence.functor

Deformation.formalObjectsYonedaEquivalence_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/YonedaEquivalence.lean, line 411. The attribute's comment: “formal_objects_yoneda_equivalence”.

The quasi-inverse of the Yoneda equivalence is the composite Ψ ∘ ι specified in the source.

public theorem formalObjectsYonedaEquivalence_inverse
    (hp : IsCofiberedInGroupoids p)
    (R : CompleteLocalAlgCat.{u, v, w} Λ k)
    (P : ChosenCompletePushforwards (FormalObject.projection (p := p))) :
    (formalObjectsYonedaEquivalence hp R P).inverse = iotaCompPsi hp R P

Deformation.associatedMorphism_maps_to_canonicalEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/YonedaEquivalence.lean, line 665. The attribute's comment: “formal_objects_yoneda_equivalence”.

The explicit morphism ξ̲ associated to a formal object ξ maps to ξ under the Yoneda equivalence: evaluating the equivalence constructed in Tag 06SK on associatedMorphism hp ξ pushforwards returns ξ, up to an isomorphism over its complete local base.

public theorem associatedMorphism_maps_to_canonicalEquivalence
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : IsCofiberedInGroupoids p)
    (ξ : FormalObject p)
    (pushforwards : ChosenPushforwards p) :
    Nonempty
      ((representableMorphismFormalObjectEquivalence p hp ξ.base).equivalence.functor.obj
        (associatedMorphism hp ξ pushforwards).toBasedFunctor ≅
          (Functor.Fiber.mk rfl : (FormalObject.projection (p := p)).Fiber ξ.base))

Deformation.psiIotaIsoAssociatedMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/YonedaEquivalence.lean, line 700. The attribute's comment: “formal_objects_yoneda_equivalence”.

The explicit Ψ(ι(ξ)) is isomorphic, over the Artinian base, to the morphism ξ̲ associated to ξ using any chosen pushforwards in the original category.

public noncomputable def psiIotaIsoAssociatedMorphism
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : IsCofiberedInGroupoids p)
    (ξ : FormalObject p)
    (pushforwards : ChosenPushforwards p)
    (P : ChosenCompletePushforwards (FormalObject.projection (p := p))) :
    (psi hp ξ.base).obj ((iota ξ.base P).obj
        (Functor.Fiber.mk rfl : (FormalObject.projection (p := p)).Fiber ξ.base)) ≅
      (associatedMorphism hp ξ pushforwards).toBasedFunctor

Deformation.iotaIsoCompletionAssociatedMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/YonedaEquivalence.lean, line 719. The attribute's comment: “formal_objects_yoneda_equivalence”.

Under the canonical represented-completion identification, ι(ξ) is the completion of the associated morphism ξ̲: Φ is the unit followed by levelwise completion, as in 06HA.

public noncomputable def iotaIsoCompletionAssociatedMorphism
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : IsCofiberedInGroupoids p)
    (ξ : FormalObject p)
    (pushforwards : ChosenPushforwards p)
    (P : ChosenCompletePushforwards (FormalObject.projection (p := p))) :
    (iota ξ.base P).obj
        (Functor.Fiber.mk rfl : (FormalObject.projection (p := p)).Fiber ξ.base) ≅
      (unitBasedFunctor (representedProjection ξ.base)
        (representedProjection_cofibered ξ.base)).comp
          (completionMap
            ((extendRepresentedHom p ξ.base).obj
              (associatedMorphism hp ξ pushforwards).toBasedFunctor))

Declarations registered for the tag:

representableMorphismFormalObjectEquivalence registered with add_to_stacks in StacksFrontier/Deformation/FormalObject/YonedaEquivalence.lean, line 419 (StacksFrontier): “formal_objects_yoneda_equivalence”.

Tag 06SK, an equation

Tag 06SK in the Stacks Project.

Deformation.representableMorphismFormalObjectEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/RepresentableMorphism/FormalObjectEquivalence.lean, line 70.

Morphisms from the restriction of the functor represented by R to a category cofibered in groupoids are canonically equivalent to formal objects over R.

public noncomputable def representableMorphismFormalObjectEquivalence
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (R : CompleteLocalAlgCat.{u, v, w} Λ k) :
    RepresentableMorphismFormalObjectEquivalence p R

Tag 06SL, a remark

Tag 06SL in the Stacks Project.

Deformation.associatedMorphism_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/AssociatedMorphismMap.lean, line 193. The attribute's comment: “existence and component square”.

A morphism of formal objects gives the canonical 2-cell between the associated morphisms of restricted representable categories. Its component at an Artinian point is characterized by the square with the corresponding level map of formal objects.

public theorem associatedMorphism_map
    (hp : IsCofiberedInGroupoids p)
    {ξ η : FormalObject p} (a : ξ ⟶ η)
    (pushforwards : ChosenPushforwards p) :
    let f := restrictedRepresentableMap a.base
    let X := associatedMorphism hp ξ pushforwards
    let Y := associatedMorphism hp η pushforwards
    ∃ τ : BasedFunctor.comp f X.toBasedFunctor ≅ Y.toBasedFunctor,
      ∀ α, ∃ h : X.level (f.obj α) = Y.level α,
        X.pointInclusion (f.obj α) ≫ τ.hom.app α =
          a.app (X.level (f.obj α)) ≫
            eqToHom (congrArg η.level h) ≫ Y.pointInclusion α

Deformation.associatedMorphism_map_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/AssociatedMorphismMap.lean, line 413. The attribute's comment: “uniqueness”.

The commuting square with the level map determines the canonical Yoneda 2-cell uniquely.

public theorem associatedMorphism_map_unique
    (hp : IsCofiberedInGroupoids p)
    {ξ η : FormalObject p} (a : ξ ⟶ η)
    (pushforwards : ChosenPushforwards p) :
    let f := restrictedRepresentableMap a.base
    let X := associatedMorphism hp ξ pushforwards
    let Y := associatedMorphism hp η pushforwards
    ∀ (τ σ : BasedFunctor.comp f X.toBasedFunctor ≅ Y.toBasedFunctor),
      (∀ α, ∃ h : X.level (f.obj α) = Y.level α,
        X.pointInclusion (f.obj α) ≫ τ.hom.app α =
          a.app (X.level (f.obj α)) ≫
            eqToHom (congrArg η.level h) ≫ Y.pointInclusion α) →
      (∀ α, ∃ h : X.level (f.obj α) = Y.level α,
        X.pointInclusion (f.obj α) ≫ σ.hom.app α =
          a.app (X.level (f.obj α)) ≫
            eqToHom (congrArg η.level h) ≫ Y.pointInclusion α) →
      τ = σ

Tag 06HD, a remark

Tag 06HD in the Stacks Project.

Deformation.ProrepresentableMorphism, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/ProrepresentableMorphism.lean, line 82. The attribute's comment: “the data equivalent to a formal object”.

Stacks 06HD. A prorepresentable functor on 𝒞_Λ together with a morphism from its category of elements to a category cofibered over 𝒞_Λ. This is the data Stacks 06HD exhibits as equivalent to a formal object.

structure ProrepresentableMorphism (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)

Deformation.ProrepresentableMorphism.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/ProrepresentableMorphism.lean, line 107. The attribute's comment: “morphisms of the data”.

Stacks 06HD. A morphism of prorepresentable pairs: a natural transformation of the functors in the Yoneda direction, together with a morphism over 𝒞_Λ from the restriction of the source's morphism along it to the target's morphism.

structure Hom {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (X Y : ProrepresentableMorphism p)

Deformation.restrictedCoyonedaMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/ProrepresentableMorphism.lean, line 149. The attribute's comment: “Yoneda for the restricted representable functors”.

Stacks 06HD. Yoneda for 𝒞_Λ: precomposition is a bijection from maps R ⟶ S of complete local algebras onto natural transformations of the restricted representable functors in the opposite direction. The inverse reads off the compatible system of quotient points determined by a natural transformation and uses the completion description of Stacks 06HE.

theorem restrictedCoyonedaMap_bijective (R S : CompleteLocalAlgCat.{u, v, w} Λ k) :
    Function.Bijective (restrictedCoyonedaMap (R := R) (S := S))

Deformation.formalObjectsProrepresentableMorphismEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/ProrepresentableMorphism.lean, line 422. The attribute's comment: “the equivalence with formal objects”.

Stacks 06HD. Spelling out Stacks 06HC: the prorepresentable pairs over p carry a category structure whose morphisms are ProrepresentableMorphism.Hom, and the category of formal objects of p is equivalent to it. The hom equivalence is for the total categories, so it pins down the morphisms between pairs with different prorepresentable functors, not only those over a fixed one.

theorem formalObjectsProrepresentableMorphismEquivalence
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (hp : IsCofiberedInGroupoids p) :
    ∃ c : Category (ProrepresentableMorphism p),
      letI := c
      c.Hom = (fun X Y => ProrepresentableMorphism.Hom X Y) ∧
      Nonempty (FormalObject p ≌ ProrepresentableMorphism p)

Sources

LeanDeformation.FormalObject · Deformation.FormalObject.Hom · Deformation.FormalObject.instCategory · Deformation.formalObjectProjection_isCofiberedInGroupoids · Deformation.FormalObject.projection · Deformation.filteredFormalObjectsEquivalence · Deformation.cofiberedCompletion_obj_equiv_formalObject · Deformation.restrictionCompletionEquivalence

Section90.8 Smooth morphisms #

Section 90.8 of the Stacks Project, Tag 06HF. 11 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06HG, a definition

Tag 06HG in the Stacks Project.

Deformation.IsSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Basic.lean, line 102. References: SGA 7 VI (2.1), “smooth”.

A morphism of categories over \mathcal C_\Lambda is smooth if every lifting problem over a surjective map B \to A has a compatible solution over B.

public abbrev IsSmooth {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, v, w} Λ
  k)} {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, v, w} Λ k)} (φ : BasedFunctor 𝓕 𝓖) : Prop

Tag 06HH, a lemma

Tag 06HH in the Stacks Project.

Deformation.isSmooth_of_lifts_smallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SmoothMorphisms.lean, line 173. References: SGA 7 VI (2.2(a)), “(iii) => (i)”.

For a morphism of categories cofibered in groupoids, the lifting property for small extensions implies the lifting property for every surjective morphism, and hence smoothness.

theorem isSmooth_of_lifts_smallExtensions
    {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p)
    (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖)
    (h : ∀ ⦃B A : ArtinianLocalAlgCat.{u, v, w} Λ k⦄ (f : B ⟶ A),
      IsSmallExtension (CommRingCat.ofHom f.hom.toRingHom) →
        ∀ (y : 𝓖.obj) (x : 𝓕.obj) (g : y ⟶ φ.obj x),
          𝓖.p.IsHomLift f g →
            ∃ (x' : 𝓕.obj) (lift : x' ⟶ x) (a : φ.obj x' ⟶ y),
              𝓕.p.IsHomLift f lift ∧
                𝓖.p.IsHomLift (𝟙 B) a ∧ φ.map lift = a ≫ g) :
    IsSmooth φ

Tag 06HI, a remark

Tag 06HI in the Stacks Project.

Deformation.pushforwardFunctorsFormTwoCommutativeSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Pushforward.lean, line 493. The attribute's comment: “pushforward_square”.

Chosen pushforwards along an arrow in the base give functors between the fibres, and a morphism of categories cofibered in groupoids intertwines these functors up to a natural isomorphism.

public theorem pushforwardFunctorsFormTwoCommutativeSquare
    {C : Type uC} [Category.{vC} C]
    {F : Type uF} [Category.{vF} F] {G : Type uG} [Category.{vG} G]
    (pF : F ⥤ C) (pG : G ⥤ C)
    (hG : IsCofiberedInGroupoids pG)
    (φ : F ⥤ G) (hφ : φ ⋙ pG = pF)
    {B A : C} {f : B ⟶ A}
    (PF : PushforwardChoice pF f) (PG : PushforwardChoice pG f) :
    Nonempty (PushforwardSquare φ hφ PF PG)

Deformation.inducedFunctorToPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Pushforward.lean, line 527. The attribute's comment: “induced_functor”. References: SGA 7 VI (2.6(b)), “induced functor to 2-fp”.

The functor from the source fibre to the categorical pullback induced by a chosen two-commutative pushforward square.

public def inducedFunctorToPullback
    {C : Type uC} [Category.{vC} C]
    {F : Type uF} [Category.{vF} F] {G : Type uG} [Category.{vG} G]
    {pF : F ⥤ C} {pG : G ⥤ C} {φ : F ⥤ G} {hφ : φ ⋙ pG = pF}
    {B A : C} {f : B ⟶ A}
    {PF : PushforwardChoice pF f}
    {PG : PushforwardChoice pG f}
    (Q : PushforwardSquare φ hφ PF PG) :
    pF.Fiber B ⥤
      Limits.CategoricalPullback
        (Functor.Fiber.inducedFunctor (p := pG) (S := A)
          (F := Functor.Fiber.fiberInclusion (p := pF) (S := A) ⋙ φ)
          (by simpa only [Functor.assoc, hφ] using
            (Functor.Fiber.fiberInclusion_comp_eq_const (p := pF) (S := A))))
        Q.target.toFunctor

Deformation.essSurj_inducedFunctorToPullback_of_isSmooth, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/PushforwardSmooth.lean, line 90. The attribute's comment: “smooth_iff_essSurj”.

Stacks Project, Tag 06HI. For a smooth morphism of categories cofibered in groupoids, the functor to the 2-fibre product determined by any choice of pushforwards along a surjection of the base is essentially surjective.

public lemma essSurj_inducedFunctorToPullback_of_isSmooth
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p) (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖) (hsm : IsSmooth φ)
    {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A)
    (hf : Function.Surjective f.hom)
    (PF : PushforwardChoice 𝓕.p f) (PG : PushforwardChoice 𝓖.p f) :
    (inducedFunctorToPullback
      (pushforwardSquareOfChoices 𝓕.p 𝓖.p h𝓖 φ.toFunctor φ.w PF PG)).EssSurj

Deformation.exists_lift_of_inducedFunctorToPullback_essSurj, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/PushforwardSmooth.lean, line 157. The attribute's comment: “smooth_iff_essSurj”. References: SGA 7 VI (2.6(b)), “The 'if' direction”.

Stacks Project, Tag 06HI. If the functor to the 2-fibre product determined by some choice of pushforwards along an arrow f of the base is essentially surjective, then every lifting problem over f has a compatible solution.

public lemma exists_lift_of_inducedFunctorToPullback_essSurj
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p) (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖)
    {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A)
    (hes : ∀ (PF : PushforwardChoice 𝓕.p f) (PG : PushforwardChoice 𝓖.p f),
      (inducedFunctorToPullback
        (pushforwardSquareOfChoices 𝓕.p 𝓖.p h𝓖 φ.toFunctor φ.w PF PG)).EssSurj)
    (y : 𝓖.obj) (x : 𝓕.obj) (g : y ⟶ φ.obj x) (hg : 𝓖.p.IsHomLift f g) :
    ∃ (x' : 𝓕.obj) (lift : x' ⟶ x) (a : φ.obj x' ⟶ y),
      𝓕.p.IsHomLift f lift ∧ 𝓖.p.IsHomLift (𝟙 B) a ∧ φ.map lift = a ≫ g

Deformation.isSmooth_iff_inducedFunctorToPullback_essSurj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/PushforwardSmooth.lean, line 210. The attribute's comment: “smooth_iff_essSurj”.

Stacks Project, Tag 06HI. A morphism of categories cofibered in groupoids over 𝒞_Λ is smooth if and only if, for every surjection B → A of the base and every choice of pushforwards along it, the functor 𝓕(B) ⟶ 𝓕(A) ×_{𝓖(A)} 𝓖(B) determined by those choices is essentially surjective.

public theorem isSmooth_iff_inducedFunctorToPullback_essSurj
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p) (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖) :
    IsSmooth φ ↔
      ∀ ⦃B A : ArtinianLocalAlgCat.{u, v, w} Λ k⦄ (f : B ⟶ A),
        Function.Surjective f.hom →
        ∀ (PF : PushforwardChoice 𝓕.p f) (PG : PushforwardChoice 𝓖.p f),
          (inducedFunctorToPullback
            (pushforwardSquareOfChoices 𝓕.p 𝓖.p h𝓖 φ.toFunctor φ.w PF PG)).EssSurj

Deformation.isSmooth_iff_inducedFunctorToPullback_essSurj_smallExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/PushforwardSmooth.lean, line 227. The attribute's comment: “smooth_iff_essSurj_smallExtension”.

Stacks Project, Tag 06HI. The same equivalence, tested only on small extensions: by Tag 06HH the lifting property for small extensions already implies smoothness.

public theorem isSmooth_iff_inducedFunctorToPullback_essSurj_smallExtension
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p) (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖) :
    IsSmooth φ ↔
      ∀ ⦃B A : ArtinianLocalAlgCat.{u, v, w} Λ k⦄ (f : B ⟶ A),
        IsSmallExtension (CommRingCat.ofHom f.hom.toRingHom) →
        ∀ (PF : PushforwardChoice 𝓕.p f) (PG : PushforwardChoice 𝓖.p f),
          (inducedFunctorToPullback
            (pushforwardSquareOfChoices 𝓕.p 𝓖.p h𝓖 φ.toFunctor φ.w PF PG)).EssSurj

Tag 06HJ, a remark

Tag 06HJ in the Stacks Project.

Deformation.isSmooth_elementsBasedFunctor_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SmoothMorphisms.lean, line 239.

Smoothness of a morphism between categories of elements is equivalent to surjectivity of the usual map to the fibre product for every surjection in 𝒞_Λ.

theorem isSmooth_elementsBasedFunctor_iff
    {F G : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type t} (α : F ⟶ G) :
    IsSmooth (elementsBasedFunctor α) ↔
      ∀ ⦃B A : ArtinianLocalAlgCat.{u, v, w} Λ k⦄ (f : B ⟶ A),
        Function.Surjective f.hom →
          ∀ (xA : F.obj A) (yB : G.obj B),
            α.app A xA = G.map f yB →
            ∃ xB : F.obj B, F.map f xB = xA ∧ α.app B xB = yB

Tag 06HK, a remark

Tag 06HK in the Stacks Project.

Deformation.isSmooth_toIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/IsomorphismClasses.lean, line 425.

The canonical morphism from a category cofibered in groupoids to its associated functor of isomorphism classes is smooth.

public theorem isSmooth_toIsomorphismClasses
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, v, w} Λ k))
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p) :
    IsSmooth (toIsomorphismClasses 𝓕 h𝓕)

Tag 06HL, a lemma

Tag 06HL in the Stacks Project.

Deformation.restrictedRepresentableMap_isSmooth_iff_isPowerSeriesOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/PowerSeries.lean, line 1001. The attribute's comment: “smooth if and only if a power series ring”. References: SGA 7 VI (2.2(c)); SGA 1 III (1.5), “complete local case”.

The morphism between restricted representable categories induced by f : R ⟶ S is smooth if and only if f exhibits S as a formal power series ring in finitely many variables over R.

public theorem restrictedRepresentableMap_isSmooth_iff_isPowerSeriesOver
    {R S : CompleteLocalAlgCat.{u, v, w} Λ k} (f : R ⟶ S) :
    IsSmooth (restrictedRepresentableMap f) ↔ IsPowerSeriesOver f

Tag 06HM, a lemma

Tag 06HM in the Stacks Project.

Deformation.isSmooth_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Basic.lean, line 122. The attribute's comment: “smooth_comp”. References: SGA 7 VI (2.3), “(a)”.

The composite of two smooth morphisms of categories over \mathcal C_\Lambda is smooth.

public theorem isSmooth_comp
    {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓗 : BasedCategory.{v₃, u₃} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    (φ : BasedFunctor 𝓕 𝓖) (ψ : BasedFunctor 𝓖 𝓗)
    (hφ : IsSmooth φ) (hψ : IsSmooth ψ) :
    IsSmooth (BasedFunctor.comp φ ψ)

Deformation.isSmooth_twoFibreProductSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Basic.lean, line 184. The attribute's comment: “smooth_base_change”.

A base change of a smooth morphism of categories cofibered in groupoids is smooth.

public theorem isSmooth_twoFibreProductSnd
    {𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓖 : BasedCategory.{vG, uG} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓖' : BasedCategory.{vG', uG'} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖) (θ : BasedFunctor 𝓖' 𝓖)
    (hφ : IsSmooth φ) : IsSmooth (twoFibreProductSnd φ θ)

Deformation.isSmooth_of_essSurj_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Basic.lean, line 249. The attribute's comment: “smooth_of_essentially_surjective_smooth_comp”. References: SGA 7 VI (2.3), “(b)”.

If the first of two morphisms of categories cofibered in groupoids is essentially surjective and their composite is smooth, then the second morphism is smooth.

public theorem isSmooth_of_essSurj_comp
    {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓗 : BasedCategory.{v₃, u₃} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p)
    (φ : BasedFunctor 𝓕 𝓖) (ψ : BasedFunctor 𝓖 𝓗) [φ.toFunctor.EssSurj]
    (h : IsSmooth (BasedFunctor.comp φ ψ)) : IsSmooth ψ

Tag 06HN, a lemma

Tag 06HN in the Stacks Project.

Deformation.essSurj_of_isSmooth_of_fiber_essSurj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/EssentiallySurjective.lean, line 63. The attribute's comment: “essentially_surjective”.

A smooth morphism of categories over \mathcal C_\Lambda with cofibered target is essentially surjective whenever its special-fibre functor is.

public theorem essSurj_of_isSmooth_of_fiber_essSurj
    {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k)}
    {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, w, w} Λ k)}
    (φ : BasedFunctor 𝓕 𝓖)
    (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (hφ : IsSmooth φ)
    (h₀ : (fiberFunctor φ (residueFieldObject Λ k)).EssSurj) :
    φ.toFunctor.EssSurj

Deformation.completionMap_essSurj_of_isSmooth_of_fiber_essSurj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/EssentiallySurjective.lean, line 278. The attribute's comment: “completion_essentially_surjective”.

A smooth morphism, essentially surjective over the residue field, is essentially surjective after completion.

public theorem completionMap_essSurj_of_isSmooth_of_fiber_essSurj
    {F : Type uF} [Category.{vF} F] {G : Type uG} [Category.{vG} G]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    {q : G ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (hq : IsCofiberedInGroupoids q)
    (hφ : IsSmooth φ)
    (h₀ : (fiberFunctor φ (residueFieldObject Λ k)).EssSurj) :
    (completionMap φ).toFunctor.EssSurj

Tag 06HR, a definition

Tag 06HR in the Stacks Project.

Deformation.IsVersal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Versal.lean, line 94. References: SGA 7 VI (1.19), “(1)”; SGA 7 VI (1.9), “versal formal object”.

A formal object is versal when its associated morphism from the represented functor is smooth, independently of the auxiliary pushforward choices.

public abbrev IsVersal (hp : IsCofiberedInGroupoids p)
    (ξ : FormalObject p) : Prop

Tag 06HS, a remark

Tag 06HS in the Stacks Project.

Deformation.isVersal_iff_lifts_artinian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/VersalLifting.lean, line 716. The attribute's comment: “lifting criterion”. References: SGA 7 VI (2.2(d)), “lifting criterion”; SGA 7 VI (1.9), “versal formal object”; SGA 7 VI (1.19), “(1)”.

Versality is equivalent to solving every lifting triangle in the completion whose lower arrow is a surjective map of Artinian local algebras.

public theorem isVersal_iff_lifts_artinian
    (hp : IsCofiberedInGroupoids p) (ξ : FormalObject p) :
    IsVersal hp ξ ↔
      ∀ {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A),
        Function.Surjective f.hom →
          ∀ {y x : FormalObject p} (g : y ⟶ x),
            (FormalObject.projection (p := p)).IsHomLift
              (artinianToComplete.map f) g →
              ∀ (a : ξ ⟶ x), ∃ b : ξ ⟶ y, b ≫ g = a

Deformation.isVersal_iff_lifts_smallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/VersalLifting.lean, line 745. The attribute's comment: “small-extension criterion”.

In the intrinsic lifting criterion, it suffices to test small extensions of Artinian local algebras.

public theorem isVersal_iff_lifts_smallExtensions
    (hp : IsCofiberedInGroupoids p) (ξ : FormalObject p) :
    IsVersal hp ξ ↔
      ∀ {B A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : B ⟶ A),
        InfinitesimalLifting.IsSmallExtension
          (CommRingCat.ofHom f.hom.toRingHom) →
          ∀ {y x : FormalObject p} (g : y ⟶ x),
            (FormalObject.projection (p := p)).IsHomLift
              (artinianToComplete.map f) g →
              ∀ (a : ξ ⟶ x), ∃ b : ξ ⟶ y, b ≫ g = a

Deformation.isSmooth_associatedMorphism_iff_isVersal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/VersalLifting.lean, line 812. The attribute's comment: “independence of pushforwards”. References: SGA 7 VI (2.2(d)), “smooth ⟺ versal”.

Smoothness of the morphism associated to a formal object is independent of the choices of pushforwards used to construct that morphism.

public theorem isSmooth_associatedMorphism_iff_isVersal
    (hp : IsCofiberedInGroupoids p) (ξ : FormalObject p)
    (pushforwards : ChosenPushforwards p) :
    IsSmooth (associatedMorphism hp ξ pushforwards).toBasedFunctor ↔
      IsVersal hp ξ

Tag 06HT, a lemma

Tag 06HT in the Stacks Project.

Deformation.nonempty_hom_of_isVersal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/MapsToFormalObject.lean, line 306.

A versal formal object admits a morphism to every formal object.

public theorem nonempty_hom_of_isVersal (hp : IsPredeformationCategory p)
    (ξ η : FormalObject p) (hξ : IsVersal hp.cofibered ξ) :
    Nonempty (ξ ⟶ η)

Sources

LeanDeformation.IsSmooth · Deformation.isSmooth_of_lifts_smallExtensions · Deformation.pushforwardFunctorsFormTwoCommutativeSquare · Deformation.inducedFunctorToPullback · Deformation.essSurj_inducedFunctorToPullback_of_isSmooth · Deformation.exists_lift_of_inducedFunctorToPullback_essSurj · Deformation.isSmooth_iff_inducedFunctorToPullback_essSurj · Deformation.isSmooth_iff_inducedFunctorToPullback_essSurj_smallExtension

Section90.9 Smooth or unobstructed categories #

Section 90.9 of the Stacks Project, Tag 0DYK. 4 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06HP, a definition

Tag 06HP in the Stacks Project.

Deformation.IsSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Basic.lean, line 102. The attribute's comment: “smoothness of the structure morphism, i.e. an unobstructed cofibered category”. References: SGA 7 VI (2.1), “smooth”.

A morphism of categories over \mathcal C_\Lambda is smooth if every lifting problem over a surjective map B \to A has a compatible solution over B.

public abbrev IsSmooth {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, v, w} Λ
  k)} {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, v, w} Λ k)} (φ : BasedFunctor 𝓕 𝓖) : Prop

Tag 0DYL, a lemma

Tag 0DYL in the Stacks Project.

Deformation.smooth_formallySmooth_flat_specialFibre_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/CompleteLocalAlgebra/LiftingCriterion.lean, line 662. The attribute's comment: “conditions (1)--(4)”. References: EGA 0 (19.7.1), “complete local case”; EGA 0 (19.6.5), “complete, K=k: (2)⇔(3)”; SGA 7 VI (1.14), “Prorepresentable case”.

Stacks 0DYL. Smoothness of the restricted representable category of R, formal smoothness of Λ → R in the m_R-adic topology, and the two conditions combining flatness with regularity of the special fibre over k' = Λ / ker(Λ → k), are equivalent.

public theorem smooth_formallySmooth_flat_specialFibre_tfae
    (R : CompleteLocalAlgCat.{u, v, w} Λ k) :
    let k' := Λ ⧸ RingHom.ker (algebraMap Λ k)
    letI : (RingHom.ker (algebraMap Λ k)).IsMaximal :=
      Algebra.ker_algebraMap_isMaximal_of_isIntegral Λ k
    letI : Field k' := Ideal.Quotient.field _
    let Bbar := R ⊗[Λ] k'
    letI : Algebra k' Bbar := Algebra.TensorProduct.rightAlgebra
    List.TFAE [
      IsSmooth (restrictedCoyonedaProjection R),
      RingHom.FormallySmoothNAdic.{max u v} (algebraMap Λ R) (maximalIdeal R),
      Module.Flat Λ R ∧ Algebra.IsGeometricallyRegular k' Bbar,
      Module.Flat Λ R ∧
        RingHom.FormallySmoothNAdic.{max u v} (algebraMap k' Bbar)
          ((maximalIdeal R).map Algebra.TensorProduct.includeLeftRingHom)]

Deformation.smooth_formallySmooth_flat_specialFibre_powerSeries_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/CompleteLocalAlgebra/PowerSeriesCase.lean, line 182. The attribute's comment: “condition (5), classical case”. References: EGA 0 (19.7.1), “classical case”; EGA 0 (19.6.5), “complete, K=k: (2)⇔(5)”.

Stacks 0DYL. If the base is classical, the four smoothness conditions are also equivalent to R being a formal power series algebra in finitely many variables over Λ.

public theorem smooth_formallySmooth_flat_specialFibre_powerSeries_tfae
    (R : CompleteLocalAlgCat.{u, v, w} Λ k) (hΛ : IsClassical Λ k) :
    let k' := Λ ⧸ RingHom.ker (algebraMap Λ k)
    letI : (RingHom.ker (algebraMap Λ k)).IsMaximal :=
      Algebra.ker_algebraMap_isMaximal_of_isIntegral Λ k
    letI : Field k' := Ideal.Quotient.field _
    let Bbar := R ⊗[Λ] k'
    letI : Algebra k' Bbar := Algebra.TensorProduct.rightAlgebra
    List.TFAE [
      IsSmooth (restrictedCoyonedaProjection R),
      RingHom.FormallySmoothNAdic.{max u v} (algebraMap Λ R) (maximalIdeal R),
      Module.Flat Λ R ∧ Algebra.IsGeometricallyRegular k' Bbar,
      Module.Flat Λ R ∧
        RingHom.FormallySmoothNAdic.{max u v} (algebraMap k' Bbar)
          ((maximalIdeal R).map Algebra.TensorProduct.includeLeftRingHom),
      ∃ n : ℕ, Nonempty (R ≃ₐ[Λ] MvPowerSeries (Fin n) Λ)]

Tag 0DZK, a lemma

Tag 0DZK in the Stacks Project.

Deformation.isSmooth_baseProjection_iff_formallySmoothNAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Unobstructed.lean, line 196. The attribute's comment: “conditions (1) and (2)”. References: SGA 7 VI (2.4), “P smooth <=> R f.smooth”.

Stacks 0DZK. A predeformation category with a versal formal object over R is unobstructed if and only if Λ → R is formally smooth in the m_R-adic topology.

public theorem isSmooth_baseProjection_iff_formallySmoothNAdic
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hp : IsPredeformationCategory p)
    (ξ : FormalObject p) (hξ : IsVersal hp.cofibered ξ) :
    IsSmooth (baseProjection p) ↔
      RingHom.FormallySmoothNAdic.{max u (max v w)}
        (algebraMap Λ ξ.base) (maximalIdeal ξ.base)

Deformation.isSmooth_baseProjection_iff_powerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Smooth/Unobstructed.lean, line 223. The attribute's comment: “condition (3), classical case”. References: SGA 7 VI (2.4), “P smooth <=> R=Λ[[x]]”; SGA 7 VI (1.14), “more general”.

Stacks 0DZK. In the classical case, a predeformation category with a versal formal object over R is unobstructed if and only if R is a formal power series algebra in finitely many variables over Λ.

public theorem isSmooth_baseProjection_iff_powerSeries
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hp : IsPredeformationCategory p)
    (ξ : FormalObject p) (hξ : IsVersal hp.cofibered ξ)
    (hΛ : IsClassical Λ k) :
    IsSmooth (baseProjection p) ↔
      ∃ n : ℕ, Nonempty (ξ.base ≃ₐ[Λ] MvPowerSeries (Fin n) Λ)

Tag 06SM, a lemma

Tag 06SM in the Stacks Project.

Deformation.smoothModel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/SmoothModel.lean, line 944. The attribute's comment: “the object”.

A complete local algebra realizing the smooth deformation base.

public noncomputable def smoothModel : CompleteLocalAlgCat.{u, max u w, w} Λ k

Deformation.smoothModel_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/SmoothModel.lean, line 957. The attribute's comment: “smoothness”.

The chosen complete local algebra is formally smooth over Λ for the maximal-ideal-adic topology.

public theorem smoothModel_formallySmooth :
    RingHom.FormallySmoothNAdic.{max u w}
      (algebraMap Λ (smoothModel (Λ := Λ) (k := k)))
      (maximalIdeal (smoothModel (Λ := Λ) (k := k)))

Deformation.smoothModel_h1Cotangent_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/SmoothModel.lean, line 968. The attribute's comment: “first cotangent homology”.

For the chosen complete local algebra R, the canonical map H₁(L_{k/Λ}) → H₁(L_{k/R}) is bijective. Since R → k is surjective the target is canonically the conormal module 𝔪_R/𝔪_R², so this is the conormal description of H₁(L_{k/Λ}).

public theorem smoothModel_h1Cotangent_bijective :
    let R := smoothModel (Λ := Λ) (k := k)
    letI : Algebra R k := (smoothModelResidue (Λ := Λ) (k := k)).toRingHom.toAlgebra
    letI : IsScalarTower Λ R k :=
      IsScalarTower.of_algebraMap_eq'
        (smoothModelResidue (Λ := Λ) (k := k)).comp_algebraMap.symm
    Function.Bijective (Algebra.H1Cotangent.map Λ R k k)

Deformation.smoothModel_mapBaseChange_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Completed/SmoothModel.lean, line 981. The attribute's comment: “differentials”.

For the chosen complete local algebra R, the canonical base-change map k ⊗_R Ω[R⁄Λ] → Ω[k⁄Λ] is bijective.

public theorem smoothModel_mapBaseChange_bijective :
    let R := smoothModel (Λ := Λ) (k := k)
    letI : Algebra R k := (smoothModelResidue (Λ := Λ) (k := k)).toRingHom.toAlgebra
    letI : IsScalarTower Λ R k :=
      IsScalarTower.of_algebraMap_eq'
        (smoothModelResidue (Λ := Λ) (k := k)).comp_algebraMap.symm
    Function.Bijective (KaehlerDifferential.mapBaseChange Λ R k)

Sources

LeanDeformation.IsSmooth · Deformation.smooth_formallySmooth_flat_specialFibre_tfae · Deformation.smooth_formallySmooth_flat_specialFibre_powerSeries_tfae · Deformation.isSmooth_baseProjection_iff_formallySmoothNAdic · Deformation.isSmooth_baseProjection_iff_powerSeries · Deformation.smoothModel · Deformation.smoothModel_formallySmooth · Deformation.smoothModel_h1Cotangent_bijective

Section90.10 Schlessinger's conditions #

Section 90.10 of the Stacks Project, Tag 06HV. 9 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06HW, a definition

Tag 06HW in the Stacks Project.

Deformation.SchlessingerConditionS1, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Basic.lean, line 148. The attribute's comment: “condition (S1)”. References: SGA 7 VI (1.16), “(I)”.

Schlessinger's condition (S1): every cospan whose second base map is surjective has a completion over a pullback square in C_Λ.

public structure SchlessingerConditionS1
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] {F : Type u₁} [Category.{v₁} F]
      (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) : Prop

Deformation.SchlessingerConditionS2, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Basic.lean, line 161. The attribute's comment: “condition (S2)”.

Schlessinger's condition (S2): completions exist when the second map is the dual-number projection, and any two completions over the same base square admit the required fibrewise comparison morphism.

public structure SchlessingerConditionS2
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] {F : Type u₁} [Category.{v₁} F]
      (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) : Prop

Tag 06SP, an equation

Tag 06SP in the Stacks Project.

Deformation.squareComparisonFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Comparison.lean, line 92.

Stacks Project, Tag 06SP. For a pullback square of Artinian local Λ-algebras with f₂ surjective, choices of pushforwards in a category cofibered in groupoids determine the canonical comparison functor F(P) ⟶ F(A₁) ×_{F(A)} F(A₂).

public noncomputable def squareComparisonFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (_hp : IsCofiberedInGroupoids p)
    {P A₁ A₂ A : ArtinianLocalAlgCat.{u, v, w} Λ k}
    (p₁ : P ⟶ A₁) (p₂ : P ⟶ A₂) (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A)
    (hP : IsPullback p₁ p₂ f₁ f₂) (_hf₂ : Function.Surjective f₂.hom)
    (P₁ : PushforwardChoice p p₁) (P₂ : PushforwardChoice p p₂)
    (F₁ : PushforwardChoice p f₁) (F₂ : PushforwardChoice p f₂)
    (Qp₁ : PushforwardFunctor P₁) (Qp₂ : PushforwardFunctor P₂)
    (Qf₁ : PushforwardFunctor F₁) (Qf₂ : PushforwardFunctor F₂) :
    SquareComparisonFunctor p p₁ p₂ f₁ f₂ P₁ P₂ F₁ F₂ Qp₁ Qp₂ Qf₁ Qf₂

Tag 06HX, a lemma

Tag 06HX in the Stacks Project.

Deformation.schlessingerConditionS1_of_smallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SmallExtensions.lean, line 288.

The small-extension cases of the completion property suffice for Schlessinger's condition (S1).

theorem schlessingerConditionS1_of_smallExtensions
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : IsCofiberedInGroupoids p)
    (h : ∀ {x₁ x₂ x : F} (f₁ : x₁ ⟶ x) (f₂ : x₂ ⟶ x),
      IsSmallExtension (CommRingCat.ofHom (p.map f₂).hom.toRingHom) →
        ∀ {A₁₂ : ArtinianLocalAlgCat.{u, v, w} Λ k}
          (g₁ : A₁₂ ⟶ p.obj x₁) (g₂ : A₁₂ ⟶ p.obj x₂),
          IsPullback g₂ g₁ (p.map f₂) (p.map f₁) →
            Nonempty (PullbackCompletion p f₁ f₂ g₁ g₂)) :
    SchlessingerConditionS1 p

Tag 06HY, a remark

Tag 06HY in the Stacks Project.

Deformation.schlessingerConditionS1_elements_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SetValuedFunctor.lean, line 119. The attribute's comment: “condition (S1)”.

For the category of elements of F : 𝒞_Λ ⥤ Type t, Schlessinger's condition (S1) says that the map F(A₁ ×_A A₂) → F(A₁) ×_{F(A)} F(A₂) is surjective whenever A₂ → A is surjective.

theorem schlessingerConditionS1_elements_iff
    (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type t) :
    SchlessingerConditionS1 (Functor.Elements.π F) ↔
      ∀ ⦃A₁ A₂ A A₁₂ : ArtinianLocalAlgCat.{u, v, w} Λ k⦄ (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A),
        Function.Surjective f₂.hom →
          ∀ (g₁ : A₁₂ ⟶ A₁) (g₂ : A₁₂ ⟶ A₂) (hPB : IsPullback g₂ g₁ f₂ f₁),
            Function.Surjective (fibreProductComparison F g₁ g₂ f₁ f₂ hPB.w)

Deformation.schlessingerConditionS2_elements_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SetValuedFunctor.lean, line 140. The attribute's comment: “condition (S2)”.

For the category of elements of F : 𝒞_Λ ⥤ Type t, Schlessinger's condition (S2) says that the map F(A ×_k k[ε]) → F(A) ×_{F(k)} F(k[ε]) is bijective.

theorem schlessingerConditionS2_elements_iff
    (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type t) :
    SchlessingerConditionS2 (Functor.Elements.π F) ↔
      ∀ ⦃A A₀ Aε B : ArtinianLocalAlgCat.{u, v, w} Λ k⦄ (d : A ⟶ A₀) (e : Aε ⟶ A₀),
        IsDualNumberProjection e →
          ∀ (g : B ⟶ A) (gε : B ⟶ Aε) (hPB : IsPullback gε g e d),
            Function.Bijective (fibreProductComparison F g gε d e hPB.w)

Tag 06HZ, a lemma

Tag 06HZ in the Stacks Project.

Deformation.schlessingerConditionS2_completion_squareZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SquareZeroExtension.lean, line 1201. The attribute's comment: “existence of completions”.

The existence clause of (S2) extends from dual numbers to k[V] for finite-dimensional V.

theorem schlessingerConditionS2_completion_squareZero
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {V : Type z} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p) (hS2 : SchlessingerConditionS2 p)
    {x xV x₀ : F} (d : x ⟶ x₀) (e : xV ⟶ x₀)
    (he : IsSquareZeroProjection (V := V) (p.map e))
    {AV : ArtinianLocalAlgCat.{u, v, w} Λ k}
    (g : AV ⟶ p.obj x) (gV : AV ⟶ p.obj xV)
    (hpb : IsPullback gV g (p.map e) (p.map d)) :
    Nonempty (PullbackCompletion p d e g gV)

Deformation.schlessingerConditionS2_comparison_squareZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SquareZeroExtension.lean, line 1218. The attribute's comment: “comparison of completions”.

The comparison clause of (S2) extends from dual numbers to k[V] for finite-dimensional V.

theorem schlessingerConditionS2_comparison_squareZero
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {V : Type z} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p) (hS2 : SchlessingerConditionS2 p)
    {x xV x₀ : F} (d : x ⟶ x₀) (e : xV ⟶ x₀)
    (he : IsSquareZeroProjection (V := V) (p.map e))
    {AV : ArtinianLocalAlgCat.{u, v, w} Λ k}
    (g : AV ⟶ p.obj x) (gV : AV ⟶ p.obj xV)
    (hpb : IsPullback gV g (p.map e) (p.map d))
    (P Q : PullbackCompletion p d e g gV) :
    ∃ b : P.apex ⟶ Q.apex,
      (P.toFirst = b ≫ Q.toFirst) ∧
        (p.map b = eqToHom P.apex_eq ≫ eqToHom Q.apex_eq.symm)

Tag 06I0, a lemma

Tag 06I0 in the Stacks Project.

Deformation.schlessingerConditionS2_of_isIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/AssociatedFunctor.lean, line 450. The attribute's comment: “s2_associated_functor”.

The associated functor of isomorphism classes of a category cofibered in groupoids inherits (S2) if the special fibre is a setoid or automorphisms over the residue field lift along dual-number projections. In particular this holds for a predeformation category.

public theorem schlessingerConditionS2_of_isIsomorphismClasses
    (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p)
    (hS2 : SchlessingerConditionS2 𝓕.p)
    (hSpecial :
      (IsPredeformationCategory 𝓕.p) ∨
      (IsSetoidCategory (𝓕.p.Fiber (residueFieldObject Λ k))) ∨
      (∀ {xε x₀ : 𝓕.obj} (e : xε ⟶ x₀),
        IsDualNumberProjection (𝓕.p.map e) →
        ∀ a : x₀ ≅ x₀, 𝓕.p.map a.hom = 𝟙 (𝓕.p.obj x₀) →
          ∃ b : xε ≅ xε,
            (𝓕.p.map b.hom = 𝟙 (𝓕.p.obj xε)) ∧
              (b.hom ≫ e = e ≫ a.hom))) :
    SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕))

Deformation.schlessingerConditionS1_of_isIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Basic.lean, line 354. The attribute's comment: “s1_associated_functor”. References: SGA 7 VI (1.13), “partial”.

The associated functor of isomorphism classes of a category cofibered in groupoids inherits Schlessinger's condition (S1).

public theorem schlessingerConditionS1_of_isIsomorphismClasses
    {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, v, w} Λ k)}
    (φ : BasedFunctor 𝓕 𝓖)
    (hφ : IsIsomorphismClasses φ)
    (hS1 : SchlessingerConditionS1 𝓕.p) :
    SchlessingerConditionS1 𝓖.p

Tag 06SQ, a lemma

Tag 06SQ in the Stacks Project.

Deformation.schlessingerConditionS1_objectsOverFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Basic.lean, line 288. The attribute's comment: “condition (S1)”.

Condition (S1) passes to the category of objects over a fixed object.

public theorem schlessingerConditionS1_objectsOverFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (x : F)
    (hS1 : SchlessingerConditionS1 p) :
    SchlessingerConditionS1
      (objectsOverFunctor p x)

Deformation.schlessingerConditionS2_objectsOverFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Basic.lean, line 304. The attribute's comment: “condition (S2)”.

Condition (S2) passes to the category of objects over a fixed object.

public theorem schlessingerConditionS2_objectsOverFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (x : F)
    (hS2 : SchlessingerConditionS2 p) :
    SchlessingerConditionS2
      (objectsOverFunctor p x)

Deformation.schlessingerConditionS2_isomorphismClasses_objectsOverFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/PredeformationLinear.lean, line 69. The attribute's comment: “condition (S2) for the associated functor of a slice”.

Stacks Project, Tag 06SQ. Schlessinger's condition (S2) passes from a category cofibered in groupoids to the associated functor of isomorphism classes of its slice predeformation category at a point over the residue field.

theorem schlessingerConditionS2_isomorphismClasses_objectsOverFunctor
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (hS2 : SchlessingerConditionS2 p)
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses
        (BasedCategory.ofFunctor (objectsOverFunctor p x.1))
        (isPredeformationCategory_objectsOverFunctor p hp x).cofibered))

Tag 06IS, a lemma

Tag 06IS in the Stacks Project.

Deformation.exists_section_iff_exists_dualNumberLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Basic.lean, line 190.

Stacks Project, Tag 06IS. In a square over the pullback of an Artinian local algebra and the dual numbers over the residue field, a section of the first projection exists precisely when the bottom arrow lifts across the dual-number projection.

public theorem exists_section_iff_exists_dualNumberLift
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (hS2 : SchlessingerConditionS2 p)
    {y xε x x₀ : F} (b : y ⟶ xε) (a : y ⟶ x)
    (e : xε ⟶ x₀) (d : x ⟶ x₀)
    (hcomm : b ≫ e = a ≫ d)
    (hdual : IsDualNumberProjection (p.map e))
    (hPB : IsPullback (p.map b) (p.map a) (p.map e) (p.map d)) :
    (∃ s : x ⟶ y, s ≫ a = 𝟙 x) ↔
      (∃ sε : x ⟶ xε, sε ≫ e = d)

Tag 06IT, a lemma

Tag 06IT in the Stacks Project.

Deformation.exists_lift_of_pushforward_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SchlessingerConditions/SmallExtensionLift.lean, line 1035. References: SGA 7 VI (1.5), “(2)”.

A map from x₁ to the pushforward of y along the canonical infinitesimal-coordinate map produces a lift x₁ → x₂.

theorem exists_lift_of_pushforward_map
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p)
    (hS2 : SchlessingerConditionS2 p)
    {y x₁ x₂ x z : F}
    (a : y ⟶ x₁) (c : y ⟶ x₂) (a₁ : x₁ ⟶ x) (a₂ : x₂ ⟶ x)
    (hcomm : c ≫ a₂ = a ≫ a₁)
    (hPB : IsPullback (p.map c) (p.map a) (p.map a₂) (p.map a₁))
    (hsmall : InfinitesimalLifting.IsSmallExtension
      (CommRingCat.ofHom (p.map a₂).hom.toRingHom))
    (h : p.obj x₁ ⟶ p.obj x₂)
    (hh : h ≫ p.map a₂ = p.map a₁)
    (target_eq : p.obj z =
      (infinitesimalMap (p.map a₁) (p.map a₂) hsmall h hh
        (p.map a) (p.map c) hPB).target)
    (q : y ⟶ z)
    (hqmap : p.map q =
      (infinitesimalMap (p.map a₁) (p.map a₂) hsmall h hh
        (p.map a) (p.map c) hPB).g ≫ eqToHom target_eq.symm)
    (_hq : p.IsCocartesian (p.map q) q)
    (lift : x₁ ⟶ z) :
    ∃ b : x₁ ⟶ x₂, b ≫ a₂ = a₁

Sources

LeanDeformation.SchlessingerConditionS1 · Deformation.SchlessingerConditionS2 · Deformation.squareComparisonFunctor · Deformation.schlessingerConditionS1_of_smallExtensions · Deformation.schlessingerConditionS1_elements_iff · Deformation.schlessingerConditionS2_elements_iff · Deformation.schlessingerConditionS2_completion_squareZero · Deformation.schlessingerConditionS2_comparison_squareZero

Section90.11 Tangent spaces of functors #

Section 90.11 of the Stacks Project, Tag 06I2. 14 tags here are carried by 35 declarations of the repository (all in StacksFrontier) and 9 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06I3, a definition

Tag 06I3 in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Functor.Additive registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch90.lean, line 17 (StacksFrontier): “additivity on Hom_R(M, N)”. References: EGA III (7.2.6); SGA 4 XVII (1.1.11); SGA 4 XVII (2.2.13.1); SGA 4½ Etat 0 (1.3.3), “partial”; SGA 5 V (2.3.4); SGA 6 I (1.1.3), “partial”.
CategoryTheory.Functor.Linear registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch90.lean, line 18 (StacksFrontier): “R-homogeneity: L(r • f) = r • L(f)”. References: EGA III (7.1.2).
CategoryTheory.Functor.mapLinearMap registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch90.lean, line 19 (StacksFrontier): “L on Hom_R(M, N) as a map of R-modules”.

Tag 06I5, a remark

Tag 06I5 in the Stacks Project.

Declarations registered for the tag:

preservesFiniteProductsOfAdditive registered with add_to_stacks in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 675 (StacksFrontier): “preservation of finite products”.
map_isZero registered with add_to_stacks in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 677 (StacksFrontier): “zero modules are sent to zero modules”.
fgModuleCat_linearFunctorLift_unique registered with add_to_stacks in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 679 (StacksFrontier): “unique linear lift”.

Tag 06I6, a lemma

Tag 06I6 in the Stacks Project.

Deformation.linearFunctorLift_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 613. The attribute's comment: “arbitrary linear source category”.

Stacks Project, Tag 06I6, general source category. A finite-product-preserving set-valued functor on any preadditive R-linear category with a terminal object, binary products and a zero object has a unique R-linear lift to R-modules. The two cases of the source are the instances of this for the category of all modules and for the category of finitely generated ones; it is also what applies to the full subcategories of the module category that arise as the domain of a tangent functor.

theorem linearFunctorLift_unique
    (R : Type uR) [CommRing R]
    {C : Type uC} [Category.{vC} C] [Preadditive C] [Linear R C]
    [HasTerminal C] [HasBinaryProducts C] [HasZeroObject C]
    (F : C ⥤ Type uM) [PreservesFiniteProducts F] :
    Nonempty (Unique (LinearFunctorLift R F))

Deformation.fgModuleCat_linearFunctorLift_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 634. The attribute's comment: “finitely generated modules”.

Stacks Project, Tag 06I6, finitely generated case. A finite-product-preserving set-valued functor on finitely generated R-modules which takes the zero module to a singleton has a unique R-linear lift to R-modules.

theorem fgModuleCat_linearFunctorLift_unique
    (R : Type uR) [CommRing R] (F : FGModuleCat.{vM} R ⥤ Type uM)
    [PreservesFiniteProducts F] [Unique (F.obj (FGModuleCat.of R PUnit))] :
    Nonempty (Unique (LinearFunctorLift R F))

Deformation.moduleCat_linearFunctorLift_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 654. The attribute's comment: “all modules”.

Stacks Project, Tag 06I6, unrestricted case. A finite-product-preserving set-valued functor on R-modules which takes the zero module to a singleton has a unique R-linear lift to R-modules.

theorem moduleCat_linearFunctorLift_unique
    (R : Type uR) [CommRing R] (F : ModuleCat.{vM} R ⥤ Type uM)
    [PreservesFiniteProducts F] [Unique (F.obj (ModuleCat.of R PUnit))] :
    Nonempty (Unique (LinearFunctorLift R F))

Tag 06I7, a lemma

Tag 06I7 in the Stacks Project.

Deformation.fgModuleCat_linearFunctorLift_natTrans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 746.

Stacks Project, Tag 06I7. A natural transformation between product-preserving set-valued functors on finitely generated modules uniquely lifts to a natural transformation between their canonical linear lifts. Its underlying natural transformation is the original one.

theorem fgModuleCat_linearFunctorLift_natTrans
    (R : Type uR) [CommRing R]
    (F G : FGModuleCat.{vM} R ⥤ Type uM)
    [PreservesFiniteProducts F] [Unique (F.obj (FGModuleCat.of R PUnit))]
    [PreservesFiniteProducts G] [Unique (G.obj (FGModuleCat.of R PUnit))]
    (t : F ⟶ G) :
    ∃! τ : (fgModuleCatLinearFunctorLift R F).functor ⟶
        (fgModuleCatLinearFunctorLift R G).functor,
      Functor.whiskerRight τ (forget (ModuleCat.{uM} R)) =
        eqToHom (fgModuleCatLinearFunctorLift R F).forget_comp ≫
          t ≫
            eqToHom (fgModuleCatLinearFunctorLift R G).forget_comp.symm

Tag 06I8, a lemma

Tag 06I8 in the Stacks Project.

Deformation.linearFunctor_iso_tensorLeft, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/LinearFunctor.lean, line 912.

Stacks Project, Tag 06I8. A linear functor from finite-dimensional vector spaces over a field to vector spaces is naturally isomorphic to tensoring with its value on the ground field.

theorem linearFunctor_iso_tensorLeft (K : Type u) [Field K]
    (L : FGModuleCat.{u} K ⥤ ModuleCat.{u} K) [L.Additive] [L.Linear K] :
    Nonempty
      (((forget₂ (FGModuleCat.{u} K) (ModuleCat.{u} K)) ⋙
          MonoidalCategory.tensorLeft (L.obj (FGModuleCat.of K K))) ≅ L)

Tag 06I9, a lemma

Tag 06I9 in the Stacks Project.

Deformation.trivSqZeroExtFunctor_preservesFiniteProducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Functor.lean, line 179. References: SGA 7 VI (1.3(c)), “more general”.

The trivial square-zero extension functor from R-modules to S-algebras over R preserves finite products.

theorem trivSqZeroExtFunctor_preservesFiniteProducts :
    PreservesFiniteProducts (trivSqZeroExtFunctor S R)

Tag 06IA, a lemma

Tag 06IA in the Stacks Project.

Deformation.tangentSpaceModuleStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Functor.lean, line 346. References: SGA 3 XI (1.9), “partial”.

Stacks Project, Tag 06IA. A set-valued functor on a strictly full subcategory of S-algebras over R which takes the zero square-zero extension and products of square-zero extensions to the corresponding products of sets has a natural R-linear module-valued lift on all finitely generated R-modules.

noncomputable def tangentSpaceModuleStructure
    (P : ObjectProperty (Over (CommAlgCat.of S R))) [P.IsClosedUnderIsomorphisms]
    (hP : ∀ M : FGModuleCat.{u} R, P ((squareZeroExtensionFunctor S R).obj M))
    (F : P.FullSubcategory ⥤ Type v)
    (hF : TangentSpaceFunctorConditions S R P hP F) :
    LinearFunctorLift R (tangentSpaceSetFunctor S R P hP F)

Tag 06IB, a definition

Tag 06IB in the Stacks Project.

Deformation.TangentSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Functor.lean, line 430. References: SGA 7 VI (1.15), “special case”.

Stacks Project, Tag 06IB. The tangent space of a set-valued functor is its value on the dual numbers.

abbrev TangentSpace
    (P : ObjectProperty (Over (CommAlgCat.of S R)))
    (hε : P (dualNumbersOver S R))
    (F : P.FullSubcategory ⥤ Type w) : Type w

Tag 06SR, an example

Tag 06SR in the Stacks Project.

Deformation.artinianTangentSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Functor.lean, line 626. The attribute's comment: “Definition 06IB applied to the category of augmented Artinian local algebras”.

The tangent space of a functor on 𝒞_Λ, through its canonical augmented-algebra model.

noncomputable abbrev artinianTangentSpace
    (F : ArtinianLocalAlgCat.{s, u, u} Λ k ⥤ Type w) : Type w

Deformation.artinianTangentSpace_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Functor.lean, line 634. The attribute's comment: “Definition 06IB applied to the category of augmented Artinian local algebras”.

Evaluation on the Artinian square-zero object agrees with the Over-model tangent space.

theorem artinianTangentSpace_eq
    (F : ArtinianLocalAlgCat.{s, u, u} Λ k ⥤ Type w) :
    artinianTangentSpace Λ k F =
      F.obj ((artinianSquareZeroExtensionFunctor Λ k).obj (FGModuleCat.of k k))

Tag 06IC, an example

Tag 06IC in the Stacks Project.

Deformation.isProrepresentable_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/ProrepresentableLimits.lean, line 198. The attribute's comment: “prorepresentable_preserves_limits”.

Stacks Project, Tag 06IC. A prorepresentable functor on Artinian local Λ-algebras preserves finite limits.

theorem isProrepresentable_preservesFiniteLimits
    (F : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type v) (hF : IsProrepresentable F) :
    PreservesFiniteLimits F

Deformation.tangentSpaceDerivationsLinearEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Derivations.lean, line 97. The attribute's comment: “tangent_space_derivations”.

Stacks Project, Tag 06IC. The tangent space of the functor represented by S is canonically linearly equivalent to the Λ-derivations from S to its residue field.

noncomputable def tangentSpaceDerivationsLinearEquiv
    (S : CompleteLocalAlgCat.{u, max v w, w} Λ k) :
    letI : Algebra S k := (residueHom S).toRingHom.toAlgebra
    tangentSpaceArtinian Λ k (restrictedCoyoneda S) ≃ₗ[k] Derivation Λ S k

Deformation.tangentSpaceDerivationsLinearEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Derivations.lean, line 119. The attribute's comment: “tangent_space_derivations”.

A tangent vector corresponds to the downlifted square-zero component.

theorem tangentSpaceDerivationsLinearEquiv_apply
    (S : CompleteLocalAlgCat.{u, max v w, w} Λ k)
    (f : tangentSpaceArtinian Λ k (restrictedCoyoneda S)) (s : S) :
    letI : Algebra S k := (residueHom S).toRingHom.toAlgebra
    tangentSpaceDerivationsLinearEquiv S f s = (f.hom s).snd.down

Deformation.tangentSpaceDerivationsLinearEquiv_precomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Derivations.lean, line 152. The attribute's comment: “tangent_space_derivations”.

The identification commutes with precomposition by morphisms of representing algebras.

theorem tangentSpaceDerivationsLinearEquiv_precomp
    (T S : CompleteLocalAlgCat.{u, max v w, w} Λ k) (g : T ⟶ S)
    (f : tangentSpaceArtinian Λ k (restrictedCoyoneda S)) (t : T) :
    tangentSpaceDerivationsLinearEquiv T (g ≫ f) t =
      tangentSpaceDerivationsLinearEquiv S f (g.hom t)

Deformation.tangentSpace_finiteDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Derivations.lean, line 164. The attribute's comment: “finite_tangent_space”. References: SGA 7 VI (1.11), “(ii), special case”.

Stacks Project, Tag 06IC. The tangent space of a prorepresentable functor is finite-dimensional, under the chapter's standing assumption that Λ → k is finite.

theorem tangentSpace_finiteDimensional [Module.Finite Λ k]
    (S : CompleteLocalAlgCat.{u, max v w, w} Λ k) :
    FiniteDimensional k (tangentSpaceArtinian Λ k (restrictedCoyoneda S))

Deformation.squareZeroPointsDerivationsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 218. The attribute's comment: “square_zero_points_derivations”.

noncomputable def squareZeroPointsDerivationsEquiv
    (S : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) [AddCommGroup V] [Module k V] :
    SquareZeroPoint S V ≃ Derivations S V

Deformation.squareZeroPointsDerivationsEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 226. The attribute's comment: “square_zero_points_derivations”.

In the forward identification, the derivation associated to f is the square-zero component of f, i.e. s ↦ f(s) - q(s).

theorem squareZeroPointsDerivationsEquiv_apply
    (S : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) [AddCommGroup V] [Module k V]
    (f : SquareZeroPoint S V) (s : S) :
    squareZeroPointsDerivationsEquiv S V f s = (f.1 s).snd

Deformation.squareZeroPointsDerivationsEquiv_symm_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 235. The attribute's comment: “square_zero_points_derivations”.

In the inverse identification, a derivation D is sent to the map s ↦ q(s) + D(s) into k[V].

theorem squareZeroPointsDerivationsEquiv_symm_apply
    (S : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) [AddCommGroup V] [Module k V]
    (D : Derivations S V) (s : S) :
    ((squareZeroPointsDerivationsEquiv S V).symm D).1 s =
      (residueHom S s, D s)

Deformation.squareZeroPointsDerivationsEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 244. The attribute's comment: “square_zero_points_derivations”.

The canonical identification is functorial in the finite-dimensional vector space.

theorem squareZeroPointsDerivationsEquiv_naturality
    (S : CompleteLocalAlgCat.{u, v, w} Λ k)
    {V : Type x} {W : Type y} [AddCommGroup V] [Module k V]
    [AddCommGroup W] [Module k W] (l : V →ₗ[k] W)
    (f : SquareZeroPoint S V) (s : S) :
    squareZeroPointsDerivationsEquiv S W (f.map S l) s =
      l (squareZeroPointsDerivationsEquiv S V f s)

Deformation.squareZeroPointsDerivationsEquiv_precomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 257. The attribute's comment: “square_zero_points_derivations”.

The canonical identification is natural under precomposition in the representing complete local algebra.

theorem squareZeroPointsDerivationsEquiv_precomp
    (S : CompleteLocalAlgCat.{u, v, w} Λ k)
    (T : CompleteLocalAlgCat.{u, y, w} Λ k)
    (g : T →ₐ[Λ] S) (hg : (residueHom S).comp g = residueHom T)
    (V : Type x) [AddCommGroup V] [Module k V]
    (f : SquareZeroPoint S V) (t : T) :
    squareZeroPointsDerivationsEquiv T V (f.precomp S T g hg V) t =
      squareZeroPointsDerivationsEquiv S V f (g t)

Deformation.squareZeroExtensionObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 359. The attribute's comment: “square_zero_points_derivations”.

A finite-dimensional trivial square-zero extension, as an object of the category of complete local Λ-algebras, with its algebra coordinates and residue augmentation.

noncomputable def squareZeroExtensionObject
    (V : Type x) [AddCommGroup V] [Module k V] [FiniteDimensional k V] :
    { A : CompleteLocalAlgCat.{u, max w x, w} Λ k //
      ∃ e : A ≃+* TrivSqZeroExt k V,
        (∀ r : Λ, e (algebraMap Λ A r) = (algebraMap Λ k r, 0)) ∧
        (∀ a : A, (e a).fst = residueHom A a) }

Deformation.squareZeroPointsDerivationsEquivHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 430. The attribute's comment: “square_zero_points_derivations”.

The identification for the actual morphism type of the category of complete local Λ-algebras. The equivalence e identifies the chosen object A with k[V], and he says that its residue map is the square-zero augmentation.

noncomputable def squareZeroPointsDerivationsEquivHom
    (S A : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) [AddCommGroup V] [Module k V]
    (e : A ≃+* TrivSqZeroExt k V)
    (hΛ : ∀ r : Λ, e (algebraMap Λ A r) = (algebraMap Λ k r, 0))
    (he : ∀ a : A, (e a).fst = residueHom A a) :
    (S ⟶ A) ≃ Derivations S V

Deformation.squareZeroPointsDerivationsEquivHom_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 443. The attribute's comment: “square_zero_points_derivations”.

A categorical morphism f : S ⟶ k[V] determines the derivation given by its square-zero component.

theorem squareZeroPointsDerivationsEquivHom_apply
    (S A : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) [AddCommGroup V] [Module k V]
    (e : A ≃+* TrivSqZeroExt k V)
    (hΛ : ∀ r : Λ, e (algebraMap Λ A r) = (algebraMap Λ k r, 0))
    (he : ∀ a : A, (e a).fst = residueHom A a)
    (f : S ⟶ A) (s : S) :
    squareZeroPointsDerivationsEquivHom S A V e hΛ he f s =
      (e (f.hom s)).snd

Deformation.squareZeroPointsDerivationsEquivHom_symm_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 457. The attribute's comment: “square_zero_points_derivations”.

Conversely, the categorical morphism determined by D is s ↦ q(s) + D(s) in square-zero coordinates.

theorem squareZeroPointsDerivationsEquivHom_symm_apply
    (S A : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) [AddCommGroup V] [Module k V]
    (e : A ≃+* TrivSqZeroExt k V)
    (hΛ : ∀ r : Λ, e (algebraMap Λ A r) = (algebraMap Λ k r, 0))
    (he : ∀ a : A, (e a).fst = residueHom A a)
    (D : Derivations S V) (s : S) :
    e (((squareZeroPointsDerivationsEquivHom S A V e hΛ he).symm D).hom s) =
      (residueHom S s, D s)

Deformation.squareZeroPointsDerivationsEquivHom_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 474. The attribute's comment: “square_zero_points_derivations”.

The categorical identification commutes with maps between square-zero extensions.

theorem squareZeroPointsDerivationsEquivHom_naturality
    (S A B : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) (W : Type y)
    [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
    (eA : A ≃+* TrivSqZeroExt k V)
    (hΛA : ∀ r : Λ, eA (algebraMap Λ A r) = (algebraMap Λ k r, 0))
    (heA : ∀ a : A, (eA a).fst = residueHom A a)
    (eB : B ≃+* TrivSqZeroExt k W)
    (hΛB : ∀ r : Λ, eB (algebraMap Λ B r) = (algebraMap Λ k r, 0))
    (heB : ∀ b : B, (eB b).fst = residueHom B b)
    (g : A ⟶ B) (l : V →ₗ[k] W)
    (hg : ∀ a : A, (eB (g.hom a)).snd = l (eA a).snd)
    (f : S ⟶ A) (s : S) :
    squareZeroPointsDerivationsEquivHom S B W eB hΛB heB (f ≫ g) s =
      l (squareZeroPointsDerivationsEquivHom S A V eA hΛA heA f s)

Deformation.squareZeroPointsDerivationsEquivHom_precomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/SquareZero.lean, line 495. The attribute's comment: “square_zero_points_derivations”.

The categorical identification is natural in the representing algebra.

theorem squareZeroPointsDerivationsEquivHom_precomp
    (T S A : CompleteLocalAlgCat.{u, v, w} Λ k)
    (V : Type x) [AddCommGroup V] [Module k V]
    (e : A ≃+* TrivSqZeroExt k V)
    (hΛ : ∀ r : Λ, e (algebraMap Λ A r) = (algebraMap Λ k r, 0))
    (he : ∀ a : A, (e a).fst = residueHom A a)
    (g : T ⟶ S) (f : S ⟶ A) (t : T) :
    squareZeroPointsDerivationsEquivHom T A V e hΛ he (g ≫ f) t =
      squareZeroPointsDerivationsEquivHom S A V e hΛ he f (g.hom t)

Tag 06SS, an example

Tag 06SS in the Stacks Project.

Deformation.existsUnique_derivationRelativeCotangentDualEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/RelativeCotangentDual.lean, line 275. The attribute's comment: “derivations are the dual of the relative cotangent space”. References: SGA 3 VIIA (1.3.1), “special case”.

Stacks 06SS. For a base Λ whose residue field k₀ has k separable over it, the Λ-derivations from an object S of \widehat{𝒞_Λ} to k are the k-linear dual of the relative cotangent space of S over Λ, by the unique k-linear equivalence that restricts a derivation to the maximal ideal of S.

theorem existsUnique_derivationRelativeCotangentDualEquiv
    {k₀ : Type*} [Field k₀] [Algebra Λ k₀] [Algebra k₀ k] [IsScalarTower Λ k₀ k]
    [IsLocalRing Λ] [Algebra.IsSeparable k₀ k]
    (hbase : Function.Surjective (algebraMap Λ k₀))
    (S : CompleteLocalAlgCat.{u, v, w} Λ k) :
    ∃ hlocal : IsLocalHom (algebraMap Λ S),
      letI := hlocal
      letI : Module k (relativeCotangentSpace (algebraMap Λ S)) :=
        Module.compHom _ S.residueEquiv.symm.toRingHom
      letI : Algebra S k := (residueHom S).toRingHom.toAlgebra
      ∃! e : Derivation Λ S k ≃ₗ[k]
          (relativeCotangentSpace (algebraMap Λ S) →ₗ[k] k),
        ∀ (D : Derivation Λ S k) (x : IsLocalRing.maximalIdeal S),
          e D (Submodule.Quotient.mk x) = D (x : S)

Deformation.existsUnique_tangentSpaceRelativeCotangentDualEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/RelativeCotangentDual.lean, line 343. The attribute's comment: “the tangent space is the relative tangent space”.

Stacks 06SS. The tangent space of the functor prorepresented by S is the relative tangent space of S over Λ, that is the k-linear dual of the relative cotangent space. The equivalence is characterized by taking the coefficient of the square-zero coordinate of the image of an element of the maximal ideal, and is unique with that property.

theorem existsUnique_tangentSpaceRelativeCotangentDualEquiv
    {k₀ : Type*} [Field k₀] [Algebra Λ k₀] [Algebra k₀ k] [IsScalarTower Λ k₀ k]
    [IsLocalRing Λ] [Algebra.IsSeparable k₀ k]
    (hbase : Function.Surjective (algebraMap Λ k₀))
    (S : CompleteLocalAlgCat.{u, max v w, w} Λ k) :
    ∃ hlocal : IsLocalHom (algebraMap Λ S),
      letI := hlocal
      letI : Module k (relativeCotangentSpace (algebraMap Λ S)) :=
        Module.compHom _ S.residueEquiv.symm.toRingHom
      ∃! e : tangentSpaceArtinian Λ k (restrictedCoyoneda S) ≃ₗ[k]
          (relativeCotangentSpace (algebraMap Λ S) →ₗ[k] k),
        ∀ (t : tangentSpaceArtinian Λ k (restrictedCoyoneda S))
          (x : IsLocalRing.maximalIdeal S),
          e t (Submodule.Quotient.mk x) = (t.hom (x : S)).snd.down

Deformation.existsUnique_tangentSpaceRelativeCotangentDualEquiv_of_isClassical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/RelativeCotangentDual.lean, line 378. The attribute's comment: “classical case”.

Stacks 06SS. The classical case: when Λ is a Noetherian complete local ring with residue field k, the tangent space of the functor prorepresented by S is the k-linear dual of the relative cotangent space of S over Λ. Separability is automatic here, the residue extension being trivial.

theorem existsUnique_tangentSpaceRelativeCotangentDualEquiv_of_isClassical
    (hΛ : IsClassical Λ k) (S : CompleteLocalAlgCat.{u, max v w, w} Λ k) :
    letI : IsLocalRing Λ := (Classical.choose hΛ).isLocal
    ∃ hlocal : IsLocalHom (algebraMap Λ S),
      letI := hlocal
      letI : Module k (relativeCotangentSpace (algebraMap Λ S)) :=
        Module.compHom _ S.residueEquiv.symm.toRingHom
      ∃! e : tangentSpaceArtinian Λ k (restrictedCoyoneda S) ≃ₗ[k]
          (relativeCotangentSpace (algebraMap Λ S) →ₗ[k] k),
        ∀ (t : tangentSpaceArtinian Λ k (restrictedCoyoneda S))
          (x : IsLocalRing.maximalIdeal S),
          e t (Submodule.Quotient.mk x) = (t.hom (x : S)).snd.down

Tag 06ID, a lemma

Tag 06ID in the Stacks Project.

Deformation.naturalTransformation_linearMapOnSquareZeroExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Functor.lean, line 687.

Stacks Project, Tag 06ID. A natural transformation between functors satisfying the tangent-space hypotheses is R-linear on every trivial square-zero extension R[M], with respect to the natural module structures of Tag 06IA. The case M = R is the induced linear map on tangent spaces.

theorem naturalTransformation_linearMapOnSquareZeroExtensions
    (P : ObjectProperty (Over (CommAlgCat.of S R))) [P.IsClosedUnderIsomorphisms]
    (hP : ∀ M : FGModuleCat.{u} R,
      P ((squareZeroExtensionFunctor S R).obj M))
    (F G : P.FullSubcategory ⥤ Type v)
    (hF : TangentSpaceFunctorConditions S R P hP F)
    (hG : TangentSpaceFunctorConditions S R P hP G)
    (t : F ⟶ G) (M : FGModuleCat.{u} R) :
    let LF := tangentSpaceModuleStructure S R P hP F hF
    let LG := tangentSpaceModuleStructure S R P hP G hG
    let eF := congrArg (fun H : FGModuleCat.{u} R ⥤ Type v ↦ H.obj M) LF.forget_comp
    let eG := congrArg (fun H : FGModuleCat.{u} R ⥤ Type v ↦ H.obj M) LG.forget_comp
    ∃ l : LF.functor.obj M ⟶ LG.functor.obj M, ∀ x : LF.functor.obj M,
      cast eG (l x) =
        t.app ((squareZeroExtensionRestriction S R P hP).obj M) (cast eF x)

Tag 06ST, an example

Tag 06ST in the Stacks Project.

Deformation.tangentSpaceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/FunctorMap.lean, line 60. The attribute's comment: “linear tangent map”.

The k-linear map on tangent spaces induced contravariantly by a morphism f : R ⟶ S of complete local Λ-algebras, written on derivation spaces: it sends a Λ-derivation S → k to its restriction along f.

noncomputable def tangentSpaceMap
    {R S : CompleteLocalAlgCat.{u, v, w} Λ k} (f : R ⟶ S) :
    letI : Algebra S k := (residueHom S).toRingHom.toAlgebra
    letI : Algebra R k := (residueHom R).toRingHom.toAlgebra
    Derivation Λ S k →ₗ[k] Derivation Λ R k

Deformation.tangentSpaceMap_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/FunctorMap.lean, line 76. The attribute's comment: “action on derivations”.

Under the canonical identification of the tangent space with a space of derivations, the induced tangent map is precomposition with the morphism of representing algebras.

theorem tangentSpaceMap_apply
    {R S : CompleteLocalAlgCat.{u, v, w} Λ k} (f : R ⟶ S)
    (d : letI : Algebra S k := (residueHom S).toRingHom.toAlgebra
      Derivation Λ S k) (r : R) :
    tangentSpaceMap f d r = d (f.hom r)

Deformation.tangentSpaceMapArtinian, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/FunctorMap.lean, line 86. The attribute's comment: “linear tangent map on Artinian tangent spaces”.

The induced map on the tangent spaces themselves, the values of the two restricted representable functors at the dual numbers: tangentSpaceMap transported along the canonical identification with derivation spaces.

noncomputable def tangentSpaceMapArtinian
    {R S : CompleteLocalAlgCat.{u, max v w, w} Λ k} (f : R ⟶ S) :
    tangentSpaceArtinian Λ k (restrictedCoyoneda S) →ₗ[k]
      tangentSpaceArtinian Λ k (restrictedCoyoneda R)

Deformation.tangentSpaceMapArtinian_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/FunctorMap.lean, line 96. The attribute's comment: “action on Artinian tangent vectors”.

On a tangent vector, that is on a k[ε]-point of the functor represented by S, the induced tangent map is precomposition with the morphism of representing algebras.

theorem tangentSpaceMapArtinian_apply
    {R S : CompleteLocalAlgCat.{u, max v w, w} Λ k} (f : R ⟶ S)
    (x : tangentSpaceArtinian Λ k (restrictedCoyoneda S)) :
    tangentSpaceMapArtinian f x = f ≫ x

Declarations registered for the tag:

Deformation.restrictedCoyonedaMap, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/TangentSpace/FunctorMap.lean, line 47 (StacksFrontier): “the transformation of functors induced by a map of representing algebras”.
Deformation.squareZeroPointsDerivationsEquiv_precomp, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/TangentSpace/FunctorMap.lean, line 50 (StacksFrontier): “naturality of the square-zero-point description of the tangent space”.
Deformation.tangentSpaceDerivationsLinearEquiv_precomp, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/TangentSpace/FunctorMap.lean, line 53 (StacksFrontier): “naturality of the identification of the tangent space with derivations”.

Tag 06IE, a lemma

Tag 06IE in the Stacks Project.

Deformation.tangentSpaceFunctor_iso_tensorLeft, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Functor.lean, line 741.

Stacks Project, Tag 06IE. Over a field, the functor V ↦ F(K[V]), with its natural linear structure, is naturally isomorphic to tensoring V with the tangent space F(K[ε]).

theorem tangentSpaceFunctor_iso_tensorLeft
    (S : Type s) (K : Type u) [CommRing S] [Field K] [Algebra S K]
    (P : ObjectProperty (Over (CommAlgCat.of S K)))
    [P.IsClosedUnderIsomorphisms]
    (hP : ∀ V : FGModuleCat.{u} K,
      P ((squareZeroExtensionFunctor S K).obj V))
    (F : P.FullSubcategory ⥤ Type u)
    (hF : TangentSpaceFunctorConditions S K P hP F) :
    let L := (tangentSpaceModuleStructure S K P hP F hF).functor
    Nonempty
      (L ≅
        (forget₂ (FGModuleCat.{u} K) (ModuleCat.{u} K) ⋙
          MonoidalCategory.tensorLeft (L.obj (FGModuleCat.of K K))))

Sources

LeanCategoryTheory.Functor.Additive · CategoryTheory.Functor.Linear · CategoryTheory.Functor.mapLinearMap · preservesFiniteProductsOfAdditive · map_isZero · fgModuleCat_linearFunctorLift_unique · Deformation.linearFunctorLift_unique · Deformation.fgModuleCat_linearFunctorLift_unique

Section90.12 Tangent spaces of predeformation categories #

Section 90.12 of the Stacks Project, Tag 06I1. 8 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06IG, a definition

Tag 06IG in the Stacks Project.

Deformation.predeformationTangentSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/DerivationAction.lean, line 207. References: SGA 7 VI (1.18).

The tangent space of a predeformation category, formed from its associated functor of isomorphism classes.

noncomputable abbrev predeformationTangentSpace
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p) : Type u₁

Tag 06IH, a lemma

Tag 06IH in the Stacks Project.

Deformation.associatedTangentSpaceModuleStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/TangentVectorSpace.lean, line 638. The attribute's comment: “natural vector space structure”.

Stacks Project, Tag 06IH. The natural k-linear structure on the values of the associated functor at finite-dimensional square-zero extensions. In particular its value on k[ε] is the tangent space of the predeformation category.

noncomputable def associatedTangentSpaceModuleStructure
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) :
    LinearFunctorLift k
      (squareZeroExtensionArtinian.{u, w, max v w} Λ k ⋙
        isomorphismClasses 𝓕 h𝓕.cofibered)

Deformation.associatedTangentSpaceFunctor_iso_tensorLeft, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/TangentVectorSpace.lean, line 863. The attribute's comment: “tensor equivalence”. References: SGA 7 VI (1.3(c)), “T ⊗ V ≅ [A(k[V])]”; SGA 7 VI (1.18), “(1)”.

Stacks Project, Tag 06IH. The canonical equivalence from tangent vectors tensored with V to the associated functor evaluated on k[V].

noncomputable def associatedTangentSpaceFunctor_iso_tensorLeft
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) :
    let L := (associatedTangentSpaceModuleStructure.{u, v, w} 𝓕 h𝓕 hS2).functor
    letI : Fact (IsPredeformationCategory.{u, v, w} 𝓕.p) := ⟨h𝓕⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) := ⟨hS2⟩
    let T := tangentSpaceArtinian.{u, w, v} Λ k (isomorphismClasses 𝓕 h𝓕.cofibered)
    ∀ V : FGModuleCat.{max v w} k,
      LinearEquiv (RingHom.id k) (TensorProduct k T V)
        ((L.obj V : ModuleCat.{u₁} k) : Type u₁)

Deformation.associatedTangentSpaceFunctor_iso_tensorLeft_pure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/TangentVectorSpace.lean, line 879. The attribute's comment: “pure-tensor formula”.

Stacks Project, Tag 06IH. On pure tensors, the canonical equivalence is induced by the map ULift k → V carrying 1 to v.

theorem associatedTangentSpaceFunctor_iso_tensorLeft_pure
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) :
    let L := (associatedTangentSpaceModuleStructure.{u, v, w} 𝓕 h𝓕 hS2).functor
    letI : Fact (IsPredeformationCategory.{u, v, w} 𝓕.p) := ⟨h𝓕⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) := ⟨hS2⟩
    let T := tangentSpaceArtinian.{u, w, v} Λ k (isomorphismClasses 𝓕 h𝓕.cofibered)
    ∀ (V : FGModuleCat.{max v w} k) (t : T) (v : V),
      associatedTangentSpaceFunctor_iso_tensorLeft.{u, v, w} 𝓕 h𝓕 hS2 V (t ⊗ₜ[k] v) =
        (L.map (FGModuleCat.ofHom
          (LinearMap.smulRight (ULift.moduleEquiv : ULift.{v} k ≃ₗ[k] k).toLinearMap v))).hom
          (cast (associatedTangentSpaceModuleStructure_carrier.{u, v, w}
            𝓕 h𝓕 hS2).symm t)

Deformation.associatedTangentSpaceFunctor_iso_tensorLeft_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/TangentVectorSpace.lean, line 906. The attribute's comment: “naturality”.

Stacks Project, Tag 06IH. The canonical tensor equivalences commute with every linear map between finite-dimensional vector spaces.

theorem associatedTangentSpaceFunctor_iso_tensorLeft_naturality
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) :
    let L := (associatedTangentSpaceModuleStructure.{u, v, w} 𝓕 h𝓕 hS2).functor
    letI : Fact (IsPredeformationCategory.{u, v, w} 𝓕.p) := ⟨h𝓕⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) := ⟨hS2⟩
    let T := tangentSpaceArtinian.{u, w, v} Λ k (isomorphismClasses 𝓕 h𝓕.cofibered)
    ∀ (V W : FGModuleCat.{max v w} k) (f : V ⟶ W) (z : TensorProduct k T V),
      (L.map f).hom
          (associatedTangentSpaceFunctor_iso_tensorLeft.{u, v, w} 𝓕 h𝓕 hS2 V z) =
        associatedTangentSpaceFunctor_iso_tensorLeft.{u, v, w} 𝓕 h𝓕 hS2 W
          (TensorProduct.map (LinearMap.id : T →ₗ[k] T) f.hom.hom z)

Deformation.associatedTangentSpaceFunctorConditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/AssociatedTangentSpace.lean, line 546. The attribute's comment: “tangent-space functor conditions”.

Stacks Project, Tag 06IH. Schlessinger's condition (S2) for the associated functor of a predeformation category supplies the singleton and binary-product conditions that the natural module structure of Stacks 06IA requires.

theorem associatedTangentSpaceFunctorConditions
    (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsPredeformationCategory 𝓕.p)
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) :
    TangentSpaceFunctorConditions Λ k (artinianLocalOver Λ k)
      (squareZeroExtension_mem_artinianLocalOver Λ k)
      (artinianLocalOverToArtinian Λ k ⋙ isomorphismClasses 𝓕 h𝓕.cofibered)

Declarations registered for the tag:

associatedTangentSpaceAddCommGroupUnlifted registered with add_to_stacks in StacksFrontier/Deformation/Schlessinger/AssociatedTangentSpace.lean, line 573 (StacksFrontier): “additive structure”.
associatedTangentSpaceModuleUnlifted registered with add_to_stacks in StacksFrontier/Deformation/Schlessinger/AssociatedTangentSpace.lean, line 575 (StacksFrontier): “scalar structure”.

Tag 06II, a definition

Tag 06II in the Stacks Project.

Deformation.differential, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Predeformation.lean, line 96.

Stacks Project, Tag 06II. The differential is the map on associated isomorphism-class functors evaluated at the dual numbers.

noncomputable abbrev differential
    {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k)}
    {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, w, w} Λ k)}
    (h𝓕 : IsCofiberedInGroupoids 𝓕.p)
    (h𝓖 : IsCofiberedInGroupoids 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖) :
    artinianTangentSpace Λ k (isomorphismClasses 𝓕 h𝓕) →
      artinianTangentSpace Λ k (isomorphismClasses 𝓖 h𝓖)

Tag 06IJ, a lemma

Tag 06IJ in the Stacks Project.

Deformation.differential_isLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/DifferentialLinear.lean, line 168.

Stacks Project, Tag 06IJ. The differential of a morphism of predeformation categories is k-linear for the natural tangent-space vector structures when both associated functors satisfy (S2).

theorem differential_isLinearMap
    (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsPredeformationCategory 𝓕.p)
    (h𝓖 : IsPredeformationCategory 𝓖.p)
    (hS2𝓕 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered)))
    (hS2𝓖 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓖 h𝓖.cofibered)))
    (φ : BasedFunctor 𝓕 𝓖) :
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨h𝓕⟩
    letI : Fact (IsPredeformationCategory 𝓖.p) := ⟨h𝓖⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) := ⟨hS2𝓕⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓖 h𝓖.cofibered))) := ⟨hS2𝓖⟩
    IsLinearMap k (differential h𝓕.cofibered h𝓖.cofibered φ)

Deformation.mapIsomorphismClasses_isLinearMap_artinianDualNumbers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/PredeformationLinear.lean, line 134. The attribute's comment: “lifted dual numbers”.

Stacks Project, Tag 06IJ. The map induced on associated functors of isomorphism classes by a morphism of predeformation categories is k-linear at the universe-lifted dual numbers, when both associated functors satisfy (S2).

This is Deformation.differential_isLinearMap for the universe-lifted presentation of the dual numbers used by the tangent space at a point.

theorem mapIsomorphismClasses_isLinearMap_artinianDualNumbers
    (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (h𝓕 : IsPredeformationCategory.{u, v, w} 𝓕.p)
    (h𝓖 : IsPredeformationCategory.{u, v, w} 𝓖.p)
    (hS2𝓕 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered)))
    (hS2𝓖 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓖 h𝓖.cofibered)))
    (φ : BasedFunctor 𝓕 𝓖) :
    letI : Fact (IsPredeformationCategory.{u, v, w} 𝓕.p) := ⟨h𝓕⟩
    letI : Fact (IsPredeformationCategory.{u, v, w} 𝓖.p) := ⟨h𝓖⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered))) := ⟨hS2𝓕⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓖 h𝓖.cofibered))) := ⟨hS2𝓖⟩
    IsLinearMap k (mapIsomorphismClasses h𝓕.cofibered h𝓖.cofibered φ
      (artinianDualNumbers.{u, w, v} Λ k))

Tag 06IK, a remark

Tag 06IK in the Stacks Project.

Deformation.tangentSpaceAtPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Predeformation.lean, line 118. The attribute's comment: “tangent_space_at_a_point”.

The tangent space of a category cofibered over 𝒞_Λ at a point over k: the tangent space of its slice predeformation category.

noncomputable abbrev tangentSpaceAtPoint
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) : Type (max u₁ v₁)

Deformation.sliceBasedFunctorAtPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Predeformation.lean, line 154. The attribute's comment: “differential_at_point”.

The morphism of slice predeformation categories induced by a based functor: it sends an arrow y ⟶ x to its image arrow φ(y) ⟶ φ(x).

def sliceBasedFunctorAtPoint
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    BasedFunctor
      (BasedCategory.ofFunctor
        (objectsOverFunctor p x.1))
      (BasedCategory.ofFunctor
        (objectsOverFunctor q (imagePoint φ x).1))

Deformation.differentialAtPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Predeformation.lean, line 175. The attribute's comment: “differential_at_point”.

The differential of a morphism of cofibered categories at a point over k: the differential of its induced morphism between slice predeformation categories.

noncomputable abbrev differentialAtPoint
    (hp : IsCofiberedInGroupoids p)
    (hq : IsCofiberedInGroupoids q)
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    tangentSpaceAtPoint p hp x →
      tangentSpaceAtPoint q hq (imagePoint φ x)

Deformation.tangentSpaceAtPointAddCommGroup, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/PredeformationLinear.lean, line 90. The attribute's comment: “vector_space_structure”.

Stacks Project, Tag 06IK. The additive group underlying the natural k-vector space structure on the tangent space of a category cofibered in groupoids at a point over the residue field, available when the category satisfies Schlessinger's condition (S2).

noncomputable instance tangentSpaceAtPointAddCommGroup
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    [hS2 : Fact (SchlessingerConditionS2 p)]
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    AddCommGroup (tangentSpaceAtPoint.{u, v, w} p hp x)

Deformation.tangentSpaceAtPointModule, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/PredeformationLinear.lean, line 105. The attribute's comment: “vector_space_structure”.

Stacks Project, Tag 06IK. The natural action of the residue field on the tangent space of a category cofibered in groupoids at a point over the residue field, available when the category satisfies Schlessinger's condition (S2).

noncomputable instance tangentSpaceAtPointModule
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    [hS2 : Fact (SchlessingerConditionS2 p)]
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    Module k (tangentSpaceAtPoint.{u, v, w} p hp x)

Deformation.differentialAtPoint_isLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/PredeformationLinear.lean, line 231. The attribute's comment: “differential_at_point_linear”.

Stacks Project, Tag 06IK. If both categories cofibered in groupoids satisfy Schlessinger's condition (S2), then the differential of a morphism between them at a point over the residue field is k-linear for the natural vector space structures on the tangent spaces at that point and its image.

theorem differentialAtPoint_isLinearMap
    (hp : IsCofiberedInGroupoids p)
    (hq : IsCofiberedInGroupoids q)
    (hS2p : SchlessingerConditionS2 p)
    (hS2q : SchlessingerConditionS2 q)
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    letI : Fact (SchlessingerConditionS2 p) := ⟨hS2p⟩
    letI : Fact (SchlessingerConditionS2 q) := ⟨hS2q⟩
    IsLinearMap k (differentialAtPoint.{u, v, w} hp hq φ x)

Tag 06SU, a lemma

Tag 06SU in the Stacks Project.

Deformation.action_eq_add_gamma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/DerivationActionTranslation.lean, line 78. The attribute's comment: “action_translation”.

Stacks Project, Tag 06SU. The derivation action on deformations over k[V] is translation by the image of the derivation under the canonical derivation map.

theorem action_eq_add_gamma
    (𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsPredeformationCategory 𝓕.p)
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered)))
    (V : FGModuleCat.{w} k)
    (A₀ : ArtinianLocalAlgCat.{u, w, w} Λ k)
    (i₀ : A₀ ≃ₐ[Λ] k)
    (hi₀ : ∀ a : A₀, A₀.residueEquiv (IsLocalRing.residue A₀ a) = i₀ a)
    (x₀ : 𝓕.obj) (hx₀ : 𝓕.p.obj x₀ = A₀)
    (hiV : ∀ a : (squareZeroExtensionArtinian.{u, w, w} Λ k).obj V,
      ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V).residueEquiv
        (IsLocalRing.residue ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V) a) =
          (TrivSqZeroExt.fstHom Λ k V) (squareZeroCoordinates.{u, w, w} V a))
    (a : DerivationMapAndAction 𝓕.p A₀
      ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V) i₀
      (squareZeroCoordinates.{u, w, w} V) hi₀ hiV x₀ hx₀)
    (D : Derivation Λ k V)
    (x : Skeleton (𝓕.p.Fiber ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V))) :
    let L := associatedTangentSpaceModuleStructureUnlifted 𝓕 h𝓕 hS2
    let e : Skeleton (𝓕.p.Fiber ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V)) ≃
        ((L.functor.obj V : ModuleCat.{u₁} k) : Type u₁) :=
      Equiv.cast (by
        calc
          Skeleton (𝓕.p.Fiber ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V)) =
              (isomorphismClasses 𝓕 h𝓕.cofibered).obj
                ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V) :=
            (isomorphismClasses_obj 𝓕 h𝓕.cofibered _).symm
          _ = ((L.functor.obj V : ModuleCat.{u₁} k) : Type u₁) :=
            (congrArg (fun H : FGModuleCat.{w} k ⥤ Type u₁ => H.obj V) L.forget_comp).symm)
    e (a.action D x) = e x + e (a.gamma D)

Deformation.derivationMap_linear, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/DerivationMapLinear.lean, line 157. The attribute's comment: “gamma_linear”.

Stacks Project, Tag 06SU. The map γ_V defined by pushforward along derivations is linear for the canonical vector-space structure on the associated functor.

theorem derivationMap_linear
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.cofibered)))
    (V : FGModuleCat.{w} k)
    (hiV : ∀ a : (squareZeroExtensionArtinian.{u, w, w} Λ k).obj V,
      ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V).residueEquiv
        (IsLocalRing.residue ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V) a) =
          (TrivSqZeroExt.fstHom Λ k V) (squareZeroCoordinates.{u, w, w} V a))
    (d : DerivationMapAndAction 𝓕.p A₀
      ((squareZeroExtensionArtinian.{u, w, w} Λ k).obj V) i₀
      (squareZeroCoordinates.{u, w, w} V) hi₀ hiV x₀ hx₀) :
    let L := (associatedTangentSpaceModuleStructureUnlifted 𝓕 h𝓕 hS2).functor
    let AV := (squareZeroExtensionArtinian.{u, w, w} Λ k).obj V
    let hcarrier : ((L.obj V : ModuleCat.{u₁} k) : Type u₁) =
        (isomorphismClasses 𝓕 h𝓕.cofibered).obj AV :=
      congrArg (fun H : FGModuleCat.{w} k ⥤ Type u₁ ↦ H.obj V)
        (associatedTangentSpaceModuleStructureUnlifted 𝓕 h𝓕 hS2).forget_comp
    ∃ γ : Derivation Λ k V →ₗ[k] ((L.obj V : ModuleCat.{u₁} k) : Type u₁),
      ∀ D : Derivation Λ k V,
        γ D = cast hcarrier.symm
          (cast (isomorphismClasses_obj 𝓕 h𝓕.cofibered AV).symm (d.gamma D))

Tag 06SV, an equation

Tag 06SV in the Stacks Project.

Deformation.derivationToTangentSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Predeformation.lean, line 379. The attribute's comment: “the map”.

The canonical map Der_Λ(k,k) → T𝓕.

noncomputable def derivationToTangentSpace :
    Derivation Λ k k → tangentSpaceArtinian Λ k
      (isomorphismClasses (BasedCategory.ofFunctor p) hp.cofibered)

Deformation.derivationToTangentSpace_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/Predeformation.lean, line 399. The attribute's comment: “naturality”.

A morphism of predeformation categories commutes with the derivation maps on tangent spaces.

theorem derivationToTangentSpace_naturality
    {G : Type u₂} [Category.{v₂} G]
    (q : G ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hq : IsPredeformationCategory q)
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (D : Derivation Λ k k) :
    mapIsomorphismClasses hp.cofibered hq.cofibered φ
      (artinianDualNumbers.{u, w, v} Λ k)
      (derivationToTangentSpace p hp D) =
        derivationToTangentSpace q hq D

Tag 06SW, an equation

Tag 06SW in the Stacks Project.

Deformation.derivationAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/DerivationAction.lean, line 245. References: SGA 7 VI (1.18), “partial”.

Stacks Project, Tag 06SW. Residue-field derivations act on the tangent space of any predeformation category by the twisting automorphisms of the dual numbers.

noncomputable def derivationAction
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p) : DerivationActionData.{u, v, w} p hp

Deformation.derivationAction_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/PredeformationTangent/DerivationAction.lean, line 298. The attribute's comment: “naturality”.

Stacks Project, Tag 06SW. The tangent map induced by a morphism of predeformation categories commutes with the action of residue-field derivations.

theorem derivationAction_natural
    {G : Type u₁} [Category.{v₁} G]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (q : G ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p) (hq : IsPredeformationCategory q)
    (φ : BasedFunctor (BasedCategory.ofFunctor p) (BasedCategory.ofFunctor q))
    (D : Derivation Λ k k)
    (x : predeformationTangentSpace.{u, v, w} p hp) :
    mapIsomorphismClasses hp.cofibered hq.cofibered φ
        (artinianDualNumbers.{u, w, v} Λ k)
        ((derivationAction.{u, v, w} p hp).action (D, x)) =
      (derivationAction.{u, v, w} q hq).action
        (D, mapIsomorphismClasses hp.cofibered hq.cofibered φ
          (artinianDualNumbers.{u, w, v} Λ k) x)

Sources

LeanDeformation.predeformationTangentSpace · Deformation.associatedTangentSpaceModuleStructure · Deformation.associatedTangentSpaceFunctor_iso_tensorLeft · Deformation.associatedTangentSpaceFunctor_iso_tensorLeft_pure · Deformation.associatedTangentSpaceFunctor_iso_tensorLeft_naturality · Deformation.associatedTangentSpaceFunctorConditions · associatedTangentSpaceAddCommGroupUnlifted · associatedTangentSpaceModuleUnlifted

Section90.13 Versal formal objects #

Section 90.13 of the Stacks Project, Tag 06SX. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06SY, a lemma

Tag 06SY in the Stacks Project.

Deformation.schlessingerConditionS1_of_versal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Basic.lean, line 788.

A predeformation category with a versal formal object satisfies Schlessinger's condition (S1).

public theorem schlessingerConditionS1_of_versal
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p)
    (ξ : FormalObject p)
    (hξ : IsVersal hp.cofibered ξ) :
    SchlessingerConditionS1 p

Tag 06IU, a lemma

Tag 06IU in the Stacks Project.

Deformation.isVersal_iff_differential_surjective_and_base_lifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/VersalCriterion.lean, line 1263.

Surjectivity on tangent spaces together with lifting the map of underlying complete local algebras across every small-extension triangle characterizes versality for a predeformation category satisfying (S1) and (S2).

public theorem isVersal_iff_differential_surjective_and_base_lifts
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hpre : IsPredeformationCategory 𝓕.p)
    (hS1 : SchlessingerConditionS1 𝓕.p)
    (hS2 : SchlessingerConditionS2 𝓕.p)
    (ξ : FormalObject 𝓕.p)
    (pushforwards : ChosenPushforwards 𝓕.p) :
    IsVersal hpre.cofibered ξ ↔
      (Function.Surjective
        (mapIsomorphismClasses
          (categoryOfElements_projection_isCofibered
            (restrictedCoyoneda ξ.base))
          hpre.cofibered
          (associatedMorphism
            hpre.cofibered ξ pushforwards).toBasedFunctor
          (artinianDualNumbers Λ k)) ∧
       ∀ ⦃B A : ArtinianLocalAlgCat.{u, max v w, w} Λ k⦄ (f : B ⟶ A),
         InfinitesimalLifting.IsSmallExtension
           (CommRingCat.ofHom f.hom.toRingHom) →
         ∀ ⦃y x : FormalObject 𝓕.p⦄ (g : y ⟶ x),
           (FormalObject.projection (p := 𝓕.p)).IsHomLift
             (artinianToComplete.map f) g →
         ∀ (a : ξ ⟶ x), ∃ b : ξ.base ⟶ y.base,
             b ≫ g.base = a.base)

Tag 06SZ, a lemma

Tag 06SZ in the Stacks Project.

Deformation.exists_least_lifting_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/LeastLiftingIdeal.lean, line 126.

The ideals of the kernel of a surjection B ⟶ A over whose quotients an object over A lifts have a least member when (S1) holds.

theorem exists_least_lifting_ideal
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (hS1 : SchlessingerConditionS1 p)
    {B : ArtinianLocalAlgCat.{u, v, w} Λ k} (x : F)
    (f : B ⟶ p.obj x) (hf : Function.Surjective f.hom)
    (hI : maximalIdeal B * RingHom.ker f.hom.toRingHom = ⊥) :
    let lifts : Set (Ideal B) :=
      {J | J ≤ RingHom.ker f.hom.toRingHom ∧
        ∃ (C : ArtinianLocalAlgCat.{u, v, w} Λ k)
          (q : B ⟶ C) (g : C ⟶ p.obj x),
          Function.Surjective q.hom ∧
          RingHom.ker q.hom.toRingHom = J ∧
          q ≫ g = f ∧
          ∃ (y : F) (hy : p.obj y = C) (a : y ⟶ x),
            p.map a = eqToHom hy ≫ g};
    ∃ J : Ideal B, J ∈ lifts ∧ (∀ K : Ideal B, K ∈ lifts → J ≤ K)

Tag 06IW, a lemma

Tag 06IW in the Stacks Project.

Deformation.exists_versalFormalObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/VersalExistence.lean, line 1981. The attribute's comment: “existence of a versal formal object”. References: SGA 7 VI (1.11), “(i)+(ii) => versal”.

Schlessinger's existence theorem. A predeformation category over 𝒞_Λ which satisfies his conditions (S1) and (S2) and whose tangent space is finite dimensional has a versal formal object. The formal object is the limit of the tower of presentations of Stacks 06SZ over a power series algebra on a basis of the tangent space, taken over a complete local algebra which is formally smooth over Λ; versality is checked through the criterion of Stacks 06IU, whose condition (1) comes from the choice of the bottom stage of the tower and whose condition (2) is the key lifting step.

The finite-dimensionality hypothesis speaks about the canonical k-vector space structure of Stacks 06IH on the tangent space, which is available as soon as 𝓕 is a predeformation category whose functor of isomorphism classes satisfies (S2); both of those are consequences of the hypotheses — the second is Deformation.schlessingerConditionS2_of_isIsomorphismClasses applied to hS2 — so they are installed by the letI prefix of hfin rather than assumed.

public theorem exists_versalFormalObject
    (Λ : Type u) (k : Type w) [CommRing Λ] [IsNoetherianRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hpre : IsPredeformationCategory.{u, v, w} 𝓕.p)
    (hS1 : SchlessingerConditionS1 𝓕.p)
    (hS2 : SchlessingerConditionS2 𝓕.p)
    (hfin :
      letI : Fact (IsPredeformationCategory.{u, v, w} 𝓕.p) := ⟨hpre⟩
      letI : Fact (SchlessingerConditionS2
          (CategoryOfElements.π (isomorphismClasses 𝓕 hpre.cofibered))) :=
        ⟨schlessingerConditionS2_of_isIsomorphismClasses 𝓕 hpre.cofibered hS2 (Or.inl hpre)⟩
      FiniteDimensional k (tangentSpaceArtinian.{u, w, v} Λ k
        (isomorphismClasses 𝓕 hpre.cofibered))) :
    ∃ ξ : FormalObject 𝓕.p, IsVersal hpre.cofibered ξ

Tag 0D3G, a remark

Tag 0D3G in the Stacks Project.

Deformation.exists_versalFormalObject_of_schlessingerConditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/SetValuedExistence.lean, line 307. The attribute's comment: “(H1) + (H2) + (H3) implies a versal formal object exists”. References: SGA 7 VI (1.11), “set-valued functor”.

Stacks Project, Tag 0D3G. A set-valued predeformation functor on 𝒞_Λ satisfying Schlessinger's conditions (H1) and (H2) — that is, (S1) and (S2) in the elementary form of Stacks 06HY — and his condition (H3), the finite-dimensionality of the tangent space, has a versal formal object.

This is Stacks 06IW read through the identifications of Stacks 06GT and 06HY: the category of elements of F is a predeformation category satisfying (S1) and (S2), and its functor of isomorphism classes is a copy of F by Deformation.elementsIsomorphismClassesEquiv, so the tangent space whose dimension is bounded is TF.

Condition (H3) is stated about TF = F(k[ε]) itself, for the canonical k-vector-space structure of Stacks 06IH transported to it by Deformation.setValuedTangentSpaceLinearEquiv; the form Stacks 06IW consumes is obtained inside the proof by Deformation.finiteDimensional_tangentSpace_isomorphismClasses_of_setValued. The predeformation and (S2) properties that structure needs are the images of hpre and hH2 under Stacks 06GT and 06HY, the latter followed by Deformation.schlessingerConditionS2_of_isIsomorphismClasses, so the statement installs them itself rather than assuming them.

public theorem exists_versalFormalObject_of_schlessingerConditions
    (Λ : Type u) (k : Type w) [CommRing Λ] [IsNoetherianRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k]
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t)
    (hpre : IsPredeformationFunctor.{u, v, w, t} F)
    (hH1 : ∀ ⦃A₁ A₂ A A₁₂ : ArtinianLocalAlgCat.{u, max v w, w} Λ k⦄
      (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A), Function.Surjective f₂.hom →
        ∀ (g₁ : A₁₂ ⟶ A₁) (g₂ : A₁₂ ⟶ A₂) (hPB : IsPullback g₂ g₁ f₂ f₁),
          Function.Surjective (fibreProductComparison F g₁ g₂ f₁ f₂ hPB.w))
    (hH2 : ∀ ⦃A A₀ Aε B : ArtinianLocalAlgCat.{u, max v w, w} Λ k⦄
      (d : A ⟶ A₀) (e : Aε ⟶ A₀), IsDualNumberProjection e →
        ∀ (g : B ⟶ A) (gε : B ⟶ Aε) (hPB : IsPullback gε g e d),
          Function.Bijective (fibreProductComparison F g gε d e hPB.w))
    (hH3 :
      letI : Fact (IsPredeformationCategory.{u, v, w}
          (BasedCategory.ofFunctor (CategoryOfElements.π F)).p) :=
        ⟨(isPredeformationCategory_iff F).2 hpre⟩
      letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
          (isomorphismClasses (BasedCategory.ofFunctor (CategoryOfElements.π F))
            ((isPredeformationCategory_iff F).2 hpre).cofibered))) :=
        ⟨schlessingerConditionS2_of_isIsomorphismClasses
          (BasedCategory.ofFunctor (CategoryOfElements.π F))
          ((isPredeformationCategory_iff F).2 hpre).cofibered
          ((schlessingerConditionS2_elements_iff F).2 hH2)
          (Or.inl ((isPredeformationCategory_iff F).2 hpre))⟩
      letI := setValuedTangentSpaceAddCommGroup.{u, v, w, t} F
        ((isPredeformationCategory_iff F).2 hpre)
      letI := setValuedTangentSpaceModule.{u, v, w, t} F
        ((isPredeformationCategory_iff F).2 hpre)
      FiniteDimensional k (tangentSpaceArtinian.{u, w, v} Λ k F)) :
    ∃ ξ : FormalObject (CategoryOfElements.π F),
      IsVersal ((isPredeformationCategory_iff F).2 hpre).cofibered ξ

Sources

LeanDeformation.schlessingerConditionS1_of_versal · Deformation.isVersal_iff_differential_surjective_and_base_lifts · Deformation.exists_least_lifting_ideal · Deformation.exists_versalFormalObject · Deformation.exists_versalFormalObject_of_schlessingerConditions

Section90.14 Minimal versal formal objects #

Section 90.14 of the Stacks Project, Tag 06T0. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06T1, a lemma

Tag 06T1 in the Stacks Project.

Deformation.exists_minimal_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/MinimalDescent.lean, line 195. The attribute's comment: “minimality_lifted”.

Every minimal descent object of x is, up to isomorphism, the image of a minimal descent object of y when y ⟶ x lies over a surjection and (S1) holds.

theorem exists_minimal_preimage
    {Λ : Type u} {k : Type w} [CommRing Λ] [IsNoetherianRing Λ]
    [Field k] [Algebra Λ k] [Module.Finite Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (hS1 : SchlessingerConditionS1 p)
    {y x : F} (g : y ⟶ x)
    (hg : Function.Surjective (p.map g).hom)
    (X : DescentObject p x) (hX : IsMinimalObject X) :
    ∃ Y : DescentObject p y,
      IsMinimalObject Y ∧ Nonempty ((descentPushforward p hp g).functor.obj Y ≅ X)

Deformation.isMinimal_descentPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/MinimalDescent.lean, line 280. The attribute's comment: “minimality_preserved”.

Pushforward along a morphism preserves minimal descent objects under (S1).

theorem isMinimal_descentPushforward
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k)
    (hp : IsCofiberedInGroupoids p)
    (hS1 : SchlessingerConditionS1 p)
    {y x : F} (g : y ⟶ x)
    (X : DescentObject p y)
    (hX : IsMinimalObject X) :
    IsMinimalObject
      ((descentPushforward p hp g).functor.obj X)

Tag 06T2, a lemma

Tag 06T2 in the Stacks Project.

Deformation.exists_smallestDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/MinimalVersal/Existence.lean, line 44.

Stacks Project, Tag 06T2. A versal formal object of a category cofibered in groupoids satisfying (S1) admits a smallest formal descent: a descent over a complete local subalgebra of its base that stays minimal after every Artinian base change and admits no proper further descent.

public theorem exists_smallestDescent
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hp : IsCofiberedInGroupoids p)
    (hS1 : SchlessingerConditionS1 p)
    (ξ : FormalObject p) (hξ : IsVersal hp ξ) :
    Nonempty (SmallestDescent ξ)

Tag 06T3, a lemma

Tag 06T3 in the Stacks Project.

Deformation.isVersal_smallestDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/MinimalVersal/DescentVersality.lean, line 65. The attribute's comment: “descended object versal”.

A smallest descent of a versal formal object of a category cofibered in groupoids is again a versal formal object.

public theorem isVersal_smallestDescent
    (hp : IsCofiberedInGroupoids p) {ξ : FormalObject p} (hξ : IsVersal hp ξ)
    (d : SmallestDescent ξ) : IsVersal hp d.object

Deformation.exists_mvPowerSeries_algEquiv_of_smallestDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/MinimalVersal/PowerSeriesDecomposition.lean, line 519. The attribute's comment: “power series decomposition”. References: SGA 7 VI (2.10), “smallest descent case”.

Stacks Project, Tag 06T3. The base of a versal formal object is a power series algebra over the base of a smallest descent of it, compatibly with the descended-base inclusion: the isomorphism carries a constant to the image of its coefficient.

public theorem exists_mvPowerSeries_algEquiv_of_smallestDescent
    (hp : IsCofiberedInGroupoids p) (ξ : FormalObject p) (hξ : IsVersal hp ξ)
    (d : SmallestDescent ξ) :
    ∃ r : ℕ, ∃ e : MvPowerSeries (Fin r) d.object.base ≃ₐ[Λ] ξ.base,
      ∀ a : d.object.base, e (MvPowerSeries.C a) = d.inclusion.base.hom a

Tag 06T4, a definition

Tag 06T4 in the Stacks Project.

Deformation.IsMinimalVersal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/MinimalVersal.lean, line 45. References: SGA 7 VI (1.19), “(2)”.

A formal object is minimal versal if it is versal and every morphism from a formal object into it is surjective on its underlying complete local algebra.

public abbrev IsMinimalVersal (hp : IsCofiberedInGroupoids p)
    (ξ : FormalObject p) : Prop

Tag 06T5, a lemma

Tag 06T5 in the Stacks Project.

Deformation.exists_minimalVersalFormalObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/MinimalExistence.lean, line 52. The attribute's comment: “existence”.

Stacks 06T5. A predeformation category with a versal formal object has a minimal versal formal object: a smallest descent of the given versal object is one.

public theorem exists_minimalVersalFormalObject (hp : IsPredeformationCategory p)
    (hξ : ∃ ξ : FormalObject p, IsVersal hp.cofibered ξ) :
    ∃ ξ : FormalObject p, IsMinimalVersal hp.cofibered ξ

Deformation.exists_minimalVersal_powerSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/MinimalPowerSeries.lean, line 62. The attribute's comment: “power_series_extension”.

Stacks 06T5. Any versal formal object ξ of a predeformation category is the pushforward of a minimal versal formal object η along a power series ring extension: there is a morphism η ⟶ ξ which is strongly cocartesian over its base map, and an isomorphism of Λ-algebras η.base[[x_1, …, x_r]] ≃ ξ.base carrying a constant to the image of its coefficient under that base map.

public theorem exists_minimalVersal_powerSeries [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hp : IsPredeformationCategory p) (ξ : FormalObject p) (hξ : IsVersal hp.cofibered ξ) :
    ∃ η : FormalObject p, ∃ f : η ⟶ ξ, IsMinimalVersal hp.cofibered η ∧
      (FormalObject.projection (p := p)).IsStronglyCocartesian f.base f ∧
      ∃ r : ℕ, ∃ e : MvPowerSeries (Fin r) η.base ≃ₐ[Λ] ξ.base,
        ∀ a : η.base, e (MvPowerSeries.C a) = f.base.hom a

Deformation.isomorphic_of_isMinimalVersal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/MinimalUniqueness.lean, line 46. The attribute's comment: “uniqueness”. References: SGA 7 VI (1.20), “uniqueness”; SGA 7 VI (1.10), “(ii) uniqueness”.

Any two minimal versal formal objects are isomorphic.

public theorem isomorphic_of_isMinimalVersal (hp : IsPredeformationCategory p)
    (ξ η : FormalObject p) (hξ : IsMinimalVersal hp.cofibered ξ)
    (hη : IsMinimalVersal hp.cofibered η) :
    Nonempty (ξ ≅ η)

Sources

LeanDeformation.exists_minimal_preimage · Deformation.isMinimal_descentPushforward · Deformation.exists_smallestDescent · Deformation.isVersal_smallestDescent · Deformation.exists_mvPowerSeries_algEquiv_of_smallestDescent · Deformation.IsMinimalVersal · Deformation.exists_minimalVersalFormalObject · Deformation.exists_minimalVersal_powerSeries

Section90.15 Miniversal formal objects and tangent spaces #

Section 90.15 of the Stacks Project, Tag 06IL. 10 tags here are carried by 31 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06IM, an equation

Tag 06IM in the Stacks Project.

Deformation.HasBijectiveDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/TangentSpace/BijectiveDifferential.lean, line 98.

Stacks Project, Tag 06IM. The differential of the morphism associated to a formal object is bijective from Λ-derivations to its tangent space.

public def HasBijectiveDifferential
    (hp : Deformation.IsCofiberedInGroupoids p)
    (ξ : Deformation.FormalObject p) : Prop

Tag 06T6, an equation

Tag 06T6 in the Stacks Project.

Deformation.HasBijectiveDifferentialOnDerivationOrbits, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/DerivationOrbits.lean, line 101. The attribute's comment: “the condition, as a predicate on formal objects”.

Stacks Project, Tag 06T6, the condition itself. The differential of a formal object is a well-defined, equivariant map from derivations of its underlying algebra to the tangent space, surjective on tangent vectors, and bijective after passing to Der_Λ(k, k)-orbits on both sides. That this holds for a minimal versal formal object is Stacks 06T8, Deformation.minimalVersal_hasBijectiveDifferentialOnDerivationOrbits.

public noncomputable def HasBijectiveDifferentialOnDerivationOrbits
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p) (ξ : FormalObject p) : Prop

Deformation.hasBijectiveDifferentialOnDerivationOrbits_of_hasBijectiveDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/DerivationOrbitsOfBijective.lean, line 61. The attribute's comment: “the condition holds for a formal object with bijective differential”.

Stacks Project, Tag 06T6. The condition holds for a formal object whose differential is bijective: the differential of such an object is a well-defined, equivariant and surjective map from derivations of its underlying complete local algebra to the tangent space, and it is bijective on Der_Λ(k, k)-orbits.

public theorem hasBijectiveDifferentialOnDerivationOrbits_of_hasBijectiveDifferential
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p) (ξ : FormalObject p)
    (hbij : HasBijectiveDifferential hp.cofibered ξ) :
    HasBijectiveDifferentialOnDerivationOrbits.{u, v, w} p hp ξ

Deformation.minimalVersal_hasBijectiveDifferentialOnDerivationOrbits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/MinimalVersalOrbitBijection.lean, line 703. The attribute's comment: “the condition holds for a minimal versal formal object”.

The differential of a minimal versal formal object of a predeformation category satisfying Schlessinger's condition (S2) is well defined, surjective and equivariant, and induces a bijection on Der_Λ(k, k)-orbits.

public theorem minimalVersal_hasBijectiveDifferentialOnDerivationOrbits
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p)
    (hS2 : SchlessingerConditionS2 p)
    (ξ : FormalObject p)
    (hξ : IsMinimalVersal hp.cofibered ξ) :
    HasBijectiveDifferentialOnDerivationOrbits.{u, v, w} p hp ξ

Tag 06IR, a lemma

Tag 06IR in the Stacks Project.

Deformation.isMinimalVersal_of_hasBijectiveDifferentialOnDerivationOrbits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/DerivationOrbitCriterion.lean, line 146. The attribute's comment: “minimality”.

A versal formal object of a predeformation category whose differential is bijective on derivation orbits is a minimal versal formal object.

public theorem isMinimalVersal_of_hasBijectiveDifferentialOnDerivationOrbits
    (hp : IsPredeformationCategory p) (ξ : FormalObject p) (hξ : IsVersal hp.cofibered ξ)
    (hd : HasBijectiveDifferentialOnDerivationOrbits.{u, v, w} p hp ξ) :
    IsMinimalVersal hp.cofibered ξ

Deformation.isomorphic_of_hasBijectiveDifferentialOnDerivationOrbits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/DerivationOrbitCriterion.lean, line 212. The attribute's comment: “uniqueness”. References: SGA 7 VI (1.20), “uniqueness”.

Any two versal formal objects whose differentials are bijective on derivation orbits are isomorphic.

public theorem isomorphic_of_hasBijectiveDifferentialOnDerivationOrbits
    (hp : IsPredeformationCategory p) (ξ η : FormalObject p)
    (hξ : IsVersal hp.cofibered ξ) (hη : IsVersal hp.cofibered η)
    (hdξ : HasBijectiveDifferentialOnDerivationOrbits.{u, v, w} p hp ξ)
    (hdη : HasBijectiveDifferentialOnDerivationOrbits.{u, v, w} p hp η) :
    Nonempty (ξ ≅ η)

Tag 06IV, a lemma

Tag 06IV in the Stacks Project.

Deformation.schlessingerConditionS1_of_versal_bijectiveDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/VersalBijectiveDifferential.lean, line 407. The attribute's comment: “part (1): condition (S1)”.

A versal formal object with bijective differential forces Schlessinger's condition (S1). The bijectivity of the differential is not used.

public theorem schlessingerConditionS1_of_versal_bijectiveDifferential
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ Deformation.ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : Deformation.IsPredeformationCategory p)
    (ξ : Deformation.FormalObject p)
    (hversal : Deformation.IsVersal hp.cofibered ξ)
    (_hbij : Deformation.HasBijectiveDifferential hp.cofibered ξ) :
    Deformation.SchlessingerConditionS1 p

Deformation.schlessingerConditionS2_of_versal_bijectiveDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/VersalBijectiveDifferential.lean, line 421. The attribute's comment: “part (2): condition (S2)”.

A versal formal object with bijective differential forces Schlessinger's condition (S2).

public theorem schlessingerConditionS2_of_versal_bijectiveDifferential
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ Deformation.ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : Deformation.IsPredeformationCategory p)
    (ξ : Deformation.FormalObject p)
    (hversal : Deformation.IsVersal hp.cofibered ξ)
    (hbij : Deformation.HasBijectiveDifferential hp.cofibered ξ) :
    Deformation.SchlessingerConditionS2 p

Deformation.finiteDimensional_tangentSpace_of_versal_bijectiveDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/VersalBijectiveDifferential.lean, line 726. The attribute's comment: “part (3): finite-dimensional tangent space”.

A versal formal object with bijective differential has a finite-dimensional tangent space.

public theorem finiteDimensional_tangentSpace_of_versal_bijectiveDifferential
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k]
    (𝓕 : BasedCategory.{vF, uF} (Deformation.ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hp : Deformation.IsPredeformationCategory 𝓕.p)
    (ξ : Deformation.FormalObject 𝓕.p)
    (hversal : Deformation.IsVersal hp.cofibered ξ)
    (hbij : Deformation.HasBijectiveDifferential hp.cofibered ξ) :
    let hS2 := schlessingerConditionS2_of_versal_bijectiveDifferential
      𝓕.p hp ξ hversal hbij
    let hAssocS2 :=
      Deformation.schlessingerConditionS2_of_isIsomorphismClasses
        𝓕 hp.cofibered hS2 (Or.inl hp)
    letI : Fact (Deformation.IsPredeformationCategory 𝓕.p) := ⟨hp⟩
    letI : Fact (Deformation.SchlessingerConditionS2
      (CategoryOfElements.π (Deformation.isomorphismClasses 𝓕 hp.cofibered))) :=
      ⟨hAssocS2⟩
    FiniteDimensional k
      (Deformation.tangentSpaceArtinian Λ k
        (Deformation.isomorphismClasses 𝓕 hp.cofibered))

Declarations registered for the tag:

Deformation.schlessingerConditionS1_of_versal, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/Schlessinger/VersalBijectiveDifferential.lean, line 402 (StacksFrontier): “part (1): condition (S1)”.

Tag 06T7, an example

Tag 06T7 in the Stacks Project.

Deformation.exists_versal_orbitBijective_not_schlessingerConditionS2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/OrbitBijectivityWarning.lean, line 772.

There is a predeformation category carrying a versal formal object whose differential is bijective on Der_Λ(k, k)-orbits and which does not satisfy Schlessinger's condition (S2).

theorem exists_versal_orbitBijective_not_schlessingerConditionS2 :
    ∃ (B : BasedCategory.{0, 1} (ArtinianLocalAlgCat.{0, 0, 0} Lam Kay))
      (hp : IsPredeformationCategory.{0, 0, 0} B.p) (ksi : FormalObject B.p),
      IsVersal hp.cofibered ksi ∧
        HasBijectiveDifferentialOnDerivationOrbits.{0, 0, 0} B.p hp ksi ∧
          ¬ SchlessingerConditionS2 B.p

Tag 06T8, a lemma

Tag 06T8 in the Stacks Project.

Deformation.minimalVersal_hasBijectiveDifferentialOnDerivationOrbits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/MinimalVersalOrbitBijection.lean, line 703.

The differential of a minimal versal formal object of a predeformation category satisfying Schlessinger's condition (S2) is well defined, surjective and equivariant, and induces a bijection on Der_Λ(k, k)-orbits.

public theorem minimalVersal_hasBijectiveDifferentialOnDerivationOrbits
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p)
    (hS2 : SchlessingerConditionS2 p)
    (ξ : FormalObject p)
    (hξ : IsMinimalVersal hp.cofibered ξ) :
    HasBijectiveDifferentialOnDerivationOrbits.{u, v, w} p hp ξ

Tag 06IX, a theorem

Tag 06IX in the Stacks Project.

Deformation.schlessingerConditionS1_of_minimalVersal_hasBijectiveDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FormalObject/DerivationOrbits.lean, line 123. The attribute's comment: “(1) implies (3a)”.

Stacks Project, Tag 06IX, the implication (1) ⟹ (3a). Condition (1) of that theorem is that the predeformation category have a minimal versal formal object whose differential is bijective, Stacks 06IM; condition (3a) is Schlessinger's condition (S1). Neither the minimality nor the bijectivity of the differential is used: versality alone gives (S1), by Stacks 06SY.

public theorem schlessingerConditionS1_of_minimalVersal_hasBijectiveDifferential
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsPredeformationCategory p)
    (hξ : ∃ ξ : FormalObject p,
      IsMinimalVersal hp.cofibered ξ ∧ HasBijectiveDifferential hp.cofibered ξ) :
    SchlessingerConditionS1 p

Deformation.exists_minimalVersal_hasBijectiveDifferentialOnDerivationOrbits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/MiniversalExistence.lean, line 44. The attribute's comment: “(3) implies (2)”. References: SGA 7 VI (1.11), “(i)”; SGA 7 VI (1.20), “special case”.

A predeformation category satisfying Schlessinger's conditions (S1) and (S2) whose tangent space is finite dimensional has a minimal versal formal object whose differential is bijective on Der_Λ(k, k)-orbits.

public theorem exists_minimalVersal_hasBijectiveDifferentialOnDerivationOrbits
    (Λ : Type u) (k : Type w) [CommRing Λ] [IsNoetherianRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hpre : IsPredeformationCategory.{u, v, w} 𝓕.p)
    (hS1 : SchlessingerConditionS1 𝓕.p)
    (hS2 : SchlessingerConditionS2 𝓕.p)
    (hfin :
      letI : Fact (IsPredeformationCategory.{u, v, w} 𝓕.p) := ⟨hpre⟩
      letI : Fact (SchlessingerConditionS2
          (CategoryOfElements.π (isomorphismClasses 𝓕 hpre.cofibered))) :=
        ⟨schlessingerConditionS2_of_isIsomorphismClasses 𝓕 hpre.cofibered hS2 (Or.inl hpre)⟩
      FiniteDimensional k (tangentSpaceArtinian.{u, w, v} Λ k
        (isomorphismClasses 𝓕 hpre.cofibered))) :
    ∃ ξ : FormalObject 𝓕.p,
      IsMinimalVersal hpre.cofibered ξ ∧
        HasBijectiveDifferentialOnDerivationOrbits.{u, v, w} 𝓕.p hpre ξ

Deformation.schlessingerConditionS2_of_minimalVersal_hasBijectiveDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/MiniversalSeparable.lean, line 149. The attribute's comment: “(1) implies (3b)”.

Stacks Project, Tag 06IX, the implication (1) implies (3b). A predeformation category with a minimal versal formal object whose differential is bijective — that is, one satisfying the condition of Stacks 06IM — satisfies Schlessinger's condition (S2).

This is part (2) of Stacks 06IV, which asks only for versality, restated under the hypothesis (1) of Stacks 06IX.

public theorem schlessingerConditionS2_of_minimalVersal_hasBijectiveDifferential
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{vF, uF} (Deformation.ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hpre : Deformation.IsPredeformationCategory 𝓕.p)
    (hξ : ∃ ξ : Deformation.FormalObject 𝓕.p,
      Deformation.IsMinimalVersal hpre.cofibered ξ ∧
        Deformation.HasBijectiveDifferential hpre.cofibered ξ) :
    Deformation.SchlessingerConditionS2 𝓕.p

Deformation.finiteDimensional_tangentSpace_of_minimalVersal_hasBijectiveDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/MiniversalSeparable.lean, line 172. The attribute's comment: “(1) implies (3c)”. References: SGA 7 VI (1.11), “(ii)”.

Stacks Project, Tag 06IX, the implication (1) implies (3c). The tangent space of a predeformation category with a minimal versal formal object whose differential is bijective — that is, one satisfying the condition of Stacks 06IM — is finite dimensional.

This is part (3) of Stacks 06IV, which asks only for versality, restated under the hypothesis (1) of Stacks 06IX. The canonical k-vector-space structure of Stacks 06IH on the tangent space needs the predeformation property of 𝓕 and condition (S2) for its functor of isomorphism classes; the first is hpre and the second comes from Deformation.schlessingerConditionS2_of_minimalVersal_hasBijectiveDifferential, the implication (1) implies (3b), so both are installed by the letI prefix of the conclusion and neither is assumed.

public theorem finiteDimensional_tangentSpace_of_minimalVersal_hasBijectiveDifferential
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (𝓕 : BasedCategory.{vF, uF} (Deformation.ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hpre : Deformation.IsPredeformationCategory 𝓕.p)
    (hξ : ∃ ξ : Deformation.FormalObject 𝓕.p,
      Deformation.IsMinimalVersal hpre.cofibered ξ ∧
        Deformation.HasBijectiveDifferential hpre.cofibered ξ) :
    letI : Fact (Deformation.IsPredeformationCategory 𝓕.p) := ⟨hpre⟩
    letI : Fact (Deformation.SchlessingerConditionS2 (CategoryOfElements.π
        (Deformation.isomorphismClasses 𝓕 hpre.cofibered))) :=
      ⟨Deformation.schlessingerConditionS2_of_isIsomorphismClasses 𝓕 hpre.cofibered
        (schlessingerConditionS2_of_minimalVersal_hasBijectiveDifferential 𝓕 hpre hξ)
        (Or.inl hpre)⟩
    FiniteDimensional k
      (Deformation.tangentSpaceArtinian Λ k
        (Deformation.isomorphismClasses 𝓕 hpre.cofibered))

Deformation.exists_minimalVersal_hasBijectiveDifferential_of_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/MiniversalSeparable.lean, line 379. The attribute's comment: “(2) implies (1) under separability”.

If k is separable over the image field of Λ, orbitwise bijectivity of a minimal versal formal object's differential is ordinary bijectivity.

public theorem exists_minimalVersal_hasBijectiveDifferential_of_separable
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    [Algebra.IsSeparable (Deformation.residueImageField Λ k) k]
    (𝓕 : BasedCategory.{vF, uF} (Deformation.ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hpre : Deformation.IsPredeformationCategory 𝓕.p)
    (hξ : ∃ ξ : Deformation.FormalObject 𝓕.p,
      Deformation.IsMinimalVersal hpre.cofibered ξ ∧
        Deformation.HasBijectiveDifferentialOnDerivationOrbits 𝓕.p hpre ξ) :
    ∃ ξ : Deformation.FormalObject 𝓕.p,
      Deformation.IsMinimalVersal hpre.cofibered ξ ∧
        Deformation.HasBijectiveDifferential hpre.cofibered ξ

Declarations registered for the tag:

Deformation.schlessingerConditionS1_of_versal, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/FormalObject/DerivationOrbits.lean, line 137 (StacksFrontier): “(1) implies (3a)”.
Deformation.schlessingerConditionS2_of_versal_bijectiveDifferential, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/Schlessinger/MiniversalSeparable.lean, line 192 (StacksFrontier): “(1) implies (3b)”.
Deformation.finiteDimensional_tangentSpace_of_versal_bijectiveDifferential, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/Schlessinger/MiniversalSeparable.lean, line 194 (StacksFrontier): “(1) implies (3c)”.

Tag 06IY, a remark

Tag 06IY in the Stacks Project.

Deformation.IsHull, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/IsomorphismClassesHull.lean, line 43. The attribute's comment: “hull”.

A hull of a category cofibered in groupoids over 𝒞_Λ is a versal formal object whose differential dξ : T\underline{R}|_{𝒞_Λ} → T𝓕 is an isomorphism.

public abbrev IsHull {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (hp : IsCofiberedInGroupoids p) (ξ : FormalObject p) : Prop

Deformation.exists_hull_of_schlessingerConditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/SetValuedExistence.lean, line 358. The attribute's comment: “(H1) + (H2) + (H3) implies a hull exists”. References: SGA 7 VI (1.20), “set-valued functor”.

Stacks Project, Tag 06IY. A set-valued predeformation functor on 𝒞_Λ satisfying Schlessinger's conditions (H1), (H2) and (H3) has a hull, provided k is separable over the image field of Λ: a versal formal object whose differential is an isomorphism.

This is Schlessinger's theorem on the existence of hulls. It is Stacks 06IX read through the identifications of Stacks 06GT and 06HY, exactly as Deformation.exists_versalFormalObject_of_schlessingerConditions is Stacks 06IW, and (H3) is stated and discharged in the same way: about TF = F(k[ε]) itself, transported inside the proof by Deformation.finiteDimensional_tangentSpace_isomorphismClasses_of_setValued.

public theorem exists_hull_of_schlessingerConditions
    (Λ : Type u) (k : Type w) [CommRing Λ] [IsNoetherianRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k] [Algebra.IsSeparable (residueImageField Λ k) k]
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t)
    (hpre : IsPredeformationFunctor.{u, v, w, t} F)
    (hH1 : ∀ ⦃A₁ A₂ A A₁₂ : ArtinianLocalAlgCat.{u, max v w, w} Λ k⦄
      (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A), Function.Surjective f₂.hom →
        ∀ (g₁ : A₁₂ ⟶ A₁) (g₂ : A₁₂ ⟶ A₂) (hPB : IsPullback g₂ g₁ f₂ f₁),
          Function.Surjective (fibreProductComparison F g₁ g₂ f₁ f₂ hPB.w))
    (hH2 : ∀ ⦃A A₀ Aε B : ArtinianLocalAlgCat.{u, max v w, w} Λ k⦄
      (d : A ⟶ A₀) (e : Aε ⟶ A₀), IsDualNumberProjection e →
        ∀ (g : B ⟶ A) (gε : B ⟶ Aε) (hPB : IsPullback gε g e d),
          Function.Bijective (fibreProductComparison F g gε d e hPB.w))
    (hH3 :
      letI : Fact (IsPredeformationCategory.{u, v, w}
          (BasedCategory.ofFunctor (CategoryOfElements.π F)).p) :=
        ⟨(isPredeformationCategory_iff F).2 hpre⟩
      letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
          (isomorphismClasses (BasedCategory.ofFunctor (CategoryOfElements.π F))
            ((isPredeformationCategory_iff F).2 hpre).cofibered))) :=
        ⟨schlessingerConditionS2_of_isIsomorphismClasses
          (BasedCategory.ofFunctor (CategoryOfElements.π F))
          ((isPredeformationCategory_iff F).2 hpre).cofibered
          ((schlessingerConditionS2_elements_iff F).2 hH2)
          (Or.inl ((isPredeformationCategory_iff F).2 hpre))⟩
      letI := setValuedTangentSpaceAddCommGroup.{u, v, w, t} F
        ((isPredeformationCategory_iff F).2 hpre)
      letI := setValuedTangentSpaceModule.{u, v, w, t} F
        ((isPredeformationCategory_iff F).2 hpre)
      FiniteDimensional k (tangentSpaceArtinian.{u, w, v} Λ k F)) :
    ∃ ξ : FormalObject (CategoryOfElements.π F),
      IsHull ((isPredeformationCategory_iff F).2 hpre).cofibered ξ

Deformation.exists_hull_of_schlessingerConditions_isClassical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/SetValuedExistence.lean, line 414. The attribute's comment: “(H1) + (H2) + (H3) implies a hull exists, classical case”. References: SGA 7 VI (1.20), “special case”.

Stacks Project, Tag 06IY. In the classical case — Λ a Noetherian complete local ring whose residue field is identified with k — a set-valued predeformation functor satisfying Schlessinger's conditions (H1), (H2) and (H3) has a hull.

A classical base satisfies the three standing hypotheses of Deformation.exists_hull_of_schlessingerConditions: it is Noetherian, k is a finite Λ-module, and k is separable over the image field of Λ because that image field is all of k.

public theorem exists_hull_of_schlessingerConditions_isClassical
    (Λ : Type u) (k : Type w) [CommRing Λ] [Field k] [Algebra Λ k] (hΛ : IsClassical Λ k)
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t)
    (hpre : IsPredeformationFunctor.{u, v, w, t} F)
    (hH1 : ∀ ⦃A₁ A₂ A A₁₂ : ArtinianLocalAlgCat.{u, max v w, w} Λ k⦄
      (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A), Function.Surjective f₂.hom →
        ∀ (g₁ : A₁₂ ⟶ A₁) (g₂ : A₁₂ ⟶ A₂) (hPB : IsPullback g₂ g₁ f₂ f₁),
          Function.Surjective (fibreProductComparison F g₁ g₂ f₁ f₂ hPB.w))
    (hH2 : ∀ ⦃A A₀ Aε B : ArtinianLocalAlgCat.{u, max v w, w} Λ k⦄
      (d : A ⟶ A₀) (e : Aε ⟶ A₀), IsDualNumberProjection e →
        ∀ (g : B ⟶ A) (gε : B ⟶ Aε) (hPB : IsPullback gε g e d),
          Function.Bijective (fibreProductComparison F g gε d e hPB.w))
    (hH3 :
      letI : Fact (IsPredeformationCategory.{u, v, w}
          (BasedCategory.ofFunctor (CategoryOfElements.π F)).p) :=
        ⟨(isPredeformationCategory_iff F).2 hpre⟩
      letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
          (isomorphismClasses (BasedCategory.ofFunctor (CategoryOfElements.π F))
            ((isPredeformationCategory_iff F).2 hpre).cofibered))) :=
        ⟨schlessingerConditionS2_of_isIsomorphismClasses
          (BasedCategory.ofFunctor (CategoryOfElements.π F))
          ((isPredeformationCategory_iff F).2 hpre).cofibered
          ((schlessingerConditionS2_elements_iff F).2 hH2)
          (Or.inl ((isPredeformationCategory_iff F).2 hpre))⟩
      letI := setValuedTangentSpaceAddCommGroup.{u, v, w, t} F
        ((isPredeformationCategory_iff F).2 hpre)
      letI := setValuedTangentSpaceModule.{u, v, w, t} F
        ((isPredeformationCategory_iff F).2 hpre)
      FiniteDimensional k (tangentSpaceArtinian.{u, w, v} Λ k F)) :
    ∃ ξ : FormalObject (CategoryOfElements.π F),
      IsHull ((isPredeformationCategory_iff F).2 hpre).cofibered ξ

Tag 06IZ, a remark

Tag 06IZ in the Stacks Project.

Deformation.mapIsomorphismClasses_bijective_of_isIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/IsomorphismClasses.lean, line 98. The attribute's comment: “bijective on isomorphism classes”.

A based functor realizing the functor of isomorphism classes is bijective on isomorphism classes over every object of the base: injective because its fibres are skeletal and identify exactly the isomorphism classes upstairs, surjective because it is essentially surjective on each fibre.

public theorem mapIsomorphismClasses_bijective_of_isIsomorphismClasses
    {𝓐 : BasedCategory.{v₁, u₁} C} {𝓑 : BasedCategory.{v₂, u₂} C}
    (h𝓐 : IsCofiberedInGroupoids 𝓐.p) (h𝓑 : IsCofiberedInGroupoids 𝓑.p)
    (φ : BasedFunctor 𝓐 𝓑) (hφ : IsIsomorphismClasses φ) (A : C) :
    Function.Bijective (mapIsomorphismClasses h𝓐 h𝓑 φ A)

Deformation.isSmooth_associatedMorphism_toIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/IsomorphismClasses.lean, line 322. The attribute's comment: “smooth composite”.

Stacks Project, Tag 06IZ. The composite of the morphism associated to a versal formal object with the canonical morphism to the functor of isomorphism classes is smooth.

public theorem isSmooth_associatedMorphism_toIsomorphismClasses
    (ξ : FormalObject 𝓕.p) (hξ : IsVersal hpre.cofibered ξ)
    (pushforwards : ChosenPushforwards 𝓕.p) :
    IsSmooth (BasedFunctor.comp
      (associatedMorphism hpre.cofibered ξ pushforwards).toBasedFunctor
      (toIsomorphismClasses 𝓕 hpre.cofibered))

Deformation.isVersal_imageInIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/IsomorphismClasses.lean, line 337. The attribute's comment: “versal image”.

Stacks Project, Tag 06IZ. The image of a versal formal object in the functor of isomorphism classes is versal.

public theorem isVersal_imageInIsomorphismClasses
    (ξ : FormalObject 𝓕.p) (hξ : IsVersal hpre.cofibered ξ) :
    IsVersal
      (categoryOfElements_projection_isCofibered (isomorphismClasses 𝓕 hpre.cofibered))
      (imageInIsomorphismClasses 𝓕 hpre ξ)

Deformation.hasBijectiveDifferential_imageInIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/IsomorphismClasses.lean, line 358. The attribute's comment: “tangent isomorphism”. References: SGA 7 VI (1.13), “tangent iso for [A]”.

Stacks Project, Tag 06IZ. The image in the functor of isomorphism classes of a formal object with bijective differential has bijective differential: the canonical morphism identifies the two tangent spaces.

public theorem hasBijectiveDifferential_imageInIsomorphismClasses
    (ξ : FormalObject 𝓕.p) (hξ : HasBijectiveDifferential hpre.cofibered ξ) :
    HasBijectiveDifferential
      (categoryOfElements_projection_isCofibered (isomorphismClasses 𝓕 hpre.cofibered))
      (imageInIsomorphismClasses 𝓕 hpre ξ)

Deformation.differential_toIsomorphismClasses_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/IsomorphismClasses.lean, line 405. The attribute's comment: “tangent spaces of the canonical morphism”.

Stacks Project, Tag 06IZ. The canonical morphism from a predeformation category to its functor of isomorphism classes identifies tangent spaces.

public theorem differential_toIsomorphismClasses_bijective :
    Function.Bijective
      (differential hpre.cofibered
        (categoryOfElements_projection_isCofibered (isomorphismClasses 𝓕 hpre.cofibered))
        (toIsomorphismClasses 𝓕 hpre.cofibered))

Deformation.exists_hull_isomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/VersalObject/IsomorphismClassesHull.lean, line 54. The attribute's comment: “existence of a hull”. References: SGA 7 VI (1.20), “existence”.

A predeformation category satisfying Schlessinger's conditions (S1) and (S2), with finite-dimensional tangent space and separable residue field extension, has a versal formal object with bijective differential whose image in the associated functor of isomorphism classes is again versal with bijective differential, hence a hull of that functor.

public theorem exists_hull_isomorphismClasses
    (Λ : Type u) (k : Type w) [CommRing Λ] [IsNoetherianRing Λ] [Field k] [Algebra Λ k]
    [Module.Finite Λ k] [Algebra.IsSeparable (residueImageField Λ k) k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hpre : IsPredeformationCategory.{u, v, w} 𝓕.p)
    (hS1 : SchlessingerConditionS1 𝓕.p)
    (hS2 : SchlessingerConditionS2 𝓕.p)
    (hfin :
      letI : Fact (IsPredeformationCategory.{u, v, w} 𝓕.p) := ⟨hpre⟩
      letI : Fact (SchlessingerConditionS2
          (CategoryOfElements.π (isomorphismClasses 𝓕 hpre.cofibered))) :=
        ⟨schlessingerConditionS2_of_isIsomorphismClasses 𝓕 hpre.cofibered hS2 (Or.inl hpre)⟩
      FiniteDimensional k (tangentSpaceArtinian.{u, w, v} Λ k
        (isomorphismClasses 𝓕 hpre.cofibered))) :
    ∃ ξ : FormalObject 𝓕.p,
      IsHull hpre.cofibered ξ ∧
      IsHull
        (categoryOfElements_projection_isCofibered (isomorphismClasses 𝓕 hpre.cofibered))
        (imageInIsomorphismClasses 𝓕 hpre ξ)

Tag 06T9, an example

Tag 06T9 in the Stacks Project.

Deformation.isPredeformationCategory_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/BaseCategoryOverItself.lean, line 121. The attribute's comment: “predeformation category”.

The base category 𝒞_Λ, regarded through the identity functor as a category cofibered in groupoids over itself, is a predeformation category.

public theorem isPredeformationCategory_id :
    IsPredeformationCategory.{u, v, w} (𝟭 (ArtinianLocalAlgCat.{u, max v w, w} Λ k))

Deformation.schlessingerConditionS1_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/BaseCategoryOverItself.lean, line 129. The attribute's comment: “condition (S1)”.

𝒞_Λ over itself satisfies Schlessinger's condition (S1).

public theorem schlessingerConditionS1_id :
    SchlessingerConditionS1 (𝟭 (ArtinianLocalAlgCat.{u, max v w, w} Λ k))

Deformation.schlessingerConditionS2_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/BaseCategoryOverItself.lean, line 140. The attribute's comment: “condition (S2)”.

𝒞_Λ over itself satisfies Schlessinger's condition (S2).

public theorem schlessingerConditionS2_id :
    SchlessingerConditionS2 (𝟭 (ArtinianLocalAlgCat.{u, max v w, w} Λ k))

Deformation.unique_predeformationTangentSpace_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/BaseCategoryOverItself.lean, line 200. The attribute's comment: “vanishing of the tangent space”.

The tangent space of 𝒞_Λ over itself vanishes: it has exactly one element.

public theorem unique_predeformationTangentSpace_id :
    Nonempty (Unique (predeformationTangentSpace.{u, v, w}
      (𝟭 (ArtinianLocalAlgCat.{u, max v w, w} Λ k)) (isPredeformationCategory_id Λ k)))

Deformation.isMinimalVersal_selfFormalObject_smoothModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/BaseCategoryOverItself.lean, line 454. The attribute's comment: “the smooth model of Stacks 06SM carries a minimal versal formal object”.

The object R constructed in Stacks 06SM carries a minimal versal formal object of 𝒞_Λ regarded as cofibered in groupoids over itself.

public theorem isMinimalVersal_selfFormalObject_smoothModel :
    IsMinimalVersal isCofiberedInGroupoids_id
      (selfFormalObject.{u, u, w} (smoothModel.{u, w} (Λ := Λ) (k := k)))

Deformation.isMinimalVersal_id_base_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/BaseCategoryOverItself.lean, line 465. The attribute's comment: “the cotangent identifications and the comparison with Stacks 06SM”.

The complete local algebra S underlying any minimal versal formal object of 𝒞_Λ over itself is formally smooth over Λ in the 𝔪_S-adic topology, its module of differentials satisfies Ω_{S/Λ} ⊗_S k = Ω_{k/Λ}, its conormal module satisfies H₁(L_{k/Λ}) = 𝔪_S/𝔪_S², and it is isomorphic to the object constructed in Stacks 06SM.

public theorem isMinimalVersal_id_base_properties
    (ξ : FormalObject (𝟭 (ArtinianLocalAlgCat.{u, max u w, w} Λ k)))
    (hξ : IsMinimalVersal isCofiberedInGroupoids_id ξ) :
    letI : Algebra ξ.base k := (residueHom ξ.base).toRingHom.toAlgebra
    letI : IsScalarTower Λ ξ.base k :=
      IsScalarTower.of_algebraMap_eq' (residueHom ξ.base).comp_algebraMap.symm
    RingHom.FormallySmoothNAdic.{max u w} (algebraMap Λ ξ.base) (maximalIdeal ξ.base) ∧
      Function.Bijective (KaehlerDifferential.mapBaseChange Λ ξ.base k) ∧
        Function.Bijective (Algebra.H1Cotangent.map Λ ξ.base k k) ∧
          Nonempty (ξ.base ≅ smoothModel.{u, w} (Λ := Λ) (k := k))

Sources

LeanDeformation.HasBijectiveDifferential · Deformation.HasBijectiveDifferentialOnDerivationOrbits · Deformation.hasBijectiveDifferentialOnDerivationOrbits_of_hasBijectiveDifferential · Deformation.minimalVersal_hasBijectiveDifferentialOnDerivationOrbits · Deformation.isMinimalVersal_of_hasBijectiveDifferentialOnDerivationOrbits · Deformation.isomorphic_of_hasBijectiveDifferentialOnDerivationOrbits · Deformation.schlessingerConditionS1_of_versal_bijectiveDifferential · Deformation.schlessingerConditionS2_of_versal_bijectiveDifferential

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

90.3 The base category to 90.15 Miniversal formal objects…

Section90.3 The base category#

Tag 06GC, a definition

Tag 06GD, a definition

Tag 06GE, a lemma

Tag 06S2, an equation

Tag 06GG, a lemma

Tag 06S3, a lemma

Tag 06GY, a definition

Tag 06GH, a lemma

Tag 06GF, a definition

Tag 06S5, a lemma

Tag 06S6, an equation

Tag 06S7, an equation

Tag 06S8, an equation

Tag 06S9, a lemma

Tag 06H0, a lemma

Sources

Section90.4 The completed base category#

Tag 06GW, a definition

Tag 06GZ, a lemma

Tag 06SB, a lemma

Tag 06H1, a lemma

Tag 06SC, a lemma

Tag 06SD, a lemma

Tag 06SE, a lemma

Tag 06SF, a lemma

Tag 06SG, a lemma

Sources

Section90.5 Categories cofibered in groupoids#

Tag 06GJ, a definition

Tag 06GK, remarks

Tag 07W5, an item

Tag 0DZJ, an item

Sources

Section90.6 Prorepresentable functors and predeformation categories#

Tag 06GX, a definition

Tag 06GS, a definition

Tag 06GT, a remark

Tag 06GU, a remark

Sources

Section90.7 Formal objects and completion categories#

Tag 06H3, a definition

Tag 06H4, a lemma

Tag 06H5, a definition

Tag 06H6, a lemma

Tag 06H8, a remark

Tag 06SJ, a remark

Tag 06H9, a remark

Tag 06HA, a remark

Tag 06HB, a remark

Tag 06HE, a remark

Tag 06HC, a remark

Tag 06SK, an equation

Tag 06SL, a remark

Tag 06HD, a remark

Sources

Section90.8 Smooth morphisms#

Tag 06HG, a definition

Tag 06HH, a lemma

Tag 06HI, a remark

Tag 06HJ, a remark

Tag 06HK, a remark

Tag 06HL, a lemma

Tag 06HM, a lemma

Tag 06HN, a lemma

Tag 06HR, a definition

Tag 06HS, a remark

Tag 06HT, a lemma

Sources

Section90.9 Smooth or unobstructed categories#

Tag 06HP, a definition

Tag 0DYL, a lemma

Tag 0DZK, a lemma

Tag 06SM, a lemma

Sources

Section90.10 Schlessinger's conditions#

Tag 06HW, a definition

Tag 06SP, an equation

Tag 06HX, a lemma

Section90.3 The base category #

Section90.4 The completed base category #

Section90.5 Categories cofibered in groupoids #

Section90.6 Prorepresentable functors and predeformation categories #

Section90.7 Formal objects and completion categories #

Section90.8 Smooth morphisms #

Section90.9 Smooth or unobstructed categories #

Section90.10 Schlessinger's conditions #

Section90.11 Tangent spaces of functors #

Section90.12 Tangent spaces of predeformation categories #

Section90.13 Versal formal objects #

Section90.14 Minimal versal formal objects #

Section90.15 Miniversal formal objects and tangent spaces #