98.3 Predeformation categories to 98.20 Strong formal…

Section98.3 Predeformation categories#

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

Tag 07T2, the section

Tag 07T2 in the Stacks Project.

Deformation.Artin.factorizationEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Predeformation/Factorization.lean, line 395. The attribute's comment: “the category 𝒞_Λ is equivalent to the opposite of the category of factorizations Spec k ⟶ Spec A ⟶ S of the point, with A Artinian local and its residue field identified with k”.

The category 𝒞_Λ is equivalent to the opposite of the category of factorizations Spec k ⟶ Spec A ⟶ S of the given point by the spectrum of an Artinian local ring with residue field identified with k.

public def factorizationEquivalence :
    ArtinianLocalAlgCat.{u, u, u} Λ k ≌ (ArtinianLocalFactorization S k x)ᵒᵖ

Deformation.Artin.artinianLocalAlgCatEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Predeformation/Factorization.lean, line 419. The attribute's comment: “the category 𝒞_Λ is independent, up to canonical equivalence, of the choice of the affine open Spec Λ ⊂ S the point factors through”.

The category 𝒞_Λ does not depend, up to canonical equivalence, on the choice of the affine open Spec Λ ⊂ S through which the point factors. Both are equivalent to the opposite of the category of factorizations of the point, which refers only to the point.

public def artinianLocalAlgCatEquiv :
    ArtinianLocalAlgCat.{u, u, u} Λ k ≌ ArtinianLocalAlgCat.{u, u, u} Λ' k

Declarations registered for the tag:

Tag 07T3, an equation

Tag 07T3 in the Stacks Project.

Deformation.Artin.ArtinianLocalFactorization, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Predeformation.lean, line 72.

A factorization Spec(k) ⟶ Spec(A) ⟶ S of a finite-type field-valued point of a locally Noetherian scheme, where A is an Artinian local ring and the first arrow identifies k with its residue field.

public structure ArtinianLocalFactorization (S : Scheme.{u}) (k : Type u) [Field k]
    (x : Spec (CommRingCat.of k) ⟶ S) [IsLocallyNoetherian S] [LocallyOfFiniteType x]
    [QuasiCompact x]
Tag 07T4, an equation

Tag 07T4 in the Stacks Project.

Deformation.Artin.predeformationCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Predeformation.lean, line 225.

The predeformation category 𝓕_{𝓧,k,x₀} and its canonical functor to 𝒞_Λ.

public noncomputable def predeformationCategory :
    PredeformationConstruction iΛ q x₀ hx₀
Tag 07T5, a lemma

Tag 07T5 in the Stacks Project.

Deformation.Artin.predeformationCategory_isPredeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ArtinCriteria/Predeformation.lean, line 646.

The canonical deformation category of a point of a fibred category is a predeformation category.

public theorem predeformationCategory_isPredeformationCategory
    (hp : p.IsFiberedInGroupoids) :
    let C := Deformation.Artin.predeformationCategory iΛ
      (p ⋙ Over.post B.inclusion) x₀ hx₀
    letI : Category C.carrier := C.category
    Deformation.IsPredeformationCategory C.projection
Tag 07WJ, an equation

Tag 07WJ in the Stacks Project.

Deformation.Artin.mapPredeformationCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Predeformation.lean, line 439.

A morphism over the base induces a canonical functor of predeformation categories over 𝒞_Λ.

public def mapPredeformationCategory :
    InducedPredeformationFunctor iΛ qX qY F hF x₀ hx₀
Tag 07WK, a lemma

Tag 07WK in the Stacks Project.

Deformation.Artin.isSmoothOnPredeformationCategories_of_isFormallySmoothOnObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/SmoothPredeformation.lean, line 523. The attribute's comment: “formally smooth on objects”.

Stacks 07WK, case (1). A 1-morphism of categories fibred in groupoids over the big fppf category of S which is formally smooth on objects induces a smooth functor of predeformation categories at every finite type field-valued point of the source.

This is also the formally-smooth-on-objects clause of Stacks 07XW — the condition the openness-of-versality statement is about — so both tags are registered here, on the declaration that carries the proof.

public theorem isSmoothOnPredeformationCategories_of_isFormallySmoothOnObjects
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) [IsLocallyNoetherian S]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hp : Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p) :
    IsSmoothOnPredeformationCategories B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor p)
      (CatFiberedInGroupoids.homFunctor_comp_p p)

Deformation.Artin.isSmoothOnPredeformationCategories_of_isRelativelyFormallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/SmoothPredeformation.lean, line 847. The attribute's comment: “representably formally smooth”.

Stacks 07WK, case (2). A 1-morphism of categories fibred in groupoids over the big fppf category of S which is representable by algebraic spaces and formally smooth induces a smooth functor of predeformation categories at every finite type field-valued point of the source.

public theorem isSmoothOnPredeformationCategories_of_isRelativelyFormallySmooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) [IsLocallyNoetherian S]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hrep : Stack.IsRepresentableByAlgebraicSpaces B S hS p.hom)
    (hform : BigFppfOver.IsRelativelyFormallySmooth B S hS p) :
    IsSmoothOnPredeformationCategories B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor p)
      (CatFiberedInGroupoids.homFunctor_comp_p p)

Deformation.Artin.isSmoothOnPredeformationCategories_of_formallySmooth_or_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/SmoothPredeformationCases.lean, line 52.

Stacks 07WK. Let S be a locally Noetherian scheme and F : 𝒳 → 𝒴 a 1-morphism of categories fibred in groupoids over the big fppf category of S which is (1) formally smooth on objects, or (2) representable by algebraic spaces and formally smooth, or (3) representable by algebraic spaces and smooth. Then for every finite type field k over S and every object x₀ of 𝒳 over Spec k the induced functor of predeformation categories is smooth.

theorem isSmoothOnPredeformationCategories_of_formallySmooth_or_smooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) [IsLocallyNoetherian S]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (h : Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p ∨
      (Stack.IsRepresentableByAlgebraicSpaces B S hS p.hom ∧
        BigFppfOver.IsRelativelyFormallySmooth B S hS p) ∨
      Stack.IsRelativelySmooth B S hS p) :
    IsSmoothOnPredeformationCategories B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor p)
      (CatFiberedInGroupoids.homFunctor_comp_p p)

Declarations registered for the tag:

Tag 07WL, a lemma

Tag 07WL in the Stacks Project.

Deformation.Artin.fibreProductOfPredeformationCategories, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Predeformation/FibreProduct.lean, line 1248.

Let 𝒲 be a 2-fibre product of 𝒳 ⟶ 𝒴 and 𝒵 ⟶ 𝒴 in categories fibred in groupoids over schemes over S, and let w₀ be an object of 𝒲 over Spec k with images x₀, z₀, y₀ = F(x₀). Then the square of predeformation categories 𝓕_{𝒲,k,w₀} ⟶ 𝓕_{𝒵,k,z₀}, 𝓕_{𝒳,k,x₀} ⟶ 𝓕_{𝒴,k,y₀} is a 2-fibre product of predeformation categories.

public def fibreProductOfPredeformationCategories (hG : G ⋙ qY = qZ)
    (hψ : ∀ w : W, qY.IsHomLift (𝟙 (qW.obj w)) (ψ.hom.app w))
    (hqW : qW.IsFiberedInGroupoids) (_hqX : qX.IsFiberedInGroupoids)
    (_hqZ : qZ.IsFiberedInGroupoids) (_hqY : qY.IsFiberedInGroupoids)
    (hfp : (TwoFibreProductOver.lift qX qZ qY F G qW A B hA hB ψ hψ).IsEquivalence) :
    PredeformationFibreProductData iΛ qW qX qZ qY A B F G hA hB hF ψ w₀ hw₀

Deformation.Artin.fibreProductOfPredeformationCategoriesOfEssSurj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Predeformation/FibreProduct.lean, line 1263. The attribute's comment: “the essential surjectivity of the ambient comparison functor supplied directly”.

The square of predeformation categories of a 2-fibre product is a 2-fibre product, given the essential surjectivity of the ambient comparison functor strictly over the base in place of the fibredness of qW.

public def fibreProductOfPredeformationCategoriesOfEssSurj (hG : G ⋙ qY = qZ)
    (hψ : ∀ w : W, qY.IsHomLift (𝟙 (qW.obj w)) (ψ.hom.app w))
    (hess : ∀ (U : Over S) (t : TwoFibreProductOver qX qZ qY F G),
      (TwoFibreProductOver.structureFunctor qX qZ qY F G).obj t = U →
      ∃ w : W, qW.obj w = U ∧ ∃ e :
        (TwoFibreProductOver.lift qX qZ qY F G qW A B hA hB ψ hψ).obj w ≅ t,
        (TwoFibreProductOver.structureFunctor qX qZ qY F G).IsHomLift (𝟙 U) e.hom)
    (hfp : (TwoFibreProductOver.lift qX qZ qY F G qW A B hA hB ψ hψ).IsEquivalence) :
    PredeformationFibreProductData iΛ qW qX qZ qY A B F G hA hB hF ψ w₀ hw₀
Sources
LeanDeformation.Artin.factorizationEquivalence · Deformation.Artin.artinianLocalAlgCatEquiv · Deformation.Artin.predeformationCategory · Deformation.Artin.ArtinianLocalFactorization · Deformation.Artin.predeformationCategory_isPredeformationCategory · Deformation.Artin.mapPredeformationCategory · Deformation.Artin.isSmoothOnPredeformationCategories_of_isFormallySmoothOnObjects · Deformation.Artin.isSmoothOnPredeformationCategories_of_isRelativelyFormallySmooth

Section98.4 Pushouts and stacks#

Section 98.4 of the Stacks Project, Tag 07WM. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07WN, a lemma

Tag 07WN in the Stacks Project.

AlgebraicGeometry.Stack.ThickeningPushout.fiberSquareComparison_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningPushoutEquivalence.lean, line 66.

Let Y' = Y ⨿_X X' be the pushout of a thickening i : X ⟶ X' and an affine morphism f : X ⟶ Y of schemes over S, and let 𝒵 be an algebraic stack over S. The functor of fibre categories 𝒵_{Y'} ⟶ 𝒵_Y ×_{𝒵_X} 𝒵_{X'} is an equivalence.

theorem fiberSquareComparison_isEquivalence.{w'}
    (𝒵 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (h𝒵 : IsAlgebraicStack.{u, w'} B S hS 𝒵)
    {X X' Y Y' : BigFppfOver B S hS} (i : X ⟶ X') (f : X ⟶ Y) (a : X' ⟶ Y') (b : Y ⟶ Y')
    (w : i ≫ a = f ≫ b)
    (hi : Stacks.Thickenings.IsThickening ((BigFppfOver.toScheme B S hS).map i))
    [IsAffineHom ((BigFppfOver.toScheme B S hS).map f)]
    (hsq : IsPushout ((BigFppfOver.toScheme B S hS).map i)
      ((BigFppfOver.toScheme B S hS).map f) ((BigFppfOver.toScheme B S hS).map a)
      ((BigFppfOver.toScheme B S hS).map b)) :
    letI : 𝒵.p.IsFibered := (Classical.choose h𝒵).isFibered
    (Deformation.Artin.fiberSquareComparison 𝒵.p 𝒵.p.chosenPullbacks f i b a
      w.symm).IsEquivalence
Sources
LeanAlgebraicGeometry.Stack.ThickeningPushout.fiberSquareComparison_isEquivalence

Section98.5 The Rim-Schlessinger condition#

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

Tag 07WP, a definition

Tag 07WP in the Stacks Project.

Deformation.Artin.SatisfiesRS, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/ConditionRS.lean, line 79.

Condition (RS): restriction across a finite-type local Artinian pushout along a closed immersion is an equivalence onto the two-fibre product of fibres.

public abbrev SatisfiesRS (hp : p.IsFiberedInGroupoids) : Prop
Tag 07WQ, a lemma

Tag 07WQ in the Stacks Project.

AlgebraicGeometry.Stack.ThickeningPushout.satisfiesRS, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ThickeningPushoutEquivalence.lean, line 87.

Stacks 07WQ. An algebraic stack satisfies the Rim–Schlessinger condition (RS). The source states this over a locally Noetherian base; the hypothesis is not needed, since the proof is Stacks 07WN, which holds over any base.

theorem satisfiesRS.{w'} (𝒵 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (h𝒵 : IsAlgebraicStack.{u, w'} B S hS 𝒵) :
    Deformation.Artin.SatisfiesRS B S hS 𝒵.p (Classical.choose h𝒵)

Deformation.Artin.satisfiesRS_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/ArtinianAtlas.lean, line 221.

Stacks 07WQ: an algebraic stack satisfies condition (RS). Let 𝒳 be an algebraic stack over S. At every pushout Y' = Y ⨿_X X' of spectra of Artinian local rings of finite type over S along a closed immersion X ⟶ X', the comparison from the fibre over Y' to the two-fibre product of the fibres over Y and X' over the fibre over X is an equivalence.

Full faithfulness comes from the representable diagonal alone (Deformation.Artin.fullyFaithful_fiberSquareComparison_of_hasRepresentableDiagonal). For essential surjectivity, a span of 𝒳 over the square has a cocone (Deformation.Artin.nonempty_cocone_of_atlas_of_hasLiftsAlong): its object over Y lifts along the smooth presentation (Sch/U) ⟶ 𝒳 étale-locally, the étale neighbourhoods extend across the thickening Y ⟶ Y', and over each of them the lift is carried across the base change of X ⟶ X'. That base change is a closed immersion with nilpotent kernel into an affine scheme étale, hence finite, over the Artinian local X', and the presentation has lifts along it (AlgebraicGeometry.Stack.hasLiftsAlong_of_isNilpotent): it is formally smooth on objects against such test objects because a smooth morphism of algebraic spaces lifts over them (AlgebraicGeometry.Space.formallySmoothOn_hasFiniteLocalNilpotentSections_of_isSmooth).

theorem satisfiesRS_of_isAlgebraicStack (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) :
    SatisfiesRS B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
Tag 07WR, a lemma

Tag 07WR in the Stacks Project.

Deformation.Artin.satisfiesRS_twoFibreProductOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ArtinCriteria/RimSchlessinger.lean, line 1177.

Condition (RS) is preserved by the two-fibre product of categories fibred in groupoids over the big fppf site.

public theorem satisfiesRS_twoFibreProductOver
    (p𝒳 : 𝒳 ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (p𝒴 : 𝒴 ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (p𝒵 : 𝒵 ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (F : 𝒳 ⥤ 𝒴) (G : 𝒵 ⥤ 𝒴)
    (h𝒳 : p𝒳.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (h𝒵 : p𝒵.IsFiberedInGroupoids)
    (hF : F ⋙ p𝒴 = p𝒳) (hG : G ⋙ p𝒴 = p𝒵)
    (hRS𝒳 : Deformation.Artin.SatisfiesRS B S hS p𝒳 h𝒳)
    (hRS𝒴 : Deformation.Artin.SatisfiesRS B S hS p𝒴 h𝒴)
    (hRS𝒵 : Deformation.Artin.SatisfiesRS B S hS p𝒵 h𝒵) :
    Deformation.Artin.SatisfiesRS B S hS
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 F G)
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 F G
        h𝒳 h𝒵 h𝒴 hF hG)
Sources
LeanDeformation.Artin.SatisfiesRS · AlgebraicGeometry.Stack.ThickeningPushout.satisfiesRS · Deformation.Artin.satisfiesRS_of_isAlgebraicStack · Deformation.Artin.satisfiesRS_twoFibreProductOver

Section98.6 Deformation categories#

Section 98.6 of the Stacks Project, Tag 07WT. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07WU, a lemma

Tag 07WU in the Stacks Project.

Deformation.Artin.isDeformationCategory_predeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/DeformationCategory.lean, line 1184.

Stacks Project, Tag 07WU. The predeformation category of a finite-type field-valued point in a fibred category satisfying (RS) is a deformation category.

public theorem isDeformationCategory_predeformationCategory
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type u₁} [Category.{v₁} 𝒳]
    (p : 𝒳 ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids)
    (hRS : SatisfiesRS B S hS p hp)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ S)
    (x₀ : 𝒳)
    (hx₀ : (p ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
      (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hqc : QuasiCompact
      (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let D := predeformationCategory iΛ
      (p ⋙ Over.post B.inclusion) x₀ hx₀
    letI := D.category
    Deformation.IsDeformationCategory D.projection
Tag 07WV, a remark

Tag 07WV in the Stacks Project.

Deformation.Artin.schlessingerConditionS1_isomorphismClasses_of_isDeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Basic.lean, line 57. The attribute's comment: “condition (S1) for isomorphism classes”.

The functor of isomorphism classes associated to a deformation category satisfies Schlessinger's condition (S1).

public theorem schlessingerConditionS1_isomorphismClasses_of_isDeformationCategory
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{v₁, u₁}
      (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (h𝓕 : IsDeformationCategory 𝓕.p) :
    SchlessingerConditionS1
      (CategoryOfElements.π
        (isomorphismClassesData 𝓕 h𝓕.predeformation.cofibered).classes)

Deformation.Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Basic.lean, line 73. The attribute's comment: “condition (S2) for isomorphism classes”.

The functor of isomorphism classes associated to a deformation category satisfies Schlessinger's condition (S2).

public theorem schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{v₁, u₁}
      (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (h𝓕 : IsDeformationCategory 𝓕.p) :
    SchlessingerConditionS2
      (CategoryOfElements.π
        (isomorphismClassesData 𝓕 h𝓕.predeformation.cofibered).classes)

Declarations registered for the tag:

Sources
LeanDeformation.Artin.isDeformationCategory_predeformationCategory · Deformation.Artin.schlessingerConditionS1_isomorphismClasses_of_isDeformationCategory · Deformation.Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory · Deformation.schlessingerConditionS1_of_satisfiesRS · Deformation.schlessingerConditionS2_of_satisfiesRS

Section98.7 Change of field#

Section 98.7 of the Stacks Project, Tag 07WW. 1 tag here is carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07WX, a lemma

Tag 07WX in the Stacks Project.

Deformation.Artin.changeOfFieldFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/ChangeOfField.lean, line 770. The attribute's comment: “the canonical functor; the ambient base category is the category of all S-schemes rather than the big fppf site”.

Stacks Project, Tag 07WX. The canonical functor from the change of residue field of the predeformation category of x₀ to the predeformation category of its restriction x_{l,0}.

def changeOfFieldFunctor :
    Deformation.ChangeOfFieldsCategory T D.projection ⥤ E.carrier

Deformation.Artin.changeOfFieldFunctor_projection_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/ChangeOfField.lean, line 841. The attribute's comment: “the canonical functor lies over 𝒞_{Λ,l}; the ambient base category is the category of all S-schemes rather than the big fppf site”.

Stacks Project, Tag 07WX. The canonical functor is a functor of categories over 𝒞_{Λ,l}.

theorem changeOfFieldFunctor_projection_comm :
    changeOfFieldFunctor T iΛ hxₗ hη c D E ⋙ E.projection =
      Deformation.changeOfFieldsProjection T D.projection

Deformation.Artin.changeOfFieldFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/ChangeOfField/Equivalence.lean, line 1357. The attribute's comment: “the functor is an equivalence under (RS); the ambient base category is the category of all S-schemes rather than the big fppf site, and (RS) is taken in the matching form over that category”.

Stacks Project, Tag 07WX. The canonical functor (𝓕_{𝒳,k,x₀})_{l/k} ⥤ 𝓕_{𝒳,l,x_{l,0}} of Tag 07WX is an equivalence when 𝒳 satisfies the Rim–Schlessinger condition (RS).

public theorem changeOfFieldFunctor_isEquivalence
    (hq : q.IsFiberedInGroupoids) (hRS : SatisfiesRSOver q c)
    (hfinK : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap T.Λ T.k)) ≫ iΛ))
    (hqcK : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap T.Λ T.k)) ≫ iΛ))
    (hfinL : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap T.Λ T.l)) ≫ iΛ))
    (hqcL : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap T.Λ T.l)) ≫ iΛ)) :
    (changeOfFieldFunctor T iΛ hxₗ hη c D E).IsEquivalence

Deformation.Artin.Site.changeOfFieldFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/ChangeOfField/SiteRestriction/Equivalence.lean, line 571. The attribute's comment: “the canonical functor is an equivalence under (RS), for a category fibred in groupoids over the big fppf site”.

Under (RS), restriction of deformations is an equivalence over the Artinian local algebras with residue field l.

public theorem changeOfFieldFunctor_isEquivalence
    (hp : p.IsFiberedInGroupoids)
    (hη : p.IsCartesian (p.map η) η)
    (hηbase : eqToHom (congrArg Over.left hxₗ).symm ≫
      ((p ⋙ Over.post B.inclusion).map η).left ≫
      eqToHom (congrArg Over.left hx₀) =
        Spec.map (CommRingCat.ofHom (algebraMap T.k T.l)))
    (hfinite : LocallyOfFiniteType
        (Spec.map (CommRingCat.ofHom (algebraMap T.Λ T.k)) ≫ iΛ) ∧
      QuasiCompact
        (Spec.map (CommRingCat.ofHom (algebraMap T.Λ T.k)) ≫ iΛ))
    (hRS : Deformation.Artin.SatisfiesRS B S hS p hp) :
    (changeOfFieldFunctor T iΛ B hS p x₀ xₗ hx₀ hxₗ η hp hη hηbase).toFunctor.IsEquivalence

Deformation.Artin.Site.changeOfFieldFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/ChangeOfField/SiteRestriction/Functor.lean, line 693. The attribute's comment: “the canonical functor, for a category fibred in groupoids over the big fppf site”.

The canonical functor (𝓕_{𝒳,k,x₀})_{l/k} ⥤ 𝓕_{𝒳,l,x_{l,0}} over 𝒞_{Λ,l}, restricting deformations along Spec A ⟶ Spec (A ×_l k).

public noncomputable def changeOfFieldFunctor
    (hp : p.IsFiberedInGroupoids)
    (_hη : p.IsCartesian (p.map η) η)
    (hηbase : eqToHom (congrArg Over.left hxₗ).symm ≫
      ((p ⋙ Over.post B.inclusion).map η).left ≫
      eqToHom (congrArg Over.left hx₀) =
        Spec.map (CommRingCat.ofHom (algebraMap T.k T.l))) :
    ChangeOfFieldFunctor T iΛ B hS p x₀ xₗ hx₀ hxₗ η
Sources
LeanDeformation.Artin.changeOfFieldFunctor · Deformation.Artin.changeOfFieldFunctor_projection_comm · Deformation.Artin.changeOfFieldFunctor_isEquivalence · Deformation.Artin.Site.changeOfFieldFunctor_isEquivalence · Deformation.Artin.Site.changeOfFieldFunctor

Section98.8 Tangent spaces#

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

Tag 07WY, the section

Tag 07WY in the Stacks Project.

Deformation.Artin.tangentSpaceModuleOfSatisfiesRS, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/TangentSpaceVectorStructure.lean, line 99. The attribute's comment: “if X satisfies (RS), TF_{X,k,x_0} has a natural k-vector space structure (Lemma 06IH, assumptions by Lemma 07WU and Remark 07WV)”.

The tangent space as a vector space. For 𝒳 satisfying (RS), the tangent space T𝓕_{𝒳,k,x₀} of the predeformation category, with the natural k-vector space structure of Stacks 06IH.

def tangentSpaceModuleOfSatisfiesRS : ModuleCat.{max (u + 1) v w} k

Deformation.Artin.tangentSpaceModuleOfSatisfiesRS_carrier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/TangentSpaceVectorStructure.lean, line 116. The attribute's comment: “the underlying set of the k-vector space TF_{X,k,x_0} is the set of isomorphism classes of objects of F_{X,k,x_0} over k[ε]”.

The underlying set of the k-vector space tangentSpaceModuleOfSatisfiesRS is the tangent space T𝓕_{𝒳,k,x₀}: the set of isomorphism classes of the fibre of 𝓕_{𝒳,k,x₀} over the dual numbers k[ε], that is of morphisms x₀ ⟶ x of 𝒳 over Spec k ⟶ Spec k[ε].

theorem tangentSpaceModuleOfSatisfiesRS_carrier :
    let D := predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀
    letI := D.category
    ((tangentSpaceModuleOfSatisfiesRS B S hS p hp hRS iΛ x₀ hx₀ hfinite hqc : ModuleCat k) :
        Type _) =
      Quotient (isIsomorphicSetoid
        (D.projection.Fiber (artinianDualNumbers.{u, u, u} Λ k)))

Deformation.Artin.infinitesimalAutomorphismModuleOfSatisfiesRS, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/TangentSpaceVectorStructure.lean, line 133. The attribute's comment: “Inf(F_{X,k,x_0}) has a natural k-vector space structure (Lemma 06JX)”.

Infinitesimal automorphisms as a vector space. For 𝒳 satisfying (RS), the infinitesimal automorphisms Inf(𝓕_{𝒳,k,x₀}) at an object x of 𝓕_{𝒳,k,x₀} over k and a choice P of pushforwards of x, with the natural k-vector space structure of Stacks 06JX (the value at the rank-one module of the canonical linear lift of M ↦ Inf(x[M]/x)).

def infinitesimalAutomorphismModuleOfSatisfiesRS
    (x : (letI := (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).category
      (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection.Fiber
        (residueFieldObject.{u, u, u} Λ k)))
    (P : letI := (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).category
      ChosenPushforwardsAt (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection
        x.1) :
    ModuleCat.{max u w} k

Deformation.Artin.infinitesimalAutomorphismModuleOfSatisfiesRS_carrier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/TangentSpaceVectorStructure.lean, line 154. The attribute's comment: “the k-vector space structure on Inf(F_{X,k,x_0}) is such that addition agrees with composition of automorphisms”.

Addition on Inf is composition. The underlying set of infinitesimalAutomorphismModuleOfSatisfiesRS is the kernel of the restriction homomorphism Aut(x'₀) ⟶ Aut(x) from the automorphisms of the chosen dual-number pushforward x'₀ of x to those of x over k; under this identification addition is composition of automorphisms, and multiplication by c ∈ k is transport along the scaling ε ↦ cε of the dual numbers.

theorem infinitesimalAutomorphismModuleOfSatisfiesRS_carrier
    (x : (letI := (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).category
      (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection.Fiber
        (residueFieldObject.{u, u, u} Λ k)))
    (P : letI := (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).category
      ChosenPushforwardsAt (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection
        x.1) :
    letI := (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).category
    ∃ h : ((infinitesimalAutomorphismModuleOfSatisfiesRS B S hS p hp hRS iΛ x₀ hx₀ hfinite hqc
        x P : ModuleCat k) : Type _) =
        infinitesimalAutomorphismKernel P
          (squareZeroUnderRed (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀
            hx₀).projection x.1 (FGModuleCat.of k (ULift.{u} k))),
      (∀ a b, cast h (a + b) = cast h a * cast h b) ∧
        ∀ (c : k) a, (cast h (c • a)).1 =
          P.transportAutHom (squareZeroUnderMap
            (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection x.1
            (FGModuleCat.ofHom (c • LinearMap.id : ULift.{u} k →ₗ[k] ULift.{u} k)))
            (cast h a).1

Deformation.Artin.isFiniteDimensionalDeformationCategory_predeformationCategory_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/TangentSpaceVectorStructure.lean, line 198. The attribute's comment: “the natural condition: the vector spaces TF_{X,k,x_0} and Inf(F_{X,k,x_0}) have finite dimension”.

The finite-dimensionality condition. For 𝒳 satisfying (RS), the condition Deformation.IsFiniteDimensionalDeformationCategory on 𝓕_{𝒳,k,x₀} holds exactly when the two vector spaces T𝓕_{𝒳,k,x₀} and Inf(𝓕_{𝒳,k,x₀}) (at every object over k and every choice of pushforwards) are finite dimensional.

theorem isFiniteDimensionalDeformationCategory_predeformationCategory_iff :
    letI := (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).category
    IsFiniteDimensionalDeformationCategory.{u, u, u}
        (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection ↔
      FiniteDimensional k
          (tangentSpaceModuleOfSatisfiesRS B S hS p hp hRS iΛ x₀ hx₀ hfinite hqc) ∧
        ∀ x P, FiniteDimensional k
          (infinitesimalAutomorphismModuleOfSatisfiesRS B S hS p hp hRS iΛ x₀ hx₀ hfinite hqc
            x P)
Tag 07WZ, an equation

Tag 07WZ in the Stacks Project.

Deformation.Artin.squareZeroLiftClasses, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TangentFunctor.lean, line 923. The attribute's comment: “lift classes at the dual numbers”.

Isomorphism classes of lifts of x to Spec A[M], together with their identification with x after restriction to Spec A.

public abbrev squareZeroLiftClasses (M : SiteModule A B) : Type _
Tag 07X0, an equation

Tag 07X0 in the Stacks Project.

Deformation.Artin.infinitesimalAutomorphisms_equiv_restrictionKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/TangentSpace.lean, line 403.

Infinitesimal automorphisms of 𝓕_{𝓧,k,x₀}. Let 𝓧 be fibred in groupoids over the big fppf site of S and let x₀ lie over Spec k. For a pushforward z₀ ⟶ zε of a point of the special fibre along the constant inclusion k ⟶ k[ε], the infinitesimal automorphisms of the predeformation category 𝓕_{𝓧,k,x₀} are canonically the kernel of the restriction homomorphism from the automorphisms of the dual-number object x₀' of 𝓧 to the automorphisms of x₀; the identification keeps the underlying arrow of 𝓧.

public theorem infinitesimalAutomorphisms_equiv_restrictionKernel
    (B : BigFppfSite.{u})
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    {S : Scheme.{u}} (contains : B.Contains S) (iΛ : Spec (.of Λ) ⟶ S)
    {X : Type v} [Category.{w} X]
    (p : X ⥤ BigFppfOver B S contains)
    (fibered : p.IsFiberedInGroupoids) (x₀ : X)
    (hx₀ : (p ⋙ Over.post B.inclusion).obj x₀ = Over.mk
      (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let D := predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀
    letI : Category.{max u w} D.carrier := D.category
    ∀ {A₀ Aε : ArtinianLocalAlgCat.{u, u, u} Λ k}
      {z₀ : D.projection.Fiber A₀} {zε : D.projection.Fiber Aε}
      (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀)
      (hpair : IsCanonicalDualNumberPair g e)
      (i : z₀.1 ⟶ zε.1) (hi : D.projection.IsHomLift g i),
      let y := (D.objects zε.1).point
      let xε' : p.op.Fiber (Opposite.op (p.obj y)) := ⟨Opposite.op y, rfl⟩
      let x₀' : p.op.Fiber (Opposite.op (p.obj x₀)) := ⟨Opposite.op x₀, rfl⟩
      let r := (D.objects zε.1).arrow
      let restriction : Aut xε' →* Aut x₀' :=
        pushforwardAutomorphismHom
          (p := p.op) (x' := xε') (x := x₀')
          (isCofiberedInGroupoids_op_of_isFiberedInGroupoids fibered)
          (p.op.map r.op) r.op (Functor.IsHomLift.map (p := p.op) r.op)
      ∃! E : ↥(infinitesimalAutomorphisms
          (predeformationCategory_isPredeformationCategory B contains iΛ p x₀ hx₀
            fibered).cofibered g e hpair i hi) ≃* ↥(MonoidHom.ker restriction),
        ∀ a, (E a).val.asIso.hom.val.unop =
          (D.morphisms zε.1 zε.1 a.val.asIso.hom.val).arrow
Tag 07X1, a lemma

Tag 07X1 in the Stacks Project.

Deformation.Artin.isFiniteDimensionalDeformationCategory_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/AlgebraicStackFiniteDimensional.lean, line 351.

Stacks Project, Tag 07X1. Let S be a locally Noetherian scheme, 𝒳 an algebraic stack over S, U a scheme locally of finite type over S, and (Sch/U) ⟶ 𝒳 a smooth surjective 1-morphism. For every deformation category 𝓕 = 𝓕_{𝒳,k,x₀} of Tag 07T2 — a point x₀ of 𝒳 over a field k of finite type over S, and an affine open Spec Λ ⊂ S through which Spec k ⟶ S factors with Λ ⟶ k finite — the tangent space T𝓕 and the space of infinitesimal automorphisms Inf(𝓕) are finite dimensional over k.

theorem isFiniteDimensionalDeformationCategory_of_isAlgebraicStack [IsLocallyNoetherian S]
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) (U : BigFppfOver B S hS)
    [LocallyOfFiniteType (B.inclusion.map U.hom)]
    (a : Stack.schemeStack.{u, w} B S hS U ⟶ 𝒳)
    (hsurj : Stack.IsSurjective B S hS a) (hsm : Stack.AlgebraicStacks.IsSmooth B S hS a)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (iΛ : Spec (.of Λ) ⟶ S) [IsOpenImmersion iΛ]
    (x₀ : 𝒳.val.val.obj)
    (hx₀ : (𝒳.val.val.p ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hqc : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let D := predeformationCategory iΛ (𝒳.val.val.p ⋙ Over.post B.inclusion) x₀ hx₀
    letI := D.category
    IsFiniteDimensionalDeformationCategory D.projection

Deformation.Artin.isFiniteDimensionalDeformationCategory_of_algebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FiniteDimensional/AlgebraicStack.lean, line 53.

Let S be a locally Noetherian scheme, 𝒳 an algebraic stack over S, U a scheme locally of finite type over S and f : (Sch/U)_{fppf} ⟶ 𝒳 a smooth surjective 1-morphism. Then for every 𝓕 = 𝓕_{𝒳,k,x₀} as in Section 07T2 — k a field of finite type over S, Spec Λ ⊆ S an affine open through which Spec k ⟶ S factors with Λ → k finite, x₀ an object of 𝒳 over Spec k — the tangent space T𝓕 and the infinitesimal automorphisms Inf(𝓕) are finite-dimensional over k, for the vector-space structures of the deformation category 𝓕.

theorem isFiniteDimensionalDeformationCategory_of_algebraicStack [IsLocallyNoetherian S]
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS)
    (U : BigFppfOver B S hS) [LocallyOfFiniteType (B.inclusion.map U.hom)]
    (f : Stack.schemeFibredCategory B S hS U ⟶ 𝒳.val)
    (hf : Stack.IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hsmoothsurj : ∀ (W : BigFppfOver B S hS)
      (yv : BigFppfOver B W.left.1 W.left.2 ⥤ 𝒳.val.val.obj)
      (_hyv : yv ⋙ 𝒳.val.val.p = Over.map W.hom)
      (F : (BigFppfOver B W.left.1 W.left.2)ᵒᵖ ⥤ Type u)
      (hF : IsAlgebraicSpace B W.left.1 W.left.2 F),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map W.hom) (Stack.schemeFibredCategory B S hS U).val.p
          𝒳.val.val.p yv (CatFiberedInGroupoids.homFunctor f))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      (let h := (algebraicSpaceMap B S hS W
        ((spacesOverSmallerBaseFunctor B W.left.1 S W.left.2 hS W.hom).obj ⟨F, hF⟩)).hom
       Space.IsSurjective B S hS h ∧ Space.IsSmooth B S hS h))
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (iΛ : Spec (.of Λ) ⟶ S) (hiΛ : IsOpenImmersion iΛ) (x₀ : 𝒳.val.val.obj)
    (hx₀ : (𝒳.val.val.p ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) ∧
      QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    letI := (predeformationCategory iΛ (𝒳.val.val.p ⋙ Over.post B.inclusion) x₀ hx₀).category
    IsFiniteDimensionalDeformationCategory
      (predeformationCategory iΛ (𝒳.val.val.p ⋙ Over.post B.inclusion) x₀ hx₀).projection
Tag 07X2, a lemma

Tag 07X2 in the Stacks Project.

Deformation.Artin.sixTermExact_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ArtinCriteria/TangentSpace/SixTermExact.lean, line 202.

Stacks Project, Tag 07X2, the full six-term exact sequence.

Let S be a locally Noetherian scheme, let Φ : 𝒳 ⟶ 𝒴 and Ψ : 𝒵 ⟶ 𝒴 be 1-morphisms of categories fibred in groupoids over the big fppf site of S, and assume 𝒳, 𝒴, 𝒵 satisfy (RS). Let k be a field of finite type over S and let w₀ be an object of 𝒲 = 𝒳 ×_𝒴 𝒵 over k, with induced objects x₀, y₀ = Φ(x₀), z₀ of 𝒳, 𝒴, 𝒵. Then

0 → Inf(𝓕_𝒲) → Inf(𝓕_𝒳) ⊕ Inf(𝓕_𝒵) → Inf(𝓕_𝒴) → T𝓕_𝒲 → T𝓕_𝒳 ⊕ T𝓕_𝒵 → T𝓕_𝒴

is an exact sequence, with the first pair of maps induced by the two projections of 𝒲, the first difference by the maps induced by Φ and by Ψ (the latter transported along the comparison isomorphism ψ(w₀) : Φ(x₀) ≅ Ψ(z₀)), a boundary map out of Inf(𝓕_𝒴), and again the pair of projections and the difference of the maps induced by Φ and Ψ, now on tangent spaces.

The square of predeformation categories is a 2-fibre product (Tag 07WL): the comparison 1-morphism from 𝒲 to CategoryTheory.TwoFibreProductOver is an equivalence (Deformation.Artin.fibreProductOfPredeformationCategoriesOfEssSurj). Each of the five exactness/injectivity claims of the abstract six-term sequence for the literal 2-fibre product (Tag 06L5, Deformation.SixTerm.twoFibreProduct_sixTermExact) is transported along this equivalence, respectively by Deformation.injective_infProjPairOfLift, Deformation.exact_infProjPairOfLift, Deformation.exact_infLegDiff_infBoundaryLinearMapOfLift, Deformation.exact_infBoundaryLinearMapOfLift_tangentProjPairOfLift and Deformation.exact_tangentPairOfLift_tangentLegDiffOfEq.

public theorem sixTermExact_twoFibreProduct
    (hΦ : Φ ⋙ p𝒴 = p𝒳) (hΨ : Ψ ⋙ p𝒴 = p𝒵)
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (h𝒵 : p𝒵.IsFiberedInGroupoids)
    (hRS𝒳 : SatisfiesRS B S hS p𝒳 h𝒳) (hRS𝒴 : SatisfiesRS B S hS p𝒴 h𝒴)
    (hRS𝒵 : SatisfiesRS B S hS p𝒵 h𝒵)
    (w₀ : TwoFibreProductOver p𝒳 p𝒵 p𝒴 Φ Ψ)
    (hw₀base : (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ ⋙
      Over.post B.inclusion).obj w₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
      (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hqc : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let hA := fst_comp_post_eq B S hS p𝒳 p𝒴 p𝒵 Φ Ψ
    let hB := snd_comp_post_eq B S hS p𝒳 p𝒴 p𝒵 Φ Ψ
    let hF : Φ ⋙ p𝒴 ⋙ Over.post B.inclusion = p𝒳 ⋙ Over.post B.inclusion :=
      congrArg (fun H => H ⋙ Over.post B.inclusion) hΦ
    let hG : Ψ ⋙ p𝒴 ⋙ Over.post B.inclusion = p𝒵 ⋙ Over.post B.inclusion :=
      congrArg (fun H => H ⋙ Over.post B.inclusion) hΨ
    let hX := imageBasePoint (qY := p𝒳 ⋙ Over.post B.inclusion) iΛ
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ ⋙ Over.post B.inclusion)
      (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ) hA w₀ hw₀base
    let hZ := imageBasePoint (qY := p𝒵 ⋙ Over.post B.inclusion) iΛ
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ ⋙ Over.post B.inclusion)
      (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 Φ Ψ) hB w₀ hw₀base
    let hY := imageBasePoint (qY := p𝒴 ⋙ Over.post B.inclusion) iΛ
      (p𝒳 ⋙ Over.post B.inclusion) Φ hF ((TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀) hX
    let D𝒲 := predeformationCategory iΛ
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ ⋙ Over.post B.inclusion) w₀ hw₀base
    let D𝒳 := predeformationCategory iΛ (p𝒳 ⋙ Over.post B.inclusion)
      ((TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀) hX
    let D𝒵 := predeformationCategory iΛ (p𝒵 ⋙ Over.post B.inclusion)
      ((TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀) hZ
    let D𝒴 := predeformationCategory iΛ (p𝒴 ⋙ Over.post B.inclusion)
      (Φ.obj ((TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀)) hY
    letI := D𝒲.category
    letI := D𝒳.category
    letI := D𝒵.category
    letI := D𝒴.category
    let mA := mapPredeformationCategory iΛ
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ ⋙ Over.post B.inclusion)
      (p𝒳 ⋙ Over.post B.inclusion) (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ) hA w₀ hw₀base
    let mB := mapPredeformationCategory iΛ
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ ⋙ Over.post B.inclusion)
      (p𝒵 ⋙ Over.post B.inclusion) (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 Φ Ψ) hB w₀ hw₀base
    let mF := mapPredeformationCategory iΛ (p𝒳 ⋙ Over.post B.inclusion)
      (p𝒴 ⋙ Over.post B.inclusion) Φ hF
      ((TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀) hX
    let data := fibreProductOfPredeformationCategoriesOfEssSurj iΛ
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ ⋙ Over.post B.inclusion)
      (p𝒳 ⋙ Over.post B.inclusion) (p𝒵 ⋙ Over.post B.inclusion)
      (p𝒴 ⋙ Over.post B.inclusion) (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ)
      (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 Φ Ψ) Φ Ψ hA hB hF
      (TwoFibreProductOver.psiIso p𝒳 p𝒵 p𝒴 Φ Ψ) w₀ hw₀base hG
      (isHomLift_psiIso_post B S hS p𝒳 p𝒴 p𝒵 Φ Ψ)
      (exists_liftPost_iso_over_base B S hS p𝒳 p𝒴 p𝒵 Φ Ψ)
      (isEquivalence_liftPost B S hS p𝒳 p𝒴 p𝒵 Φ Ψ)
    let hD𝒲 := isDeformationCategory_predeformationCategory B S hS
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 Φ Ψ)
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 Φ Ψ h𝒳 h𝒵 h𝒴 hΦ hΨ)
      (satisfiesRS_twoFibreProductOver B S hS p𝒳 p𝒴 p𝒵 Φ Ψ h𝒳 h𝒴 h𝒵 hΦ hΨ
        hRS𝒳 hRS𝒴 hRS𝒵) iΛ w₀ hw₀base hfinite hqc
    let hD𝒳 := isDeformationCategory_predeformationCategory B S hS p𝒳 h𝒳 hRS𝒳 iΛ
      ((TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀) hX hfinite hqc
    let hD𝒵 := isDeformationCategory_predeformationCategory B S hS p𝒵 h𝒵 hRS𝒵 iΛ
      ((TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀) hZ hfinite hqc
    let hD𝒴 := isDeformationCategory_predeformationCategory B S hS p𝒴 h𝒴 hRS𝒴 iΛ
      (Φ.obj ((TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 Φ Ψ).obj w₀)) hY hfinite hqc
    let hA' : mA.toFunctor ⋙ (mF.toFunctor ⋙ D𝒴.projection) = D𝒲.projection :=
      (congrArg (mA.toFunctor ⋙ ·) mF.projection_comm).trans mA.projection_comm
    let hB' : mB.toFunctor ⋙ (data.rightFunctor ⋙ D𝒴.projection) = D𝒲.projection :=
      (congrArg (mB.toFunctor ⋙ ·) data.rightFunctor_projection).trans mB.projection_comm
    let hH' : IsDeformationCategory (mF.toFunctor ⋙ D𝒴.projection) := mF.projection_comm ▸ hD𝒳
    let hG' : IsDeformationCategory (data.rightFunctor ⋙ D𝒴.projection) :=
      data.rightFunctor_projection ▸ hD𝒵
    let hlift' : (TwoFibreProductOver.lift (mF.toFunctor ⋙ D𝒴.projection)
        (data.rightFunctor ⋙ D𝒴.projection) D𝒴.projection mF.toFunctor data.rightFunctor
        D𝒲.projection mA.toFunctor mB.toFunctor hA' hB' data.filler
        data.filler_vertical).IsEquivalence :=
      Deformation.isEquivalence_lift_congr D𝒴.projection D𝒲.projection mF.toFunctor
        data.rightFunctor mA.toFunctor mB.toFunctor D𝒳.projection
        (mF.toFunctor ⋙ D𝒴.projection) mF.projection_comm.symm D𝒵.projection
        (data.rightFunctor ⋙ D𝒴.projection) data.rightFunctor_projection.symm
        mA.projection_comm hA' mB.projection_comm hB' data.filler data.filler_vertical
        data.isEquivalence
    letI := hlift'
    let w₀' : D𝒲.projection.Fiber (Deformation.residueFieldObject Λ k) :=
      (Classical.choice hD𝒲.predeformation.specialFiber).inverse.obj ⟨PUnit.unit⟩
    let hw₀ : (mF.toFunctor ⋙ D𝒴.projection).obj (mA.toFunctor.obj w₀'.1) =
        Deformation.residueFieldObject Λ k :=
      (Functor.congr_obj mF.projection_comm (mA.toFunctor.obj w₀'.1)).trans
        ((Functor.congr_obj mA.projection_comm w₀'.1).trans w₀'.2)
    let PW := Deformation.chosenPushforwardsAtOfCofiberedInGroupoids
      hD𝒲.predeformation.cofibered w₀'.1
    let QH := Deformation.chosenPushforwardsAtOfCofiberedInGroupoids
      hH'.predeformation.cofibered (mA.toFunctor.obj w₀'.1)
    let QG := Deformation.chosenPushforwardsAtOfCofiberedInGroupoids
      hG'.predeformation.cofibered (mB.toFunctor.obj w₀'.1)
    let PF := Deformation.chosenPushforwardsAtOfCofiberedInGroupoids
      hD𝒴.predeformation.cofibered (mF.toFunctor.obj (mA.toFunctor.obj w₀'.1))
    let PF' := Deformation.chosenPushforwardsAtOfCofiberedInGroupoids
      hD𝒴.predeformation.cofibered (data.rightFunctor.obj (mB.toFunctor.obj w₀'.1))
    let PL := Deformation.transportChosenPushforwardsAt
      (TwoFibreProductOver.lift (mF.toFunctor ⋙ D𝒴.projection)
        (data.rightFunctor ⋙ D𝒴.projection) D𝒴.projection mF.toFunctor data.rightFunctor
        D𝒲.projection mA.toFunctor mB.toFunctor hA' hB' data.filler data.filler_vertical)
      (TwoFibreProductOver.lift_comp_structureFunctor ..) w₀'.1 PW
    letI := Deformation.naturalLocalizedTangentAddCommGroup PW hD𝒲.satisfiesRS
    letI := Deformation.naturalLocalizedTangentModule PW hD𝒲.satisfiesRS
    letI := Deformation.naturalLocalizedTangentAddCommGroup QH hH'.satisfiesRS
    letI := Deformation.naturalLocalizedTangentModule QH hH'.satisfiesRS
    letI := Deformation.naturalLocalizedTangentAddCommGroup QG hG'.satisfiesRS
    letI := Deformation.naturalLocalizedTangentModule QG hG'.satisfiesRS
    letI := Deformation.naturalLocalizedTangentAddCommGroup PF hD𝒴.satisfiesRS
    letI := Deformation.naturalLocalizedTangentModule PF hD𝒴.satisfiesRS
    Function.Injective
      (LinearMap.prod
        (Deformation.inducedInfinitesimalLinearMapOfEq mA.toFunctor hA' hD𝒲.satisfiesRS
          hH'.satisfiesRS PW QH)
        (Deformation.inducedInfinitesimalLinearMapOfEq mB.toFunctor hB' hD𝒲.satisfiesRS
          hG'.satisfiesRS PW QG)) ∧
    Function.Exact
      (LinearMap.prod
        (Deformation.inducedInfinitesimalLinearMapOfEq mA.toFunctor hA' hD𝒲.satisfiesRS
          hH'.satisfiesRS PW QH)
        (Deformation.inducedInfinitesimalLinearMapOfEq mB.toFunctor hB' hD𝒲.satisfiesRS
          hG'.satisfiesRS PW QG))
      (Deformation.infLegDiff D𝒴.projection mF.toFunctor data.rightFunctor hH' hG' hD𝒴
        (w₀ :=
          (⟨D𝒲.projection.obj w₀'.1, mA.toFunctor.obj w₀'.1, mB.toFunctor.obj w₀'.1,
              Functor.congr_obj hA' w₀'.1, Functor.congr_obj hB' w₀'.1,
              data.filler.app w₀'.1, data.filler_vertical w₀'.1⟩ :
            TwoFibreProductOver (mF.toFunctor ⋙ D𝒴.projection)
              (data.rightFunctor ⋙ D𝒴.projection) D𝒴.projection mF.toFunctor
              data.rightFunctor))
        QH QG PF PF' hw₀) ∧
    Function.Exact
      (Deformation.infLegDiff D𝒴.projection mF.toFunctor data.rightFunctor hH' hG' hD𝒴
        (w₀ :=
          (⟨D𝒲.projection.obj w₀'.1, mA.toFunctor.obj w₀'.1, mB.toFunctor.obj w₀'.1,
              Functor.congr_obj hA' w₀'.1, Functor.congr_obj hB' w₀'.1,
              data.filler.app w₀'.1, data.filler_vertical w₀'.1⟩ :
            TwoFibreProductOver (mF.toFunctor ⋙ D𝒴.projection)
              (data.rightFunctor ⋙ D𝒴.projection) D𝒴.projection mF.toFunctor
              data.rightFunctor))
        QH QG PF PF' hw₀)
      (Deformation.infBoundaryLinearMapOfLift D𝒴.projection D𝒲.projection mF.toFunctor
        data.rightFunctor mA.toFunctor mB.toFunctor hA' hB' data.filler data.filler_vertical
        hlift' hD𝒲 hH' hG' hD𝒴 QH QG PF) ∧
    Function.Exact
      (Deformation.infBoundaryLinearMapOfLift D𝒴.projection D𝒲.projection mF.toFunctor
        data.rightFunctor mA.toFunctor mB.toFunctor hA' hB' data.filler data.filler_vertical
        hlift' hD𝒲 hH' hG' hD𝒴 QH QG PF)
      (LinearMap.prod
        (Deformation.tangentMapAt hD𝒲 hH'
          ({ toFunctor := mA.toFunctor, w := hA' } :
            BasedCategory.ofFunctor D𝒲.projection ⥤ᵇ
              BasedCategory.ofFunctor (mF.toFunctor ⋙ D𝒴.projection))
          (FGModuleCat.of k (ULift.{u} k)))
        (Deformation.tangentMapAt hD𝒲 hG'
          ({ toFunctor := mB.toFunctor, w := hB' } :
            BasedCategory.ofFunctor D𝒲.projection ⥤ᵇ
              BasedCategory.ofFunctor (data.rightFunctor ⋙ D𝒴.projection))
          (FGModuleCat.of k (ULift.{u} k)))) ∧
    Function.Exact
      (LinearMap.prod
        (Deformation.tangentMapAt hD𝒲 hH'
          ({ toFunctor := mA.toFunctor, w := hA' } :
            BasedCategory.ofFunctor D𝒲.projection ⥤ᵇ
              BasedCategory.ofFunctor (mF.toFunctor ⋙ D𝒴.projection))
          (FGModuleCat.of k (ULift.{u} k)))
        (Deformation.tangentMapAt hD𝒲 hG'
          ({ toFunctor := mB.toFunctor, w := hB' } :
            BasedCategory.ofFunctor D𝒲.projection ⥤ᵇ
              BasedCategory.ofFunctor (data.rightFunctor ⋙ D𝒴.projection))
          (FGModuleCat.of k (ULift.{u} k))))
      ((Deformation.tangentMapAt hH' hD𝒴
            ({ toFunctor := mF.toFunctor, w := rfl } :
              BasedCategory.ofFunctor (mF.toFunctor ⋙ D𝒴.projection) ⥤ᵇ
                BasedCategory.ofFunctor D𝒴.projection)
            (FGModuleCat.of k (ULift.{u} k))).comp
          (LinearMap.fst k
            ↥(Deformation.tangentModuleAt
              (BasedCategory.ofFunctor (mF.toFunctor ⋙ D𝒴.projection)) hH'
              (FGModuleCat.of k (ULift.{u} k)))
            ↥(Deformation.tangentModuleAt
              (BasedCategory.ofFunctor (data.rightFunctor ⋙ D𝒴.projection)) hG'
              (FGModuleCat.of k (ULift.{u} k)))) -
        (Deformation.tangentMapAt hG' hD𝒴
            ({ toFunctor := data.rightFunctor, w := rfl } :
              BasedCategory.ofFunctor (data.rightFunctor ⋙ D𝒴.projection) ⥤ᵇ
                BasedCategory.ofFunctor D𝒴.projection)
            (FGModuleCat.of k (ULift.{u} k))).comp
          (LinearMap.snd k
            ↥(Deformation.tangentModuleAt
              (BasedCategory.ofFunctor (mF.toFunctor ⋙ D𝒴.projection)) hH'
              (FGModuleCat.of k (ULift.{u} k)))
            ↥(Deformation.tangentModuleAt
              (BasedCategory.ofFunctor (data.rightFunctor ⋙ D𝒴.projection)) hG'
              (FGModuleCat.of k (ULift.{u} k)))))
Sources
LeanDeformation.Artin.tangentSpaceModuleOfSatisfiesRS · Deformation.Artin.tangentSpaceModuleOfSatisfiesRS_carrier · Deformation.Artin.infinitesimalAutomorphismModuleOfSatisfiesRS · Deformation.Artin.infinitesimalAutomorphismModuleOfSatisfiesRS_carrier · Deformation.Artin.isFiniteDimensionalDeformationCategory_predeformationCategory_iff · Deformation.Artin.squareZeroLiftClasses · Deformation.Artin.infinitesimalAutomorphisms_equiv_restrictionKernel · Deformation.Artin.isFiniteDimensionalDeformationCategory_of_isAlgebraicStack

Section98.9 Formal objects#

Section 98.9 of the Stacks Project, Tag 07X3. 8 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07X3, the section

Tag 07X3 in the Stacks Project.

Deformation.Artin.FormalObject.mapFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObjectsSection.lean, line 49. The attribute's comment: “a 1-morphism induces a functor between categories of formal objects”.

The functor between categories of formal objects induced by a 1-morphism of categories fibred in groupoids: every level and every level map is pushed forward.

def FormalObject.mapFunctor : FormalObject B S hS 𝒳.val.p ⥤ FormalObject B S hS 𝒴.val.p

Declarations registered for the tag:

Tag 07X4, a definition

Tag 07X4 in the Stacks Project.

Deformation.Artin.FormalObject, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject.lean, line 147. The attribute's comment: “formal objects”.

A formal object of a category over the big fppf site of S.

public structure FormalObject {F : Type v} [Category.{w} F]
    (p : F ⥤ BigFppfOver B S hS)

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

A compatible family of morphisms between formal objects.

public structure Hom (X Y : FormalObject B S hS p)

Deformation.Artin.FormalObject.Hom.baseMapData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject.lean, line 214. The attribute's comment: “the induced map of complete bases”.

A compatible family induces a unique map between its complete local bases.

public noncomputable def Hom.baseMapData {X Y : FormalObject B S hS p} (f : Hom X Y) :
    {a : Spec (.of X.base.R) ⟶ Spec (.of Y.base.R) //
      f.IsBaseMap a ∧ ∀ b, f.IsBaseMap b → b = a}
Tag 0CXH, a remark

Tag 0CXH in the Stacks Project.

Deformation.Artin.FormalObject.exists_predeformationFormalObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/Predeformation.lean, line 326.

A formal object of a category over the big fppf site of S gives a formal object of the predeformation category of its closed fibre, with the same levels, the same transition maps and the same complete local base.

theorem FormalObject.exists_predeformationFormalObject
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : Type v} [Category.{w} F]
    (p : F ⥤ BigFppfOver B S hS)
    (ξ : FormalObject B S hS p)
    (Λ : Type u) [CommRing Λ] [Algebra Λ ξ.base.R]
    (iΛ : Spec (.of Λ) ⟶ S)
    (hR : Spec.map (CommRingCat.ofHom (algebraMap Λ ξ.base.R)) ≫ iΛ =
      ξ.base.toS) :
    let R := ξ.base.R
    letI : CommRing R := ξ.base.commRing
    letI : IsLocalRing R := ξ.base.localRing
    let k := ResidueField R
    letI : Field k := ResidueField.field R
    letI : Algebra Λ k := ResidueField.algebra R
    let q : F ⥤ Over S := p ⋙ Over.post B.inclusion
    ∃ hx₀ : q.obj (ξ.level 0) = Over.mk
        (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ),
      let C := predeformationCategory iΛ q (ξ.level 0) hx₀
      letI : Category C.carrier := C.category
      ∃ η : Deformation.FormalObject C.projection,
        η.base = ξ.completeLocalBase Λ ∧
          (∀ n, (C.objects (η.level n)).point = ξ.level n) ∧
          (∀ n, HEq (C.objects (η.level n)).arrow
            (FormalObject.closedPointArrow ξ n)) ∧
          (∀ n, HEq (C.morphisms (η.level (n + 1)) (η.level n)
            (η.transition n)).arrow (ξ.transition n))
Tag 07X5, a lemma

Tag 07X5 in the Stacks Project.

Deformation.Artin.exists_formalObject_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/SmoothLift.lean, line 249.

If F : 𝒳 ⟶ 𝒴 is formally smooth on objects, every formal object η of 𝒴 whose closed-point level lifts to 𝒳 is, up to isomorphism, the image of a formal object of 𝒳 over the same complete local base and with the given closed-point lift.

public theorem exists_formalObject_lift
    (hp : Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p)
    (η : FormalObject B S hS 𝒴.val.p)
    (ξ₀ : 𝒳.val.p.Fiber (truncationOver B S hS η.base η.contains 0))
    (hξ₀ : (Functor.Fiber.mapOfComp 𝒳.val.p 𝒴.val.p (CatFiberedInGroupoids.homFunctor p)
      (CatFiberedInGroupoids.homFunctor_comp_p p)
      (truncationOver B S hS η.base η.contains 0)).obj ξ₀ ≅
        ⟨η.level 0, η.level_eq 0⟩) :
    ∃ ξ : FormalObject B S hS 𝒳.val.p,
      ξ.base = η.base ∧ ξ.level 0 = ξ₀.1 ∧
        Nonempty (FormalObject.map B S hS 𝒳 𝒴 p ξ ≅ η)
Tag 07X6, an equation

Tag 07X6 in the Stacks Project.

Deformation.Artin.approximationFunctorData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject.lean, line 1049.

The canonical functor taking an object over a complete local ring to its compatible system of restrictions to the infinitesimal thickenings.

public noncomputable def approximationFunctorData
    (hp : p.IsFiberedInGroupoids) :
    {G : CompleteLocalObjects B S hS p ⥤ FormalObject B S hS p //
      IsApproximationFunctor B S hS p G}
Tag 07X7, a definition

Tag 07X7 in the Stacks Project.

Deformation.Artin.FormalObject.IsEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject.lean, line 1253.

A formal object is effective if it comes, up to isomorphism, from an object over its complete local base by approximation.

public abbrev IsEffective (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F : Type v} [Category.{w} F]
    (p : F ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids)
    (ξ : FormalObject B S hS p) : Prop
Tag 07X8, a lemma

Tag 07X8 in the Stacks Project.

Deformation.Artin.isEquivalence_approximationFunctor_algebraicStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/ApproximationEssSurj.lean, line 265.

Stacks 07X8. Let 𝒳 be an algebraic stack over a scheme S. The functor (Stacks 07X6) from objects of 𝒳 over spectra of Noetherian complete local S-algebras with residue field of finite type over S (and morphisms inducing local homomorphisms) to formal objects of 𝒳, which restricts an object to the infinitesimal thickenings of the closed point, is an equivalence: full and faithful (Deformation.Artin.full_approximationFunctor_algebraicStacks, Deformation.Artin.faithful_approximationFunctor_algebraicStacks) and essentially surjective (Deformation.Artin.essSurj_approximationFunctor_algebraicStacks). The scheme S is not assumed locally Noetherian.

theorem isEquivalence_approximationFunctor_algebraicStacks
    (𝒳 : Stack.AlgebraicStacks.{u, w} B S hS) :
    (approximationFunctor B S hS 𝒳.val.val.p 𝒳.val.property).IsEquivalence

Deformation.Artin.faithful_approximationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/ApproximationRepresentable.lean, line 440. The attribute's comment: “faithfulness of the functor only, and only for a category fibred in groupoids whose structure functor is faithful, i.e. one fibred in setoids, with the faithfulness of that functor as an added hypothesis the source lacks; this covers the category represented by an object of the site, but neither fullness, nor essential surjectivity, nor a general algebraic stack”.

Stacks 07X8, faithfulness of the functor (Stacks 07X6), for a category fibred in groupoids whose structure functor is faithful, i.e. one fibred in setoids. This covers the category fibred in groupoids represented by an object of the big fppf site over S, i.e. by a scheme over S, which is Case I of the source proof.

Faithfulness of p is a hypothesis the source does not impose; it holds exactly when p is fibred in setoids, so it excludes a general algebraic stack. The source's hypothesis that S is locally Noetherian is, on the other hand, not needed here.

public theorem faithful_approximationFunctor [p.Faithful]
    (hp : p.IsFiberedInGroupoids) :
    (approximationFunctor B S hS p hp).Faithful

Deformation.Artin.full_approximationFunctor_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/ApproximationRepresentable.lean, line 665. The attribute's comment: “fullness of the functor only, and only for the category fibred in groupoids represented by an object of the big fppf site over S, i.e. by a scheme over S; this is half of Case I of the source proof, and covers neither essential surjectivity nor the algebraic space of Case II nor the general algebraic stack of Case III”.

Stacks 07X8, fullness of the functor (Stacks 07X6), for the category fibred in groupoids represented by an object Xo of the big fppf site over S, i.e. by a scheme over S. This is the fullness half of Case I of the source proof.

The source's hypothesis that S is locally Noetherian is not needed.

public theorem full_approximationFunctor_representable (Xo : BigFppfOver B S hS) :
    (approximationFunctor B S hS (Over.forget Xo)
      (Functor.IsFiberedInGroupoids.over_forget Xo)).Full
Tag 07X9, a lemma

Tag 07X9 in the Stacks Project.

Deformation.Artin.isEquivalence_approximationFunctor_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/ApproximationTwoFibreProduct.lean, line 905.

Stacks 07X9. The approximation equivalence is stable under 2-fibre products of categories fibred in groupoids over the big fppf site: if the approximation functor is an equivalence for pX, pY and pZ, then it is an equivalence for pX ×_pY pZ.

public theorem isEquivalence_approximationFunctor_twoFibreProduct
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type vX} [Category.{wX} X]
    {Y : Type vY} [Category.{wY} Y]
    {Z : Type vZ} [Category.{wZ} Z]
    (pX : X ⥤ BigFppfOver B S hS)
    (pY : Y ⥤ BigFppfOver B S hS)
    (pZ : Z ⥤ BigFppfOver B S hS)
    (f : X ⥤ Y) (g : Z ⥤ Y)
    (hpX : pX.IsFiberedInGroupoids) (hpY : pY.IsFiberedInGroupoids)
    (hpZ : pZ.IsFiberedInGroupoids)
    (hf : f ⋙ pY = pX) (hg : g ⋙ pY = pZ)
    (hX : (approximationFunctor B S hS pX hpX).IsEquivalence)
    (hY : (approximationFunctor B S hS pY hpY).IsEquivalence)
    (hZ : (approximationFunctor B S hS pZ hpZ).IsEquivalence) :
    (approximationFunctor B S hS
      (TwoFibreProductOver.structureFunctor pX pZ pY f g)
      (TwoFibreProductOver.isFiberedInGroupoids pX pZ pY f g
        hpX hpZ hpY hf hg)).IsEquivalence
Sources
LeanDeformation.Artin.FormalObject.mapFunctor · Deformation.Artin.FormalObject · Deformation.Artin.FormalObject.Hom · Deformation.Artin.FormalObject.exists_predeformationFormalObject · Deformation.Artin.exists_formalObject_lift · Deformation.Artin.approximationFunctorData · Deformation.Artin.FormalObject.IsEffective · Deformation.Artin.isEquivalence_approximationFunctor_algebraicStacks

Section98.10 Approximation#

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

Tag 07XB, a lemma

Tag 07XB in the Stacks Project.

Deformation.Artin.Approximation.exists_finiteType_approximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Approximation/FiniteType.lean, line 84. The attribute's comment: “clauses (1)-(6): the finite type algebra, its maximal ideal, the object, the isomorphism of Nth neighbourhoods, the compatible isomorphism of the restricted objects, and the isomorphism of graded k-algebras. Stacks 07QZ, the source's one external input here, is proved: Stacks.Smoothing.exists_localEtaleSolution_of_isGRing”.

Stacks Project, Tag 07XB. Approximation of a fibred object over a Noetherian complete local ring by an object over a finite type S-algebra.

Let S be a locally Noetherian scheme, let 𝒳 be a category fibred in groupoids over the big fppf site of S, and let x be an object of 𝒳 over Spec R for R a Noetherian complete local ring whose residue field is of finite type over S. Let s ∈ S be the image of Spec k. If O_{S, s} is a G-ring and the structure morphism of 𝒳 is limit preserving on objects, then for every N ≥ 1 there are a finite type S-algebra A, a maximal ideal m_A ⊆ A, an object x_A of 𝒳 over Spec A, an S-isomorphism R/m_R^N ≅ A/m_A^N, an isomorphism of the restrictions of x and x_A to those truncations compatible with it, and an isomorphism of graded k-algebras Gr_{m_R}(R) ≅ Gr_{m_A}(A).

These are clauses (1)-(6) of the tag. Clause (6) is the final existential: a ring isomorphism of the associated graded rings which carries each homogeneous summand to the summand of the same degree and which, in degree zero, agrees with the truncation isomorphism φ of clause (4).

Artin approximation over a G-ring (Stacks 07QZ) is used in the proof and is discharged by Stacks.Smoothing.exists_localEtaleSolution_of_isGRing, so the statement below carries no hypothesis beyond the source's own.

public theorem exists_finiteType_approximation
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S]
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (Site B S hS))
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (hR : B.Contains (Spec (.of R)))
    (fR : Spec (.of R) ⟶ S)
    (hfinite : LocallyOfFiniteType
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (maximalIdeal R))) ≫ fR))
    (hquasi : QuasiCompact
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (maximalIdeal R))) ≫ fR))
    (s : S)
    (hs : fR (closedPoint R) = s)
    (hG : IsGRing (S.presheaf.stalk s))
    (hp : AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B S hS 𝒳
      (baseFiberedCategory B S hS) (structureMorphism B S hS 𝒳))
    (x : 𝒳.val.p.Fiber (siteObject B S hS hR fR))
    (N : ℕ) (hN : 1 ≤ N) :
    ∃ (A : Type u) (_ : CommRing A) (mA : Ideal A) (_ : mA.IsMaximal)
      (fA : Spec (.of A) ⟶ S)
      (hA : B.Contains (Spec (.of A)))
      (hRN : B.Contains (Spec (.of (R ⧸ maximalIdeal R ^ N))))
      (hAN : B.Contains (Spec (.of (A ⧸ mA ^ N))))
      (xA : 𝒳.val.p.Fiber (siteObject B S hS hA fA)),
      LocallyOfFiniteType fA ∧ QuasiCompact fA ∧
      ∃ (φ : (R ⧸ maximalIdeal R ^ N) ≃+* (A ⧸ mA ^ N)),
        Spec.map (CommRingCat.ofHom φ.symm.toRingHom) ≫
            Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (mA ^ N))) ≫ fA =
          Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk ((maximalIdeal R) ^ N))) ≫ fR ∧
        ∃ (iR : siteObject B S hS hRN
              (Spec.map (CommRingCat.ofHom
                (Ideal.Quotient.mk ((maximalIdeal R) ^ N))) ≫ fR) ⟶
              siteObject B S hS hR fR)
          (iA : siteObject B S hS hAN
              (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (mA ^ N))) ≫ fA) ⟶
              siteObject B S hS hA fA)
          (eBase : siteObject B S hS hRN
              (Spec.map (CommRingCat.ofHom
                (Ideal.Quotient.mk ((maximalIdeal R) ^ N))) ≫ fR) ⟶
              siteObject B S hS hAN
                (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (mA ^ N))) ≫ fA))
          (xRN : 𝒳.val.p.Fiber (siteObject B S hS hRN
              (Spec.map (CommRingCat.ofHom
                (Ideal.Quotient.mk ((maximalIdeal R) ^ N))) ≫ fR)))
          (xAN : 𝒳.val.p.Fiber (siteObject B S hS hAN
              (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (mA ^ N))) ≫ fA)))
          (r : xRN.1 ⟶ x.1) (a : xAN.1 ⟶ xA.1)
          (e : xRN.1 ⟶ xAN.1),
          (AlgebraicGeometry.BigFppfOver.toScheme B S hS).map iR =
              Spec.map (CommRingCat.ofHom
                (Ideal.Quotient.mk ((maximalIdeal R) ^ N))) ∧
          (AlgebraicGeometry.BigFppfOver.toScheme B S hS).map iA =
              Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (mA ^ N))) ∧
          (AlgebraicGeometry.BigFppfOver.toScheme B S hS).map eBase =
              Spec.map (CommRingCat.ofHom φ.symm.toRingHom) ∧
          𝒳.val.p.IsStronglyCartesian iR r ∧
          𝒳.val.p.IsStronglyCartesian iA a ∧
          𝒳.val.p.IsHomLift eBase e ∧ IsIso e ∧
          ∃ (gr : AssociatedGraded.gradedRing (maximalIdeal R) ≃+*
              AssociatedGraded.gradedRing mA),
            (∀ n (z : AssociatedGraded.piece (M := R) (maximalIdeal R) n),
              ∃ w : AssociatedGraded.piece (M := A) mA n,
                gr (DirectSum.of _ n z) = DirectSum.of _ n w) ∧
            ∀ (r₀ : R) (a₀ : A),
              φ (Ideal.Quotient.mk ((maximalIdeal R) ^ N) r₀) =
                  Ideal.Quotient.mk (mA ^ N) a₀ →
              gr (DirectSum.of _ 0
                    (AssociatedGraded.mk (maximalIdeal R) 0
                      (⟨r₀, by simp⟩ :
                        AssociatedGraded.power (M := R) (maximalIdeal R) 0))) =
                DirectSum.of _ 0
                  (AssociatedGraded.mk mA 0
                    (⟨a₀, by simp⟩ : AssociatedGraded.power (M := A) mA 0))
Tag 07XC, an equation

Tag 07XC in the Stacks Project.

AdicCompletion.exists_surjective_adicCompletionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AdicCompletion/PolynomialSurjection.lean, line 68.

Stacks Project, Tag 07XC. A map from a polynomial ring to a Noetherian complete local ring which is surjective modulo the square of the maximal ideal extends to a surjective local map from the completion of its localization at the residue-field kernel.

theorem exists_surjective_adicCompletionMap
    (Λ R : Type*) [CommRing Λ] [CommRing R] [Algebra Λ R]
    [IsNoetherianRing Λ] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (s : ℕ) (p : Ideal (MvPolynomial (Fin s) Λ)) [p.IsMaximal]
    (f : MvPolynomial (Fin s) Λ →ₐ[Λ] R)
    (hp : Ideal.comap f.toRingHom (maximalIdeal R) = p)
    (hmod : Function.Surjective
      ((Ideal.Quotient.mk ((maximalIdeal R) ^ 2)).comp f.toRingHom)) :
    let A := Localization.AtPrime p
    let P := AdicCompletion (maximalIdeal A) A
    IsNoetherianRing P ∧ IsLocalRing P ∧
      IsAdicComplete (maximalIdeal P) P ∧
      ∃ g : A →+* R,
        g.comp (algebraMap (MvPolynomial (Fin s) Λ) A) = f.toRingHom ∧
        IsLocalHom g ∧
        ∃ φ : P →+* R,
          φ.comp (algebraMap A P) = g ∧
            Function.Surjective φ ∧ IsLocalHom φ ∧
              ∀ ψ : P →+* R,
                ψ.comp (algebraMap A P) = g → IsLocalHom ψ → ψ = φ
Sources
LeanDeformation.Artin.Approximation.exists_finiteType_approximation · AdicCompletion.exists_surjective_adicCompletionMap

Section98.11 Limit preserving#

Section 98.11 of the Stacks Project, Tag 07XK. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07XL, a definition

Tag 07XL in the Stacks Project.

Deformation.Artin.IsLimitPreserving, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/LimitPreserving.lean, line 144.

A category fibred in groupoids is limit preserving if for every directed inverse limit of affine schemes the canonical comparison colim 𝒳_{Tᵢ} ⥤ 𝒳_T is an equivalence of categories.

public abbrev IsLimitPreserving
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (𝒳 : CatFiberedInGroupoids.{u, vX, u + 1, uX}
      (BigFppfOver B S hS)) : Prop
Tag 07XM, a lemma

Tag 07XM in the Stacks Project.

AlgebraicGeometry.Stack.isLimitPreserving_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingTwoFibreProduct.lean, line 715. The attribute's comment: “part (2)”.

Stacks 07XM, part (2). If 𝒳, 𝒴 and 𝒵 are limit preserving categories fibred in groupoids over (Sch/S)_{fppf}, then so is the 2-fibre product 𝒳 ×_𝒴 𝒵: for every directed inverse system of affine schemes with limit T, the canonical comparison from the colimit of the fibre categories over the stages to the fibre category over T is an equivalence.

theorem isLimitPreserving_twoFibreProduct
    (h𝒳 : Deformation.Artin.IsLimitPreserving.{u, v, w, u + 1, u} B S hS 𝒳)
    (h𝒴 : Deformation.Artin.IsLimitPreserving.{u, v, w, u + 1, u} B S hS 𝒴)
    (h𝒵 : Deformation.Artin.IsLimitPreserving.{u, v, w, u + 1, u} B S hS 𝒵) :
    Deformation.Artin.IsLimitPreserving.{u, v, w, u + 1, u} B S hS
      (BigFppfOver.twoFibreProduct.{u, u, u + 1} B S hS 𝒳 𝒴 𝒵 pf qf)

AlgebraicGeometry.Stack.isLimitPreservingOnObjects_toTerminalCFG_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingTwoFibreProductObjects.lean, line 435. The attribute's comment: “part (1)”.

Stacks 07XM, part (1). If the structure morphisms of 𝒳 and of 𝒵 to (Sch/S)_{fppf} are limit preserving on objects and 𝒴 is limit preserving, then the structure morphism of the 2-fibre product 𝒳 ×_𝒴 𝒵 to (Sch/S)_{fppf} is limit preserving on objects.

Part (2) of Stacks 07XM, that 𝒳 ×_𝒴 𝒵 is limit preserving when 𝒳, 𝒴 and 𝒵 are, is AlgebraicGeometry.Stack.isLimitPreserving_twoFibreProduct.

theorem isLimitPreservingOnObjects_toTerminalCFG_twoFibreProduct
    (h𝒳 : BigFppfOver.IsLimitPreservingOnObjects.{u, v, w, u, u + 1} B S hS 𝒳
      (terminalCFG B S hS) (Bicategory.InducedBicategory.mkHom (toTerminalCFG B S hS 𝒳)))
    (h𝒵 : BigFppfOver.IsLimitPreservingOnObjects.{u, v, w, u, u + 1} B S hS 𝒵
      (terminalCFG B S hS) (Bicategory.InducedBicategory.mkHom (toTerminalCFG B S hS 𝒵)))
    (h𝒴 : Deformation.Artin.IsLimitPreserving.{u, v, w, u + 1, u} B S hS 𝒴) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, v, w, u, u + 1} B S hS
      (BigFppfOver.twoFibreProduct.{u, u, u + 1} B S hS 𝒳 𝒴 𝒵 pf qf) (terminalCFG B S hS)
      (Bicategory.InducedBicategory.mkHom (toTerminalCFG B S hS
        (BigFppfOver.twoFibreProduct.{u, u, u + 1} B S hS 𝒳 𝒴 𝒵 pf qf)))
Tag 07XN, a lemma

Tag 07XN in the Stacks Project.

AlgebraicGeometry.Stack.isStackInSetoids_and_isLimitPreservingOnObjects_of_isRepresentableBySpaceLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingSetoidRepresentable.lean, line 206. The attribute's comment: “the implication (3) ⟹ (1), with condition (3) read as IsRepresentableBySpaceLocallyOfFinitePresentation and limit preservation on objects for cofiltered index categories in the universe of the schemes, which is the scope of the library's form of Tag 06CX that the proof uses”.

Stacks 07XN, the implication (3) ⟹ (1). A category fibred in groupoids over the big fppf site of S which is representable by an algebraic space locally of finite presentation over S is a stack in setoids whose structure morphism to (Sch/S)_{fppf} is limit preserving on objects.

The setoid clause is the implication (3) ⟹ (1) of Stacks 04SZ, and the limit-preservation clause is Stacks 06CX read at the structure morphism. Neither algebraicity nor any cited hypothesis is used.

theorem isStackInSetoids_and_isLimitPreservingOnObjects_of_isRepresentableBySpaceLocallyOfFinitePresentation
    (h : IsRepresentableBySpaceLocallyOfFinitePresentation B S hS 𝒳) :
    𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS) ∧
      BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B S hS 𝒳
        (terminalCFG B S hS)
        (Bicategory.InducedBicategory.mkHom (toTerminalCFG B S hS 𝒳))

AlgebraicGeometry.Stack.isStackInSetoids_isLimitPreserving_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingStackInSetoids.lean, line 303.

Stacks 07XN. For an algebraic stack 𝒳 over the big fppf site of a scheme S the following are equivalent:

  1. 𝒳 is a stack in setoids and its structure morphism 𝒳 ⟶ (Sch/S)_{fppf} is limit preserving on objects in the sense of Stacks 06CU;
  2. 𝒳 is a stack in setoids and is limit preserving in the sense of Stacks 07XL;
  3. 𝒳 is representable by an algebraic space over S which is locally of finite presentation over S, i.e. AlgebraicGeometry.Stack.IsRepresentableBySpaceLocallyOfFinitePresentation.

The three implications proved are the cycle (1) ⟹ (3) ⟹ (2) ⟹ (1). Inverse systems are indexed by categories in the universe u of the schemes, which is the size the source's directed inverse systems have and the size at which the inputs of the two nontrivial implications are available.

theorem isStackInSetoids_isLimitPreserving_tfae
    (halg : IsAlgebraicStack.{u, t} B S hS 𝒳.val) :
    List.TFAE
      [𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS) ∧
          BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B S hS 𝒳
            (terminalCFG B S hS) (Bicategory.InducedBicategory.mkHom (toTerminalCFG B S hS 𝒳)),
        𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS) ∧
          Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u} B S hS 𝒳,
        IsRepresentableBySpaceLocallyOfFinitePresentation B S hS 𝒳]

AlgebraicGeometry.Stack.isStackInSetoids_and_isLimitPreservingOnObjects_of_isLimitPreserving, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LimitPreservingStructureMorphism.lean, line 216. The attribute's comment: “the implication (2) ⟹ (1)”.

Stacks 07XN, the implication (2) ⟹ (1). A category fibred in groupoids over the big fppf site of S which is a stack in setoids and is limit preserving is a stack in setoids whose structure morphism to (Sch/S)_{fppf} is limit preserving on objects.

The stack-in-setoids clause is common to the two conditions, and the limit-preservation clause weakens from an equivalence of categories to essential surjectivity. The remaining implications of Stacks 07XN are not proved here; see the implementation notes of this module.

theorem isStackInSetoids_and_isLimitPreservingOnObjects_of_isLimitPreserving
    (h : 𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS) ∧
      Deformation.Artin.IsLimitPreserving.{u, v, w, u + 1, u} B S hS 𝒳) :
    𝒳.val.p.IsStackInSetoids (BigFppfOver.topology B S hS) ∧
      BigFppfOver.IsLimitPreservingOnObjects.{u, v, w, u, u + 1} B S hS 𝒳
        (terminalCFG B S hS)
        (Bicategory.InducedBicategory.mkHom (toTerminalCFG B S hS 𝒳))
Tag 0CXI, a lemma

Tag 0CXI in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyOfFiniteType_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/DiagonalLocallyOfFiniteType.lean, line 239.

Stacks 0CXI. Let 𝒳 be a category fibred in groupoids over the big fppf site of a scheme S whose diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 is representable by algebraic spaces. If 𝒳 is limit preserving then Δ is locally of finite type.

The base change of Δ along a scheme-valued point of 𝒳 × 𝒳 over U is the presheaf of vertical morphisms between the two components of that point, so a section of the representing algebraic space over an affine inverse limit is a vertical morphism there, and limit preservation of 𝒳 makes it the restriction of one at a finite stage. The surjectivity criterion of Stacks 0CM6 turns that into local finite presentation of the representing space over U, and Stacks 0464 into local finite type.

theorem isLocallyOfFiniteType_diagonal
    (hΔ : IsRepresentableByAlgebraicSpaces B S hS (diagonal.{u, u, u + 1} B S hS 𝒳).hom)
    (h𝒳 : Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u} B S hS 𝒳) :
    HasRelativeProperty.{u, u, u + 1, u} B S hS (Space.locallyOfFiniteTypeProperty B S hS)
      (diagonal.{u, u, u + 1} B S hS 𝒳) hΔ
Sources
LeanDeformation.Artin.IsLimitPreserving · AlgebraicGeometry.Stack.isLimitPreserving_twoFibreProduct · AlgebraicGeometry.Stack.isLimitPreservingOnObjects_toTerminalCFG_twoFibreProduct · AlgebraicGeometry.Stack.isStackInSetoids_and_isLimitPreservingOnObjects_of_isRepresentableBySpaceLocallyOfFinitePresentation · AlgebraicGeometry.Stack.isStackInSetoids_isLimitPreserving_tfae · AlgebraicGeometry.Stack.isStackInSetoids_and_isLimitPreservingOnObjects_of_isLimitPreserving · AlgebraicGeometry.Stack.isLocallyOfFiniteType_diagonal

Section98.12 Versality#

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

Tag 0CXJ, a definition

Tag 0CXJ in the Stacks Project.

Deformation.Artin.FormalObject.IsVersal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/Versal.lean, line 124.

A formal object ξ of a category fibred in groupoids over the big fppf site of S is versal, relative to a ring Λ through which the structure morphism of its complete local base factors, when the formal object of the predeformation category of its closed fibre determined by ξ is versal.

def FormalObject.IsVersal (hp : p.IsFiberedInGroupoids) (ξ : FormalObject B S hS p)
    (Λ : Type u) [CommRing Λ] [Algebra Λ ξ.base.R] (iΛ : Spec (.of Λ) ⟶ S)
    (hR : Spec.map (CommRingCat.ofHom (algebraMap Λ ξ.base.R)) ≫ iΛ = ξ.base.toS) : Prop
Tag 07XE, an equation

Tag 07XE in the Stacks Project.

Deformation.Artin.hatX, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality.lean, line 214.

The map \hat x : 𝓕_{(Sch/U)_{fppf},k,u₀} ⟶ 𝓕_{𝓧,k,x₀} over 𝒞_Λ, for the 2-Yoneda functor associated to the given object over U.

public noncomputable def hatX
    (x : X) (hx : q.obj x = U) (_ : q.IsFiberedInGroupoids) :
    HatXConstruction iΛ U q u₀ hu₀ x hx
Tag 07XF, a definition

Tag 07XF in the Stacks Project.

Deformation.Artin.IsVersalAt, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality.lean, line 108.

An object x over U is versal at u₀ if the induced map of predeformation categories is smooth: for a surjection B ⟶ A of Artinian local algebras, an arrow y ⟶ z over Spec A ⟶ Spec B and an arrow y ⟶ x restricting to u₀ extend to an arrow z ⟶ x making the triangle commute.

public noncomputable abbrev IsVersalAt
    (u₀ : U.left) (x : X) (hx : q.obj x = U) : Prop
Tag 0CXK, a lemma

Tag 0CXK in the Stacks Project.

Deformation.Artin.isVersalAt_iff_isVersal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/FormalObjectVersal/VersalityCriterion.lean, line 293.

With the notation of Stacks 07XF, let R be the completed local ring of U at a finite type point u₀, presented by a ring equivalence e, and let ξ be the formal object attached by the approximation functor of Stacks 07X6 to a Cartesian restriction x_R of x over Spec R. Then x is versal at u₀ exactly when ξ is versal in the sense of Stacks 0CXJ.

public theorem isVersalAt_iff_isVersal
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : Type v} [Category.{w} F]
    (p : F ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids)
    (U : Over S) (x : F)
    (hx : (p ⋙ Over.post B.inclusion).obj x = U)
    (u₀ : U.left)
    [IsLocallyNoetherian S] [LocallyOfFiniteType U.hom]
    (_hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀)
    (xR : Deformation.Artin.CompleteLocalObjects B S hS p)
    (ξ : Deformation.Artin.FormalObject B S hS p)
    (hξ : ξ = (Deformation.Artin.approximationFunctor B S hS p hp).obj xR)
    (e : AlgebraicGeometry.Scheme.completedLocalRing U.left u₀ ≃+* ξ.base.R)
    (g : Spec (.of ξ.base.R) ⟶ U.left)
    (hg : g = Spec.map (CommRingCat.ofHom e.toRingHom) ≫
      Spec.map (CommRingCat.ofHom
        (algebraMap (U.left.presheaf.stalk u₀)
          (AlgebraicGeometry.Scheme.completedLocalRing U.left u₀))) ≫
      U.left.fromSpecStalk u₀)
    (hbase : ξ.base.toS = g ≫ U.hom)
    (r : xR.obj.1 ⟶ x)
    (_hr : p.IsCartesian (p.map r) r)
    (hrbase : HEq
      ((eqToHom (Deformation.Artin.chosenBase_eq B S hS p xR.obj).symm ≫
        p.map r).left.hom ≫ eqToHom (congrArg Over.left hx)) g)
    (Λ : Type u) [CommRing Λ] [Algebra Λ ξ.base.R]
    (hΛstalk : CommRingCat.of Λ = S.presheaf.stalk (Deformation.Artin.basePoint U u₀))
    (iΛ : Spec (.of Λ) ⟶ S)
    (hiΛ : HEq iΛ (S.fromSpecStalk (Deformation.Artin.basePoint U u₀)))
    (hΛ : Spec.map (CommRingCat.ofHom (algebraMap Λ ξ.base.R)) ≫ iΛ =
      ξ.base.toS) :
    Deformation.Artin.IsVersalAt U (p ⋙ Over.post B.inclusion) u₀ x hx ↔
      Deformation.Artin.FormalObject.IsVersal B S hS p hp ξ Λ iΛ hΛ
Tag 0CXL, a lemma

Tag 0CXL in the Stacks Project.

Deformation.Artin.smoothAt_iff_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ArtinCriteria/Versality.lean, line 214.

Smoothness at a finite-type point is equivalent to versality of the corresponding object of the slice fibred over schemes over S.

public theorem smoothAt_iff_isVersalAt
    {U V S : Scheme.{u}} (f : U ⟶ V) (g : V ⟶ S)
    [IsLocallyNoetherian S] [LocallyOfFiniteType (f ≫ g)]
    [LocallyOfFiniteType g] (u₀ : U)
    (hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀) :
    InfinitesimalLifting.SmoothAt f u₀ ↔
      Deformation.Artin.IsVersalAt (Over.mk (f ≫ g))
        (Over.forget (Over.mk g)) u₀
        (Over.mk (Over.homMk f (by simp))) rfl
Tag 07XG, a lemma

Tag 07XG in the Stacks Project.

Deformation.Artin.isSmooth_mapPredeformationCategory_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/FiniteResidueFieldExtension/Smoothness.lean, line 1235.

Stacks 07XG. Let 𝒳 be a category fibred in groupoids over the big fppf site of a locally Noetherian scheme S, let x be an object of 𝒳 over a scheme U locally of finite type over S, and let u₀ be a finite type point of U. Let l be a finite extension of κ(u₀) and let u_{l,0} : Spec l ⟶ U be the induced l-valued point of U. If 𝒳 satisfies (RS) and x is versal at u₀, then the morphism of predeformation categories 𝓕_{(Sch/U)_fppf, l, u_{l,0}} ⟶ 𝓕_{𝒳, l, x_{l,0}} is smooth.

public theorem isSmooth_mapPredeformationCategory_of_isVersalAt
    [IsLocallyNoetherian S] (hp : p.IsFiberedInGroupoids)
    (hU : LocallyOfFiniteType ((p ⋙ Over.post B.inclusion).obj x).hom)
    (u₀ : ((p ⋙ Over.post B.inclusion).obj x).left)
    (hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀)
    [Algebra (((p ⋙ Over.post B.inclusion).obj x).left.residueField u₀) l]
    [Module.Finite (((p ⋙ Over.post B.inclusion).obj x).left.residueField u₀) l]
    (hfieldPoint : fieldPointMap B S hS p x iΛ uₗ₀ huₗ₀ =
      Spec.map (CommRingCat.ofHom (algebraMap
          (((p ⋙ Over.post B.inclusion).obj x).left.residueField u₀) l)) ≫
        ((p ⋙ Over.post B.inclusion).obj x).left.fromSpecResidueField u₀)
    (hversal : IsVersalAt ((p ⋙ Over.post B.inclusion).obj x)
      (p ⋙ Over.post B.inclusion) u₀ x rfl)
    (hRS : SatisfiesRS B S hS p hp) :
  letI : p.IsFibered := hp.isFibered
  Deformation.IsSmooth
    (mapPredeformationCategory iΛ
      (Over.forget (p.obj x) ⋙ Over.post B.inclusion)
      (p ⋙ Over.post B.inclusion)
      (p.chosenPullbacks.sliceFunctor (⟨x, rfl⟩ : p.Fiber (p.obj x)))
      (sliceFunctor_comp_post B S hS p p.chosenPullbacks x) uₗ₀ huₗ₀).toBasedFunctor
Tag 0CXM, a lemma

Tag 0CXM in the Stacks Project.

Deformation.Artin.BaseChange.isSmoothAt_baseChange_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ArtinCriteria/VersalBaseChange/Smoothness.lean, line 268.

Stacks 0CXM. Let 𝒳 be a category fibred in groupoids over the big fppf site of a locally Noetherian scheme S, let x be an object of 𝒳 over a scheme U locally of finite type over S, and let u₀ be a finite type point of U. Assume the diagonal of 𝒳 is representable by algebraic spaces and locally of finite type, and that 𝒳 satisfies (RS). Let V be a scheme locally of finite type over S, let y be an object of 𝒳 over V, let F be the algebraic space representing the 2-fibre product 𝒵 = (Sch/V)_{fppf} ×_𝒳 (Sch/U)_{fppf} over V, and let z₀ be a finite type point of F lying over u₀. If x is versal at u₀, then F ⟶ V is smooth at z₀.

public theorem isSmoothAt_baseChange_of_isVersalAt
    [IsLocallyNoetherian S]
    (hΔ : AlgebraicGeometry.Stack.HasRepresentableDiagonal B S hS 𝒳)
    (hΔlft :
      letI : 𝒳.val.p.IsFibered := 𝒳.isFiberedInGroupoids.isFibered
      ∀ (T : AlgebraicGeometry.BigFppfOver B S hS)
        (a b : 𝒳.val.p.Fiber T)
        (G : (AlgebraicGeometry.BigFppfOver B T.left.1 T.left.2)ᵒᵖ ⥤ Type u),
        AlgebraicGeometry.IsAlgebraicSpace B T.left.1 T.left.2 G →
        Nonempty (G ⋙ uliftFunctor.{v, u} ≅
          ((Over.iteratedSliceBackward T).op ⋙ 𝒳.val.p.isomPresheaf a b) ⋙
            uliftFunctor.{u, v}) →
        AlgebraicGeometry.Space.IsLocallyOfFiniteType B T.left.1 T.left.2
          (terminal.from G : G ⟶
            ⊤_ ((AlgebraicGeometry.BigFppfOver B T.left.1 T.left.2)ᵒᵖ ⥤ Type u)))
    (hRS : Deformation.Artin.SatisfiesRS B S hS 𝒳.val.p
      𝒳.isFiberedInGroupoids)
    (U V : AlgebraicGeometry.BigFppfOver B S hS)
    [LocallyOfFiniteType (B.inclusion.map U.hom)]
    [LocallyOfFiniteType (B.inclusion.map V.hom)]
    (x : 𝒳.val.obj) (hx : 𝒳.val.p.obj x = U)
    (u₀ : U.left.1)
    (hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀)
    (y : AlgebraicGeometry.BigFppfOver B V.left.1 V.left.2 ⥤ 𝒳.val.obj)
    (hy : y ⋙ 𝒳.val.p = Over.map V.hom)
    (F : (AlgebraicGeometry.BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u)
    (hF : AlgebraicGeometry.IsAlgebraicSpace B V.left.1 V.left.2 F)
    (e : BaseChangeEquivalence B S hS 𝒳 U V x hx y F)
    (z₀ : AlgebraicGeometry.Space.FieldValuedPoint B V.left.1 V.left.2 F)
    (hz₀ : AlgebraicGeometry.Space.IsFiniteTypePoint B V.left.1 V.left.2 F
      (z₀.class B V.left.1 V.left.2 F))
    (hzu :
      letI : Category (TwoFibreProductOver (Over.map V.hom)
        (Over.forget U) 𝒳.val.p y
        (Functor.TwoYoneda.liftBased 𝒳.val.p
          𝒳.isFiberedInGroupoids U ⟨x, hx⟩).toFunctor) :=
            TwoFibreProductOver.instCategory
      let P := e.inv.functor.obj ⟨z₀.siteObject, Discrete.mk z₀.value⟩
      ∃ hP : P.x = z₀.siteObject,
        (B.inclusion.map
          ((eqToHom (P.hx.trans P.hy.symm) ≫ P.y.hom).left))
          ((B.inclusion.map (eqToHom (congrArg Over.left hP).symm))
            (IsLocalRing.closedPoint z₀.carrier)) = u₀)
    (hversal : Deformation.Artin.IsVersalAt (Over.mk (B.inclusion.map U.hom))
      (𝒳.val.p ⋙ Over.post B.inclusion) u₀ x
      (by simpa using congrArg (Over.post B.inclusion).obj hx)) :
    AlgebraicGeometry.Space.IsSmoothAt B V.left.1 V.left.2
      (terminal.from F : F ⟶
        ⊤_ ((AlgebraicGeometry.BigFppfOver B V.left.1 V.left.2)ᵒᵖ ⥤ Type u))
      (z₀.class B V.left.1 V.left.2 F)
Tag 07XH, a lemma

Tag 07XH in the Stacks Project.

Deformation.Artin.exists_finiteType_versal_approximation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/FormalObjectApproximation/StalkBaseVersality.lean, line 905. The attribute's comment: “the whole statement, unconditionally: Stacks 07QZ — Artin approximation over a G-ring — is proved in this library, so the Stacks 07XB that this uses is itself unconditional”.

An effective versal formal object over a locally Noetherian base whose local ring at the image point is a G-ring is the system of infinitesimal restrictions of an object over a finite-type neighbourhood, versal at a finite type point with the same residue field.

public theorem exists_finiteType_versal_approximation
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S]
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1}
      (AlgebraicGeometry.BigFppfOver B S hS))
    (ξ : Deformation.Artin.FormalObject B S hS 𝒳.val.p)
    (heffective : Deformation.Artin.FormalObject.IsEffective B S hS 𝒳.val.p
      𝒳.property ξ)
    (s : S) (hs : ξ.base.toS (closedPoint ξ.base.R) = s)
    (hG : IsGRing (S.presheaf.stalk s))
    (hlimit : AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B S hS 𝒳
      (baseFiberedCategory B S hS)
      (structureMorphism B S hS 𝒳))
    [Algebra (S.presheaf.stalk s : Type u) ξ.base.R]
    (iΛ : Spec (.of (S.presheaf.stalk s : Type u)) ⟶ S)
    (hiΛ : iΛ = S.fromSpecStalk s)
    (hΛ : Spec.map (CommRingCat.ofHom
        (algebraMap (S.presheaf.stalk s : Type u) ξ.base.R)) ≫ iΛ = ξ.base.toS)
    (hversal : Deformation.Artin.FormalObject.IsVersal B S hS 𝒳.val.p 𝒳.property
      ξ (S.presheaf.stalk s : Type u) iΛ hΛ) :
    ∃ (U : Over S) (u₀ : U.left)
      (V : AlgebraicGeometry.BigFppfOver B S hS)
      (_ : (Over.post B.inclusion).obj V = U)
      (x : 𝒳.val.p.Fiber V)
      (hx : (𝒳.val.p ⋙ Over.post B.inclusion).obj x.1 = U),
      LocallyOfFiniteType U.hom ∧ QuasiCompact U.hom ∧
      AlgebraicGeometry.IsFiniteTypePoint u₀ ∧
      (letI : CommRing ξ.base.R := ξ.base.commRing
       letI : IsLocalRing ξ.base.R := ξ.base.localRing
       Nonempty (U.left.residueField u₀ ≃+* ResidueField ξ.base.R)) ∧
      Deformation.Artin.IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u₀ x.1 hx ∧
      ∃ (xR : Deformation.Artin.CompleteLocalObjects B S hS 𝒳.val.p)
        (e : ξ ≅ (Deformation.Artin.approximationFunctor B S hS 𝒳.val.p
          𝒳.property).obj xR)
        (r : xR.obj.1 ⟶ x.1)
        (eR : AlgebraicGeometry.Scheme.completedLocalRing U.left u₀ ≃+*
          (Deformation.Artin.chosenBase B S hS 𝒳.val.p xR.obj).R),
        𝒳.val.p.IsCartesian (𝒳.val.p.map r) r ∧
        ((eqToHom (Deformation.Artin.chosenBase_eq B S hS 𝒳.val.p xR.obj).symm ≫
            𝒳.val.p.map r).left.hom ≫ eqToHom (congrArg Over.left hx)) =
          (Spec.map (CommRingCat.ofHom
            eR.toRingHom) ≫
            Spec.map (CommRingCat.ofHom
              (algebraMap (U.left.presheaf.stalk u₀)
                (AlgebraicGeometry.Scheme.completedLocalRing U.left u₀))) ≫
            U.left.fromSpecStalk u₀)
Tag 07XI, an example

Tag 07XI in the Stacks Project.

Deformation.Artin.GRingCounterexample.stack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingCounterexample.lean, line 210. The attribute's comment: “the Example's construction: the functor F on the big fppf site of S = Spec(Λ), which is a one-point set on a T whose structure morphism factors through S' = (S ∖ {𝔪}) ⨿ Spec(C) and empty otherwise, and the category 𝒳 = 𝒮_F fibred in sets that it defines. The source's three assertions about them are Deformation.Artin.GRingCounterexample.isLimitPreservingOnObjects_stack, Deformation.Artin.GRingCounterexample.isEffective_formalObject and Deformation.Artin.GRingCounterexample.isVersal_formalObject, about the formal object Deformation.Artin.GRingCounterexample.formalObject; the Example whole -- those assertions together with the Example's conditional conclusion, which assumes the conclusion of Stacks 07XH for these 𝒳 rather than any G-ring property -- is Deformation.Artin.GRingCounterexample.exists_algHom_henselian.”.

The category 𝒳 = 𝒮_F fibred in groupoids over the big fppf site of S, built from the functor F via the Grothendieck construction of Stacks 0458.

public def stack (m : Ideal Λ) [m.IsMaximal] (C : Type u) [CommRing C] (φ : Λ →+* C)
    (B : AlgebraicGeometry.BigFppfSite.{u}) (hS : B.Contains (Spec (.of Λ))) :
    CategoryTheory.CatFiberedInGroupoids (BigFppfOver B (Spec (.of Λ)) hS)

Deformation.Artin.GRingCounterexample.formalObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingCounterexample.lean, line 367. The attribute's comment: “the formal object ξ over R = Λ_𝔪^∧ whose existence the Example asserts: the complete local base R over S = Spec(Λ), the level of ξ at each infinitesimal neighbourhood of the closed point of Spec(R), and the transitions. That ξ is effective (Deformation.Artin.FormalObject.IsEffective, Stacks 07X7) is Deformation.Artin.GRingCounterexample.isEffective_formalObject, and that it is versal (Deformation.Artin.FormalObject.IsVersal, Stacks 0CXJ) is Deformation.Artin.GRingCounterexample.isVersal_formalObject. The Example whole -- the three assertions together with the Example's conditional conclusion, which assumes the conclusion of Stacks 07XH for these 𝒳 rather than any G-ring property -- is Deformation.Artin.GRingCounterexample.exists_algHom_henselian.”.

The formal object ξ over R = Λ_𝔪^∧ of the Example. Each level is the unique point of F(Spec(R/𝔪_R^{n+1})), which is nonempty because the Example's factorization Λ → C → R makes every infinitesimal neighbourhood of the closed point map to Spec(C), and the transitions are the unique morphisms of 𝒳 = 𝒮_F lying over the closed immersions Spec(R/𝔪_R^{n+1}) ↪ Spec(R/𝔪_R^{n+2}), the fibres of 𝒮_F being discrete and F taking only subsingleton values.

public def formalObject (ψ : C →+* completion m)
    (hψ : ψ.comp φ = algebraMap Λ (completion m))
    (hR : B.Contains (Spec (.of (completion m)))) :
    Deformation.Artin.FormalObject B (Spec (.of Λ)) hS (stack m C φ B hS).val.p

Deformation.Artin.GRingCounterexample.isLimitPreservingOnObjects_stack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingCounterexample.lean, line 481. The attribute's comment: “the Example's assertion that 𝒳 = 𝒮_F ⟶ (Sch/S)_{fppf} is limit preserving on objects. The construction of F and 𝒳 is Deformation.Artin.GRingCounterexample.stack, and the other two assertions, about the formal object ξ over R = Λ_𝔪^∧, are Deformation.Artin.GRingCounterexample.isEffective_formalObject and Deformation.Artin.GRingCounterexample.isVersal_formalObject. The Example whole is Deformation.Artin.GRingCounterexample.exists_algHom_henselian.”.

𝒳 = 𝒮_F is limit preserving on objects, the first of the Example's three assertions about 𝒳.

public theorem isLimitPreservingOnObjects_stack [IsNoetherianRing Λ]
    (hφ : RingHom.FiniteType φ) :
    AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1}
      B (Spec (.of Λ)) hS (stack m C φ B hS)
      (Deformation.Artin.Approximation.baseFiberedCategory B (Spec (.of Λ)) hS)
      (Deformation.Artin.Approximation.structureMorphism B (Spec (.of Λ)) hS
        (stack m C φ B hS))

Deformation.Artin.GRingCounterexample.isEffective_formalObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingCounterexampleEffective.lean, line 116. The attribute's comment: “the Example's assertion that the formal object ξ over R = Λ_𝔪^∧ is effective. The construction of F, 𝒳 = 𝒮_F and ξ is in StacksFrontier.Deformation.Artin.Versality.GRingCounterexample, limit preservation on objects is Deformation.Artin.GRingCounterexample.isLimitPreservingOnObjects_stack, and versality is Deformation.Artin.GRingCounterexample.isVersal_formalObject. The Example whole -- these three assertions together with the Example's conditional conclusion, which assumes the conclusion of Stacks 07XH for these 𝒳 rather than any G-ring property -- is Deformation.Artin.GRingCounterexample.exists_algHom_henselian. NOT covered, and formalized nowhere: the Example's closing step from solvability in the henselization to Λ_𝔪^h and Λ_𝔪 being G-rings, which the Stacks Project itself defers ("insert future reference here"), so there is no statement to formalize against.”.

The formal object ξ over R = Λ_𝔪^∧ is effective, the first of the Example's two assertions about ξ.

public theorem isEffective_formalObject :
    Deformation.Artin.FormalObject.IsEffective B (Spec (.of Λ)) hS (stack m C φ B hS).val.p
      ((stack m C φ B hS).isFiberedInGroupoids) (formalObject m C φ B hS ψ hψ hR)

Deformation.Artin.GRingCounterexample.isVersal_formalObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingCounterexampleVersal.lean, line 75. The attribute's comment: “the Example's assertion that the formal object ξ over R = Λ_𝔪^∧ is versal, relative to Λ_𝔪, through which the structure morphism of R factors. The construction of F, 𝒳 = 𝒮_F and ξ is in StacksFrontier.Deformation.Artin.Versality.GRingCounterexample, limit preservation on objects is Deformation.Artin.GRingCounterexample.isLimitPreservingOnObjects_stack, and effectivity is Deformation.Artin.GRingCounterexample.isEffective_formalObject. Versality relative to the local ring of S at 𝔪, which is the form Stacks 07XH consumes, is Deformation.Artin.GRingCounterexample.isVersal_formalObject_stalk, and the Example whole is Deformation.Artin.GRingCounterexample.exists_algHom_henselian. NOT covered, and formalized nowhere: the Example's closing step from solvability in the henselization to Λ_𝔪^h and Λ_𝔪 being G-rings, which the Stacks Project itself defers ("insert future reference here"), so there is no statement to formalize against.”.

The formal object ξ over R = Λ_𝔪^∧ is versal, the last of the Example's three assertions about 𝒳 = 𝒮_F. Versality is relative to Λ_𝔪, through which the structure morphism of R factors by Deformation.Artin.GRingCounterexample.base_toS_eq.

public theorem isVersal_formalObject :
    Deformation.Artin.FormalObject.IsVersal B (Spec (.of Λ)) hS (stack m C φ B hS).val.p
      ((stack m C φ B hS).isFiberedInGroupoids) (formalObject m C φ B hS ψ hψ hR)
      (Localization.AtPrime m) (localChart m) (base_toS_eq m C φ B hS ψ hψ hR)

Deformation.Artin.GRingCounterexample.exists_algHom_henselian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingExample.lean, line 844. The attribute's comment: “the Example whole, in the Example's own logical direction: the functor F on the big fppf site of S = Spec(Λ) (Deformation.Artin.GRingCounterexample.functor, whose displayed defining property -- a one-point set on a T whose structure morphism factors through S' = (S ∖ {𝔪}) ⨿ Spec(C), empty otherwise -- is the first conjunct below), the category 𝒳 = 𝒮_F fibred in sets it defines (Deformation.Artin.GRingCounterexample.stack), the formal object ξ over R = Λ_𝔪^∧ (Deformation.Artin.GRingCounterexample.formalObject), the source's three assertions about them -- limit preservation on objects, effectivity and versality of ξ -- and the Example's conditional conclusion: IF the conclusion of Stacks 07XH holds for all these 𝒳, i.e. if every finite type factorization Λ → C' → R carries the three-item datum the Example reads off it (Deformation.Artin.AlgebraizesFiniteTypeFactorizations: a finite type Λ-algebra A, a maximal ideal 𝔪_A over 𝔪 with κ(𝔪) = κ(𝔪_A) and condition (4) of Stacks 02HT, and a Λ-algebra map C' → A), THEN C maps over Λ to every henselian local Λ-algebra whose maximal ideal contracts to 𝔪 and every polynomial system over Λ with a solution in R has a solution in a henselization of Λ_𝔪 -- the approximation property for Λ_𝔪^h, which is the source's closing sentence. The G-ring property is NOT hypothesised anywhere here: in the Example it is the conclusion drawn from that approximation property (\"In this example we show that the local ring O_{S, s} has to be a G-ring in order for the result of Lemma 07XH to be true\"), and the conclusion of 07XH is assumed, in the antecedent, rather than derived from a G-ring assumption. NOT covered: the source's final step, from the approximation property of Λ_𝔪^h to Λ_𝔪^h and then Λ_𝔪 being G-rings, which the Stacks Project itself defers (\"insert future reference here\"), so there is no statement to formalize against.”.

Let Λ be a Noetherian ring, let 𝔪 ⊂ Λ be a maximal ideal, let R = Λ_𝔪^∧, and let Λ → C → R be a factorization with C of finite type over Λ. Set S = Spec(Λ), U = S ∖ {𝔪} and S' = U ⨿ Spec(C), and let F, 𝒳 = 𝒮_F and ξ be the functor on the big fppf site of S, the category fibred in sets it defines, and the formal object over R that the Example builds from that factorization. Then

  • F is the functor the Example displays: its value at T is a subsingleton, and it is nonempty exactly when the structure morphism of T factors through S',
  • 𝒳 → (Sch/S)_{fppf} is limit preserving on objects,
  • ξ is effective,
  • ξ is versal, relative to 𝒪_{S, 𝔪}, and
  • if the conclusion of Stacks 07XH holds for all of these 𝒳 -- that is, if every factorization Λ → C' → R with C' of finite type over Λ carries the three-item datum Deformation.Artin.AlgebraizesFiniteTypeFactorizations that the Example reads off that conclusion, namely a finite type Λ-algebra A with a maximal ideal 𝔪_A over 𝔪 such that κ(𝔪) = κ(𝔪_A), such that Λ → A satisfies condition (4) of Stacks 02HT at 𝔪_A -- hence is smooth there -- and such that C' maps to A over Λ -- then C maps to every henselian local Λ-algebra H whose maximal ideal contracts to 𝔪 by a Λ-algebra map, and every finite system of polynomial equations over Λ with a solution in R has a solution in a henselization of Λ_𝔪.

No G-ring hypothesis is made, and the conclusion of Stacks 07XH is assumed rather than used: it enters only as the antecedent of the last clause.

public theorem exists_algHom_henselian (hφ : RingHom.FiniteType φ) :
    (∀ T : (AlgebraicGeometry.BigFppfOver B (Spec (CommRingCat.of Λ)) hS)ᵒᵖ,
        Subsingleton ((functor m C φ B hS).obj T) ∧
          (Nonempty ((functor m C φ B hS).obj T) ↔ Factors m C φ B hS T.unop)) ∧
      AlgebraicGeometry.BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B
        (Spec (CommRingCat.of Λ)) hS (stack m C φ B hS)
        (Deformation.Artin.Approximation.baseFiberedCategory B (Spec (CommRingCat.of Λ)) hS)
        (Deformation.Artin.Approximation.structureMorphism B (Spec (CommRingCat.of Λ)) hS
          (stack m C φ B hS)) ∧
      Deformation.Artin.FormalObject.IsEffective B (Spec (CommRingCat.of Λ)) hS
        (stack m C φ B hS).val.p ((stack m C φ B hS).isFiberedInGroupoids)
        (formalObject m C φ B hS ψ hψ hR) ∧
      (@Deformation.Artin.FormalObject.IsVersal B (Spec (CommRingCat.of Λ)) hS _ _
        (stack m C φ B hS).val.p ((stack m C φ B hS).isFiberedInGroupoids)
        (formalObject m C φ B hS ψ hψ hR) (stalkPoint m) _
        (algebra_formalObject_base_stalk m C φ B hS ψ hψ hR)
        ((Spec (CommRingCat.of Λ)).fromSpecStalk (point m))
        (base_toS_eq_stalk m C φ B hS ψ hψ hR)) ∧
      (Deformation.Artin.AlgebraizesFiniteTypeFactorizations Λ m (completion m) →
        (∀ (H : Type u) [CommRing H] [HenselianLocalRing H] [Algebra Λ H],
            m = (maximalIdeal H).comap (algebraMap Λ H) →
            ∃ χ : C →+* H, χ.comp φ = algebraMap Λ H) ∧
          ∀ (H : Type u) [CommRing H] [IsLocalRing H] [Algebra Λ H]
              [Algebra (Localization.AtPrime m) H]
              [IsScalarTower Λ (Localization.AtPrime m) H]
              [IsHenselization (Localization.AtPrime m)
                (ResidueField (Localization.AtPrime m)) H]
              (n k : ℕ) (f : Fin k → MvPolynomial (Fin n) Λ) (a : Fin n → completion m),
            (∀ j, MvPolynomial.aeval a (f j) = 0) →
              ∃ b : Fin n → H, ∀ j, MvPolynomial.aeval b (f j) = 0)

Deformation.Artin.GRingNecessity.hasApproximationProperty_and_isGRing_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingNecessity.lean, line 87. The attribute's comment: “the approximation property of the henselization Λ_𝔪^h and, by Rotthaus' theorem (the reference the source leaves missing), that Λ_𝔪^h is a G-ring”.

Stacks Example 98.12.8 (Tag 07XI), the approximation property of Λ_𝔪^h. If the conclusion of Lemma 98.12.7 holds for the categories 𝒳 = 𝒮_F and formal objects ξ of the Example, then every henselization H of Λ_𝔪 has the approximation property (a system of polynomial equations over H with a solution in the completion of H has a solution in H) and is a G-ring. The second assertion is Rotthaus' theorem, the reference missing in the source.

theorem hasApproximationProperty_and_isGRing_henselization
    (h : ∀ (C : Type u) [CommRing C] [Algebra Λ C], Algebra.FiniteType Λ C →
      ∀ φ : C →ₐ[Λ] Completion 𝔪,
        AlgebraizationConclusion B (AlgebraicGeometry.Spec (.of Λ)) hS
          (factorizationCategory 𝔪 C B hS) (formalObject 𝔪 C φ B hS))
    (H : Type u) [CommRing H] [IsLocalRing H] [Algebra Λ H] [Algebra (Localization.AtPrime 𝔪) H]
    [IsScalarTower Λ (Localization.AtPrime 𝔪) H]
    [IsHenselization (Localization.AtPrime 𝔪) (ResidueField (Localization.AtPrime 𝔪)) H] :
    HasApproximationProperty H ∧ IsGRing H

Deformation.Artin.GRingNecessity.isGRing_of_forall_algebraizationConclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingNecessity.lean, line 113. The attribute's comment: “the conclusion of the Example: if the conclusion of Lemma 98.12.7 (07XH) holds for every 𝒳 = 𝒮_F as above, then Λ_𝔪 is a G-ring; the conclusion of 07XH is AlgebraizationConclusion, copied verbatim from the formalization of 07XH”.

Stacks Example 98.12.8 (Tag 07XI). Let Λ be a Noetherian ring and 𝔪 a maximal ideal of Λ. If for every finite type Λ-algebra C and every Λ-algebra map φ : C → Λ_𝔪^∧ the conclusion of Lemma 98.12.7 (Tag 07XH) holds for the category 𝒳 = 𝒮_F fibred in sets over the big fppf site of S = Spec Λ attached to S' = (S ∖ {𝔪}) ⨿ Spec C and its effective versal formal object ξ over Λ_𝔪^∧, then Λ_𝔪 is a G-ring.

theorem isGRing_of_forall_algebraizationConclusion
    (h : ∀ (C : Type u) [CommRing C] [Algebra Λ C], Algebra.FiniteType Λ C →
      ∀ φ : C →ₐ[Λ] Completion 𝔪,
        AlgebraizationConclusion B (AlgebraicGeometry.Spec (.of Λ)) hS
          (factorizationCategory 𝔪 C B hS) (formalObject 𝔪 C φ B hS)) :
    IsGRing (Localization.AtPrime 𝔪)

Deformation.Artin.GRingNecessity.isGRing_of_forall_algebraizationLemmaHolds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingNecessity.lean, line 130. The attribute's comment: “with Lemma 98.12.7 assumed in lemma form (for every formal object of 𝒳 satisfying its hypotheses other than the G-ring hypothesis): Λ_𝔪 is a G-ring”.

Stacks Example 98.12.8 (Tag 07XI), with Lemma 98.12.7 assumed in lemma form. If for every finite type Λ-algebra C the statement of Lemma 98.12.7 (Tag 07XH) without its G-ring hypothesis holds for the category 𝒳 = 𝒮_F of the Example (AlgebraizationLemmaHolds), then Λ_𝔪 is a G-ring.

theorem isGRing_of_forall_algebraizationLemmaHolds
    (h : ∀ (C : Type u) [CommRing C] [Algebra Λ C], Algebra.FiniteType Λ C →
      AlgebraizationLemmaHolds 𝔪 B hS C) :
    IsGRing (Localization.AtPrime 𝔪)

Deformation.Artin.GRingNecessity.exists_lift_smallExtension_of_algebraizationConclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingNecessity/Datum.lean, line 147. The attribute's comment: “the datum read off the conclusion of 07XH: A of finite type, 𝔪_A over 𝔪 with κ(𝔪) = κ(𝔪_A), condition (4) of 02HT for Λ → A at 𝔪_A, and C → A”.

Stacks Example 98.12.8, from the conclusion of Stacks 07XH to the datum. Let C be a finite type Λ-algebra (as in the source; the proof does not use this) and φ : C → Λ_𝔪^∧ a Λ-algebra map. If the conclusion of Stacks Lemma 98.12.7 holds for the category 𝒳 = 𝒮_F and the formal object ξ of the Example, then there are a finite type Λ-algebra A and a maximal ideal 𝔪_A of A lying over 𝔪, with κ(𝔪) → κ(𝔪_A) bijective and Λ → A, 𝔪_A satisfying condition (4) of Stacks 02HT (the last condition of Algebra.isSmoothAt_tfae), together with a Λ-algebra map C → A.

theorem exists_lift_smallExtension_of_algebraizationConclusion [Algebra.FiniteType Λ C]
    (h : AlgebraizationConclusion B (Spec (.of Λ)) hS (factorizationCategory 𝔪 C B hS)
      (formalObject 𝔪 C φ B hS)) :
    ∃ (A : Type u) (_ : CommRing A) (_ : Algebra Λ A), Algebra.FiniteType Λ A ∧
      ∃ (mA : Ideal A) (_ : mA.IsMaximal) (hmA : 𝔪 = mA.comap (algebraMap Λ A)),
        Function.Bijective (Ideal.ResidueField.map 𝔪 mA (algebraMap Λ A) hmA) ∧
        (∀ (T₂ T₁ : Type u) [CommRing T₂] [CommRing T₁] [IsLocalRing T₂] [IsLocalRing T₁]
          [IsArtinianRing T₂] [IsArtinianRing T₁] [Algebra Λ T₂] [Algebra Λ T₁]
          (e : T₂ →ₐ[Λ] T₁), Function.Surjective e →
          IsSimpleModule T₂ (RingHom.ker (e : T₂ →+* T₁)) →
          ∀ (g : A →ₐ[Λ] T₁) (hq : (maximalIdeal T₁).comap (g : A →+* T₁) = mA),
            Function.Surjective (Ideal.ResidueField.mapₐ mA (maximalIdeal T₁) g hq.symm) →
            ∃ g' : A →ₐ[Λ] T₂, e.comp g' = g) ∧
        Nonempty (C →ₐ[Λ] A)

Deformation.Artin.GRingNecessity.isLimitPreservingOnObjects_and_formalObject_isEffective_isVersal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/GRingNecessity/Hypotheses.lean, line 60. The attribute's comment: “first assertion of the Example: 𝒳 = 𝒮_F is limit preserving on objects and has an effective, versal formal object ξ over R = Λ_𝔪^∧”.

Stacks Example 98.12.8 (Tag 07XI), the properties of 𝒳 and ξ. Let C be a finite type Λ-algebra and φ : C → Λ_𝔪^∧ a Λ-algebra map. The category 𝒳 = 𝒮_F fibred in sets over the big fppf site of S = Spec Λ is limit preserving on objects, and ξ is a formal object of 𝒳 over R = Λ_𝔪^∧ (its base is isomorphic to R over S) which is effective and versal. Versality holds over the local ring 𝒪_{S,s} of S at any point s, for every algebra structure of the base of ξ over 𝒪_{S,s} compatible with the structure morphisms, and such a structure exists at the image formalObjectPoint of the closed point of the base, where the versality hypothesis of Lemma 98.12.7 is formulated.

theorem isLimitPreservingOnObjects_and_formalObject_isEffective_isVersal
    (C : Type u) [CommRing C] [Algebra Λ C] [Algebra.FiniteType Λ C]
    (φ : C →ₐ[Λ] Completion 𝔪) :
    BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B (Spec (.of Λ)) hS
        (factorizationCategory 𝔪 C B hS)
        (Approximation.baseFiberedCategory B (Spec (.of Λ)) hS)
        (Approximation.structureMorphism B (Spec (.of Λ)) hS (factorizationCategory 𝔪 C B hS)) ∧
      IsCompletionBase 𝔪 (formalObject 𝔪 C φ B hS).base ∧
      FormalObject.IsEffective B (Spec (.of Λ)) hS (factorizationCategory 𝔪 C B hS).val.p
        (factorizationCategory 𝔪 C B hS).property (formalObject 𝔪 C φ B hS) ∧
      (∃ _ : Algebra ((Spec (.of Λ)).presheaf.stalk (formalObjectPoint 𝔪 C B hS φ) : Type u)
          (formalObject 𝔪 C φ B hS).base.R,
        Spec.map (CommRingCat.ofHom (algebraMap
            ((Spec (.of Λ)).presheaf.stalk (formalObjectPoint 𝔪 C B hS φ) : Type u)
            (formalObject 𝔪 C φ B hS).base.R)) ≫
          (Spec (.of Λ)).fromSpecStalk (formalObjectPoint 𝔪 C B hS φ) =
        (formalObject 𝔪 C φ B hS).base.toS) ∧
      ∀ (s : Spec (.of Λ))
        [Algebra ((Spec (.of Λ)).presheaf.stalk s : Type u) (formalObject 𝔪 C φ B hS).base.R]
        (iΛ : Spec (.of ((Spec (.of Λ)).presheaf.stalk s : Type u)) ⟶ Spec (.of Λ))
        (_ : iΛ = (Spec (.of Λ)).fromSpecStalk s)
        (hΛ : Spec.map (CommRingCat.ofHom (algebraMap
            ((Spec (.of Λ)).presheaf.stalk s : Type u) (formalObject 𝔪 C φ B hS).base.R)) ≫ iΛ =
          (formalObject 𝔪 C φ B hS).base.toS),
        FormalObject.IsVersal B (Spec (.of Λ)) hS (factorizationCategory 𝔪 C B hS).val.p
          (factorizationCategory 𝔪 C B hS).property (formalObject 𝔪 C φ B hS)
          ((Spec (.of Λ)).presheaf.stalk s : Type u) iΛ hΛ
Sources
LeanDeformation.Artin.FormalObject.IsVersal · Deformation.Artin.hatX · Deformation.Artin.IsVersalAt · Deformation.Artin.isVersalAt_iff_isVersal · Deformation.Artin.smoothAt_iff_isVersalAt · Deformation.Artin.isSmooth_mapPredeformationCategory_of_isVersalAt · Deformation.Artin.BaseChange.isSmoothAt_baseChange_of_isVersalAt · Deformation.Artin.exists_finiteType_versal_approximation

Section98.13 Openness of versality#

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

Tag 07XQ, a definition

Tag 07XQ in the Stacks Project.

Deformation.Artin.IsOpenVersality, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/Basic.lean, line 147. The attribute's comment: “part (1)”.

Versality of objects at finite-type points persists on an open neighbourhood.

public abbrev IsOpenVersality {S : Scheme.{u}} {X : Type vX} [Category.{wX} X]
    (q : X ⥤ Over S) (_hq : q.IsFiberedInGroupoids) : Prop

Deformation.Artin.IsOpenVersalityMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/Basic.lean, line 161. The attribute's comment: “part (2)”.

A morphism has openness of versality if its 2-fibre product with every scheme over a target object has openness of versality.

public noncomputable abbrev IsOpenVersalityMorphism {S : Scheme.{u}}
    {X : Type vX} [Category.{wX} X] {Y : Type vY} [Category.{wY} Y]
    (pX : X ⥤ Over S) (pY : Y ⥤ Over S) (F : X ⥤ Y)
    (hpX : pX.IsFiberedInGroupoids) (hpY : pY.IsFiberedInGroupoids)
    (hF : F ⋙ pY = pX) : Prop
Tag 07XR, an example

Tag 07XR in the Stacks Project.

Deformation.Artin.artinAxiomsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/Basic.lean, line 57. The attribute's comment: “functor”.

The functor which assigns a singleton to an admissible k[s,t]-algebra and the empty set to every other algebra.

public def artinAxiomsFunctor (k : Type u) [Field k] :
    CommAlgCat.{v, u} (MvPolynomial (Fin 2) k) ⥤ Type v

Deformation.Artin.artinAxiomsCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/Basic.lean, line 93. The attribute's comment: “category”.

The full subcategory of schemes over Spec k[s,t] admitting an affine open cover on which the functor of Tag 07XR has its unique value.

public abbrev artinAxiomsCategory (k : Type u) [Field k]
    (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of (MvPolynomial (Fin 2) k))))

Deformation.Artin.nonempty_artinAxiomsFunctor_iff_exists_isCompact_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/Basic.lean, line 229. The attribute's comment: “geometric_criterion”.

The functor of Tag 07XR has its unique value on A if and only if V(s,t) ⊆ Spec(A) has a quasi-compact open neighbourhood on which s vanishes.

public theorem nonempty_artinAxiomsFunctor_iff_exists_isCompact_open
    (k : Type u) [Field k]
    (A : CommAlgCat.{v, u} (MvPolynomial (Fin 2) k)) :
    Nonempty ((artinAxiomsFunctor k).obj A) ↔
      ∃ W : Set (PrimeSpectrum A),
        IsOpen W ∧ IsCompact W ∧
          PrimeSpectrum.zeroLocus
              ({algebraMap (MvPolynomial (Fin 2) k) A (MvPolynomial.X 0),
                algebraMap (MvPolynomial (Fin 2) k) A (MvPolynomial.X 1)} : Set A) ⊆ W ∧
          ∀ x ∈ W,
            algebraMap A (Localization.AtPrime x.asIdeal)
                (algebraMap (MvPolynomial (Fin 2) k) A (MvPolynomial.X 0)) = 0

Deformation.Artin.isVersalAt_sliceObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexample.lean, line 498. The attribute's comment: “the object x over U = Spec(k[s,t]/(s)) is versal at u_0 = (s,t)”.

The slice is versal at the origin.

public theorem isVersalAt_sliceObject (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of (MvPolynomial (Fin 2) k)))) :
    IsVersalAt (Over.mk (sliceImmersion k)) (artinAxiomsOver B hS) (slicePoint k)
      (sliceObject B hS) (by delta sliceObject; rfl)

Deformation.Artin.not_isVersalAt_sliceObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexample.lean, line 956. The attribute's comment: “x is versal at no other point of U”.

The slice is versal at no point other than the origin.

public theorem not_isVersalAt_sliceObject (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of (MvPolynomial (Fin 2) k))))
    (hu : (u : PrimeSpectrum (sliceRing k)) ≠ slicePoint k) :
    ¬ IsVersalAt (Over.mk (sliceImmersion k)) (artinAxiomsOver B hS) u
      (sliceObject B hS) (by delta sliceObject; rfl)

Deformation.Artin.not_isOpenVersality_artinAxiomsCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexample.lean, line 1012. The attribute's comment: “openness of versality fails for the category, hence axiom [5] fails”.

Openness of versality fails for the category of Tag 07XR, written out: the slice is versal at the origin, which is a finite-type point, but every open neighbourhood of the origin contains a closed point at which it is not versal. Axiom [5] asks openness of versality of the category and of its diagonal, so this is the failure of axiom [5].

public theorem not_isOpenVersality_artinAxiomsCategory (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (.of (MvPolynomial (Fin 2) k)))) :
    ¬ ∀ (U : Over (Spec (.of (MvPolynomial (Fin 2) k)))), LocallyOfFiniteType U.hom →
        ∀ (x : artinAxiomsCategory k B hS)
          (hx : (artinAxiomsOver B hS).obj x = U) (u₀ : ↥U.left),
          IsFiniteTypePoint u₀ →
          IsVersalAt U (artinAxiomsOver B hS) u₀ x hx →
          ∃ V : U.left.Opens, u₀ ∈ V.1 ∧
            ∀ u ∈ V.1, IsFiniteTypePoint u →
              IsVersalAt U (artinAxiomsOver B hS) u x hx

Deformation.Artin.isStackInGroupoids_artinAxiomsCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexampleAxioms.lean, line 481. The attribute's comment: “axiom [0]: the category is a stack in groupoids, for the fppf topology”.

The inclusion of the full subcategory IsArtinAxiomsObject is a stack in groupoids for the fppf topology of the big fppf site over Spec k[s,t].

public theorem isStackInGroupoids_artinAxiomsCategory :
    (ObjectProperty.ι (IsArtinAxiomsObject k B hS)).IsStackInGroupoids.{w}
      (BigFppfOver.topology B _ hS)

Deformation.Artin.satisfiesRS_artinAxiomsCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexampleAxioms.lean, line 549. The attribute's comment: “axiom [2]: the category satisfies the Rim-Schlessinger condition (RS)”.

The inclusion of the full subcategory IsArtinAxiomsObject satisfies condition (RS): for a pushout Y' = Y ⨿_X X' of finite type local Artinian schemes along a closed immersion X → X', the comparison from the fibre over Y' to the two-fibre product of the fibres over Y and X' is an equivalence.

public theorem satisfiesRS_artinAxiomsCategory :
    SatisfiesRS B _ hS (ObjectProperty.ι (IsArtinAxiomsObject k B hS))
      (isFiberedInGroupoids_artinAxiomsCategory B hS)

Deformation.Artin.isLimitPreserving_artinAxiomsCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexampleAxioms.lean, line 680. The attribute's comment: “axiom [1]: the category is limit preserving, for inverse systems indexed by a category in the universe of the schemes”.

The category fibred in groupoids artinAxiomsCFG is limit preserving: for a directed inverse system of affine schemes Tᵢ over Spec k[s,t] with limit T, the comparison colim 𝒳_{Tᵢ} ⥤ 𝒳_T is an equivalence.

public theorem isLimitPreserving_artinAxiomsCategory :
    IsLimitPreserving.{u, u, u, u + 1, u} B _ hS (artinAxiomsCFG B hS)

Deformation.Artin.finiteDimensional_tangentSpace_infinitesimalAutomorphisms_artinAxiomsCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexampleAxioms.lean, line 732. The attribute's comment: “axiom [3]: the tangent spaces and the spaces of infinitesimal automorphisms of the predeformation categories are finite dimensional”.

For every finite-type field-valued point x₀ of artinAxiomsCategory, the tangent space T𝓕_{𝒳,k,x₀} of its predeformation category is finite dimensional for its canonical vector space structure, and so is the group of infinitesimal automorphisms along every split pair A₀ → A_ε → A₀, for every vector space structure on it.

public theorem finiteDimensional_tangentSpace_infinitesimalAutomorphisms_artinAxiomsCategory
    {Λ K : Type u} [CommRing Λ] [Field K] [Algebra Λ K]
    (iΛ : Spec (.of Λ) ⟶ Spec (.of (MvPolynomial (Fin 2) k))) (x₀ : artinAxiomsCategory k B hS)
    (hx₀ : (ObjectProperty.ι (IsArtinAxiomsObject k B hS) ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ K)) ≫ iΛ))
    (hfin : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ K)) ≫ iΛ))
    (hqc : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ K)) ≫ iΛ)) :
    let D := predeformationCategory iΛ
      (ObjectProperty.ι (IsArtinAxiomsObject k B hS) ⋙ Over.post B.inclusion) x₀ hx₀
    letI := D.category
    let 𝓕 := BasedCategory.ofFunctor D.projection
    let hD : Deformation.IsDeformationCategory D.projection :=
      isDeformationCategory_predeformationCategory B _ hS _
        (isFiberedInGroupoids_artinAxiomsCategory B hS) (satisfiesRS_artinAxiomsCategory B hS)
        iΛ x₀ hx₀ hfin hqc
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses 𝓕 hD.predeformation.cofibered))) :=
      ⟨schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory 𝓕 hD⟩
    FiniteDimensional K
        (artinianTangentSpace Λ K (isomorphismClasses 𝓕 hD.predeformation.cofibered)) ∧
      ∀ {A₀ Aε : ArtinianLocalAlgCat.{u, u, u} Λ K} {z₀ : D.projection.Fiber A₀}
        {zε : D.projection.Fiber Aε} (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hge : g ≫ e = 𝟙 A₀)
        (i : z₀.1 ⟶ zε.1) (hi : D.projection.IsHomLift g i)
        [AddCommGroup ↥(infinitesimalAutomorphismsAlongSplitPair
          hD.predeformation.cofibered g e hge i hi)]
        [Module K ↥(infinitesimalAutomorphismsAlongSplitPair
          hD.predeformation.cofibered g e hge i hi)],
        FiniteDimensional K ↥(infinitesimalAutomorphismsAlongSplitPair
          hD.predeformation.cofibered g e hge i hi)

Deformation.Artin.isEquivalence_approximationFunctor_artinAxiomsCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessCounterexampleEffective.lean, line 314. The attribute's comment: “axiom [4]: the functor of Stacks 07X6 from objects over Noetherian complete local rings to formal objects is an equivalence”.

The category of the openness-of-versality example satisfies axiom [4]: the functor of Stacks 07X6, from objects over the spectra of Noetherian complete local rings to formal objects, is an equivalence.

public theorem isEquivalence_approximationFunctor_artinAxiomsCategory :
    (approximationFunctor B _ hS (ObjectProperty.ι (IsArtinAxiomsObject k B hS))
      (isFiberedInGroupoids_artinAxiomsCategory B hS)).IsEquivalence
Tag 07XS, an equation

Tag 07XS in the Stacks Project.

Deformation.Artin.IsSmoothOnPredeformationCategories, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/Basic.lean, line 110.

Smoothness of the induced map on predeformation categories at every finite-type field-valued point of the source.

public abbrev IsSmoothOnPredeformationCategories
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type v₁} [Category.{w₁} X]
    {Y : Type v₂} [Category.{w₂} Y]
    (pX : X ⥤ BigFppfOver B S hS)
    (pY : Y ⥤ BigFppfOver B S hS)
    (F : X ⥤ Y) (hF : F ⋙ pY = pX) : Prop
Tag 07XT, a lemma

Tag 07XT in the Stacks Project.

Deformation.Artin.isSmoothOnPredeformationCategories_sliceFunctor_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/SmoothnessConditionFromVersality.lean, line 63.

Stacks 07XT. Let 𝒳 be a category fibred in groupoids over the big fppf site of a locally Noetherian scheme S, let U be a scheme locally of finite type over S, and let x be an object of 𝒳 over U. If x is versal at every finite type point of U and 𝒳 satisfies (RS), then the 1-morphism x : (Sch/U)_fppf ⟶ 𝒳 satisfies the smoothness condition of Tag 07XS on predeformation categories.

public theorem isSmoothOnPredeformationCategories_sliceFunctor_of_isVersalAt
    [IsLocallyNoetherian S] (hp : p.IsFiberedInGroupoids)
    (hU : LocallyOfFiniteType ((p ⋙ Over.post B.inclusion).obj x).hom)
    (hversal : ∀ u₀ : ((p ⋙ Over.post B.inclusion).obj x).left,
      AlgebraicGeometry.IsFiniteTypePoint u₀ →
        IsVersalAt ((p ⋙ Over.post B.inclusion).obj x)
          (p ⋙ Over.post B.inclusion) u₀ x rfl)
    (hRS : SatisfiesRS B S hS p hp) :
    letI : p.IsFibered := hp.isFibered
    IsSmoothOnPredeformationCategories B S hS (Over.forget (p.obj x)) p
      (p.chosenPullbacks.sliceFunctor (⟨x, rfl⟩ : p.Fiber (p.obj x)))
      (p.chosenPullbacks.sliceFunctor_comp (⟨x, rfl⟩ : p.Fiber (p.obj x)))
Tag 07XU, a lemma

Tag 07XU in the Stacks Project.

Deformation.Artin.isSmoothOnPredeformationCategories_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/Composition.lean, line 291.

The composite of two morphisms smooth on predeformation categories is smooth on predeformation categories.

public theorem isSmoothOnPredeformationCategories_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type v₁} [Category.{w₁} X]
    {Y : Type v₂} [Category.{w₂} Y]
    {Z : Type v₃} [Category.{w₃} Z]
    (pX : X ⥤ BigFppfOver B S hS)
    (pY : Y ⥤ BigFppfOver B S hS)
    (pZ : Z ⥤ BigFppfOver B S hS)
    (F : X ⥤ Y) (G : Y ⥤ Z)
    (hF : F ⋙ pY = pX) (hG : G ⋙ pZ = pY)
    (hSmoothF : IsSmoothOnPredeformationCategories B S hS pX pY F hF)
    (hSmoothG : IsSmoothOnPredeformationCategories B S hS pY pZ G hG) :
    IsSmoothOnPredeformationCategories B S hS pX pZ (F ⋙ G)
      (by rw [Functor.assoc, hG, hF])
Tag 07XV, a lemma

Tag 07XV in the Stacks Project.

Deformation.Artin.isSmoothOnPredeformationCategories_twoFibreProductSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/Openness/BaseChange.lean, line 622.

Stacks 07XV. Smoothness on predeformation categories is stable under base change of categories fibred in groupoids: if f : 𝒳 ⟶ 𝒴 is smooth on predeformation categories, so is the projection 𝒳 ×_𝒴 𝒵 ⟶ 𝒵.

public theorem isSmoothOnPredeformationCategories_twoFibreProductSnd
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) [IsLocallyNoetherian S]
    {X : Type vX} [Category.{wX} X] {Y : Type vY} [Category.{wY} Y]
    {Z : Type vZ} [Category.{wZ} Z]
    (pX : X ⥤ BigFppfOver B S hS) (pY : Y ⥤ BigFppfOver B S hS)
    (pZ : Z ⥤ BigFppfOver B S hS) (f : X ⥤ Y) (g : Z ⥤ Y)
    (_hpX : pX.IsFiberedInGroupoids) (hpY : pY.IsFiberedInGroupoids)
    (_hpZ : pZ.IsFiberedInGroupoids)
    (hf : f ⋙ pY = pX) (hg : g ⋙ pY = pZ)
    (h : IsSmoothOnPredeformationCategories B S hS pX pY f hf) :
    IsSmoothOnPredeformationCategories B S hS
      (TwoFibreProductOver.structureFunctor pX pZ pY f g) pZ
      (TwoFibreProductOver.snd pX pZ pY f g)
      (by exact TwoFibreProductOver.snd_comp_eq)
Tag 07XW, a lemma

Tag 07XW in the Stacks Project.

Deformation.Artin.isSmoothOnPredeformationCategories_of_isRelativelySmooth', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/RepresentableSmoothVersality.lean, line 57. The attribute's comment: “the representable-and-smooth clause: representable by algebraic spaces and smooth implies smooth on predeformation categories”.

Stacks 07XW, the representable-and-smooth clause. A 1-morphism of categories fibred in groupoids over the big fppf category of a locally Noetherian scheme S which is representable by algebraic spaces and smooth induces a smooth functor of predeformation categories at every finite type field-valued point of the source; that is, it satisfies the condition of Stacks 07XS.

public theorem isSmoothOnPredeformationCategories_of_isRelativelySmooth'
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) [IsLocallyNoetherian S]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hsmooth : Stack.IsRelativelySmooth B S hS p) :
    IsSmoothOnPredeformationCategories B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor p)
      (CatFiberedInGroupoids.homFunctor_comp_p p)

Deformation.Artin.isSmoothOnPredeformationCategories_of_isRelativelySmooth_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/SmoothImpliesVersalityCondition.lean, line 109. The attribute's comment: “the representable-and-smooth clause, for a 1-morphism whose base changes along scheme-valued points of the target are representable by schemes”.

A 1-morphism p of categories fibred in groupoids over the big fppf category of a locally Noetherian scheme S which is representable by algebraic spaces and smooth, and such that each algebraic space representing a base change of p along a scheme-valued point of the target is representable by schemes (hrep), induces a smooth functor of predeformation categories at every finite type field-valued point of the source.

public theorem isSmoothOnPredeformationCategories_of_isRelativelySmooth_of_representable
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) [IsLocallyNoetherian S]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hsmooth : Stack.IsRelativelySmooth B S hS p)
    (hrep : ∀ (U : BigFppfOver B S hS)
      (y : BigFppfOver B U.left.1 U.left.2 ⥤ 𝒴.val.obj)
      (_hy : y ⋙ 𝒴.val.p = Over.map U.hom)
      (F : (BigFppfOver B U.left.1 U.left.2)ᵒᵖ ⥤ Type u)
      (_hF : IsAlgebraicSpace B U.left.1 U.left.2 F),
      Nonempty (StacksRepresentableCFG.EquivalenceOver
        (TwoFibreProductOver.fst (Over.map U.hom) 𝒳.val.p 𝒴.val.p y
          (CatFiberedInGroupoids.homFunctor p))
        (presheafOfCategories (F ⋙ typeToCat)).p) →
      yoneda.relativelyRepresentable (OverShriek.relocalizeToYoneda U.hom F)) :
    IsSmoothOnPredeformationCategories B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor p)
      (CatFiberedInGroupoids.homFunctor_comp_p p)

Deformation.Artin.isSmoothOnPredeformationCategories_of_isFormallySmoothOnObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/SmoothPredeformation.lean, line 523. The attribute's comment: “the formally-smooth-on-objects clause: formally smooth on objects implies smooth on predeformation categories”.

Stacks 07WK, case (1). A 1-morphism of categories fibred in groupoids over the big fppf category of S which is formally smooth on objects induces a smooth functor of predeformation categories at every finite type field-valued point of the source.

This is also the formally-smooth-on-objects clause of Stacks 07XW — the condition the openness-of-versality statement is about — so both tags are registered here, on the declaration that carries the proof.

public theorem isSmoothOnPredeformationCategories_of_isFormallySmoothOnObjects
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) [IsLocallyNoetherian S]
    {𝒳 𝒴 : CatFiberedInGroupoids.{u, v, u + 1, w} (BigFppfOver B S hS)} (p : 𝒳 ⟶ 𝒴)
    (hp : Stack.IsFormallySmoothOnObjects B S hS 𝒳 𝒴 p) :
    IsSmoothOnPredeformationCategories B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor p)
      (CatFiberedInGroupoids.homFunctor_comp_p p)
Tag 07XX, a lemma

Tag 07XX in the Stacks Project.

AlgebraicGeometry.Stack.isRelativelySmooth_of_isSmoothOnPredeformationCategories, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TwoFibreProductSliceAtlas.lean, line 1089. The attribute's comment: “the general 1-morphism, at the source's own hypotheses: (1) hfrep, (2) hf, (3) hlimX, (4) hlimY, and S locally Noetherian. The case of a 1-morphism induced by a morphism of schemes is smooth_of_isSmoothOnPredeformationCategories”.

Stacks 07XX. Let S be a locally Noetherian scheme and f : 𝒳 ⟶ 𝒴 a 1-morphism of categories fibred in groupoids over the big fppf site of S. If (1) f is representable by algebraic spaces, (2) f satisfies the deformation-theoretic smoothness condition of Stacks 07XS, (3) the structure morphism 𝒳 ⟶ (Sch/S)_{fppf} is limit preserving on objects in the sense of Stacks 06CU, and (4) 𝒴 is limit preserving in the sense of Stacks 07XL, then f is smooth.

AlgebraicGeometry.Stack.IsRelativelySmooth bundles the representability witness with the relative property of Stacks 03YK at the smooth property, which is what "smooth" means for a 1-morphism, so this is AlgebraicGeometry.Stack.hasRelativeProperty_smooth_of_isSmoothOnPredeformationCategories paired with hfrep. Condition (3) enters only through the cancellation for Stacks 06CU, AlgebraicGeometry.Stack.isLimitPreservingOnObjects_of_toTerminalCFG.

The case of a 1-morphism induced by a morphism of schemes — the key ingredient, where the appeal to More on Morphisms is made — is Deformation.Artin.smooth_of_isSmoothOnPredeformationCategories.

theorem isRelativelySmooth_of_isSmoothOnPredeformationCategories
    (hfrep : IsRepresentableByAlgebraicSpaces B S hS f.hom)
    (hlimX : BigFppfOver.IsLimitPreservingOnObjects.{u, u, u, u, u + 1} B S hS 𝒳
      (terminalCFG B S hS) (Bicategory.InducedBicategory.mkHom (toTerminalCFG B S hS 𝒳)))
    (hlimY : Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u} B S hS 𝒴)
    (hf : Deformation.Artin.IsSmoothOnPredeformationCategories B S hS 𝒳.val.p 𝒴.val.p
      (CatFiberedInGroupoids.homFunctor f) (CatFiberedInGroupoids.homFunctor_comp_p f)) :
    IsRelativelySmooth B S hS f

Deformation.Artin.smooth_of_isSmoothOnPredeformationCategories, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/SmoothnessFromPredeformation.lean, line 714. The attribute's comment: “the case of the 1-morphism induced by a morphism g : W ⟶ V of schemes over S. Hypothesis (2) is the hypothesis hs; hypothesis (1) is automatic for such a 1-morphism; and hypotheses (3) and (4) are replaced by W and V being locally of finite type over S, which over a locally Noetherian base is the finite-presentation content of limit preservation. The conclusion is smoothness of the morphism of schemes g -- what the relative property of Stacks 03YK amounts to for this 1-morphism, though that identification is not formalized here. The bookkeeping that reduces the general statement to this case (the 2-fibre product, its etale atlas, and part (3) of Stacks 07XN, which the library does not have) is NOT carried out, so the general 1-morphism of 07XX is not covered”.

A morphism g : W ⟶ V of schemes locally of finite type over a locally Noetherian base S whose induced 1-morphism of slice categories satisfies the deformation-theoretic smoothness condition of Stacks 07XS is a smooth morphism of schemes.

This is the case of Stacks 07XX in which the 1-morphism is the one induced by a morphism of schemes over S. It is the step the source calls the key ingredient of its proof, namely its appeal to More on Morphisms, Lemma 02HX; here that appeal is routed through the scheme-level criterion Deformation.Artin.smoothAt_iff_isVersalAt (Stacks 0CXL), which is 02HX in versality form, together with openness of the smooth locus and density of finite type points (Stacks 02J4).

public theorem smooth_of_isSmoothOnPredeformationCategories
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S]
    (W V : AlgebraicGeometry.BigFppfOver B S hS) (g : W ⟶ V)
    [LocallyOfFiniteType W.hom.hom] [LocallyOfFiniteType V.hom.hom]
    (hs : Deformation.Artin.IsSmoothOnPredeformationCategories B S hS
      (Over.map W.hom) (Over.map V.hom) (Over.map g.left)
      (by rw [← Over.mapComp_eq, g.w])) : Smooth g.left.hom
Tag 07XY, a lemma

Tag 07XY in the Stacks Project.

Deformation.Artin.exists_smooth_finiteType_neighborhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ArtinCriteria/SmoothNeighborhood.lean, line 108. The attribute's comment: “the finite-type base, the object over it, its finite type point with residue field k, the restriction of that object to x₀ there, and smoothness of the 2-Yoneda morphism attached to it”.

Stacks 07XY. Let 𝒳 be a category fibred in groupoids over the big fppf site of a locally Noetherian scheme S whose diagonal is representable by algebraic spaces, which is limit preserving (axiom [1]), satisfies (RS) (axiom [2]) and has finite-dimensional tangent spaces (the tangent-space half of axiom [3]), all of whose formal objects are effective, for which versality is open, and let x₀ be an object of 𝒳 over a quasi-compact finite-type field point i₀ : Spec k ⟶ S whose image is a point s at which the local ring of S is a G-ring.

Then there is a base U = 𝒳.val.p.obj x of finite type over S — locally of finite type and quasi-compact — an object x of 𝒳 over it, and a finite type point u₀ of U with residue field k, such that x restricts to x₀ at u₀ along a Cartesian arrow r : x₀ ⟶ x realizing that identification of residue fields, and the 1-morphism (Sch/U)_{fppf} ⟶ 𝒳 attached to x by the 2-Yoneda lemma is smooth.

The proof is the proof of the source: the versal finite-type point of Stacks 07XH, shrunk by openness of versality, carries a smooth 2-Yoneda 1-morphism by Stacks 0CXM.

public theorem exists_smooth_finiteType_neighborhood
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S]
    (𝒳 : CatFiberedInGroupoids.{u, max u v, u + 1, max (u + 1) v w}
      (AlgebraicGeometry.BigFppfOver B S hS))
    (k : Type u) [Field k]
    (i₀ : Spec (.of k) ⟶ S) (x₀ : 𝒳.val.obj)
    (hx₀ : (𝒳.val.p ⋙ Over.post B.inclusion).obj x₀ = Over.mk i₀)
    (hfinite₀ : LocallyOfFiniteType i₀) (hqc₀ : QuasiCompact i₀)
    (s : S) (hs : i₀ (IsLocalRing.closedPoint k) = s)
    (hdiag : AlgebraicGeometry.Stack.HasRepresentableDiagonal B S hS 𝒳)
    (hlimit : IsLimitPreserving.{u, u, u, max (u + 1) v w, max u v} B S hS 𝒳)
    (hRS : SatisfiesRS B S hS 𝒳.val.p 𝒳.property)
    (htangent :
      ∀ (Λ : Type u) [CommRing Λ] [Algebra Λ k]
        (_ : Λ = S.presheaf.stalk s)
        (iΛ : Spec (.of Λ) ⟶ S)
        (_ : HEq iΛ (S.fromSpecStalk s))
        (hbase : Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ = i₀),
        let hx : (𝒳.val.p ⋙ Over.post B.inclusion).obj x₀ =
          Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ) :=
          hx₀.trans (congrArg Over.mk hbase.symm)
        let D := predeformationCategory iΛ
          (𝒳.val.p ⋙ Over.post B.inclusion) x₀ hx
        letI : Category D.carrier := D.category
        ∀ hD : Deformation.IsDeformationCategory D.projection,
          let 𝓕 := BasedCategory.ofFunctor D.projection
          let hS2 := schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory 𝓕 hD
          letI : Fact (Deformation.IsPredeformationCategory 𝓕.p) :=
            ⟨hD.predeformation⟩
          letI : Fact (Deformation.SchlessingerConditionS2
            (CategoryOfElements.π
              (Deformation.isomorphismClasses 𝓕 hD.predeformation.cofibered))) :=
            ⟨hS2⟩
          let F := Deformation.isomorphismClasses 𝓕 hD.predeformation.cofibered
          let T := Deformation.artinianTangentSpace Λ k F
          letI : AddCommGroup T := Deformation.associatedTangentSpaceAddCommGroupUnlifted 𝓕
          letI : Module k T := Deformation.associatedTangentSpaceModuleUnlifted 𝓕
          FiniteDimensional k T)
    (heffective : ∀ ξ : FormalObject B S hS 𝒳.val.p,
      FormalObject.IsEffective B S hS 𝒳.val.p 𝒳.property ξ)
    (hopen : ∀ U : Over S, LocallyOfFiniteType U.hom →
      ∀ (y : 𝒳.val.obj) (hy : (𝒳.val.p ⋙ Over.post B.inclusion).obj y = U) (u : U.left),
        AlgebraicGeometry.IsFiniteTypePoint u →
        IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u y hy →
        ∃ V : U.left.Opens, u ∈ V.1 ∧
          ∀ u' : U.left, u' ∈ V.1 →
            AlgebraicGeometry.IsFiniteTypePoint u' →
            IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u' y hy)
    (hG : IsGRing (S.presheaf.stalk s)) :
    ∃ (x : 𝒳.val.obj)
      (u₀ : ((𝒳.val.p ⋙ Over.post B.inclusion).obj x).left)
      (e : ((𝒳.val.p ⋙ Over.post B.inclusion).obj x).left.residueField u₀ ≃+* k)
      (r : x₀ ⟶ x)
      (f : (AlgebraicGeometry.Stack.schemeFibredCategory B S hS
        (𝒳.val.p.obj x)).val ⥤ᵇ 𝒳.val),
      LocallyOfFiniteType ((𝒳.val.p ⋙ Over.post B.inclusion).obj x).hom ∧
      QuasiCompact ((𝒳.val.p ⋙ Over.post B.inclusion).obj x).hom ∧
      AlgebraicGeometry.IsFiniteTypePoint u₀ ∧
      𝒳.val.p.IsCartesian (𝒳.val.p.map r) r ∧
      (eqToHom hx₀.symm ≫ (𝒳.val.p ⋙ Over.post B.inclusion).map r).left =
        Spec.map (CommRingCat.ofHom e.toRingHom) ≫
          ((𝒳.val.p ⋙ Over.post B.inclusion).obj x).left.fromSpecResidueField u₀ ∧
      Nonempty ((Functor.twoYonedaEvaluation 𝒳.val.p (𝒳.val.p.obj x)).obj f ≅
        (⟨x, rfl⟩ : 𝒳.val.p.Fiber (𝒳.val.p.obj x))) ∧
      (∃ hf : AlgebraicGeometry.IsRepresentableByAlgebraicSpaces B S hS f,
        AlgebraicGeometry.Stack.HasRelativePropertyBased.{u, u, u + 1,
            max u v, max (u + 1) v w, u} B S hS
          (AlgebraicGeometry.Space.smoothMorphismProperty B S hS) f hf)
Sources
LeanDeformation.Artin.IsOpenVersality · Deformation.Artin.IsOpenVersalityMorphism · Deformation.Artin.artinAxiomsFunctor · Deformation.Artin.artinAxiomsCategory · Deformation.Artin.nonempty_artinAxiomsFunctor_iff_exists_isCompact_open · Deformation.Artin.isVersalAt_sliceObject · Deformation.Artin.not_isVersalAt_sliceObject · Deformation.Artin.not_isOpenVersality_artinAxiomsCategory

Section98.16 Algebraic spaces#

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

Tag 07Y1, a proposition

Tag 07Y1 in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_of_artinAxioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ArtinAxiomsAlgebraicSpace.lean, line 442.

Stacks 07Y1 (Artin's axioms for algebraic spaces). Let S be a locally Noetherian scheme and F a set-valued functor on the big fppf site of S. Assume that

  1. the diagonal Δ : F ⟶ F × F is representable by algebraic spaces,
  2. F satisfies Artin's axioms of Section 07XZ: [-1] the cardinalities |F(Spec k)|, for k running over the finite type fields over S, are bounded by the size of one object of the site; [0] F is a sheaf for the étale topology; [1] F is limit preserving (Stacks 049J); [2] F satisfies the Rim–Schlessinger condition; [3] every tangent space of F at a finite type field-valued point is finite dimensional; [4] every formal object of F is effective; [5] F satisfies openness of versality — axioms [2]–[5] read, as in Section 07XZ, on the category fibred in sets 𝒮_F, and
  3. the local rings 𝒪_{S,s} at the finite type points s of S are G-rings.

Then F is an algebraic space.

Axiom [5] is written out rather than through AlgebraicGeometry.IsOpenVersality, which asks its fibred category to be fibred in groupoids over all schemes over S and so cannot hold for a category over the bounded big fppf site; the written-out form is the source's definition.

The proof is AlgebraicGeometry.Space.isAlgebraicSpace_isoClassPresheafModel_of_artinAxioms for 𝒮_F, whose presheaf of isomorphism classes is F, after the translations of Section 07XZ.

theorem isAlgebraicSpace_of_artinAxioms [IsLocallyNoetherian S]
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hdiag : IsRepresentableByAlgebraicSpaces B S hS (diag F))
    (hsize : ∃ T : BigFppfOver B S hS,
      ∀ (U : BigFppfOver B S hS) (k : Type u) [Field k],
        U.left.1 = Spec (.of k) → Deformation.Artin.IsFiniteTypeOver B S hS U →
          Cardinal.mk (F.obj (op U)) ≤ T.left.1.size)
    (hF : Presheaf.IsSheaf ((AlgebraicGeometry.etaleTopology B).over (B.obj hS)) F)
    (hlimit : AlgebraicGeometry.LimitPreserving.{u, u, u, u} (BigFppfOver.toScheme B S hS) F)
    (hRS : Deformation.Artin.SatisfiesRS B S hS (fibredCategory B S hS F).val.p
      (fibredCategory B S hS F).property)
    (htangent : HasFiniteDimensionalTangentSpaces B S hS (fibredCategory B S hS F))
    (heffective : ∀ ξ : Deformation.Artin.FormalObject B S hS (fibredCategory B S hS F).val.p,
      Deformation.Artin.FormalObject.IsEffective B S hS (fibredCategory B S hS F).val.p
        (fibredCategory B S hS F).property ξ)
    (hopen : ∀ U : Over S, LocallyOfFiniteType U.hom →
      ∀ (y : (fibredCategory B S hS F).val.obj)
        (hy : ((fibredCategory B S hS F).val.p ⋙ Over.post B.inclusion).obj y = U)
        (u : U.left),
        AlgebraicGeometry.IsFiniteTypePoint u →
        Deformation.Artin.IsVersalAt U ((fibredCategory B S hS F).val.p ⋙ Over.post B.inclusion)
          u y hy →
        ∃ V : U.left.Opens, u ∈ V.1 ∧
          ∀ u' : U.left, u' ∈ V.1 →
            AlgebraicGeometry.IsFiniteTypePoint u' →
            Deformation.Artin.IsVersalAt U
              ((fibredCategory B S hS F).val.p ⋙ Over.post B.inclusion) u' y hy)
    (hG : ∀ s : S, AlgebraicGeometry.IsFiniteTypePoint s → IsGRing (S.presheaf.stalk s)) :
    IsAlgebraicSpace B S hS F
Tag 07Y2, a lemma

Tag 07Y2 in the Stacks Project.

Deformation.Artin.isAlgebraicSpace_of_injective_of_artinAxioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/AlgebraicSpaceCriterionInjective.lean, line 358.

Stacks 07Y2. Let S be a locally Noetherian scheme and a : F ⟶ G a transformation of functors (Sch/S)_{fppf}^{opp} ⟶ Sets. Assume that

  1. a is injective;
  2. F satisfies axioms [0] (F is an étale sheaf), [1] (F is limit preserving), [2] (condition (RS) for F), [4] (every formal object of 𝒮_F is effective) and [5] (openness of versality for 𝒮_F);
  3. 𝒪_{S,s} is a G-ring for every finite type point s of S;
  4. G is an algebraic space locally of finite type over S.

Then F is an algebraic space.

As in the source, the proof applies Stacks 07Y1 to F: the diagonal of F is the base change of the diagonal of G along a × a, hence representable; axiom [3] holds for F because a induces fully faithful maps of predeformation categories into those of 𝒮_G, whose tangent spaces are finite-dimensional by Stacks 07X1; and the set-theoretic condition [-1] holds for F because it holds for the algebraic space G and F(U) ⟶ G(U) is injective.

theorem isAlgebraicSpace_of_injective_of_artinAxioms [IsLocallyNoetherian S]
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G)
    (ha : ∀ U, Function.Injective (a.app U))
    (hF : Presheaf.IsSheaf ((etaleTopology B).over (B.obj hS)) F)
    (hlim : LimitPreserving.{u, u, u, u, u + 1} (BigFppfOver.toScheme B S hS) F)
    (hRS : SatisfiesRSFunctor B S hS F)
    (heff : ∀ ξ : FormalObject B S hS (Stack.fibredCategory B S hS F).val.p,
      FormalObject.IsEffective B S hS (Stack.fibredCategory B S hS F).val.p
        (Stack.fibredCategory B S hS F).property ξ)
    (hopen : ∀ (U : Over S), LocallyOfFiniteType U.hom →
      ∀ (x : (Stack.fibredCategory B S hS F).val.obj)
        (hx : ((Stack.fibredCategory B S hS F).val.p ⋙ Over.post B.inclusion).obj x = U)
        (u₀ : U.left), IsFiniteTypePoint u₀ →
        IsVersalAt U ((Stack.fibredCategory B S hS F).val.p ⋙ Over.post B.inclusion) u₀ x hx →
        ∃ W : U.left.Opens, u₀ ∈ W.1 ∧ ∀ u : U.left, u ∈ W.1 → IsFiniteTypePoint u →
          IsVersalAt U ((Stack.fibredCategory B S hS F).val.p ⋙ Over.post B.inclusion) u x hx)
    (hGring : ∀ s : S, IsFiniteTypePoint s → IsGRing (S.presheaf.stalk s))
    (hG : IsAlgebraicSpace B S hS G)
    (hGft : Space.IsLocallyOfFiniteType B S hS (terminal.from G)) :
    IsAlgebraicSpace B S hS F
Sources
LeanAlgebraicGeometry.Space.isAlgebraicSpace_of_artinAxioms · Deformation.Artin.isAlgebraicSpace_of_injective_of_artinAxioms

Section98.17 Algebraic stacks#

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

Tag 07Y4, a lemma

Tag 07Y4 in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_of_artinAxioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ArtinCriterion/Algebraicity.lean, line 429.

Stacks 07Y4 (Artin's criterion). Let S be a locally Noetherian scheme and let 𝒳 be a category fibred in groupoids over the big fppf site of S. Assume that

  1. the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 is representable by algebraic spaces,
  2. 𝒳 satisfies axioms [-1], [0], [1], [2] and [3]: the set-theoretic bound of Stacks 07Y3 (hsize), the stack condition for the étale topology (hstack), limit preservation (hlimit), the Rim–Schlessinger condition (hRS) and finite dimensionality of tangent spaces (htangent),
  3. every formal object of 𝒳 is effective,
  4. 𝒳 satisfies openness of versality, and
  5. 𝒪_{S, s} is a G-ring for all finite type points s of S.

Then 𝒳 is an algebraic stack.

Axiom [0] is the source's: 𝒳 is a stack in groupoids for the étale topology. The proof is the source's: Stacks 07XY produces, through every finite type field-valued object, a smooth finite type neighbourhood; AlgebraicGeometry.Stack.isAlgebraicStack_of_hasSmoothFiniteTypeNeighborhoods assembles them into a surjective smooth atlas; and Stacks 076V (AlgebraicGeometry.Stack.isAlgebraicStack_of_isStackInGroupoids_etale_of_smooth), where the étale stack condition of axiom [0] is used, makes 𝒳 an fppf stack and hence an algebraic stack.

Of axiom [3] only the tangent-space half is asked for, which is all Stacks 07XY uses; the index universe of the stack condition in the conclusion is free.

public theorem isAlgebraicStack_of_artinAxioms [IsLocallyNoetherian S]
    (𝒳 : CatFiberedInGroupoids.{u, max u v, u + 1, max (u + 1) v w}
      (AlgebraicGeometry.BigFppfOver B S hS))
    (hdiag : HasRepresentableDiagonal B S hS 𝒳)
    (hsize : IsSizeBounded B S hS 𝒳)
    (hstack : 𝒳.val.p.IsStackInGroupoids.{u + 1}
      ((AlgebraicGeometry.etaleTopology B).over (B.obj hS)))
    (hlimit : Deformation.Artin.IsLimitPreserving.{u, u, u, max (u + 1) v w, max u v} B S hS 𝒳)
    (hRS : Deformation.Artin.SatisfiesRS B S hS 𝒳.val.p 𝒳.property)
    (htangent : HasFiniteDimensionalTangentSpaces B S hS 𝒳)
    (heffective : ∀ ξ : Deformation.Artin.FormalObject B S hS 𝒳.val.p,
      Deformation.Artin.FormalObject.IsEffective B S hS 𝒳.val.p 𝒳.property ξ)
    (hopen : ∀ U : Over S, LocallyOfFiniteType U.hom →
      ∀ (y : 𝒳.val.obj) (hy : (𝒳.val.p ⋙ Over.post B.inclusion).obj y = U) (u : U.left),
        AlgebraicGeometry.IsFiniteTypePoint u →
        Deformation.Artin.IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u y hy →
        ∃ V : U.left.Opens, u ∈ V.1 ∧
          ∀ u' : U.left, u' ∈ V.1 →
            AlgebraicGeometry.IsFiniteTypePoint u' →
            Deformation.Artin.IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u' y hy)
    (hG : ∀ s : S, AlgebraicGeometry.IsFiniteTypePoint s → IsGRing (S.presheaf.stalk s)) :
    IsAlgebraicStack.{u, z, max u v, max (u + 1) v w} B S hS 𝒳.val
Tag 07Y5, a proposition

Tag 07Y5 in the Stacks Project.

AlgebraicGeometry.Stack.isAlgebraicStack_of_artinAxioms_of_secondDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ArtinAxiomsSecondDiagonal.lean, line 396.

Stacks 07Y5 (Artin's axioms, second diagonal form). Let S be a locally Noetherian scheme and 𝒳 a category fibred in groupoids over the big fppf site of S. Assume that

  1. the second diagonal Δ_Δ : 𝒳 ⟶ 𝒳 ×_{𝒳 × 𝒳} 𝒳 is representable by algebraic spaces,
  2. 𝒳 satisfies Artin's axioms of Section 07XJ: [-1] the cardinalities of the sets of isomorphism classes of objects and of the sets of arrows of the fibres of 𝒳 over the finite type fields over S are bounded by the size of one object of the site; [0] 𝒳 is a stack in groupoids for the étale topology; [1] 𝒳 is limit preserving; [2] 𝒳 satisfies the Rim–Schlessinger condition; [3] the tangent spaces and the infinitesimal automorphism spaces of 𝒳 at the finite type field-valued points are finite dimensional; [4] the functor of Stacks 07X6 from objects over complete local bases to formal objects is an equivalence; [5] 𝒳 and Δ : 𝒳 ⟶ 𝒳 × 𝒳 satisfy openness of versality (Stacks 07XQ: for Δ, for every scheme V locally of finite type over S and every point y of 𝒳 × 𝒳 over V, the 2-fibre product (Sch/V)_{fppf} ×_{y, 𝒳 × 𝒳, Δ} 𝒳 has openness of versality), and
  3. the local rings 𝒪_{S,s} at the finite type points s of S are G-rings.

Then 𝒳 is an algebraic stack.

Openness of versality is written out (Deformation.Artin.HasOpenVersality) rather than through Deformation.Artin.IsOpenVersality, whose fibred-in-groupoids hypothesis over all schemes over S cannot hold for a category over the bounded big fppf site. A point y of 𝒳 × 𝒳 over V is given, by the 2-Yoneda lemma, as a 1-morphism (Sch/V)_{fppf} ⟶ 𝒳 × 𝒳 over the site.

The proof is the source's: AlgebraicGeometry.Stack.hasRepresentableDiagonal_of_artinAxioms_of_secondDiagonal makes the diagonal representable (Stacks 07WH, 07WG and Proposition 07Y1 for the functors Y), and Lemma 07Y4 concludes.

theorem isAlgebraicStack_of_artinAxioms_of_secondDiagonal [IsLocallyNoetherian S]
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (BigFppfOver B S hS))
    (hΔΔ : IsRepresentableByAlgebraicSpaces B S hS
      (relativeDiagonalBasedFunctor B S hS 𝒳 (CatFiberedInGroupoids.product 𝒳 𝒳)
        (diagonalBasedFunctor B S hS 𝒳)))
    (hsize : ∃ T : BigFppfOver B S hS,
      ∀ (U : BigFppfOver B S hS) (k : Type u) [Field k],
        U.left.1 = Spec (.of k) → Deformation.Artin.IsFiniteTypeOver B S hS U →
        Cardinal.lift.{u, u + 1}
            (Cardinal.mk (Quotient (isIsomorphicSetoid (𝒳.val.p.Fiber U)))) ≤
          Cardinal.lift.{u + 1, u} T.left.1.size ∧
        Cardinal.lift.{u, u + 1} (Cardinal.mk (Σ a b : 𝒳.val.p.Fiber U, a ⟶ b)) ≤
          Cardinal.lift.{u + 1, u} T.left.1.size)
    (hstack : 𝒳.val.p.IsStackInGroupoids.{u + 1}
      ((AlgebraicGeometry.etaleTopology B).over (B.obj hS)))
    (hlimit : Deformation.Artin.IsLimitPreserving.{u, u, u, u + 1, u} B S hS 𝒳)
    (hRS : Deformation.Artin.SatisfiesRS B S hS 𝒳.val.p 𝒳.property)
    (htangent : HasFiniteDimensionalTangentSpaces B S hS 𝒳)
    (hInf : Deformation.Artin.HasFiniteDimensionalInfinitesimalAutomorphismsOf B S hS 𝒳.val.p)
    (happrox : (Deformation.Artin.approximationFunctor B S hS 𝒳.val.p 𝒳.property).IsEquivalence)
    (hopen : Deformation.Artin.HasOpenVersality (𝒳.val.p ⋙ Over.post B.inclusion))
    (hopenΔ : ∀ V : BigFppfOver B S hS, LocallyOfFiniteType (B.inclusion.map V.hom) →
      ∀ (y : BigFppfOver B V.left.1 V.left.2 ⥤ (CatFiberedInGroupoids.product 𝒳 𝒳).val.obj),
        y ⋙ (CatFiberedInGroupoids.product 𝒳 𝒳).val.p = Over.map V.hom →
        Deformation.Artin.HasOpenVersality
          (TwoFibreProductOver.fst (Over.map V.hom) 𝒳.val.p
            (CatFiberedInGroupoids.product 𝒳 𝒳).val.p y
            (diagonalBasedFunctor B S hS 𝒳).toFunctor ⋙ Over.post B.inclusion))
    (hG : ∀ s : S, AlgebraicGeometry.IsFiniteTypePoint s → IsGRing (S.presheaf.stalk s)) :
    IsAlgebraicStack.{u, z, u, u + 1} B S hS 𝒳.val
Sources
LeanAlgebraicGeometry.Stack.isAlgebraicStack_of_artinAxioms · AlgebraicGeometry.Stack.isAlgebraicStack_of_artinAxioms_of_secondDiagonal

Section98.18 Strong Rim-Schlessinger#

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

Tag 0CXN, the section

Tag 0CXN in the Stacks Project.

Deformation.Artin.locallyOfFiniteType_and_quasiCompact_of_isPullback_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/FiniteTypeCorner.lean, line 67. The attribute's comment: “observation (3): if S is locally Noetherian, A, B, B' are of finite type over S and B is finite over A, then A' = A ×_B B' is of finite type over S”.

Observation (3) of the section on condition (RS*). Let S be locally Noetherian, and let U = Spec B, V = Spec A, W = Spec B', Z = Spec A' be affine schemes with morphisms f : U ⟶ V, g : U ⟶ W, i : V ⟶ Z, j : W ⟶ Z whose square of global sections exhibits A' = A ×_B B', with B' → B surjective, and let t : Z ⟶ S give the S-algebra structures. If A and B' are of finite type over S and B is finite over A, then A' is of finite type over S.

public theorem locallyOfFiniteType_and_quasiCompact_of_isPullback_appTop
    {S U V W Z : Scheme.{u}} [IsLocallyNoetherian S]
    [IsAffine U] [IsAffine V] [IsAffine W] [IsAffine Z]
    (f : U ⟶ V) (g : U ⟶ W) (i : V ⟶ Z) (j : W ⟶ Z) (t : Z ⟶ S)
    (hsq : IsPullback i.appTop j.appTop f.appTop g.appTop)
    (hsurj : Function.Surjective g.appTop.hom) (hfin : f.appTop.hom.Finite)
    [LocallyOfFiniteType (i ≫ t)] [LocallyOfFiniteType (j ≫ t)] :
    LocallyOfFiniteType t ∧ QuasiCompact t

Deformation.Artin.isPushout_of_isPullback_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/FromThickeningPushouts.lean, line 125. The attribute's comment: “observation (1): Spec(A') = Spec(A) ⨿_{Spec(B)} Spec(B') in the category of schemes, for A' = A ×_B B' with B' → B surjective (the square-zero kernel is not needed)”.

A cartesian square of global sections of four affine schemes, one of whose maps is surjective on global sections, is a cocartesian square of schemes. This is [Stacks Project, Tag 0ET0] transported along AlgebraicGeometry.Scheme.isoSpec.

public theorem isPushout_of_isPullback_appTop {U V W Z : Scheme.{u}}
    [IsAffine U] [IsAffine V] [IsAffine W] [IsAffine Z]
    (f : U ⟶ V) (g : U ⟶ W) (i : V ⟶ Z) (j : W ⟶ Z)
    (hsq : IsPullback i.appTop j.appTop f.appTop g.appTop)
    (hsurj : Function.Surjective g.appTop.hom) : IsPushout f g i j

Deformation.Artin.satisfiesRS_of_satisfiesRSStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/RSStarImpliesRS.lean, line 685. The attribute's comment: “observation (4): if 𝒳 satisfies (RS*), then 𝒳 satisfies (RS); the base need not be locally Noetherian”.

The remark following Stacks 07Y8: condition (RS*) implies condition (RS).

Given a pushout square of finite-type local Artinian objects of the site along a closed immersion, the closed immersion is a surjection of Artinian local rings, so its kernel is nilpotent; the surjection therefore factors as a tower of square-zero surjections, each of which (RS*) covers, and the resulting squares of fibres paste to the given one.

public theorem satisfiesRS_of_satisfiesRSStar
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒵 : Type u₁} [Category.{v₁} 𝒵] (p : 𝒵 ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hRS : SatisfiesRSStar B S hS p hp) :
    SatisfiesRS B S hS p hp
Tag 07Y8, a definition

Tag 07Y8 in the Stacks Project.

Deformation.Artin.isDeformationCategory_predeformationCategory_of_satisfiesRSStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/DeformationCategory.lean, line 1221. The attribute's comment: “condition (RS*) gives a deformation category”.

Stacks Project, Tag 07Y8. The predeformation category of a finite-type field-valued point in a fibred category satisfying (RS) is a deformation category; only the square-zero squares that (RS) quantifies over are needed.

public theorem isDeformationCategory_predeformationCategory_of_satisfiesRSStar
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type u₁} [Category.{v₁} 𝒳]
    (p : 𝒳 ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids)
    (hRS : SatisfiesRSStar B S hS p hp)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ S)
    (x₀ : 𝒳)
    (hx₀ : (p ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hfinite : LocallyOfFiniteType
      (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hqc : QuasiCompact
      (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ)) :
    let D := predeformationCategory iΛ
      (p ⋙ Over.post B.inclusion) x₀ hx₀
    letI := D.category
    Deformation.IsDeformationCategory D.projection

Deformation.Artin.SatisfiesRSStar, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/Strong.lean, line 75.

Condition (RS*): for every fibre-product square of S-algebras in the big affine fppf site, with one map surjective with square-zero kernel, the canonical functor from the fibre over the pullback algebra to the two-fibre product of the other three fibres is an equivalence.

public abbrev SatisfiesRSStar
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type w} [Category X]
    (p : X ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) : Prop
Tag 0CXP, a lemma

Tag 0CXP in the Stacks Project.

Deformation.Artin.satisfiesRSStar_of_isAlgebraicStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/RimSchlessinger/AlgebraicStackRSStar.lean, line 51.

Stacks 0CXP. Every algebraic stack over S satisfies condition (RS*) of [Stacks Project, Tag 07Y8].

The atlas of the stack is representable by algebraic spaces, surjective and smooth; smooth morphisms of algebraic spaces are formally smooth (AlgebraicGeometry.Space.formallySmooth_of_isSmooth_unconditional, the implication (1) ⟹ (2) of [Stacks Project, Tag 04AM]), so the atlas is formally smooth on objects ([Stacks Project, Tag 06D3]), and Deformation.Artin.satisfiesRSStar_of_atlas applies.

theorem satisfiesRSStar_of_isAlgebraicStack
    (𝒳 : BasedCategory.{u, u + 1} (BigFppfOver B S hS))
    (h𝒳 : Stack.IsAlgebraicStack.{u, w} B S hS 𝒳) :
    ∀ hp : 𝒳.p.IsFiberedInGroupoids, SatisfiesRSStar B S hS 𝒳.p hp
Tag 0CXQ, a lemma

Tag 0CXQ in the Stacks Project.

Deformation.Artin.twoFibreProductOver_satisfiesRSStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ArtinCriteria/RimSchlessinger.lean, line 1216.

The two-fibre product of categories fibred in groupoids satisfying condition (RS) again satisfies (RS).

public theorem twoFibreProductOver_satisfiesRSStar
    {X : Type uX} [Category X]
    {Y : Type uY} [Category Y]
    {Z : Type uZ} [Category Z]
    (pX : X ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (pY : Y ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (pZ : Z ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (F : X ⥤ Y) (G : Z ⥤ Y)
    (hX : pX.IsFiberedInGroupoids) (hY : pY.IsFiberedInGroupoids)
    (hZ : pZ.IsFiberedInGroupoids)
    (hF : F ⋙ pY = pX) (hG : G ⋙ pY = pZ)
    (rsX : Deformation.Artin.SatisfiesRSStar B S hS pX hX)
    (rsY : Deformation.Artin.SatisfiesRSStar B S hS pY hY)
    (rsZ : Deformation.Artin.SatisfiesRSStar B S hS pZ hZ) :
    Deformation.Artin.SatisfiesRSStar B S hS
      (TwoFibreProductOver.structureFunctor pX pZ pY F G)
      (TwoFibreProductOver.isFiberedInGroupoids pX pZ pY F G
        hX hZ hY hF hG)
Sources
LeanDeformation.Artin.locallyOfFiniteType_and_quasiCompact_of_isPullback_appTop · Deformation.Artin.isPushout_of_isPullback_appTop · Deformation.Artin.satisfiesRS_of_satisfiesRSStar · Deformation.Artin.isDeformationCategory_predeformationCategory_of_satisfiesRSStar · Deformation.Artin.SatisfiesRSStar · Deformation.Artin.satisfiesRSStar_of_isAlgebraicStack · Deformation.Artin.twoFibreProductOver_satisfiesRSStar

Section98.19 Versality and generalizations#

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

Tag 0G2J, a lemma

Tag 0G2J in the Stacks Project.

Deformation.Artin.exists_firstOrderThickening_without_localRetraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/NonversalThickening/ThickeningWithoutRetraction.lean, line 618.

Stacks 0G2J. If an object x of a category fibred in groupoids with (RS*) over the big fppf site of a locally Noetherian scheme is not versal at a finite type point u of an affine scheme U of finite type, then x extends to an object y over a first order thickening U ⟶ T with ideal κ(u) which has no retraction to x over any open neighbourhood of u.

public theorem exists_firstOrderThickening_without_localRetraction
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : Type v} [Category.{w} F]
    (p : F ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids)
    (hRS : Deformation.Artin.SatisfiesRSStar B S hS p hp)
    (U : AlgebraicGeometry.BigFppfOver B S hS) (x : F)
    (hx : p.obj x = U)
    [IsAffine ((AlgebraicGeometry.BigFppfOver.toScheme B S hS).obj U)]
    [IsLocallyNoetherian S]
    [LocallyOfFiniteType ((Over.post B.inclusion).obj U).hom]
    (u₀ : ((Over.post B.inclusion).obj U).left)
    (_hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀)
    (hnot : ¬ Deformation.Artin.IsVersalAt
      ((Over.post B.inclusion).obj U) (p ⋙ Over.post B.inclusion)
      u₀ x (congrArg (Over.post B.inclusion).obj hx)) :
    ∃ (T : AlgebraicGeometry.BigFppfOver B S hS) (i : U ⟶ T)
      (y : F) (hy : p.obj y = T) (r : x ⟶ y),
      let V := AlgebraicGeometry.BigFppfOver.toScheme B S hS
      let iS := V.map i
      (p.map r = eqToHom hx ≫ i ≫ eqToHom hy.symm) ∧
      Stacks.Thickenings.IsFirstOrderThickening iS ∧
      Epi (SheafOfModules.unitToPushforwardObjUnit iS.toRingCatSheafHom) ∧
      Nonempty (kernel (SheafOfModules.unitToPushforwardObjUnit
        iS.toRingCatSheafHom) ≅
        (Scheme.Modules.pushforward ((V.obj T).fromSpecResidueField (iS u₀))).obj
          (SheafOfModules.unit
            (Spec ((V.obj T).residueField (iS u₀))).ringCatSheaf)) ∧
      (∀ (W : AlgebraicGeometry.BigFppfOver B S hS) (j : W ⟶ T)
          (w₀ : V.obj W) (_ : V.map j w₀ = iS u₀)
          (_ : IsOpenImmersion (V.map j))
          (z : F) (hz : p.obj z = W) (s : z ⟶ y)
          (_ : p.map s = eqToHom hz ≫ j ≫ eqToHom hy.symm)
          (_ : p.IsCartesian (p.map s) s),
        ¬ ∃ (β : z ⟶ x) (x' : F) (a : x' ⟶ x) (b : x' ⟶ z),
          p.IsCartesian (p.map a) a ∧
          p.IsCartesian (p.map b) b ∧
          IsPullback
            (V.map (p.map a ≫ eqToHom hx))
            (V.map (p.map b ≫ eqToHom hz)) iS (V.map j) ∧
          a ≫ r = b ≫ s ∧ b ≫ β = a)
Tag 0G2K, a lemma

Tag 0G2K in the Stacks Project.

Deformation.Artin.isVersalAt_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessAtGeneralization.lean, line 736.

Stacks 0G2K. Let S be a locally Noetherian scheme and 𝒳 a category fibred in groupoids over the big fppf site of S whose diagonal is representable by algebraic spaces, which satisfies (RS*) and which is limit preserving. Let x be an object of 𝒳 over a scheme U locally of finite type over S, and let u ⤳ u₀ be a specialization of points of U with u₀ of finite type. If x is versal at u₀, then x is versal at u.

The source asks U to be of finite type over S and u to be a finite type point; neither is used.

public theorem isVersalAt_of_specializes [IsLocallyNoetherian S]
    (hΔ : AlgebraicGeometry.Stack.HasRepresentableDiagonal B S hS 𝒳)
    (hRS : SatisfiesRSStar B S hS 𝒳.val.p 𝒳.isFiberedInGroupoids)
    (hlim : IsLimitPreserving.{u, u, u, w, v} B S hS 𝒳)
    (x : 𝒳.val.obj) [LocallyOfFiniteType ((𝒳.val.p ⋙ Over.post B.inclusion).obj x).hom]
    (u u₀ : ((𝒳.val.p ⋙ Over.post B.inclusion).obj x).left)
    (hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀) (hspec : u ⤳ u₀)
    (hversal : IsVersalAt ((𝒳.val.p ⋙ Over.post B.inclusion).obj x)
      (𝒳.val.p ⋙ Over.post B.inclusion) u₀ x rfl) :
    IsVersalAt ((𝒳.val.p ⋙ Over.post B.inclusion).obj x)
      (𝒳.val.p ⋙ Over.post B.inclusion) u x rfl
Sources
LeanDeformation.Artin.exists_firstOrderThickening_without_localRetraction · Deformation.Artin.isVersalAt_of_specializes

Section98.20 Strong formal effectiveness#

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

Tag 0G2S, a lemma

Tag 0G2S in the Stacks Project.

Deformation.Artin.exists_sequence_firstOrderThickenings_without_localRetraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/NonversalThickeningSequence.lean, line 1354.

Stacks Project, Tag 0G2S. Let 𝒳 be a category fibred in groupoids over the big fppf site of a locally Noetherian scheme S, satisfying (RS*), and let x be an object of 𝒳 over an affine scheme U of finite type over S. Let u 0, u 1, … be finite type points of U with no specializations between distinct ones, at none of which x is versal. Then there are morphisms x ⟶ x₁ ⟶ x₂ ⟶ … of 𝒳 over U ⟶ U₁ ⟶ U₂ ⟶ … over S such that each U ⟶ Uₙ₊₁ is a first order thickening, the ideal of Uₙ ⟶ Uₙ₊₁ is the residue field κ(u n), and x ⟶ xₙ₊₁ admits no retraction over any open neighbourhood of u n.

public theorem exists_sequence_firstOrderThickenings_without_localRetraction
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : Type v} [Category.{w} F]
    (p : F ⥤ AlgebraicGeometry.BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids)
    (hRS : SatisfiesRSStar B S hS p hp)
    (U : Over S) [IsAffine U.left] [IsLocallyNoetherian S]
    [LocallyOfFiniteType U.hom] [QuasiCompact U.hom]
    (x : F) (hx : (p ⋙ Over.post B.inclusion).obj x = U)
    (u : ℕ → U.left)
    (hfinite : ∀ n, AlgebraicGeometry.IsFiniteTypePoint (u n))
    (hincomparable : ∀ n m, n ≠ m → ¬ (u n ⤳ u m))
    (hnonversal : ∀ n,
      ¬ Deformation.Artin.IsVersalAt U (p ⋙ Over.post B.inclusion) (u n) x hx) :
    let q : F ⥤ Over S := p ⋙ Over.post B.inclusion
    ∃ (xs : ℕ → F)
      (step : ∀ n, xs n ⟶ xs (n + 1))
      (fromX : ∀ n, x ⟶ xs n),
      ∃ hzero : xs 0 = x,
        fromX 0 = eqToHom hzero.symm ∧
        (∀ n, fromX (n + 1) = fromX n ≫ step n) ∧
        (let j : ∀ n, U.left ⟶ (q.obj (xs n)).left :=
          fun n ↦ eqToHom (congrArg Over.left hx).symm ≫ (q.map (fromX n)).left
        ∀ n,
          Stacks.Thickenings.IsFirstOrderThickening (j (n + 1)) ∧
          (let i : (q.obj (xs n)).left ⟶ (q.obj (xs (n + 1))).left :=
              (q.map (step n)).left
           Epi (SheafOfModules.unitToPushforwardObjUnit i.toRingCatSheafHom) ∧
           Nonempty (kernel (SheafOfModules.unitToPushforwardObjUnit
               i.toRingCatSheafHom) ≅
             (Scheme.Modules.pushforward
                 ((q.obj (xs (n + 1))).left.fromSpecResidueField (j (n + 1) (u n)))).obj
               (SheafOfModules.unit (Spec ((q.obj (xs (n + 1))).left.residueField
                 (j (n + 1) (u n)))).ringCatSheaf))) ∧
          (∀ (y : F) (r : y ⟶ xs (n + 1)),
            IsOpenImmersion (q.map r).left →
            (∃ z : (q.obj y).left,
              (q.map r).left z = j (n + 1) (u n)) →
            ∀ (z : F) (t : z ⟶ x) (s : z ⟶ y),
              IsPullback (q.map t).left (q.map s).left
                (q.map (fromX (n + 1))).left (q.map r).left →
              ¬ ∃ β : y ⟶ x,
                s ≫ β = t ∧ t ≫ fromX (n + 1) = s ≫ r))
Tag 0CXT, a remark

Tag 0CXT in the Stacks Project.

Deformation.Artin.IsEffectiveSystem, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/Effectiveness.lean, line 63. The attribute's comment: “effectivity_of_a_system_of_objects”.

A diagram in a category over a base is effective over a specified base cocone when that cocone comes from a cocone of the objects. In a category fibred in groupoids, the lifted maps exhibit the diagram objects as the restrictions of the vertex object.

public abbrev IsEffectiveSystem {J : Type u₁} [Category.{v₁} J] {X : Type u₂}
    [Category.{v₂} X] {C : Type u₃} [Category.{v₃} C] (p : X ⥤ C) (ξ : J ⥤ X)
    (c : Cocone (ξ ⋙ p)) : Prop

Deformation.Artin.IsStronglyFormallyEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/FormalObject/Effectiveness.lean, line 81. The attribute's comment: “strong_formal_effectiveness”.

Strong formal effectiveness for a category fibred in groupoids over the big fppf site of a locally Noetherian scheme.

public abbrev IsStronglyFormallyEffective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S] {X : Type v} [Category.{w} X]
    (p : X ⥤ BigFppfOver B S hS)
    (_hp : p.IsFiberedInGroupoids) : Prop
Tag 0CXU, a lemma

Tag 0CXU in the Stacks Project.

Deformation.Artin.isOpenVersality_of_isSquareZeroEffective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessOfVersality.lean, line 443.

Stacks 0CXU. Let S be a locally Noetherian scheme and 𝒳 a category fibred in groupoids over the big fppf site of S such that

  1. the diagonal of 𝒳 is representable by algebraic spaces,
  2. 𝒳 has (RS*),
  3. 𝒳 is limit preserving,
  4. systems of objects as in Stacks 0CXT, over inverse systems of algebras whose transition maps are surjective with square-zero kernels, are effective.

Then 𝒳 satisfies openness of versality: if x is an object of 𝒳 over a scheme U locally of finite type over S, versal at a finite type point u₀ of U, then x is versal at every finite type point of an open neighbourhood of u₀.

The conclusion is the body of Deformation.Artin.IsOpenVersality (Stacks 07XQ), written out; see the implementation notes of this file.

public theorem isOpenVersality_of_isSquareZeroEffective [IsLocallyNoetherian S]
    (hΔ : AlgebraicGeometry.Stack.HasRepresentableDiagonal B S hS 𝒳)
    (hRS : SatisfiesRSStar B S hS 𝒳.val.p 𝒳.isFiberedInGroupoids)
    (hlim : IsLimitPreserving.{u, u, u, w, v} B S hS 𝒳)
    (heff : IsSquareZeroEffective B S hS 𝒳.val.p 𝒳.isFiberedInGroupoids)
    (U : Over S) (hUft : LocallyOfFiniteType U.hom) (x : 𝒳.val.obj)
    (hx : (𝒳.val.p ⋙ Over.post B.inclusion).obj x = U) (u₀ : U.left)
    (hu₀ : AlgebraicGeometry.IsFiniteTypePoint u₀)
    (hversal : IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u₀ x hx) :
    ∃ V : U.left.Opens, u₀ ∈ V.1 ∧
      ∀ u ∈ V.1, AlgebraicGeometry.IsFiniteTypePoint u →
        IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u x hx
Tag 0CXV, a remark

Tag 0CXV in the Stacks Project.

Deformation.Artin.isOpenVersality_diagonal_of_isFullyFaithfulOnSquareZeroTowers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/DiagonalOpenness.lean, line 81.

Let S be a locally Noetherian scheme and 𝒳 a category fibred in groupoids over the big fppf site of S whose second diagonal is representable by algebraic spaces, which satisfies (RS*), which is limit preserving, and for which the restriction functors 𝒳_{Spec lim Rₙ} ⟶ lim 𝒳_{Spec Rₙ} of square-zero towers are fully faithful. Then the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 satisfies openness of versality: for every scheme V locally of finite type over S and every object y of 𝒳 × 𝒳 over V, the 2-fibre product (Sch/V)_{fppf} ×_{y, 𝒳 × 𝒳, Δ} 𝒳 satisfies openness of versality — an object over a scheme U locally of finite type over V which is versal at a finite type point u₀ is versal at every finite type point of an open neighbourhood of u₀.

theorem isOpenVersality_diagonal_of_isFullyFaithfulOnSquareZeroTowers
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S]
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (AlgebraicGeometry.BigFppfOver B S hS))
    (h1 : AlgebraicGeometry.Stack.IsRepresentableByAlgebraicSpaces B S hS
      (AlgebraicGeometry.Stack.relativeDiagonalBasedFunctor B S hS 𝒳
        (CatFiberedInGroupoids.product 𝒳 𝒳)
        (AlgebraicGeometry.Stack.diagonalBasedFunctor B S hS 𝒳)))
    (h2 : SatisfiesRSStar B S hS 𝒳.val.p 𝒳.isFiberedInGroupoids)
    (h3 : IsLimitPreserving.{u, u, u, u + 1, u} B S hS 𝒳)
    (h4 : IsFullyFaithfulOnSquareZeroTowers B S hS 𝒳.val.p) :
    ∀ (V : AlgebraicGeometry.BigFppfOver B S hS), LocallyOfFiniteType (B.inclusion.map V.hom) →
      ∀ (y : AlgebraicGeometry.BigFppfOver B V.left.1 V.left.2 ⥤
          (CatFiberedInGroupoids.product 𝒳 𝒳).val.obj),
        y ⋙ (CatFiberedInGroupoids.product 𝒳 𝒳).val.p = Over.map V.hom →
        let q := TwoFibreProductOver.fst (Over.map V.hom) 𝒳.val.p
          (CatFiberedInGroupoids.product 𝒳 𝒳).val.p y
          (AlgebraicGeometry.Stack.diagonalBasedFunctor B S hS 𝒳).toFunctor ⋙
            Over.post B.inclusion
        ∀ (U : Over V.left.1), LocallyOfFiniteType U.hom →
          ∀ (x : TwoFibreProductOver (Over.map V.hom) 𝒳.val.p
              (CatFiberedInGroupoids.product 𝒳 𝒳).val.p y
              (AlgebraicGeometry.Stack.diagonalBasedFunctor B S hS 𝒳).toFunctor)
            (hx : q.obj x = U) (u₀ : U.left),
            IsFiniteTypePoint u₀ →
            IsVersalAt U q u₀ x hx →
            ∃ W : U.left.Opens, u₀ ∈ W.1 ∧
              ∀ u ∈ W.1, IsFiniteTypePoint u → IsVersalAt U q u x hx
Sources
LeanDeformation.Artin.exists_sequence_firstOrderThickenings_without_localRetraction · Deformation.Artin.IsEffectiveSystem · Deformation.Artin.IsStronglyFormallyEffective · Deformation.Artin.isOpenVersality_of_isSquareZeroEffective · Deformation.Artin.isOpenVersality_diagonal_of_isFullyFaithfulOnSquareZeroTowers

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.