93.4 Finite projective modules to 93.13 Deformations of…

Section93.4 Finite projective modules #

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

Tag 0D3I, an example

Tag 0D3I in the Stacks Project.

Deformation.Examples.FiniteProjectiveModule.Family.projection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveCofibered.lean, line 232.

The projection from finite projective modules to their Artinian local base algebras is cofibered in groupoids.

public theorem projection_isCofiberedInGroupoids
    (𝓕 : FiniteProjectiveModule.Family.{u, w, t} (Λ := Λ) (k := k)) :
    letI := 𝓕.category
    IsCofiberedInGroupoids 𝓕.projection

Deformation.Examples.FiniteProjectiveModule.specialFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveModules.lean, line 158. The attribute's comment: “finite_projective_deformation_category”.

The pair (k, V) consisting of the residue field and a finite-dimensional k-vector space: the special-fibre object whose deformations are studied.

public noncomputable def specialFiber (V : Type t) [AddCommGroup V] [Module k V]
    [Module.Finite k V] : FiniteProjectiveModule.{u, w, w, t} (Λ := Λ) (k := k)

Deformation.Examples.FiniteProjectiveModule.family, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveModules.lean, line 301. The attribute's comment: “finite_projective_deformation_category”.

The chosen category of finite projective modules over the algebras of 𝒞_Λ.

public noncomputable def family : Family.{u, w, t} (Λ := Λ) (k := k)

Deformation.Examples.FiniteProjectiveModule.deformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveModules.lean, line 307. The attribute's comment: “finite_projective_deformation_category”.

Deformations of a finite-dimensional k-vector space V: the objects of the category of finite projective modules lying over the special-fibre object (k, V).

public abbrev deformationCategory (V : Type t) [AddCommGroup V] [Module k V]
    [Module.Finite k V]

Tag 0DVP, a lemma

Tag 0DVP in the Stacks Project.

Deformation.Examples.FiniteProjectiveModule.Family.satisfiesRS_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveRimSchlessinger.lean, line 618. The attribute's comment: “Rim-Schlessinger condition”.

Finite projective modules over Artinian local algebras satisfy the Rim–Schlessinger condition: a cospan whose second base morphism is surjective is covered by the Milnor patch of the two modules over the fibre product of the base algebras.

public theorem Family.satisfiesRS_projection
    (𝓕 : FiniteProjectiveModule.Family.{u, w, t} (Λ := Λ) (k := k)) :
    letI := 𝓕.category
    SatisfiesRS 𝓕.projection

Deformation.Examples.FiniteProjectiveModule.isDeformationCategory_deformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveRimSchlessinger.lean, line 806. The attribute's comment: “deformation category”.

Deformations of a finite-dimensional vector space form a deformation category.

public theorem isDeformationCategory_deformationCategory
    (V : Type t) [AddCommGroup V] [Module k V] [Module.Finite k V] :
    let 𝓕 : FiniteProjectiveModule.Family.{u, w, t} (Λ := Λ) (k := k) :=
      FiniteProjectiveModule.family (Λ := Λ) (k := k)
    letI := 𝓕.category
    IsDeformationCategory
      (objectsOverFunctor 𝓕.projection
        (FiniteProjectiveModule.specialFiber (Λ := Λ) (k := k) V))

Tag 0DVQ, a lemma

Tag 0DVQ in the Stacks Project.

Deformation.Examples.FiniteProjectiveModule.subsingleton_tangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveTangentSpace.lean, line 489. The attribute's comment: “tangent_space_zero”.

The tangent space of the deformation category of a finite-dimensional vector space has at most one element: it is the zero vector space.

public theorem subsingleton_tangentSpace
    (V : Type t) [AddCommGroup V] [Module k V] [Module.Finite k V] :
    let 𝓖 := FiniteProjectiveModule.family.{u, w, t} (Λ := Λ) (k := k)
    letI := 𝓖.category
    let p := objectsOverFunctor 𝓖.projection (specialFiber (Λ := Λ) (k := k) V)
    let 𝓕 := BasedCategory.ofFunctor p
    let hD := isDeformationCategory_deformationCategory (Λ := Λ) V
    let hS2 := Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory 𝓕 hD
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 hD.predeformation.cofibered))) := ⟨hS2⟩
    let T := artinianTangentSpace Λ k (isomorphismClasses 𝓕 hD.predeformation.cofibered)
    letI : AddCommGroup T := associatedTangentSpaceAddCommGroupUnlifted 𝓕
    letI : Module k T := associatedTangentSpaceModuleUnlifted 𝓕
    Subsingleton T

Deformation.Examples.FiniteProjectiveModule.finiteDimensional_tangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/FiniteProjectiveTangentSpace.lean, line 549. The attribute's comment: “tangent_space_zero”.

The tangent space of the deformation category of a finite-dimensional vector space is finite-dimensional, being the zero vector space.

public theorem finiteDimensional_tangentSpace
    (V : Type t) [AddCommGroup V] [Module k V] [Module.Finite k V] :
    let 𝓖 := FiniteProjectiveModule.family.{u, w, t} (Λ := Λ) (k := k)
    letI := 𝓖.category
    let p := objectsOverFunctor 𝓖.projection (specialFiber (Λ := Λ) (k := k) V)
    let 𝓕 := BasedCategory.ofFunctor p
    let hD := isDeformationCategory_deformationCategory (Λ := Λ) V
    let hS2 := Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory 𝓕 hD
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 hD.predeformation.cofibered))) := ⟨hS2⟩
    let T := artinianTangentSpace Λ k (isomorphismClasses 𝓕 hD.predeformation.cofibered)
    letI : AddCommGroup T := associatedTangentSpaceAddCommGroupUnlifted 𝓕
    letI : Module k T := associatedTangentSpaceModuleUnlifted 𝓕
    FiniteDimensional k T

Deformation.Examples.FiniteProjectiveModule.infinitesimalAutomorphismsEquivEnd, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/InfinitesimalAutomorphisms/Endomorphisms.lean, line 1043. The attribute's comment: “infinitesimal_automorphisms”.

Infinitesimal automorphisms of a finite-dimensional vector space are its linear endomorphisms, with composition corresponding to addition.

public noncomputable def infinitesimalAutomorphismsEquivEnd
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (V : Type t) [AddCommGroup V] [Module k V] [Module.Finite k V] :
    let 𝓖 := FiniteProjectiveModule.family.{u, w, t} (Λ := Λ) (k := k)
    letI := 𝓖.category
    let p := objectsOverFunctor 𝓖.projection
      (specialFiber (Λ := Λ) (k := k) V)
    let hD := isDeformationCategory_deformationCategory (Λ := Λ) (k := k) V
    let hp : IsPredeformationCategory p := hD.predeformation
    ∀ {Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
      {x₀ : p.Fiber (residueFieldObject.{u, w, w} Λ k)}
      {xε : p.Fiber Aε}
      (g : residueFieldObject.{u, w, w} Λ k ⟶ Aε)
      (e : Aε ⟶ residueFieldObject.{u, w, w} Λ k)
      (hpair : IsCanonicalDualNumberPair g e)
      (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i),
      let iε : Aε ≃ₐ[Λ] DualNumber k :=
        Classical.choose (Classical.choose_spec hpair)
      let M := xε.1.left
      let hbase : M.base = Aε := (𝓖.projection_obj xε.1.left).symm.trans xε.2
      let ε : M.base := (eqToHom hbase.symm).hom (iε.symm DualNumber.eps)
      let r := 𝓖.homEquiv M
        (specialFiber (Λ := Λ) (k := k) V) xε.1.hom
      { E : infinitesimalAutomorphismGroup hp g e hpair i hi ≃*
          Multiplicative (Module.End k V) //
        ∀ (γ : infinitesimalAutomorphismGroup hp g e hpair i hi) (m : M.carrier),
          let a := 𝓖.homEquiv M M γ.val.asIso.hom.val.left
          ∃ n : M.carrier,
            r.linear n = (Multiplicative.toAdd (E γ)) (r.linear m) ∧
              a.linear m = m + ε • n }

Deformation.Examples.FiniteProjectiveModule.exists_infinitesimalAutomorphismsLinearEquivEnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/InfinitesimalAutomorphisms/Endomorphisms.lean, line 1082. The attribute's comment: “infinitesimal_automorphisms”.

The infinitesimal automorphism group of the deformations of V is the k-vector space Module.End k V, and is in particular finite-dimensional. The k-structure is the one of Stacks 06JV: its addition is composition of automorphisms, and multiplying by c scales the infinitesimal coordinate, which on the formula γ(m) = m + ε·n reads (c · γ)(m) = m + ε·(cb · n) for any element cb of the base reducing to c.

public theorem exists_infinitesimalAutomorphismsLinearEquivEnd
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (V : Type t) [AddCommGroup V] [Module k V] [Module.Finite k V] :
    let 𝓖 := FiniteProjectiveModule.family.{u, w, t} (Λ := Λ) (k := k)
    letI := 𝓖.category
    let p := objectsOverFunctor 𝓖.projection
      (specialFiber (Λ := Λ) (k := k) V)
    let hD := isDeformationCategory_deformationCategory (Λ := Λ) (k := k) V
    let hp : IsPredeformationCategory p := hD.predeformation
    ∀ {Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
      {x₀ : p.Fiber (residueFieldObject.{u, w, w} Λ k)}
      {xε : p.Fiber Aε}
      (g : residueFieldObject.{u, w, w} Λ k ⟶ Aε)
      (e : Aε ⟶ residueFieldObject.{u, w, w} Λ k)
      (hpair : IsCanonicalDualNumberPair g e)
      (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i),
      let iε : Aε ≃ₐ[Λ] DualNumber k :=
        Classical.choose (Classical.choose_spec hpair)
      let M := xε.1.left
      let hbase : M.base = Aε := (𝓖.projection_obj xε.1.left).symm.trans xε.2
      let ε : M.base := (eqToHom hbase.symm).hom (iε.symm DualNumber.eps)
      let r := 𝓖.homEquiv M
        (specialFiber (Λ := Λ) (k := k) V) xε.1.hom
      ∃ A : AddCommGroup (infinitesimalAutomorphismGroup hp g e hpair i hi),
        letI := A
        ∃ Mo : Module k (infinitesimalAutomorphismGroup hp g e hpair i hi),
          letI := Mo
          (∀ γ δ : infinitesimalAutomorphismGroup hp g e hpair i hi, γ + δ = γ * δ) ∧
          (∃ E : infinitesimalAutomorphismGroup hp g e hpair i hi ≃ₗ[k] Module.End k V,
            (∀ (γ : infinitesimalAutomorphismGroup hp g e hpair i hi) (m : M.carrier),
              ∃ n : M.carrier, r.linear n = E γ (r.linear m) ∧
                (𝓖.homEquiv M M γ.val.asIso.hom.val.left).linear m = m + ε • n) ∧
            ∀ (c : k) (cb : M.base), r.base.hom cb = c →
              ∀ (γ : infinitesimalAutomorphismGroup hp g e hpair i hi)
                (m n : M.carrier), r.linear n = E γ (r.linear m) →
                (𝓖.homEquiv M M γ.val.asIso.hom.val.left).linear m = m + ε • n →
                (𝓖.homEquiv M M (c • γ).val.asIso.hom.val.left).linear m =
                  m + ε • (cb • n)) ∧
          FiniteDimensional k (infinitesimalAutomorphismGroup hp g e hpair i hi)

Sources

LeanDeformation.Examples.FiniteProjectiveModule.Family.projection_isCofiberedInGroupoids · Deformation.Examples.FiniteProjectiveModule.specialFiber · Deformation.Examples.FiniteProjectiveModule.family · Deformation.Examples.FiniteProjectiveModule.deformationCategory · Deformation.Examples.FiniteProjectiveModule.Family.satisfiesRS_projection · Deformation.Examples.FiniteProjectiveModule.isDeformationCategory_deformationCategory · Deformation.Examples.FiniteProjectiveModule.subsingleton_tangentSpace · Deformation.Examples.FiniteProjectiveModule.finiteDimensional_tangentSpace

Section93.5 Representations of a group #

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

Tag 0D3J, an example

Tag 0D3J in the Stacks Project.

Deformation.Examples.FiniteProjectiveRepresentation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/Representations.lean, line 58. The attribute's comment: “representation_category: objects”.

A finite projective representation of Γ over an Artinian local Λ-algebra with residue field k.

public structure FiniteProjectiveRepresentation
    (Λ : Type u) (k : Type w) (Γ : Type*) [CommRing Λ] [Field k] [Algebra Λ k]
    [Group Γ]

Deformation.Examples.FiniteProjectiveRepresentation.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/Representations.lean, line 78. The attribute's comment: “representation_category: morphisms”.

A morphism of finite projective representations with varying coefficient ring.

public structure Hom
    {Λ : Type u} {k : Type w} {Γ : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    [Group Γ] (X Y : FiniteProjectiveRepresentation.{u, v, w, m} Λ k Γ)

Deformation.Examples.FiniteProjectiveRepresentation.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/Representations.lean, line 101. The attribute's comment: “representation_category”.

The category structure on finite projective representations with varying coefficient algebra.

public instance instCategory
    {Λ : Type u} {k : Type w} {Γ : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    [Group Γ] : Category (FiniteProjectiveRepresentation.{u, v, w, m} Λ k Γ)

Deformation.Examples.FiniteProjectiveRepresentation.specialFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/Representations.lean, line 159. The attribute's comment: “representation_deformation_category”.

The representation (V, ρ₀) over k, viewed as the special-fibre object.

public noncomputable def specialFiber
    {Λ : Type u} {k : Type w} {Γ : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    [Group Γ] (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) : FiniteProjectiveRepresentation.{u, w, w, m} Λ k Γ

Deformation.Examples.FiniteProjectiveRepresentation.deformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/Representations.lean, line 169. The attribute's comment: “representation_deformation_category”.

The category of deformations of a finite-dimensional representation of Γ.

public abbrev deformationCategory
    {Λ : Type u} {k : Type w} {Γ : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    [Group Γ] (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V)

Deformation.Examples.FiniteProjectiveRepresentation.projection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/RepresentationsCofibered.lean, line 159. The attribute's comment: “the projection”.

Forget the module and action of a finite projective representation, retaining its coefficient algebra.

public def projection :
    FiniteProjectiveRepresentation.{u, v, w, m} Λ k Γ ⥤
      ArtinianLocalAlgCat.{u, v, w} Λ k

Deformation.Examples.FiniteProjectiveRepresentation.projection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/RepresentationsCofibered.lean, line 170. The attribute's comment: “cofibered in groupoids”.

The category of finite projective representations is cofibered in groupoids over the category of Artinian local coefficient algebras.

public theorem projection_isCofiberedInGroupoids :
    IsCofiberedInGroupoids
      (projection (Λ := Λ) (k := k) (Γ := Γ) :
        FiniteProjectiveRepresentation.{u, v, w, max v m} Λ k Γ ⥤
          ArtinianLocalAlgCat.{u, v, w} Λ k)

Deformation.RepresentationCategory, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Basic.lean, line 58. The attribute's comment: “second presentation: representation_category, objects”.

A finite projective representation of Γ over an Artinian local Λ-algebra with residue field k.

structure RepresentationCategory.{u', v', w', m', x'}
    (Λ : Type u') (k : Type w') (Γ : Type x') [CommRing Λ] [Field k] [Algebra Λ k]
    [Group Γ]

Deformation.RepresentationCategory.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Basic.lean, line 78. The attribute's comment: “second presentation: representation_category, morphisms”.

A morphism of finite projective representations with varying coefficient ring.

structure Hom {Λ : Type u} {k : Type w} {Γ : Type x} [CommRing Λ] [Field k] [Algebra Λ k]
    [Group Γ] (X Y : RepresentationCategory.{u, v, w, m, x} Λ k Γ)

Deformation.RepresentationCategory.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Basic.lean, line 127. The attribute's comment: “second presentation: representation_category”.

The category structure on finite projective representations with varying coefficient algebra.

instance instCategory {Λ : Type u} {k : Type w} {Γ : Type x} [CommRing Λ] [Field k]
    [Algebra Λ k] [Group Γ] : Category (RepresentationCategory.{u, v, w, m, x} Λ k Γ)

Deformation.representationProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Basic.lean, line 187. The attribute's comment: “second presentation: representation_category”.

The coefficient algebra underlying a finite projective representation, as a functor.

def representationProjection {Λ : Type u} {k : Type w} {Γ : Type x} [CommRing Λ]
    [Field k] [Algebra Λ k] [Group Γ] :
    RepresentationCategory.{u, v, w, m, x} Λ k Γ ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k

Deformation.RepresentationCategory.specialFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Basic.lean, line 214. The attribute's comment: “second presentation: representation_deformation_category”.

The representation (V, ρ₀) over the residue field k, viewed as the special-fibre object of the category ℱ.

noncomputable def specialFiber {Λ : Type u} {k : Type w} {Γ : Type x} [CommRing Λ]
    [Field k] [Algebra Λ k] [Group Γ] (V : Type m) [AddCommGroup V] [Module k V]
    [Module.Finite k V] (ρ₀ : Representation k Γ V) :
    RepresentationCategory.{u, w, w, m, x} Λ k Γ

Deformation.RepresentationCategory.deformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Basic.lean, line 224. The attribute's comment: “second presentation: representation_deformation_category”.

The category of deformations of a finite-dimensional representation of Γ.

abbrev deformationCategory {Λ : Type u} {k : Type w} {Γ : Type x} [CommRing Λ] [Field k]
    [Algebra Λ k] [Group Γ] (V : Type m) [AddCommGroup V] [Module k V]
    [Module.Finite k V] (ρ₀ : Representation k Γ V)

Deformation.deformationCategoryProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Basic.lean, line 234. The attribute's comment: “second presentation: representation_deformation_category”.

The coefficient algebra of a deformation of ρ₀, as a functor from the deformation category of ρ₀ to 𝒞_Λ.

noncomputable def deformationCategoryProjection {Λ : Type u} {k : Type w} {Γ : Type x}
    [CommRing Λ] [Field k] [Algebra Λ k] [Group Γ] (V : Type m) [AddCommGroup V]
    [Module k V] [Module.Finite k V] (ρ₀ : Representation k Γ V) :
    RepresentationCategory.deformationCategory (Λ := Λ) V ρ₀ ⥤
      ArtinianLocalAlgCat.{u, w, w} Λ k

Deformation.RepresentationCategory.representationProjection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Cofibered.lean, line 260. The attribute's comment: “second presentation: representation_category”.

The category of finite projective representations is cofibered in groupoids over the category of Artinian local coefficient algebras.

theorem representationProjection_isCofiberedInGroupoids :
    IsCofiberedInGroupoids
      (representationProjection.{u, v, w, m, x} (Λ := Λ) (k := k) (Γ := Γ))

Tag 0DVS, a lemma

Tag 0DVS in the Stacks Project.

Deformation.Examples.FiniteProjectiveRepresentation.satisfiesRS_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/RepresentationsRimSchlessinger.lean, line 546. The attribute's comment: “Rim-Schlessinger condition”.

Finite projective representations satisfy the Rim–Schlessinger condition.

public theorem satisfiesRS_projection
    {Λ : Type u} {k : Type w} {Γ : Type*}
    [CommRing Λ] [Field k] [Algebra Λ k] [Group Γ] :
    SatisfiesRS
      (FiniteProjectiveRepresentation.projection.{u, v, w, max v m}
        (Λ := Λ) (k := k) (Γ := Γ))

Deformation.Examples.FiniteProjectiveRepresentation.isDeformationCategory_deformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/RepresentationsRimSchlessinger.lean, line 581. The attribute's comment: “deformation category”.

The deformations of a finite-dimensional representation form a deformation category.

public theorem isDeformationCategory_deformationCategory
    {Λ : Type u} {k : Type w} {Γ : Type*}
    [CommRing Λ] [Field k] [Algebra Λ k] [Group Γ]
    (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) :
    IsDeformationCategory
      (objectsOverFunctor
        (FiniteProjectiveRepresentation.projection.{u, w, w, m}
          (Λ := Λ) (k := k) (Γ := Γ))
        (FiniteProjectiveRepresentation.specialFiber (Λ := Λ) V ρ₀))

Tag 0DVT, a lemma

Tag 0DVT in the Stacks Project.

Deformation.finiteDimensional_tangentSpace_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Hull.lean, line 98. The attribute's comment: “clause 5: T Def_{V,ρ₀} is finite dimensional over k when Γ is finitely generated, for the canonical vector space structure of Stacks 06IH. The hypothesis Group.FG Γ is what separates this from clause 4, which holds for every Γ”.

The tangent space of the deformation category of a finite-dimensional representation of a finitely generated group is finite dimensional over k, for the canonical vector space structure of Stacks 06IH.

theorem finiteDimensional_tangentSpace_representation (V : Type m) [AddCommGroup V] [Module k V]
    [Module.Finite k V] [Group.FG Γ] (ρ₀ : Representation k Γ V) :
    let 𝓕 := BasedCategory.ofFunctor (deformationCategoryProjection (Λ := Λ) V ρ₀)
    let ee := tangentSpaceEquivSelfExt (Λ := Λ) V ρ₀
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨ee.1⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 ee.1.cofibered))) := ⟨ee.2.1⟩
    FiniteDimensional k (artinianTangentSpace Λ k (isomorphismClasses 𝓕 ee.1.cofibered))

Deformation.infinitesimalAutomorphismsEquivH0, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/InfinitesimalAutomorphisms.lean, line 589. The attribute's comment: “clause 3: Inf Def_{V,ρ₀} = H⁰(Γ, End_k(V)), the infinitesimal automorphisms of the deformation category of a finite-dimensional representation ρ₀ are the Γ-invariant k-endomorphisms of V, i.e. the ψ with id + εψ an automorphism of V ⊗_k k[ε]”.

The infinitesimal automorphisms of the deformation category of a finite-dimensional representation ρ₀ are the degree-zero group cohomology of the conjugation action on its endomorphisms.

noncomputable def infinitesimalAutomorphismsEquivH0
    (V : Type w) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V)
    {A₀ Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
    {x₀ : (deformationCategoryProjection (Λ := Λ) V ρ₀).Fiber A₀}
    {xε : (deformationCategoryProjection (Λ := Λ) V ρ₀).Fiber Aε}
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1)
    (hi : (deformationCategoryProjection (Λ := Λ) V ρ₀).IsHomLift g i) :
    ↥(infinitesimalAutomorphisms
        (deformationCategoryProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀)
        g e hpair i hi) ≃*
      Multiplicative (groupCohomology (Rep.of (Representation.linHom ρ₀ ρ₀)) 0)

Deformation.exists_infinitesimalAutomorphismsLinearEquivH0, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/InfinitesimalAutomorphisms.lean, line 659. The attribute's comment: “clause 4: Inf Def_{V,ρ₀} is ALWAYS finite dimensional over k, with no hypothesis whatsoever on Γ. Stated of Inf Def_{V,ρ₀} itself, which is a subgroup of an automorphism group and so is given here the k-vector space structure the claim needs: addition is composition of automorphisms and the clause-3 identification with H⁰(Γ, End_k(V)) is k-linear. Contrast clause 5, where Γ must be finitely generated”.

Stacks 0DVT, the finiteness clause for infinitesimal automorphisms, stated of Inf Def_{V,ρ₀} itself: the group of infinitesimal automorphisms of the deformation category of a finite-dimensional representation carries a k-vector space structure whose addition is composition of automorphisms, for which the identification of clause 3 with H⁰(Γ, End_k(V)) is k-linear, and it is always finite dimensional over k — no hypothesis whatsoever on the group Γ.

Inf Def_{V,ρ₀} is presented as a subgroup of the automorphism group of a dual-number pushforward (Deformation.infinitesimalAutomorphisms), so it carries no k-module structure to begin with and FiniteDimensional k does not even typecheck on it. The structure is therefore produced here, exactly as in Stacks 0DVQ's version of the same statement for finite projective modules (Deformation.Examples.FiniteProjectiveModule.exists_infinitesimalAutomorphismsLinearEquivEnd), and it is pinned: addition is composition, which fixes the additive group, and the k-linear equivalence is required to be the group isomorphism Deformation.infinitesimalAutomorphismsEquivH0 of clause 3, which fixes the scalar action. Compare Stacks 06JV (1), which puts the same structure on the tangent space at the identity of the automorphism functor of a category cofibered in groupoids satisfying (RS).

Finite dimensionality is then Deformation.finiteDimensional_groupCohomology_zero_linHom transported along that equivalence. This is in contrast with the tangent space, whose finiteness needs Γ to be finitely generated (Deformation.finiteDimensional_tangentSpace_representation).

theorem exists_infinitesimalAutomorphismsLinearEquivH0
    (V : Type w) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V)
    {A₀ Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
    {x₀ : (deformationCategoryProjection (Λ := Λ) V ρ₀).Fiber A₀}
    {xε : (deformationCategoryProjection (Λ := Λ) V ρ₀).Fiber Aε}
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1)
    (hi : (deformationCategoryProjection (Λ := Λ) V ρ₀).IsHomLift g i) :
    ∃ A : AddCommGroup ↥(infinitesimalAutomorphisms
        (deformationCategoryProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀)
        g e hpair i hi),
      letI := A
      ∃ _ : Module k ↥(infinitesimalAutomorphisms
          (deformationCategoryProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀)
          g e hpair i hi),
        (∀ a b : ↥(infinitesimalAutomorphisms
            (deformationCategoryProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀)
            g e hpair i hi), a + b = a * b) ∧
        (∃ L : ↥(infinitesimalAutomorphisms
              (deformationCategoryProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀)
              g e hpair i hi) ≃ₗ[k]
            groupCohomology (Rep.of (Representation.linHom ρ₀ ρ₀)) 0,
          ∀ a, Multiplicative.ofAdd (L a) =
            infinitesimalAutomorphismsEquivH0 (Λ := Λ) V ρ₀ g e hpair i hi a) ∧
        FiniteDimensional k ↥(infinitesimalAutomorphisms
          (deformationCategoryProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀)
          g e hpair i hi)

Deformation.selfExtEquivGroupCohomologyOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/SelfExtGroupCohomology.lean, line 74. The attribute's comment: “clause 2: Ext¹_{k[Γ]}(V, V) = H¹(Γ, End_k(V)) for the conjugation action of Γ on End_k(V), over the k[Γ]-module attached to ρ₀ by Rep.equivalenceModuleMonoidAlgebra, which is the module clause 1 states its Ext¹ over. No hypothesis on Γ”.

Stacks 0DVT. The first self-extension group over the group algebra of a finite-dimensional representation ρ₀ of Γ on V is the first group cohomology of the conjugation action of Γ on End_k(V):

Ext¹_{k[Γ]}(V, V) = H¹(Γ, End_k(V)).

The extension group is taken over the k[Γ]-module attached to ρ₀, which is the module over which the tangent-space clause Deformation.tangentSpaceEquivSelfExt of the same tag is stated. No hypothesis on Γ is needed.

def selfExtEquivGroupCohomologyOne (V : Type w) [AddCommGroup V] [Module k V]
    [Module.Finite k V] (ρ₀ : Representation k Γ V) :
    Abelian.Ext
        ((Rep.equivalenceModuleMonoidAlgebra (k := k) (G := Γ)).functor.obj (Rep.of ρ₀))
        ((Rep.equivalenceModuleMonoidAlgebra (k := k) (G := Γ)).functor.obj (Rep.of ρ₀)) 1 ≃ₗ[k]
      (groupCohomology (Rep.of (Representation.linHom ρ₀ ρ₀)) 1 : Type w)

Deformation.tangentSpaceEquivSelfExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/TangentSelfExt/Linearity.lean, line 514. The attribute's comment: “clause 1: T Def_{V,ρ₀} = Ext¹_{k[Γ]}(V, V), the tangent space of the deformation category of a finite-dimensional representation ρ₀ is its first self-extension group over the group algebra. The identification of that Ext¹ with H¹(Γ, End_k(V)) is clause 2, Deformation.selfExtEquivGroupCohomologyOne”.

The canonical tangent space of a finite-dimensional representation deformation category is linearly equivalent to its first self-Ext over the group algebra.

public noncomputable def tangentSpaceEquivSelfExt
    {Λ : Type u} {k : Type w} {Γ : Type*}
    [CommRing Λ] [Field k] [Algebra Λ k] [Group Γ]
    (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) :
    let p := deformationCategoryProjection (Λ := Λ) V ρ₀
    let 𝓕 := BasedCategory.ofFunctor p
    let M₀ := (Rep.equivalenceModuleMonoidAlgebra (k := k) (G := Γ)).functor.obj
      (Rep.of ρ₀)
    let E := Abelian.Ext M₀ M₀ 1
    Σ' (hpre : Deformation.IsPredeformationCategory 𝓕.p)
      (hS2 : Deformation.SchlessingerConditionS2
        (CategoryOfElements.π
          (Deformation.isomorphismClasses 𝓕 hpre.cofibered))),
      letI : Fact (Deformation.IsPredeformationCategory 𝓕.p) := ⟨hpre⟩
      letI : Fact (Deformation.SchlessingerConditionS2
        (CategoryOfElements.π
          (Deformation.isomorphismClasses 𝓕 hpre.cofibered))) := ⟨hS2⟩
      letI : AddCommGroup
        (Deformation.artinianTangentSpace Λ k
          (Deformation.isomorphismClasses 𝓕 hpre.cofibered)) :=
        Deformation.associatedTangentSpaceAddCommGroupUnlifted 𝓕
      letI : Module k
        (Deformation.artinianTangentSpace Λ k
          (Deformation.isomorphismClasses 𝓕 hpre.cofibered)) :=
        Deformation.associatedTangentSpaceModuleUnlifted 𝓕
      { L : Deformation.artinianTangentSpace Λ k
          (Deformation.isomorphismClasses 𝓕 hpre.cofibered) ≃ₗ[k] E //
        (∀ x : p.Fiber (Deformation.augmentedDualNumbers (Λ := Λ) (k := k)),
          ∃ (M : ModuleCat (MonoidAlgebra k Γ)) (f : M₀ ⟶ M) (g : M ⟶ M₀)
            (hfg : f ≫ g = 0),
            (ShortComplex.mk f g hfg).ShortExact ∧
              IsAssociatedSelfExtension V ρ₀ x M f g) ∧
        (∀ (x : p.Fiber (Deformation.augmentedDualNumbers (Λ := Λ) (k := k)))
          (M : ModuleCat (MonoidAlgebra k Γ)) (f : M₀ ⟶ M) (g : M ⟶ M₀)
          (hfg : f ≫ g = 0) (hexact : (ShortComplex.mk f g hfg).ShortExact),
          IsAssociatedSelfExtension V ρ₀ x M f g →
            L (Deformation.classOf 𝓕 hpre.cofibered x) = hexact.extClass) }

Tag 0ET1, a lemma

Tag 0ET1 in the Stacks Project.

Deformation.exists_hull_isomorphismClasses_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Hull.lean, line 121. The attribute's comment: “representation_hull”.

The functor of isomorphism classes of deformations of a finite-dimensional representation of a finitely generated group over a classical base has a hull: a versal formal object with bijective differential.

theorem exists_hull_isomorphismClasses_representation (V : Type m) [AddCommGroup V] [Module k V]
    [Module.Finite k V] [Group.FG Γ] (ρ₀ : Representation k Γ V) (hΛ : IsClassical Λ k) :
    let 𝓕 := BasedCategory.ofFunctor (deformationCategoryProjection (Λ := Λ) V ρ₀)
    let hpre := (tangentSpaceEquivSelfExt (Λ := Λ) V ρ₀).1
    let F := isomorphismClasses 𝓕 hpre.cofibered
    ∃ ξ : FormalObject (CategoryOfElements.π F),
      IsVersal (categoryOfElements_projection_isCofibered F) ξ ∧
        HasBijectiveDifferential (categoryOfElements_projection_isCofibered F) ξ

Deformation.isProrepresentableULift_isomorphismClasses_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Representation/Prorepresentable.lean, line 323. The attribute's comment: “prorepresentability”.

Stacks 0ET1, prorepresentability: the functor of isomorphism classes of deformations of a finite-dimensional representation of a finitely generated group over a classical base is prorepresentable, as soon as the Γ-equivariant endomorphisms of the representation are exactly the scalars, that is H⁰(Γ, End_k(V)) = k.

Prorepresentability is stated in the universe-raised form Deformation.IsProrepresentableULift, because the values of the functor of isomorphism classes lie in the universe of the objects of the deformation category rather than in the morphism universe of 𝒞_Λ. The functor is the one whose hull is Deformation.exists_hull_isomorphismClasses_representation, the other clause of this tag.

public theorem isProrepresentableULift_isomorphismClasses_representation
    (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V] [Group.FG Γ]
    (ρ₀ : Representation k Γ V) (hΛ : IsClassical Λ k)
    (h : ∀ f : IntertwiningMap ρ₀ ρ₀,
      ∃! a : k, (a • LinearMap.id : Module.End k V) = f.toLinearMap) :
    IsProrepresentableULift (isomorphismClasses
      (BasedCategory.ofFunctor (deformationCategoryProjection (Λ := Λ) V ρ₀))
      (isDeformationCategory_deformationCategoryProjection
        (Λ := Λ) V ρ₀).predeformation.cofibered)

Sources

LeanDeformation.Examples.FiniteProjectiveRepresentation · Deformation.Examples.FiniteProjectiveRepresentation.Hom · Deformation.Examples.FiniteProjectiveRepresentation.instCategory · Deformation.Examples.FiniteProjectiveRepresentation.specialFiber · Deformation.Examples.FiniteProjectiveRepresentation.deformationCategory · Deformation.Examples.FiniteProjectiveRepresentation.projection · Deformation.Examples.FiniteProjectiveRepresentation.projection_isCofiberedInGroupoids · Deformation.RepresentationCategory

Section93.6 Continuous representations #

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

Tag 0D3K, an example

Tag 0D3K in the Stacks Project.

Deformation.Examples.continuous_representation_iff_continuousSMul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentations.lean, line 45. The attribute's comment: “continuity_equivalence”.

For a finitely generated module over a semiring, a representation is continuous into the discrete general linear group if and only if the induced action on the discrete module is continuous.

public theorem continuous_representation_iff_continuousSMul
    (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M]
    (Γ : Type*) [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ]
    (ρ : Γ →* LinearMap.GeneralLinearGroup R M) :
    letI : TopologicalSpace (LinearMap.GeneralLinearGroup R M) := ⊥
    letI : TopologicalSpace M := ⊥
    letI : MulAction Γ M := MulAction.compHom M ρ
    Continuous ρ ↔ ContinuousSMul Γ M

Deformation.Examples.FiniteProjectiveRepresentation.continuousObjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsCofibered.lean, line 114. The attribute's comment: “continuous_representation_category”.

The objects of the category of finite projective representations of Stacks 0D3J whose representation is continuous. The category ℱ of Stacks 0D3K is the full subcategory they span.

public def continuousObjects (Λ : Type u) (k : Type w) (Γ : Type*) [CommRing Λ] [Field k]
    [Algebra Λ k] [Group Γ] [TopologicalSpace Γ] :
    ObjectProperty (FiniteProjectiveRepresentation.{u, v, w, m} Λ k Γ)

Deformation.Examples.FiniteProjectiveRepresentation.continuousProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsCofibered.lean, line 152. The attribute's comment: “continuous_representation_category”.

The functor remembering only the coefficient algebra of a continuous finite projective representation.

public def continuousProjection :
    (continuousObjects.{u, v, w, m} Λ k Γ).FullSubcategory ⥤
      ArtinianLocalAlgCat.{u, v, w} Λ k

Deformation.Examples.FiniteProjectiveRepresentation.continuousProjection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsCofibered.lean, line 175. The attribute's comment: “continuous_representation_category”.

The category of continuous finite projective representations is cofibered in groupoids over the category of Artinian local coefficient algebras: the pushforward of a continuous representation is continuous, and fill-ins are those of the ambient category.

public theorem continuousProjection_isCofiberedInGroupoids
    (hp : IsCofiberedInGroupoids
      (projection (Λ := Λ) (k := k) (Γ := Γ) :
        FiniteProjectiveRepresentation.{u, v, w, m} Λ k Γ ⥤
          ArtinianLocalAlgCat.{u, v, w} Λ k)) :
    IsCofiberedInGroupoids (continuousProjection.{u, v, w, m} (Λ := Λ) (k := k) (Γ := Γ))

Deformation.Examples.FiniteProjectiveRepresentation.continuousSpecialFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsCofibered.lean, line 186. The attribute's comment: “continuous_representation_deformation_category”.

The continuous representation (V, ρ₀) over the residue field k, viewed as the special-fibre object (k, V, ρ₀) of the category of continuous representations.

public noncomputable def continuousSpecialFiber (V : Type m) [AddCommGroup V] [Module k V]
    [Module.Finite k V] (ρ₀ : Representation k Γ V)
    (hρ₀ : IsContinuousRepresentation ρ₀) :
    (continuousObjects.{u, w, w, m} Λ k Γ).FullSubcategory

Deformation.Examples.FiniteProjectiveRepresentation.continuousDeformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsCofibered.lean, line 195. The attribute's comment: “continuous_representation_deformation_category”.

The category of deformations of a finite-dimensional continuous representation of Γ.

public abbrev continuousDeformationCategory (V : Type m) [AddCommGroup V]
    [Module k V] [Module.Finite k V] (ρ₀ : Representation k Γ V)
    (hρ₀ : IsContinuousRepresentation ρ₀)

Deformation.Examples.FiniteProjectiveRepresentation.isCofiberedInGroupoids_continuousProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsCofiberedUnconditional.lean, line 115. The attribute's comment: “continuous_representation_category: p is cofibred in groupoids”.

The functor p : ℱ → 𝒞_Λ sending a continuous finite projective representation (A, M, ρ) of the topological group Γ to its coefficient algebra A is cofibered in groupoids, for an arbitrary module universe and with no hypothesis on the ambient projection of finite projective representations.

public theorem isCofiberedInGroupoids_continuousProjection :
    IsCofiberedInGroupoids (continuousProjection.{u, v, w, m} (Λ := Λ) (k := k) (Γ := Γ))

Deformation.Examples.isContinuousRepresentation_iff_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsGModule.lean, line 59. The attribute's comment: “continuity_equivalence”.

The footnote of Stacks 0D3K. For a finite module over a commutative ring, a representation of a topological group is continuous into the general linear group with the discrete topology exactly when the module, with the action given by the representation, is an A-Γ-module in the sense of Stacks 04JP.

public theorem isContinuousRepresentation_iff_isContinuous
    {R : Type u} [CommRing R] {Γ : Type v} [Group Γ] [TopologicalSpace Γ]
    [IsTopologicalGroup Γ] {M : Type w} [AddCommGroup M] [Module R M] [Module.Finite R M]
    (ρ : Representation R Γ M) :
    IsContinuousRepresentation ρ ↔
      (Stacks.GroupCohomology.actionOfRepresentation R Γ M ρ).IsContinuous

Tag 0DVV, a lemma

Tag 0DVV in the Stacks Project.

Deformation.Examples.FiniteProjectiveRepresentation.satisfiesRS_continuousProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsRimSchlessinger.lean, line 167. The attribute's comment: “Rim-Schlessinger condition”.

Continuous finite projective representations of a topological group satisfy the Rim–Schlessinger condition.

public theorem satisfiesRS_continuousProjection {Λ : Type u} {k : Type w} {Γ : Type*}
    [CommRing Λ] [Field k] [Algebra Λ k] [Group Γ] [TopologicalSpace Γ] :
    SatisfiesRS
      (continuousProjection.{u, v, w, max v m} (Λ := Λ) (k := k) (Γ := Γ))

Deformation.Examples.FiniteProjectiveRepresentation.isDeformationCategory_continuousDeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsRimSchlessinger.lean, line 187. The attribute's comment: “deformation category”.

The deformations of a finite-dimensional continuous representation of a topological group form a deformation category.

public theorem isDeformationCategory_continuousDeformationCategory {Λ : Type u} {k : Type w}
    {Γ : Type*} [CommRing Λ] [Field k] [Algebra Λ k] [Group Γ] [TopologicalSpace Γ]
    (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) (hρ₀ : IsContinuousRepresentation ρ₀) :
    IsDeformationCategory
      (objectsOverFunctor
        (continuousProjection.{u, w, w, m} (Λ := Λ) (k := k) (Γ := Γ))
        (continuousSpecialFiber (Λ := Λ) V ρ₀ hρ₀))

Tag 0DVW, a lemma

Tag 0DVW in the Stacks Project.

Deformation.Examples.FiniteProjectiveRepresentation.continuousInfinitesimalAutomorphismsEquivH0, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsInfinitesimalAutomorphisms.lean, line 304. The attribute's comment: “Inf”.

The infinitesimal automorphisms of the deformation category of a finite-dimensional continuous representation ρ₀ of a topological group are the degree-zero cohomology of the conjugation action on its endomorphisms, H⁰(Γ, End_k(V)).

public noncomputable def continuousInfinitesimalAutomorphismsEquivH0
    (V : Type w) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) (hρ₀ : IsContinuousRepresentation ρ₀)
    {A₀ Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
    {x₀ : (continuousDeformationProjection (Λ := Λ) V ρ₀ hρ₀).Fiber A₀}
    {xε : (continuousDeformationProjection (Λ := Λ) V ρ₀ hρ₀).Fiber Aε}
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1)
    (hi : (continuousDeformationProjection (Λ := Λ) V ρ₀ hρ₀).IsHomLift g i) :
    ↥(infinitesimalAutomorphisms
        (continuousDeformationProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀ hρ₀)
        g e hpair i hi) ≃*
      Multiplicative (groupCohomology (Rep.of (Representation.linHom ρ₀ ρ₀)) 0)

Deformation.Examples.FiniteProjectiveRepresentation.finiteDimensional_continuousInfinitesimalAutomorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsInfinitesimalAutomorphisms.lean, line 341. The attribute's comment: “Inf is always finite dimensional”.

Stacks 0DVW, the clause that the infinitesimal automorphisms are always finite dimensional: the infinitesimal automorphism group of the deformation category of a finite-dimensional continuous representation ρ₀ carries a k-vector space structure whose addition is composition of automorphisms, and that vector space is finite dimensional.

No hypothesis on Γ is needed. The group is H⁰(Γ, End_k(V)) by continuousInfinitesimalAutomorphismsEquivH0, and degree-zero cohomology is the subspace of Γ-invariants of End_k(V), which is finite dimensional because V is.

public theorem finiteDimensional_continuousInfinitesimalAutomorphisms
    (V : Type w) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) (hρ₀ : IsContinuousRepresentation ρ₀)
    {A₀ Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
    {x₀ : (continuousDeformationProjection (Λ := Λ) V ρ₀ hρ₀).Fiber A₀}
    {xε : (continuousDeformationProjection (Λ := Λ) V ρ₀ hρ₀).Fiber Aε}
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1)
    (hi : (continuousDeformationProjection (Λ := Λ) V ρ₀ hρ₀).IsHomLift g i) :
    let G := ↥(infinitesimalAutomorphisms
      (continuousDeformationProjection_isCofiberedInGroupoids (Λ := Λ) V ρ₀ hρ₀)
      g e hpair i hi)
    ∃ hA : AddCommGroup G,
      letI := hA
      ∃ hM : Module k G,
        letI := hM
        (∀ a b : G, a + b = a * b) ∧ FiniteDimensional k G

Deformation.Examples.FiniteProjectiveRepresentation.finiteDimensional_continuousTangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsInfinitesimalAutomorphisms.lean, line 405. The attribute's comment: “the tangent space is finite dimensional”.

Stacks 0DVW, the tangent clause: for a topologically finitely generated topological group Γ the tangent space of the deformation category of a finite-dimensional continuous representation ρ₀ is finite dimensional over k.

Topological finite generation enters through a dense finitely generated subgroup H ≤ Γ. A continuous deformation is locally constant, so an H-equivariant map between two of them is Γ-equivariant: the agreement locus is closed and contains H. Hence restriction of the action to H is fully faithful, so its differential is an injective k-linear map from the tangent space into the tangent space of the deformation category of ρ₀|_H, and the latter is finite dimensional by Stacks 0DVT.

public theorem finiteDimensional_continuousTangentSpace
    (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) (hρ₀ : IsContinuousRepresentation ρ₀)
    (hΓ : ∃ H : Subgroup Γ, Group.FG ↥H ∧ Dense (H : Set Γ)) :
    let 𝓕 := BasedCategory.ofFunctor (Deformation.objectsOverFunctor
      (continuousProjection.{u, w, w, m} (Λ := Λ) (k := k) (Γ := Γ))
      (continuousSpecialFiber (Λ := Λ) V ρ₀ hρ₀))
    let hD := isDeformationCategory_continuousDeformationCategory (Λ := Λ) V ρ₀ hρ₀
    letI : Fact (Deformation.IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (Deformation.SchlessingerConditionS2 (CategoryOfElements.π
        (Deformation.isomorphismClasses 𝓕 hD.predeformation.cofibered))) :=
      ⟨Deformation.Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory
        𝓕 hD⟩
    FiniteDimensional k (Deformation.artinianTangentSpace Λ k
      (Deformation.isomorphismClasses 𝓕 hD.predeformation.cofibered))

Deformation.Examples.FiniteProjectiveRepresentation.tangentSpaceEquivContinuousCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsTangentSpace.lean, line 814. The attribute's comment: “tangent_space”.

Stacks 0DVW, the tangent clause. For a finite-dimensional continuous representation ρ₀ : Γ → GL_k(V) of a topological group, the tangent space of the deformation category of Stacks 0D3K — in its natural k-vector space structure of Stacks 06IH — is the first continuous cohomology H¹(Γ, End_k(V)) of the conjugation action on the endomorphisms of V.

The coefficient module is the dual tensor module Vᵛ ⊗_k V of Stacks 0DVE, and the second component of the statement identifies its representation equivariantly with Representation.linHom ρ₀ ρ₀, the conjugation action on End_k(V), so the cohomology on the right is H¹(Γ, End_k(V)).

The proof is the one of Stacks 0DVT: tangentSpaceEquivContinuousSelfExt identifies the tangent space with Ext¹ of V by itself in continuous discrete modules, and Stacks 0DVE turns that Ext¹ into continuous cohomology of Vᵛ ⊗_k V.

def tangentSpaceEquivContinuousCohomology [IsTopologicalGroup Γ]
    [HasDerivedCategory.{d} (Stacks.Injectives.ContinuousModule.{w, w, w} k Γ)]
    [HasDerivedCategory.{d} (ModuleCat.{w} k)]
    (V : Type w) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) (hρ₀ : IsContinuousRepresentation ρ₀) :
    let 𝓕 := BasedCategory.ofFunctor (continuousDeformationProjection (Λ := Λ) V ρ₀ hρ₀)
    let hD := isDeformationCategory_continuousDeformationCategory (Λ := Λ) V ρ₀ hρ₀
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (SchlessingerConditionS2
        (CategoryOfElements.π
          (isomorphismClasses 𝓕 hD.predeformation.cofibered))) :=
      ⟨Deformation.Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory
        𝓕 hD⟩
    letI := Stacks.ContinuousCohomology.hasExt_continuousModule.{w, w, w} k Γ
    let M := continuousModuleOfContinuousRepresentation V ρ₀ hρ₀
    letI : Module.Finite k (M.obj.obj.V : Type w) := inferInstanceAs (Module.Finite k V)
    letI : Module.Projective k (M.obj.obj.V : Type w) :=
      inferInstanceAs (Module.Projective k V)
    Σ' _ : artinianTangentSpace Λ k
          (isomorphismClasses 𝓕 hD.predeformation.cofibered) ≃ₗ[k]
        (Stacks.ContinuousCohomology.cohomologyFunctor.{d, w, w, w} k Γ 1).obj
          (Stacks.ContinuousCohomology.dualTensorContinuousModule k Γ M M),
      (Stacks.ContinuousCohomology.rep k Γ
        (Stacks.ContinuousCohomology.dualTensorContinuousModule k Γ M M)).Equiv
          (Representation.linHom ρ₀ ρ₀)

Tag 0ET2, a lemma

Tag 0ET2 in the Stacks Project.

Deformation.Examples.FiniteProjectiveRepresentation.exists_hull_continuousIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsHull.lean, line 529. The attribute's comment: “the functor has a hull”.

Stacks 0ET2, the hull: the functor of isomorphism classes of deformations of a finite-dimensional continuous representation of a topologically finitely generated group over a classical base has a hull, that is a versal formal object with bijective differential.

Both hypotheses of Stacks 06IZ beyond the Rim–Schlessinger property are discharged: condition (S1) and (S2) come from the deformation-category property of the continuous deformations of ρ₀, and the finite-dimensionality of the tangent space is the tangent clause of Stacks 0DVW.

public theorem exists_hull_continuousIsomorphismClasses
    (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) (hρ₀ : IsContinuousRepresentation ρ₀)
    (hΛ : IsClassical Λ k)
    (hΓ : ∃ H : Subgroup Γ, Group.FG ↥H ∧ Dense (H : Set Γ)) :
    let 𝓕 := BasedCategory.ofFunctor (objectsOverFunctor
      (continuousProjection.{u, w, w, m} (Λ := Λ) (k := k) (Γ := Γ))
      (continuousSpecialFiber (Λ := Λ) V ρ₀ hρ₀))
    let hpre := (isDeformationCategory_continuousDeformationCategory
      (Λ := Λ) V ρ₀ hρ₀).predeformation
    let F := isomorphismClasses 𝓕 hpre.cofibered
    ∃ ξ : FormalObject (CategoryOfElements.π F),
      IsVersal (categoryOfElements_projection_isCofibered F) ξ ∧
        HasBijectiveDifferential (categoryOfElements_projection_isCofibered F) ξ

Deformation.Examples.FiniteProjectiveRepresentation.isProrepresentableULift_continuousIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/ContinuousRepresentationsHull.lean, line 581. The attribute's comment: “prorepresentability”.

Stacks 0ET2, prorepresentability: the functor of isomorphism classes of deformations of a finite-dimensional continuous representation of a topologically finitely generated group over a classical base is prorepresentable, as soon as the Γ-equivariant endomorphisms of the representation are exactly the scalars, that is H⁰(Γ, End_k(V)) = k.

Prorepresentability is stated in the universe-raised form Deformation.IsProrepresentableULift, because the values of the functor of isomorphism classes lie in the universe of the objects of the deformation category rather than in the morphism universe of 𝒞_Λ.

public theorem isProrepresentableULift_continuousIsomorphismClasses
    (V : Type m) [AddCommGroup V] [Module k V] [Module.Finite k V]
    (ρ₀ : Representation k Γ V) (hρ₀ : IsContinuousRepresentation ρ₀)
    (hΛ : IsClassical Λ k)
    (h : ∀ f : IntertwiningMap ρ₀ ρ₀,
      ∃! a : k, (a • LinearMap.id : Module.End k V) = f.toLinearMap)
    (hΓ : ∃ H : Subgroup Γ, Group.FG ↥H ∧ Dense (H : Set Γ)) :
    IsProrepresentableULift (isomorphismClasses
      (BasedCategory.ofFunctor (objectsOverFunctor
        (continuousProjection.{u, w, w, m} (Λ := Λ) (k := k) (Γ := Γ))
        (continuousSpecialFiber (Λ := Λ) V ρ₀ hρ₀)))
      (isDeformationCategory_continuousDeformationCategory
        (Λ := Λ) V ρ₀ hρ₀).predeformation.cofibered)

Sources

Section93.7 Graded algebras #

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

Tag 0D3L, an example

Tag 0D3L in the Stacks Project.

Deformation.Examples.ProjectiveGradedAlgebra, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebras.lean, line 52. The attribute's comment: “graded_algebra_deformation_category: objects”.

A commutative graded algebra, finite projective in every degree, over an object of the category 𝒞_Λ of Artinian local Λ-algebras with residue field k.

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

Deformation.Examples.ProjectiveGradedAlgebra.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebras.lean, line 74. The attribute's comment: “graded_algebra_deformation_category: morphisms”.

A base-change morphism between graded algebras over varying base algebras: a graded ring map, semilinear over a morphism of base algebras, exhibiting the target as an extension of scalars of the source.

public structure Hom {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (X Y : ProjectiveGradedAlgebra.{u, v, w, m} Λ k)

Deformation.Examples.ProjectiveGradedAlgebra.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebras.lean, line 95. The attribute's comment: “graded_algebra_deformation_category: category structure”.

The category structure on graded algebras over the algebras of 𝒞_Λ.

public instance instCategory {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] :
    Category (ProjectiveGradedAlgebra.{u, v, w, m} Λ k)

Deformation.Examples.ProjectiveGradedAlgebra.projection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebras.lean, line 142. The attribute's comment: “graded_algebra_deformation_category: projection”.

The base-algebra projection.

public def projection {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] :
    ProjectiveGradedAlgebra.{u, v, w, m} Λ k ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k

Deformation.Examples.ProjectiveGradedAlgebra.specialFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebras.lean, line 151. The attribute's comment: “graded_algebra_deformation_category: special fiber”.

A graded algebra over k viewed as the distinguished special-fibre object.

public noncomputable def specialFiber {Λ : Type u} {k : Type w}
    [CommRing Λ] [Field k] [Algebra Λ k]
    (P : Type m) [CommRing P] [Algebra k P]
    (grading : ℕ → Submodule k P) [GradedAlgebra grading]
    [∀ d, Module.Finite k (grading d)] : ProjectiveGradedAlgebra.{u, w, w, m} Λ k

Deformation.Examples.ProjectiveGradedAlgebra.deformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebras.lean, line 163. The attribute's comment: “graded_algebra_deformation_category”.

Deformations of a fixed graded k-algebra.

public abbrev deformationCategory {Λ : Type u} {k : Type w}
    [CommRing Λ] [Field k] [Algebra Λ k]
    (P : Type m) [CommRing P] [Algebra k P]
    (grading : ℕ → Submodule k P) [GradedAlgebra grading]
    [∀ d, Module.Finite k (grading d)]

Deformation.Examples.ProjectiveGradedAlgebra.deformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebras.lean, line 163. The attribute's comment: “graded_algebra_deformation_category: deformation category”.

Deformations of a fixed graded k-algebra.

public abbrev deformationCategory {Λ : Type u} {k : Type w}
    [CommRing Λ] [Field k] [Algebra Λ k]
    (P : Type m) [CommRing P] [Algebra k P]
    (grading : ℕ → Submodule k P) [GradedAlgebra grading]
    [∀ d, Module.Finite k (grading d)]

Deformation.Examples.ProjectiveGradedAlgebra.projection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebrasCofibered.lean, line 496.

The base-algebra projection of the category of graded algebras, finite projective in each degree, is cofibered in groupoids.

public theorem projection_isCofiberedInGroupoids :
    IsCofiberedInGroupoids
      (ProjectiveGradedAlgebra.projection.{u, v, w, max v m} (Λ := Λ) (k := k))

Tag 0DVY, a lemma

Tag 0DVY in the Stacks Project.

Deformation.Examples.ProjectiveGradedAlgebra.satisfiesRS_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebrasRimSchlessinger.lean, line 881. The attribute's comment: “Rim-Schlessinger condition”.

The category of graded algebras finite projective in each degree satisfies the Rim–Schlessinger condition.

public theorem satisfiesRS_projection
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] :
    SatisfiesRS
      (ProjectiveGradedAlgebra.projection.{u, v, w, max v m} (Λ := Λ) (k := k))

Deformation.Examples.ProjectiveGradedAlgebra.isDeformationCategory_deformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebrasRimSchlessinger.lean, line 932. The attribute's comment: “deformation category”.

The deformations of a fixed graded k-algebra, finite-dimensional in each degree, form a deformation category.

public theorem isDeformationCategory_deformationCategory
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (P : Type (max w m)) [CommRing P] [Algebra k P]
    (grading : ℕ → Submodule k P) [GradedAlgebra grading]
    [∀ d, Module.Finite k (grading d)] :
    IsDeformationCategory
      (objectsOverFunctor
        (ProjectiveGradedAlgebra.projection.{u, w, w, max w m} (Λ := Λ) (k := k))
        (specialFiber (Λ := Λ) P grading))

Tag 0DVZ, a lemma

Tag 0DVZ in the Stacks Project.

Deformation.Examples.ProjectiveGradedAlgebra.infinitesimalAutomorphismGroupEquivDegreeZeroDerivations, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebraDerivations.lean, line 837. The attribute's comment: “graded_inf_derivations”.

The infinitesimal automorphism group of the deformation category of a graded algebra is the additive group of degree-preserving derivations.

public noncomputable def infinitesimalAutomorphismGroupEquivDegreeZeroDerivations
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (P : Type (max w m)) [CommRing P] [Algebra k P]
    (grading : ℕ → Submodule k P) [GradedAlgebra grading]
    [∀ d, Module.Finite k (grading d)]
    {Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
    {x₀ : (objectsOverFunctor
      (ProjectiveGradedAlgebra.projection.{u, w, w, max w m} (Λ := Λ) (k := k))
      (specialFiber (Λ := Λ) P grading)).Fiber
        (residueFieldObject.{u, w, w} Λ k)}
    {xε : (objectsOverFunctor
      (ProjectiveGradedAlgebra.projection.{u, w, w, max w m} (Λ := Λ) (k := k))
      (specialFiber (Λ := Λ) P grading)).Fiber Aε}
    (g : residueFieldObject.{u, w, w} Λ k ⟶ Aε)
    (e : Aε ⟶ residueFieldObject.{u, w, w} Λ k)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1)
    (hi : (objectsOverFunctor
      (ProjectiveGradedAlgebra.projection.{u, w, w, max w m} (Λ := Λ) (k := k))
      (specialFiber (Λ := Λ) P grading)).IsHomLift g i) :
    infinitesimalAutomorphismGroup
      (isDeformationCategory_deformationCategory P grading).predeformation
      g e hpair i hi ≃*
      Multiplicative (degreeZeroDerivations grading)

Deformation.Examples.ProjectiveGradedAlgebra.gradedAlgebra_infinitesimalAutomorphisms_finiteDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebraDerivationsFiniteDimensional.lean, line 114. The attribute's comment: “graded_inf_finite”.

Stacks 0DVZ. The infinitesimal automorphisms of the deformation category of a graded algebra of finite type over a field, with finite-dimensional graded pieces, form a finite-dimensional vector space whose addition is composition of automorphisms.

public theorem gradedAlgebra_infinitesimalAutomorphisms_finiteDimensional
    {Λ : Type u} {k : Type w} [CommRing Λ] [IsNoetherianRing Λ]
    [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (P : Type (max w m)) [CommRing P] [Algebra k P]
    (grading : ℕ → Submodule k P) [GradedAlgebra grading]
    [∀ d, Module.Finite k (grading d)] [Algebra.FiniteType k P] :
    let p := objectsOverFunctor
      (ProjectiveGradedAlgebra.projection.{u, w, w, max w m} (Λ := Λ) (k := k))
      (specialFiber (Λ := Λ) P grading)
    let hp := (isDeformationCategory_deformationCategory (Λ := Λ) P grading).predeformation
    ∀ {Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
      {x₀ : p.Fiber (residueFieldObject.{u, w, w} Λ k)}
      {xε : p.Fiber Aε}
      (g : residueFieldObject.{u, w, w} Λ k ⟶ Aε)
      (e : Aε ⟶ residueFieldObject.{u, w, w} Λ k)
      (hpair : IsCanonicalDualNumberPair g e)
      (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i),
      let G := infinitesimalAutomorphismGroup hp g e hpair i hi
      ∃ hA : AddCommGroup G,
        letI := hA
        ∃ hM : Module k G,
          letI := hM
          (∀ a b : G, a + b = a * b) ∧ FiniteDimensional k G

Deformation.Examples.ProjectiveGradedAlgebra.finiteDimensional_tangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebraTangentRecord.lean, line 706. The attribute's comment: “graded_tangent_finite”.

The tangent-space half of Stacks 0DVZ. The tangent space of the deformation category of a graded k-algebra which is finite-dimensional in each degree and of finite type over k is finite-dimensional.

The proof is Stacks' own: choose a weighted graded presentation of P (GradedAlgebra.exists_weightedGradedPresentation), attach to a lift of P over k[V] the class in W ⊗[k] V of the vector of obstructions of the lifted relations, where W is the cokernel of the graded Jacobian of the presentation (Deformation.Examples.ProjectiveGradedAlgebra.tangentRecord), and feed that map, its naturality and its injectivity to Deformation.finiteDimensional_artinianTangentSpace_of_natural_injection through finiteDimensional_tangentSpace_of_gradedJacobian_natural_injection. W is finite-dimensional because each graded piece of P is.

theorem finiteDimensional_tangentSpace :
    letI p := objectsOverFunctor
      (ProjectiveGradedAlgebra.projection.{u, w, w, max w m} (Λ := Λ) (k := k))
      (specialFiber (Λ := Λ) P grading)
    letI 𝓕 := BasedCategory.ofFunctor p
    letI hD := isDeformationCategory_deformationCategory (Λ := Λ) P grading
    letI hS2 := Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory 𝓕 hD
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 hD.predeformation.cofibered))) := ⟨hS2⟩
    letI T := artinianTangentSpace Λ k (isomorphismClasses 𝓕 hD.predeformation.cofibered)
    letI : AddCommGroup T := associatedTangentSpaceAddCommGroupUnlifted 𝓕
    letI : Module k T := associatedTangentSpaceModuleUnlifted 𝓕
    FiniteDimensional k T

Tag 0ET3, a lemma

Tag 0ET3 in the Stacks Project.

Deformation.Examples.ProjectiveGradedAlgebra.exists_hull_isomorphismClasses_gradedAlgebra_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Linear/GradedAlgebraHull.lean, line 219. The attribute's comment: “Def_P of 0D3L: finite-dimensional graded pieces define it, not an extra hypothesis”.

Stacks 0ET3. In Example 0D3L, assume P is a finitely generated graded k-algebra and Λ → k is the classical case (Λ a Noetherian complete local ring with residue field k). Then the functor A ↦ Ob(Def_P(A))/≅ of isomorphism classes has a hull: a versal formal object with bijective differential.

The section variable [∀ d, Module.Finite k (grading d)] is Example 0D3L's standing condition defining Def_P. The source requires dim_k(P_d) < ∞ for all d ≥ 0 before it forms x_0 = (k, P) and sets Def_P = F_{x_0}, and specialFiber requires the same condition to build x_0. It is not a hypothesis added to 0ET3. The only hypotheses that 0ET3 adds to Example 0D3L are finite generation, which is [Algebra.FiniteType k P], and the classical case, which is hΛ.

The proof applies exists_hull_isomorphismClasses_gradedAlgebra. Its hypothesis on the tangent space comes from finiteDimensional_tangentSpace, the tangent-space clause of Stacks 0DVZ, through the comparison of the two tangent-space models.

public theorem exists_hull_isomorphismClasses_gradedAlgebra_of_finiteType
    [Algebra.FiniteType k P] (hΛ : IsClassical Λ k) :
    ∃ ξ : FormalObject (CategoryOfElements.π (Deformation.isomorphismClasses
        (BasedCategory.ofFunctor (deformationProjection (Λ := Λ) P grading))
        (isPredeformationCategory_deformationProjection (Λ := Λ) P grading).cofibered)),
      IsVersal (categoryOfElements_projection_isCofibered (Deformation.isomorphismClasses
          (BasedCategory.ofFunctor (deformationProjection (Λ := Λ) P grading))
          (isPredeformationCategory_deformationProjection (Λ := Λ) P grading).cofibered)) ξ ∧
        HasBijectiveDifferential
          (categoryOfElements_projection_isCofibered (Deformation.isomorphismClasses
            (BasedCategory.ofFunctor (deformationProjection (Λ := Λ) P grading))
            (isPredeformationCategory_deformationProjection (Λ := Λ) P grading).cofibered))
          ξ

Sources

Section93.8 Rings #

Section 93.8 of the Stacks Project, Tag 0DY0. 11 tags here are carried by 17 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DY1, an example

Tag 0DY1 in the Stacks Project.

Deformation.Examples.ringDeformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Rings.lean, line 182. The attribute's comment: “ring_deformation_category”.

The category of deformations of the k-algebra P: flat algebras over Artinian local bases equipped with a base-change map to (k, P).

abbrev ringDeformationCategory (P : Type w) [CommRing P] [Algebra k P]

Deformation.Examples.flatAlgebraCategory_projection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Rings.lean, line 189. The attribute's comment: “flat_algebra_category_cofibered”.

Base change makes the projection from flat algebras to their Artinian bases cofibered in groupoids.

theorem flatAlgebraCategory_projection_isCofiberedInGroupoids
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] :
    IsCofiberedInGroupoids (FlatAlgebraCategory.projection (Λ := Λ) (k := k))

Declarations registered for the tag:

FlatAlgebraCategory registered with add_to_stacks in StacksFrontier/Deformation/Examples/Geometric/Rings.lean, line 271 (StacksFrontier): “flat_algebra_category”.
FlatAlgebraCategory.Hom registered with add_to_stacks in StacksFrontier/Deformation/Examples/Geometric/Rings.lean, line 272 (StacksFrontier): “flat_algebra_category”.
FlatAlgebraCategory.instCategory registered with add_to_stacks in StacksFrontier/Deformation/Examples/Geometric/Rings.lean, line 273 (StacksFrontier): “flat_algebra_category”.
FlatAlgebraCategory.projection registered with add_to_stacks in StacksFrontier/Deformation/Examples/Geometric/Rings.lean, line 274 (StacksFrontier): “flat_algebra_category”.
residueFieldAlgebra, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/Examples/Geometric/Rings.lean, line 275 (StacksFrontier): “flat_algebra_category”.

Tag 0DY2, a lemma

Tag 0DY2 in the Stacks Project.

Deformation.Examples.flatAlgebraCategory_projection_satisfiesRS, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/FibreProduct/Deformations.lean, line 348. The attribute's comment: “Rim–Schlessinger condition”.

Flat algebras over Artinian local bases satisfy the Rim–Schlessinger condition.

theorem flatAlgebraCategory_projection_satisfiesRS
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] :
    SatisfiesRS (FlatAlgebraCategory.projection (Λ := Λ) (k := k))

Deformation.Examples.ringDeformationCategory_isDeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/FibreProduct/Deformations.lean, line 357. The attribute's comment: “deformation category”.

Deformations of any k-algebra form a deformation category.

theorem ringDeformationCategory_isDeformationCategory
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (P : Type w) [CommRing P] [Algebra k P] :
    IsDeformationCategory
      (objectsOverFunctor (FlatAlgebraCategory.projection (Λ := Λ) (k := k))
        (residueFieldAlgebra (Λ := Λ) (k := k) P))

Tag 0DY3, a lemma

Tag 0DY3 in the Stacks Project.

Deformation.Examples.exists_infinitesimalAutomorphismGroupMulEquivDerivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/RingsInfinitesimalAutomorphisms.lean, line 399. The attribute's comment: “infinitesimal automorphisms”. References: SGA 1 III (6.1), “special case”; SGA 3 VIIA (1.5), “partial”.

Stacks 0DY3. The infinitesimal automorphisms of the deformation category of a commutative k-algebra P are the k-derivations of P into itself.

The statement also records the coordinates in which this holds: for any point xε of the deformation category over the dual numbers and any lift i of the constant inclusion, there is a ring isomorphism c of the flat algebra of xε with P[ε] compatible with the reduction to P and carrying the lift to the constant inclusion, and the derivation attached to an infinitesimal automorphism is the ε-coefficient of its value on a constant. The scalar action of k on the derivations is reflected by the existence of a unique rescaled infinitesimal automorphism.

public theorem exists_infinitesimalAutomorphismGroupMulEquivDerivation
    {Λ : Type u} {k P : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    [CommRing P] [Algebra k P] :
    ∃ hp : IsPredeformationCategory (ringDeformationProjection Λ k P),
      ∀ {Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
        {x₀ : (ringDeformationProjection Λ k P).Fiber (residueFieldObject.{u, w, w} Λ k)}
        {xε : (ringDeformationProjection Λ k P).Fiber Aε}
        (g : residueFieldObject.{u, w, w} Λ k ⟶ Aε)
        (e : Aε ⟶ residueFieldObject.{u, w, w} Λ k)
        (hpair : IsCanonicalDualNumberPair g e)
        (i : x₀.1 ⟶ xε.1) (hi : (ringDeformationProjection Λ k P).IsHomLift g i),
        ∃ c : xε.1.left.fiber ≃+* DualNumber P,
          (∀ y : xε.1.left.fiber, (c y).fst = xε.1.hom.map y) ∧
          (∀ y : x₀.1.left.fiber,
            c (i.left.map y) = TrivSqZeroExt.inl (x₀.1.hom.map y)) ∧
          ∃ E : infinitesimalAutomorphismGroup hp g e hpair i hi ≃*
            Multiplicative (Derivation k P P),
            (∀ (a : infinitesimalAutomorphismGroup hp g e hpair i hi) (y : P),
              (c (a.val.asIso.hom.val.left.map (c.symm (TrivSqZeroExt.inl y)))).snd =
                (Multiplicative.toAdd (E a)) y) ∧
            (∀ (s : k) (a : infinitesimalAutomorphismGroup hp g e hpair i hi),
              ∃! b : infinitesimalAutomorphismGroup hp g e hpair i hi,
                ∀ y : P,
                  (c (b.val.asIso.hom.val.left.map (c.symm (TrivSqZeroExt.inl y)))).snd =
                    s • (c (a.val.asIso.hom.val.left.map
                      (c.symm (TrivSqZeroExt.inl y)))).snd)

Deformation.Examples.ringDeformationTangentSpaceLinearEquivExtOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/RingsTangentSpaceEquivTangent.lean, line 285. The attribute's comment: “the tangent space”. References: SGA 7 VI (4.16), “(b), special case”.

Stacks 0DY3, the tangent space. Let k be a field and P a k-algebra. The tangent space of the deformation category of P of Stacks 0DY1, with the canonical k-vector-space structure of Stacks 06IH, is Ext¹_P(NL_{P/k}, P):

T𝓓_P = Ext¹_P(NL_{P/k}, P).

The identification is the family of extension classes Deformation.Examples.tangentExtClass, which sends an isomorphism class of first-order flat deformations of P over k ⊕ V to the class of Stacks 0GPT of the square-zero extension of P by P ⊗[k] V it determines. That family is natural in V, injective by Deformation.Examples.tangentExtClass_injective and surjective by Deformation.Examples.surjective_tangentExtClass, so Deformation.tangentSpaceLinearEquivOfNaturalBijection turns it into a k-linear equivalence at V = k, and Deformation.Examples.naiveCotangentExtOneTensorFunctorObjRankOne replaces the coefficients P ⊗[k] k by P.

The infinitesimal-automorphism clause Inf(𝓓_P) = Der_k(P, P) of the same tag is Deformation.Examples.exists_infinitesimalAutomorphismGroupMulEquivDerivation; the two declarations together cover the tag.

public def ringDeformationTangentSpaceLinearEquivExtOne :
    letI : Fact (IsPredeformationCategory (ringDeformationBasedCategory Λ k P).p) :=
      ⟨(ringDeformationCategory_isDeformationCategory P).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (ringDeformationBasedCategory Λ k P)
        isCofiberedInGroupoids_ringDeformationProjection))) :=
      ⟨schlessingerConditionS2_ringDeformation Λ k P⟩
    artinianTangentSpace Λ k
        (isomorphismClasses (ringDeformationBasedCategory Λ k P)
          isCofiberedInGroupoids_ringDeformationProjection)
      ≃ₗ[k] naiveCotangentExtOne k P P

Deformation.Examples.ringDeformationTangentSpaceLinearEquivExtOne_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/RingsTangentSpaceEquivTangent.lean, line 319. The attribute's comment: “the tangent space”.

The identification of Stacks 0DY3 is the classification of Stacks 0GPT. On the isomorphism class of a point of the fibre over the square-zero extension k ⊕ k of Stacks 06IB, the tangent-space identification is the class in Ext¹_P(NL_{P/k}, P ⊗[k] k) of the square-zero extension of P the point determines, read through P ⊗[k] k ≅ P.

This pins the identification down: no content is left in the transport of the vector-space structure of Stacks 06IH.

public theorem ringDeformationTangentSpaceLinearEquivExtOne_apply
    (z : (associatedTangentSpaceSetFunctor (ringDeformationBasedCategory Λ k P)
      isCofiberedInGroupoids_ringDeformationProjection).obj (FGModuleCat.of k k)) :
    letI : Fact (IsPredeformationCategory (ringDeformationBasedCategory Λ k P).p) :=
      ⟨(ringDeformationCategory_isDeformationCategory P).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (ringDeformationBasedCategory Λ k P)
        isCofiberedInGroupoids_ringDeformationProjection))) :=
      ⟨schlessingerConditionS2_ringDeformation Λ k P⟩
    ringDeformationTangentSpaceLinearEquivExtOne Λ k P z
      = naiveCotangentExtOneTensorFunctorObjRankOne k P
        (tangentExtClass (FGModuleCat.of k k) z)

Tag 0DZL, a lemma

Tag 0DZL in the Stacks Project.

Deformation.Examples.existsUnique_ringDeformationClass_artinianDualNumbers_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/RingsSmooth.lean, line 701.

Stacks 0DZL. For a smooth algebra P over a field k, the tangent space of the deformation category of P is zero: the flat deformations of P over the dual numbers form a single isomorphism class.

public theorem existsUnique_ringDeformationClass_artinianDualNumbers_of_smooth
    [Algebra.Smooth k P] :
    ∃ x : Quotient (isIsomorphicSetoid
        ((objectsOverFunctor (FlatAlgebraCategory.projection (Λ := Λ) (k := k))
          (residueFieldAlgebra (Λ := Λ) (k := k) P)).Fiber
          (artinianDualNumbers.{u, w, w} Λ k))),
      ∀ y, y = x

Tag 0DY4, a lemma

Tag 0DY4 in the Stacks Project.

Deformation.Examples.finiteDimensional_naiveCotangentExtOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/RingsTangentSpaceFinite.lean, line 524. The attribute's comment: “part (2) for the Ext group”. References: SGA 7 VI (4.14), “more general”.

Stacks 0DY4(2) for the Ext module. Let k be a field and P a k-algebra of finite type which is smooth over k outside a finite set of primes. Then the first Ext module Ext¹_P(NL_{P/k}, P) of the naive cotangent complex is finite-dimensional over k, for any k-module structure on it compatible with the P-action. Through the identification of that Ext module with the tangent space T𝓓_P of the deformation category of P, which is Tag 0DY3, this is the finite-dimensionality of the tangent space.

theorem finiteDimensional_naiveCotangentExtOne (k P : Type w) [Field k] [CommRing P]
    [Algebra k P] [Algebra.FiniteType k P]
    [Module k (Stacks.Deformation.naiveCotangentExtOne k P P)]
    [IsScalarTower k P (Stacks.Deformation.naiveCotangentExtOne k P P)]
    (hfinite : {q : PrimeSpectrum P | ¬ Algebra.IsSmoothAt k q.asIdeal}.Finite) :
    FiniteDimensional k (Stacks.Deformation.naiveCotangentExtOne k P P)

Algebra.finiteDimensional_derivation_iff_ringKrullDim_le_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Derivation/FiniteDimensional.lean, line 250. The attribute's comment: “part (1)”.

Stacks 0DY4(1). For a k-algebra P of finite type over a field, the k-derivations of P into itself are a finite-dimensional k-vector space if and only if P has Krull dimension at most zero. Through Tag 0DY3 this is the finite-dimensionality criterion for the infinitesimal automorphisms of the deformation category of P.

theorem finiteDimensional_derivation_iff_ringKrullDim_le_zero
    (k : Type u) (P : Type v) [Field k] [CommRing P] [Algebra k P]
    [Algebra.FiniteType k P] :
    FiniteDimensional k (Derivation k P P) ↔ ringKrullDim P ≤ 0

Tag 0ET4, a lemma

Tag 0ET4 in the Stacks Project.

Deformation.Examples.exists_hull_isomorphismClasses_ringDeformation_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/RingsHull.lean, line 172.

Let Λ → k be a classical base, let P be a k-algebra of finite type, and suppose Spec(P) → Spec(k) is smooth except at a finite number of points. Then the functor of fibrewise isomorphism classes of deformations of P has a hull: a versal formal object with bijective differential.

public theorem exists_hull_isomorphismClasses_ringDeformation_of_finiteType
    [Algebra.FiniteType k P]
    (hsmooth : {q : PrimeSpectrum P | ¬ Algebra.IsSmoothAt k q.asIdeal}.Finite)
    (hΛ : IsClassical Λ k) :
    ∃ ξ : FormalObject (CategoryOfElements.π (Deformation.isomorphismClasses
        (BasedCategory.ofFunctor (ringDeformationProjection Λ k P))
        (isPredeformationCategory_ringDeformationProjection (Λ := Λ) (k := k) P).cofibered)),
      IsVersal (categoryOfElements_projection_isCofibered (Deformation.isomorphismClasses
          (BasedCategory.ofFunctor (ringDeformationProjection Λ k P))
          (isPredeformationCategory_ringDeformationProjection
            (Λ := Λ) (k := k) P).cofibered)) ξ ∧
        HasBijectiveDifferential
          (categoryOfElements_projection_isCofibered (Deformation.isomorphismClasses
            (BasedCategory.ofFunctor (ringDeformationProjection Λ k P))
            (isPredeformationCategory_ringDeformationProjection
              (Λ := Λ) (k := k) P).cofibered))
          ξ

Tag 0DYS, a lemma

Tag 0DYS in the Stacks Project.

Deformation.Examples.localizationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Localization.lean, line 446.

Localization at S gives a natural functor from deformations of P to deformations of S⁻¹P, with the canonical localization map on every flat algebra.

noncomputable def localizationFunctor (S : Submonoid P) :
    LocalizationFunctorData (Λ := Λ) (k := k) S

Tag 0DYT, a lemma

Tag 0DYT in the Stacks Project.

Deformation.Examples.henselizationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Henselization.lean, line 527.

Stacks 0DYT. For a k-algebra P and an ideal J ⊆ P, henselization along the inverse image of J is a functor from the deformation category of P to that of the henselization of the pair (P, J), over the category 𝒞_Λ of Artinian local bases.

noncomputable def henselizationFunctor :
    HenselizationFunctorData (Λ := Λ) (k := k) (P := P) J

Tag 0DYU, a lemma

Tag 0DYU in the Stacks Project.

Deformation.Examples.strictHenselizationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/StrictHenselization/Functor.lean, line 780.

Stacks 0DYU. Let P be a local k-algebra and let Pˢʰ be a strict henselization of P with respect to a separable algebraic closure of its residue field. There is a natural functor from the deformation category of P to that of Pˢʰ, over the category 𝒞_Λ of Artinian local bases: strict henselize the flat algebra of each deformation.

noncomputable def strictHenselizationFunctor
    (hsh : Stacks.StrictHenselization.IsStrictHenselization P κsep Psh) :
    StrictHenselizationFunctorData (Λ := Λ) (k := k) (P := P) Psh

Tag 0DYV, a lemma

Tag 0DYV in the Stacks Project.

Deformation.Examples.adicCompletionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Completion.lean, line 1069.

The completion functor on deformations, Stacks 0DYV. Completion at the inverse image of J is a functor over 𝒞_Λ together with the identification of its fibres with the adic completions; this is one such datum, chosen from the base-compatible ones so that Deformation.Examples.isBaseCompatible_adicCompletionFunctor holds of it.

public noncomputable def adicCompletionFunctor [IsNoetherianRing P] :
    AdicCompletionFunctorData (Λ := Λ) (k := k) P J

Tag 0DY5, a lemma

Tag 0DY5 in the Stacks Project.

Deformation.Examples.hypersurface_finiteDimensional_infinitesimalAutomorphisms_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/RingsHypersurface.lean, line 67. The attribute's comment: “part (1)”.

Stacks 0DY5(1). Let k be a field, n a number of variables and f a nonzero formal power series in k[[x_1, …, x_n]] lying in the square of the ideal generated by the variables, and let P = k[[x_1, …, x_n]]/(f). At any dual-number lift of any object of the deformation category of P over the residue field, the infinitesimal automorphism group carries a k-vector-space structure whose addition is composition and which is carried by the identification of Tag 0DY3 to the k-structure of Derivation k P P, and that vector space is finite-dimensional if and only if n = 1.

public theorem hypersurface_finiteDimensional_infinitesimalAutomorphisms_iff
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (n : ℕ) (f : MvPowerSeries (Fin n) k) (hf : f ≠ 0)
    (hord : f ∈ (Ideal.span (Set.range
      (MvPowerSeries.X : Fin n → MvPowerSeries (Fin n) k))) ^ 2) :
    let P := MvPowerSeries (Fin n) k ⧸ Ideal.span {f}
    let hp := (ringDeformationCategory_isDeformationCategory (Λ := Λ) (k := k) P).predeformation
    ∀ {Aε : ArtinianLocalAlgCat.{u, w, w} Λ k}
      {x₀ : (ringDeformationProjection Λ k P).Fiber (residueFieldObject.{u, w, w} Λ k)}
      {xε : (ringDeformationProjection Λ k P).Fiber Aε}
      (g : residueFieldObject.{u, w, w} Λ k ⟶ Aε)
      (e : Aε ⟶ residueFieldObject.{u, w, w} Λ k)
      (hpair : IsCanonicalDualNumberPair g e)
      (i : x₀.1 ⟶ xε.1) (hi : (ringDeformationProjection Λ k P).IsHomLift g i),
      let G := infinitesimalAutomorphismGroup hp g e hpair i hi
      ∃ hA : AddCommGroup G,
        letI := hA
        ∃ hM : Module k G,
          letI := hM
          (∀ a b : G, a + b = a * b) ∧
          (∃ E : G ≃* Multiplicative (Derivation k P P), ∀ (s : k) (a : G),
            Multiplicative.toAdd (E (s • a)) = s • Multiplicative.toAdd (E a)) ∧
          (FiniteDimensional k G ↔ n = 1)

Deformation.Examples.hypersurface_finiteDimensional_tangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/RingsHypersurfaceTangentSpaceFinite.lean, line 326. The attribute's comment: “part (2)”.

Stacks 0DY5(2). Let k be a field, f a nonzero formal power series in k[[x_1, …, x_n]] lying in the square of the ideal generated by the variables, and P = k[[x_1, …, x_n]]/(f) the formal hypersurface it cuts out. If the Jacobian ideal (f, ∂f/∂x_1, …, ∂f/∂x_n) has radical the ideal generated by the variables, then the tangent space T𝓓_P of the deformation category of P of Stacks 0DY1 — with the canonical k-vector-space structure of Stacks 06IH — is finite dimensional over k.

The tangent space is Ext¹_P(NL_{P/k}, P) by the tangent-space clause of Stacks 0DY3, that group is the conormal cokernel of the canonical presentation of P by Stacks 0GPU, and the cokernel is finite dimensional by Deformation.Examples.finiteDimensional_conormalCokernel_hypersurface.

theorem hypersurface_finiteDimensional_tangentSpace {Λ : Type u} [CommRing Λ] [Algebra Λ k]
    (hf : f ≠ 0)
    (hord : f ∈ (Ideal.span (Set.range
      (MvPowerSeries.X : Fin n → MvPowerSeries (Fin n) k))) ^ 2)
    (hjac : (Ideal.span ({f} ∪ Set.range
      (fun i : Fin n ↦ MvPowerSeries.pderiv (R := k) i f))).radical =
      Ideal.span (Set.range (MvPowerSeries.X : Fin n → MvPowerSeries (Fin n) k))) :
    letI : Fact (IsPredeformationCategory
        (ringDeformationBasedCategory Λ k (Hypersurface n f)).p) :=
      ⟨(ringDeformationCategory_isDeformationCategory (Hypersurface n f)).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (ringDeformationBasedCategory Λ k (Hypersurface n f))
        isCofiberedInGroupoids_ringDeformationProjection))) :=
      ⟨schlessingerConditionS2_ringDeformation Λ k (Hypersurface n f)⟩
    FiniteDimensional k (artinianTangentSpace Λ k
      (isomorphismClasses (ringDeformationBasedCategory Λ k (Hypersurface n f))
        isCofiberedInGroupoids_ringDeformationProjection))

Sources

LeanDeformation.Examples.ringDeformationCategory · Deformation.Examples.flatAlgebraCategory_projection_isCofiberedInGroupoids · FlatAlgebraCategory · FlatAlgebraCategory.Hom · FlatAlgebraCategory.instCategory · FlatAlgebraCategory.projection · residueFieldAlgebra · Deformation.Examples.flatAlgebraCategory_projection_satisfiesRS

Section93.9 Schemes #

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

Tag 0DY7, an example

Tag 0DY7 in the Stacks Project.

Deformation.Examples.isCofiberedInGroupoids_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeChartEquivalence.lean, line 242. The attribute's comment: “the deformation category of an affine open presented as a spectrum is cofibered in groupoids, transported along Tag 0DYX from the ring side; the clause for a general scheme is not covered”.

The deformation category of an affine open presented as a spectrum is cofibered in groupoids. This has no scheme-side proof in this repository: it is transported from the deformation category of the coordinate ring, which is a deformation category by Tag 0DY2.

theorem isCofiberedInGroupoids_chart :
    IsCofiberedInGroupoids
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (U.ι ≫ X.hom)))

Deformation.Examples.FlatSchemeFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 78. The attribute's comment: “flat_scheme_families”.

A scheme flat over the spectrum of an object of 𝒞_Λ.

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

Deformation.Examples.FlatSchemeFamily.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 92. The attribute's comment: “flat_scheme_families”.

A cartesian base-change arrow between flat scheme families.

structure Hom (P Q : FlatSchemeFamily.{u, v, w} Λ k)

Deformation.Examples.FlatSchemeFamily.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 103. The attribute's comment: “flat_scheme_families”.

Flat scheme families over objects of 𝒞_Λ and their base-change arrows form a category.

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

Deformation.Examples.flatSchemeFamilyProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 127. The attribute's comment: “flat_scheme_families”.

The canonical functor sending a flat scheme family to its object of 𝒞_Λ.

def flatSchemeFamilyProjection :
    FlatSchemeFamily.{u, v, w} Λ k ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k

Deformation.Examples.flatSchemeFamilyProjection_cofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 136. The attribute's comment: “cofibred_projection”.

Base change makes the projection from flat scheme families cofibered in groupoids.

theorem flatSchemeFamilyProjection_cofiberedInGroupoids
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k] :
    IsCofiberedInGroupoids (flatSchemeFamilyProjection.{u, v, w} (Λ := Λ) (k := k))

Deformation.Examples.SchemeDeformationCategory, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 209. The attribute's comment: “scheme_deformation_category”. References: SGA 7 VI (1.1(c)).

A flat family over an object of 𝒞_Λ together with an identification of its fibre over the closed point with a fixed scheme over k. The identification is recorded as a cartesian square.

structure SchemeDeformationCategory (X : Over (Spec (.of k)))

Deformation.Examples.SchemeDeformationCategory.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 228. The attribute's comment: “scheme_deformation_category”.

A cartesian arrow of deformations: contravariant on the schemes, covariant on the objects of 𝒞_Λ, and compatible with the two identifications of the fibre over the closed point.

structure Hom {X : Over (Spec (.of k))}
    (P Q : SchemeDeformationCategory (Λ := Λ) (k := k) X)

Deformation.Examples.SchemeDeformationCategory.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 241. The attribute's comment: “scheme_deformation_category”. References: SGA 7 VI (1.1(c)).

Deformations of a fixed scheme over k form a category.

instance instCategory (X : Over (Spec (.of k))) :
    Category (SchemeDeformationCategory (Λ := Λ) (k := k) X)

Deformation.Examples.schemeDeformationCategoryProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 269. The attribute's comment: “scheme_deformation_category”.

The canonical projection from the category of deformations of a scheme to 𝒞_Λ.

def schemeDeformationCategoryProjection (X : Over (Spec (.of k))) :
    SchemeDeformationCategory (Λ := Λ) (k := k) X ⥤ ArtinianLocalAlgCat.{u, u, u} Λ k

Deformation.Examples.schemeDeformationCategoryProjection_cofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesCofibered.lean, line 143. The attribute's comment: “cofibred_projection, for the deformation category of a scheme”. References: SGA 7 VI (1.1(c)), “more general”.

The deformation category of a scheme is cofibered in groupoids. A deformation can be base changed along any morphism of 𝒞_Λ (Deformation.Examples.baseChangeDeformation), and an arrow out of a deformation descends uniquely through that base change, because its component on total spaces is determined by the universal property of the fibre product.

This is the lower half of the cofibered condition that Deformation.full_of_exists_lift_of_isHomLift_id asks of the source-forgetful functor of [Stacks, Tag 0E3X].

theorem schemeDeformationCategoryProjection_cofiberedInGroupoids
    (X : Over (Spec (.of k))) :
    IsCofiberedInGroupoids (schemeDeformationCategoryProjection (Λ := Λ) (k := k) X)

Deformation.Examples.isFirstOrderThickening_specialMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpecialFibreFirstOrder.lean, line 117. The attribute's comment: “the special-fibre immersion of a deformation over the dual numbers is a first-order thickening”.

The special-fibre immersion of a first-order deformation of a scheme is a first-order thickening. It is a closed immersion by Deformation.Examples.deformationSpecialMap_isClosedImmersion, being a base change of the closed point, and its ideal sheaf is square-zero because the maximal ideal of the base object is, by Deformation.Examples.maximalIdeal_sq_eq_bot_of_dualNumberEquiv.

This is the hypothesis i.ker ^ 2 = ⊥ of [Stacks Project, Tag 0CK2], discharged for the deformations over the dual numbers to which [Stacks Project, Tag 0E3V] applies it.

theorem isFirstOrderThickening_specialMap {X : Over (Spec (CommRingCat.of k))}
    (P : SchemeDeformationCategory (Λ := Λ) (k := k) X)
    (coordinate : P.base ≃ₐ[Λ] DualNumber k) :
    Stacks.Thickenings.IsFirstOrderThickening P.specialMap

Tag 0DY8, a lemma

Tag 0DY8 in the Stacks Project.

Deformation.Examples.isDeformationCategory_schemeDeformationCategoryProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesDeformationCategory.lean, line 241. The attribute's comment: “the clause that the deformation category of a fixed scheme over k is a deformation category, unconditionally; condition (RS) for the category of all flat scheme families of Example 0DY7 is Deformation.Examples.satisfiesRS_flatSchemeFamilyProjection”. References: SGA 7 VI (1.1(c)), “more general”.

The deformation category of a fixed scheme X over the residue field is a deformation category: a predeformation category satisfying (RS).

theorem isDeformationCategory_schemeDeformationCategoryProjection
    (X : Over (Spec (.of k))) :
    IsDeformationCategory.{u, u, u}
      (schemeDeformationCategoryProjection.{u} (Λ := Λ) (k := k) X)

Deformation.Examples.satisfiesRS_flatSchemeFamilyProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesRimSchlessingerSquares.lean, line 48. The attribute's comment: “condition (RS) for the category of flat scheme families of Example 0DY7, unconditionally. The two gluing clauses it rests on are the last assertion of Tag 07RV and the equivalence assertion of the closing paragraph of Tag 07RX, both proved in this repository: Stacks.Pushout.isPullback_of_isPushout_glued and Stacks.Pushout.isPushout_restrictions_of_flat. The pushout of spectra, the existence of the glued family, its flatness and both halves of the universal property are proved as well. The clause that the deformation category of a fixed scheme over k is a deformation category is Deformation.Examples.isDeformationCategory_schemeDeformationCategoryProjection”.

The category of flat families of schemes over 𝒞_Λ satisfies the Rim-Schlessinger condition (RS).

theorem satisfiesRS_flatSchemeFamilyProjection :
    SatisfiesRS (flatSchemeFamilyProjection.{u, v, w} (Λ := Λ) (k := k))

Tag 0DY9, a lemma

Tag 0DY9 in the Stacks Project.

Deformation.Examples.infinitesimalAutomorphismGroupTrivialDeformationChain, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesInfinitesimalAutomorphismsTrivial.lean, line 168. The attribute's comment: “first display: for a scheme X over the field k, Inf(Def_X) = Ext^0(NL_{X/k}, O_X) = Hom(Omega_{X/k}, O_X) = Der_k(O_X, O_X), as three identifications: Inf(Def_X) is the library's infinitesimal automorphism group of the deformation category of X at the trivial deformation X x_k Spec k[eps], and is isomorphic as a group to Der_k(O_X, O_X); Ext^0 out of the naive cotangent complex is additively Hom(Omega_{X/k}, O_X); and Hom(Omega_{X/k}, O_X) is k-linearly Der_k(O_X, O_X). The second display, T Def_X = Ext^1(NL_{X/k}, O_X), is registered separately”. References: SGA 1 III (6.1), “special case”; SGA 3 VIIA (2.5), “first component”; SGA 3 VIIA (6.4.3), “special case”; SGA 7 VI (4.16), “special case”.

The first display of [Stacks Project, Tag 0DY9]. For a scheme X over the field k,

Inf(𝓓_X) = Ext⁰_{𝒪_X}(NL_{X/k}, 𝒪_X) = Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X) = Der_k(𝒪_X, 𝒪_X),

given as the three identifications of those four groups.

Inf(𝓓_X) is the library's infinitesimal automorphism group Deformation.infinitesimalAutomorphismGroup of the deformation category of X, which is a predeformation category by [Stacks Project, Tag 0DY8], formed at its canonical data: the point X over k, its pushforward the trivial deformation X ×_{Spec k} Spec k[ε], and the pair k → k[ε] → k. That is, the automorphisms of the trivial deformation that are the identity modulo ε.

The first identification is an isomorphism of groups: composition of such automorphisms corresponds to addition of derivations (Deformation.Examples.infinitesimalAutomorphismGroupMulEquivDerivations, at the coordinate Deformation.Examples.artinianDualNumbersCoordinate of the dual-number object).

The second is AlgebraicGeometry.Scheme.naiveCotangentExtZeroAddEquiv: Ext⁰ out of the naive cotangent complex NL_{X/k} of the structure morphism of X is the Hom out of its degree 0 cohomology sheaf, which is Ω_{X/k} by [Stacks Project, Tag 0D0J].

The third is k-linear: Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X) carries the k-structure of sheaves of modules on a scheme over k (AlgebraicGeometry.modulesLinear), and the derivations of 𝒪_X over k with values in 𝒪_X the one of Deformation.Examples.schemeMorphismDerivationsModule; it is corepresentability of relative derivations (Deformation.Examples.schemeMorphismDerivationsLinearEquiv) read through the comparison AlgebraicGeometry.Scheme.Hom.cotangentSheafIso of the two constructions of the sheaf of relative differentials.

Der_k(𝒪_X, 𝒪_X) is written schemeMorphismDerivations (𝟙 X.left) X.hom, the derivations of 𝒪_X over k with values in the pushforward of 𝒪_X along the identity of X, which is 𝒪_X itself (Deformation.Examples.schemeMorphismPushforwardStructureSheaf_id, by rfl).

def infinitesimalAutomorphismGroupTrivialDeformationChain (X : Over (Spec (CommRingCat.of k))) :
    (infinitesimalAutomorphismGroup
        (isDeformationCategory_schemeDeformationCategoryProjection (Λ := Λ) X).predeformation
        (x₀ := residueTrivialFiberObj X) (xε := dualNumbersTrivialFiberObj X)
        dualNumbersInclusion.{u, u, u}
        (residueMorphism.{u, u, u} (artinianDualNumbers.{u, u, u} Λ k))
        isCanonicalDualNumberPair_dualNumbersInclusion.{u, u, u}
        (dualNumbersTrivialDeformationHom X) (dualNumbersTrivialDeformationHom_isHomLift X)
        ≃* Multiplicative (schemeMorphismDerivations (Λ := Λ) (k := k) (𝟙 X.left) X.hom))
      × (Scheme.naiveCotangentExt X.hom (structureSheafModules X.left) 0
          ≃+ (Scheme.Hom.relativeDifferentials X.hom ⟶ structureSheafModules X.left))
      × (letI : Module k (Scheme.Hom.relativeDifferentials X.hom ⟶ structureSheafModules X.left) :=
            (modulesLinear k (Over.mk X.hom)).homModule _ _;
          letI := schemeMorphismDerivationsModule (Λ := Λ) (k := k) (𝟙 X.left) X.hom
            (structureSheafModules X.left);
          ((Scheme.Hom.relativeDifferentials X.hom ⟶ structureSheafModules X.left) ≃ₗ[k]
            schemeMorphismDerivations (Λ := Λ) (k := k) (𝟙 X.left) X.hom))

Deformation.Examples.schemeTangentSpaceLinearEquivExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTangentSpaceLinearEquivExt.lean, line 251. The attribute's comment: “second display: for a scheme X over the field k, T Def_X = Ext^1(NL_{X/k}, O_X) as k-vector spaces, from the tangent space of the deformation category of X (isomorphism classes of flat deformations of X over k[eps], with the canonical vector space structure of 06IH) onto Ext^1_{O_X}(NL_{X/k}, O_X); a deformation goes to its 08UC difference class with the trivial deformation X x_k Spec k[eps], which goes to 0. The first display, Inf(Def_X) = Ext^0(NL_{X/k}, O_X) = Der_k(O_X, O_X), is registered separately”.

Stacks Project, Tag 0DY9, second display. For a scheme X over the field k,

T𝓓_X = Ext¹_{𝒪_X}(NL_{X/k}, 𝒪_X)

as k-vector spaces.

T𝓓_X is the tangent space of the deformation category of X of [Stacks Project, Tag 0DY7]: the value at the dual numbers k[ε] of its functor of isomorphism classes ([Stacks Project, Tag 06SR]), the set of isomorphism classes of flat deformations of X over k[ε], with the canonical k-vector space structure of [Stacks Project, Tag 06IH]. Ext¹_{𝒪_X}(NL_{X/k}, 𝒪_X) is AlgebraicGeometry.Scheme.naiveCotangentExt of the structure morphism of X with coefficients 𝒪_X in degree 1, a k-vector space through the k-linear structure of 𝒪_X-modules.

The identification is the source's proof: a flat deformation of X over k[V] = k ⊕ V is a solution of the deformation problem of [Stacks Project, Tag 08U7] for Spec k ⊂ Spec k[V] with ideal f^*𝒥 = 𝒪_X ⊗_k V, and its class is the difference class of [Stacks Project, Tag 08UC] against the trivial deformation X ×_k Spec k[V] (Deformation.Examples.tangentExtClassAt). These classes are bijective (Deformation.Examples.bijective_tangentExtClassAt) and natural in V (Deformation.Examples.tangentExtClassAt_naturality), so they are k-linear for the structure of Tag 06IH at V = k, where 𝒪_X ⊗_k k = 𝒪_X. The trivial deformation goes to 0 (Deformation.Examples.schemeTangentSpaceLinearEquivExt_trivial) and the class of a deformation is its difference class (Deformation.Examples.schemeTangentSpaceLinearEquivExt_classOf).

noncomputable def schemeTangentSpaceLinearEquivExt :
    letI : Fact (IsPredeformationCategory (schemeDeformationBased (Λ := Λ) X).p) :=
      ⟨(isDeformationCategory_schemeDeformationCategoryProjection (Λ := Λ) X).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (schemeDeformationBased (Λ := Λ) X) (schemeDeformation_cofibered X)))) :=
      ⟨schlessingerConditionS2_schemeDeformation X⟩
    letI := schemeTangentExtModule X (structureSheafModules X.left)
    schemeTangentSpace (Λ := Λ) (k := k) X ≃ₗ[k]
      Scheme.naiveCotangentExt X.hom (structureSheafModules X.left) 1

Tag 0DYA, a lemma

Tag 0DYA in the Stacks Project.

Deformation.Examples.finiteDimensional_schemeTangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesFiniteDimensional.lean, line 116. The attribute's comment: “the tangent space clause: for X proper over k, T Def_X (isomorphism classes of flat deformations of X over k[eps], with the canonical vector space structure of 06IH) is finite dimensional over k”.

Stacks 0DYA, the tangent space. For a scheme X proper over the field k, the tangent space T𝓓_X of its deformation category ([Stacks Project, Tag 0DY7]) — the isomorphism classes of flat deformations of X over k[ε], with the canonical vector-space structure of [Stacks Project, Tag 06IH] — is finite dimensional over k.

By [Stacks Project, Tag 0DY9] it is Ext¹_{𝒪_X}(NL_{X/k}, 𝒪_X) (Deformation.Examples.schemeTangentSpaceLinearEquivExtRankOne and Deformation.Examples.schemeTangentExtRankOneLinearEquiv, the identification of Deformation.Examples.schemeTangentSpaceLinearEquivExt before the change of model of the derived category); NL_{X/k} is in D^-_Coh(𝒪_X) by [Stacks Project, Tag 0D0K] (derivedCategoryBMinus_naiveCotangentComplex) and 𝒪_X in D^+_Coh(𝒪_X), so the Ext group is finite dimensional by [Stacks Project, Tag 0D0D].

theorem finiteDimensional_schemeTangentSpace [IsProper X.hom] :
    letI : Fact (IsPredeformationCategory (schemeDeformationBased (Λ := Λ) X).p) :=
      ⟨(isDeformationCategory_schemeDeformationCategoryProjection (Λ := Λ) X).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (schemeDeformationBased (Λ := Λ) X) (schemeDeformation_cofibered X)))) :=
      ⟨schlessingerConditionS2_schemeDeformation X⟩
    FiniteDimensional k (schemeTangentSpace (Λ := Λ) (k := k) X)

Deformation.Examples.finiteDimensional_localizedAutomorphismFunctorTangent_schemeDeformation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesFiniteDimensional.lean, line 253. The attribute's comment: “the infinitesimal automorphism clause: for X proper over k, Inf(Def_X) is finite dimensional over k, with the vector space structure of 06JV, at every point of the deformation category and every choice of pushforwards”.

Stacks 0DYA, the infinitesimal automorphisms. For a scheme X proper over the field k, the k-vector space Inf(𝓓_X) of infinitesimal automorphisms of its deformation category ([Stacks Project, Tag 0DY7]) is finite dimensional. Inf(𝓓_X) is the tangent space at the identity of the automorphism functor of a point x₀ of the deformation category, with the vector-space structure of [Stacks Project, Tag 06JV] (addition is composition, the scalar action is transport along ε ↦ cε); this holds at every point x₀ and every choice P of pushforwards, in particular at the trivial deformation X over k.

The proof is the source's: Inf(𝓓_X) embeds k-linearly in Der_k(𝒪_X, 𝒪_X) (infinitesimalAutomorphismDerivationLinearMap, injective by injective_infinitesimalAutomorphismDerivationLinearMap), the identification of [Stacks Project, Tag 0DY9], and Der_k(𝒪_X, 𝒪_X) = Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X) is finite dimensional by [Stacks Project, Tag 0D0D].

theorem finiteDimensional_localizedAutomorphismFunctorTangent_schemeDeformation [IsProper X.hom]
    {x₀ : SchemeDeformationCategory (Λ := Λ) (k := k) X}
    (P : ChosenPushforwardsAt (schemeDeformationCategoryProjection (Λ := Λ) (k := k) X) x₀) :
    letI := naturalLocalizedTangentAddCommGroup P
      (isDeformationCategory_schemeDeformationCategoryProjection (Λ := Λ) X).satisfiesRS
    letI := naturalLocalizedTangentModule P
      (isDeformationCategory_schemeDeformationCategoryProjection (Λ := Λ) X).satisfiesRS
    FiniteDimensional k (localizedAutomorphismFunctorTangent P)

Tag 0ET5, a lemma

Tag 0ET5 in the Stacks Project.

Deformation.Examples.exists_hull_isomorphismClasses_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesHull.lean, line 95. The attribute's comment: “the hull: for X proper over k and Λ a complete local ring with residue field k, the functor A ↦ Ob(Def_X(A))/≅ of isomorphism classes of deformations of X has a hull”.

Stacks Project, Tag 0ET5, the hull. Let X be a proper scheme over the field k and let Λ be a Noetherian complete local ring with residue field k (the classical case). Then the functor F : 𝒞_Λ → Sets, A ↦ Ob(Def_X(A))/≅ of isomorphism classes of deformations of X has a hull: a versal formal object of F whose differential is bijective.

Def_X is a deformation category by Stacks 0DY8 and its tangent space is finite dimensional by Stacks 0DYA (Deformation.Examples.finiteDimensional_schemeTangentSpace), so Stacks 06J7 and 06IZ give the hull.

theorem exists_hull_isomorphismClasses_scheme (hΛ : IsClassical Λ k)
    (X : Over (Spec (CommRingCat.of k))) [IsProper X.hom] :
    let F := isomorphismClasses (schemeDeformationBased (Λ := Λ) X) (schemeDeformation_cofibered X)
    ∃ ξ : FormalObject (CategoryOfElements.π F),
      IsHull (categoryOfElements_projection_isCofibered F) ξ

Deformation.Examples.isProrepresentableULift_isomorphismClasses_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesHull.lean, line 118. The attribute's comment: “prorepresentability: for X proper over k and Λ a complete local ring with residue field k, if Der_k(O_X, O_X) = 0 then the functor A ↦ Ob(Def_X(A))/≅ is prorepresentable”. References: SGA 7 X (2.27), “more general”.

Stacks Project, Tag 0ET5, prorepresentability. Let X be a proper scheme over the field k and let Λ be a Noetherian complete local ring with residue field k. If Der_k(𝒪_X, 𝒪_X) = 0, then the functor F : 𝒞_Λ → Sets, A ↦ Ob(Def_X(A))/≅ is prorepresentable.

By the first display of Stacks 0DY9, Inf(Def_X) = Der_k(𝒪_X, 𝒪_X) vanishes (Deformation.Examples.infinitesimalAutomorphisms_schemeDeformation_eq_bot), so Def_X and F are equivalent (Stacks 06K0) and F is a deformation functor with finite-dimensional tangent space (Stacks 0DYA); Schlessinger's theorem, Stacks 06JM, applies. Prorepresentability is stated in the universe-raised form Deformation.IsProrepresentableULift, the values of F lying one universe above the morphisms of 𝒞_Λ.

theorem isProrepresentableULift_isomorphismClasses_scheme (hΛ : IsClassical Λ k)
    (X : Over (Spec (CommRingCat.of k))) [IsProper X.hom]
    (hDer : ∀ D : schemeMorphismDerivations (Λ := Λ) (k := k) (𝟙 X.left) X.hom, D = 0) :
    IsProrepresentableULift
      (isomorphismClasses (schemeDeformationBased (Λ := Λ) X) (schemeDeformation_cofibered X))

Tag 0DYW, a lemma

Tag 0DYW in the Stacks Project.

Deformation.Examples.openRestrictionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/OpenSubschemes.lean, line 263. References: SGA 7 VI (4.1(d)).

Stacks 0DYW. Let X be a scheme over k and U ⊆ X an open subscheme. Restricting a deformation of X to the open corresponding to U is a functor from the deformation category of X to that of U, over the category 𝒞_Λ of Artinian local Λ-algebras.

def openRestrictionFunctor (X : Over (Spec (.of k))) (U : X.left.Opens) :
    BasedFunctor
      (BasedCategory.ofFunctor (schemeDeformationCategoryProjection (Λ := Λ) (k := k) X))
      (BasedCategory.ofFunctor
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (U.ι ≫ X.hom))))

Tag 0DYX, a lemma

Tag 0DYX in the Stacks Project.

Deformation.Examples.chartEquivalenceOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeChartEquivalence.lean, line 212. The attribute's comment: “for an affine open presented as a spectrum by an isomorphism over Spec k, which is the form Situation 0DYY provides”.

Stacks 0DYX for an affine open presented as a spectrum. The deformation category of an open U of X which is presented as Spec P over Spec k is equivalent, over 𝒞_Λ, to the deformation category of the k-algebra P: transport the deformations along the presentation and then take global sections.

def chartEquivalenceOver :
    StacksRepresentableCFG.EquivalenceOver
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (U.ι ≫ X.hom)))
      (Over.forget (residueFieldAlgebra (Λ := Λ) (k := k) P) ⋙
        FlatAlgebraCategory.projection (Λ := Λ) (k := k))

Deformation.Examples.SchemeRingDeformation.sectionsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeRingDeformation.lean, line 257. The attribute's comment: “the functor sending (A, Y) to the global sections of Y”.

Stacks 0DYX. Global sections as a functor from deformations of Spec P to deformations of P.

def sectionsFunctor :
    SchemeDeformationCategory (Λ := Λ) (k := k) (specOver k P) ⥤
      ringDeformationCategory (Λ := Λ) (k := k) P

Deformation.Examples.SchemeRingDeformation.equivalenceOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeRingDeformation.lean, line 483. The attribute's comment: “the equivalence Def_(Spec P) = Def_P; 06AD is isAffine_of_isThickening”. References: SGA 7 VI (4.1(b)).

Stacks 0DYX. For a k-algebra P, global sections are an equivalence from the deformation category of the affine scheme Spec P to the deformation category of P, over the category of Artinian local Λ-algebras with residue field k.

def equivalenceOver :
    StacksRepresentableCFG.EquivalenceOver
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (specOver k P))
      (Over.forget (residueFieldAlgebra (Λ := Λ) (k := k) P) ⋙
        FlatAlgebraCategory.projection (Λ := Λ) (k := k))

Tag 0DZM, a lemma

Tag 0DZM in the Stacks Project.

Deformation.Examples.localRingDeformationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Deformations/Schemes/LocalRing.lean, line 286. The attribute's comment: “the functor”.

Stacks 0DZM. Taking the local ring at a point of a scheme defines a functor of deformation categories over the category of Artinian local algebras.

noncomputable def localRingDeformationFunctor
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (X : Over (Spec (.of k))) (x : X.left) :
    letI : Algebra k (X.left.presheaf.stalk x) :=
      letI : Algebra k ((Spec (.of k)).presheaf.stalk (X.hom.base x)) :=
        StructureSheaf.stalkAlgebra k (X.hom.base x)
      ((X.hom.stalkMap x).hom.comp (algebraMap k _)).toAlgebra
    BasedFunctor
      (BasedCategory.ofFunctor
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) X))
      (BasedCategory.ofFunctor
        (Over.forget
          (residueFieldAlgebra (Λ := Λ) (k := k) (X.left.presheaf.stalk x)) ⋙
          FlatAlgebraCategory.projection (Λ := Λ) (k := k)))

Deformation.Examples.localRingDeformationFunctor_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Deformations/Schemes/LocalRing.lean, line 316. The attribute's comment: “fibers”.

Stacks 0DZM. The underlying algebra of the image deformation is the stalk of the deformed scheme at the image of the chosen point.

theorem localRingDeformationFunctor_fiber
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (X : Over (Spec (.of k))) (x : X.left)
    (P : SchemeDeformationCategory (Λ := Λ) (k := k) X) :
    letI : Algebra k (X.left.presheaf.stalk x) :=
      letI : Algebra k ((Spec (.of k)).presheaf.stalk (X.hom.base x)) :=
        StructureSheaf.stalkAlgebra k (X.hom.base x)
      ((X.hom.stalkMap x).hom.comp (algebraMap k _)).toAlgebra
    ((localRingDeformationFunctor X x).obj P).left.fiber =
      P.scheme.presheaf.stalk (P.specialMap.base x)

Deformation.Examples.localRingDeformationFunctor_specialMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Deformations/Schemes/LocalRing.lean, line 330. The attribute's comment: “special-fiber maps”.

Stacks 0DZM. The special-fibre map of the image is the stalk map of the special-fibre embedding.

theorem localRingDeformationFunctor_specialMap
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (X : Over (Spec (.of k))) (x : X.left)
    (P : SchemeDeformationCategory (Λ := Λ) (k := k) X) :
    letI : Algebra k (X.left.presheaf.stalk x) :=
      letI : Algebra k ((Spec (.of k)).presheaf.stalk (X.hom.base x)) :=
        StructureSheaf.stalkAlgebra k (X.hom.base x)
      ((X.hom.stalkMap x).hom.comp (algebraMap k _)).toAlgebra
    HEq ((localRingDeformationFunctor X x).obj P).hom.map.hom
      (P.specialMap.stalkMap x).hom

Deformation.Examples.localRingDeformationFunctor_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Deformations/Schemes/LocalRing.lean, line 344. The attribute's comment: “morphism maps”.

Stacks 0DZM. On morphisms, the induced algebra map is the stalk map of the morphism between the deformed schemes.

theorem localRingDeformationFunctor_map
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (X : Over (Spec (.of k))) (x : X.left)
    {P Q : SchemeDeformationCategory (Λ := Λ) (k := k) X} (f : P ⟶ Q) :
    letI : Algebra k (X.left.presheaf.stalk x) :=
      letI : Algebra k ((Spec (.of k)).presheaf.stalk (X.hom.base x)) :=
        StructureSheaf.stalkAlgebra k (X.hom.base x)
      ((X.hom.stalkMap x).hom.comp (algebraMap k _)).toAlgebra
    HEq ((localRingDeformationFunctor X x).map f).left.map.hom
      (f.map.stalkMap (Q.specialMap.base x)).hom

Tag 0DYY, a situation

Tag 0DYY in the Stacks Project.

Deformation.Examples.GluingSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/Schemes.lean, line 283.

A scheme over k, covered by two affine opens with affine intersection, together with coordinate rings for the three affine schemes.

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

Tag 0DYZ, a lemma

Tag 0DYZ in the Stacks Project.

Deformation.Examples.twoOpenComparisonFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCover.lean, line 492. The attribute's comment: “the comparison functor Def_X ⥤ Def_{U_1} ×_{Def_{U_12}} Def_{U_2} only; it is not shown to be an equivalence (that needs the glueing quasi-inverse of the proof) and the translation into the ring deformation categories Def_{P_i} is not included”.

Let X be a scheme over k with two opens U₁ and U₂. Restricting a deformation of X to U₁ and to U₂, together with the identification of the two induced deformations of U₁ ⊓ U₂, is a functor from the deformation category of X to the 2-fibre product Def_{U₁} ×_{Def_{U₁ ⊓ U₂}} Def_{U₂} over 𝒞_Λ.

def twoOpenComparisonFunctor (X : Over (Spec (.of k))) (U₁ U₂ : X.left.Opens) :
    SchemeDeformationCategory (Λ := Λ) (k := k) X ⥤
      TwoFibreProductOver
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (U₁.ι ≫ X.hom)))
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (U₂.ι ≫ X.hom)))
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk ((U₁ ⊓ U₂).ι ≫ X.hom)))
        (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_left : U₁ ⊓ U₂ ≤ U₁))
        (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_right : U₁ ⊓ U₂ ≤ U₂))

Deformation.Examples.twoOpenComparisonFunctor_comp_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCover.lean, line 542. The attribute's comment: “the comparison functor Def_X ⥤ Def_{U_1} ×_{Def_{U_12}} Def_{U_2} is a functor over 𝒞_Λ; it is not shown to be an equivalence and the ring deformation categories Def_{P_i} are not involved”.

The comparison functor of a two-open cover is strictly over 𝒞_Λ.

theorem twoOpenComparisonFunctor_comp_structureFunctor (X : Over (Spec (.of k)))
    (U₁ U₂ : X.left.Opens) :
    twoOpenComparisonFunctor (Λ := Λ) (k := k) X U₁ U₂ ⋙
        TwoFibreProductOver.structureFunctor
          (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (U₁.ι ≫ X.hom)))
          (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (U₂.ι ≫ X.hom)))
          (schemeDeformationCategoryProjection (Λ := Λ) (k := k)
            (Over.mk ((U₁ ⊓ U₂).ι ≫ X.hom)))
          (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_left : U₁ ⊓ U₂ ≤ U₁))
          (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_right : U₁ ⊓ U₂ ≤ U₂)) =
      schemeDeformationCategoryProjection (Λ := Λ) (k := k) X

Deformation.Examples.GluingSituation.comparisonFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCover.lean, line 559. The attribute's comment: “the comparison functor in Situation 0DYY; it is not shown to be an equivalence and the translation into the ring deformation categories Def_{P_i} is not included”.

The comparison functor of the two-open cover of a glueing situation.

def GluingSituation.comparisonFunctor (S : GluingSituation Λ k) :
    SchemeDeformationCategory (Λ := Λ) (k := k) S.X ⥤
      TwoFibreProductOver
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (S.U₁.ι ≫ S.X.hom)))
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk (S.U₂.ι ≫ S.X.hom)))
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k)
          (Over.mk ((S.U₁ ⊓ S.U₂).ι ≫ S.X.hom)))
        (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_left : S.U₁ ⊓ S.U₂ ≤ S.U₁))
        (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_right : S.U₁ ⊓ S.U₂ ≤ S.U₂))

Deformation.Examples.glueDeformation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCover.lean, line 1014. The attribute's comment: “the glueing construction of the proof, on objects only: an object of the 2-fibre product Def_{U_1} ×_{Def_{U_12}} Def_{U_2} is glued to a deformation of X over the same object of 𝒞_Λ, flat over it, with special fibre X, and restricting to U_1 and U_2 gives the two charts back. Not shown functorial in the datum, so not yet a quasi-inverse of twoOpenComparisonFunctor; neither the equivalence nor the Def_{P_i} form is proved”.

Let X be a scheme over k covered by two opens U₁ and U₂. An object of the 2-fibre product Def_{U₁} ×_{Def_{U₁ ⊓ U₂}} Def_{U₂} consists of a deformation of U₁, a deformation of U₂ and an isomorphism of their restrictions to U₁ ⊓ U₂; glueing the two total spaces along that isomorphism gives a deformation of X over the same object of 𝒞_Λ.

def glueDeformation : SchemeDeformationCategory (Λ := Λ) (k := k) X

Deformation.Examples.GluingSituation.glueDeformation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCover.lean, line 1274. The attribute's comment: “the glueing construction of the proof in Situation 0DYY, on objects only; see glueDeformation for the precise content and for what the equivalence still needs”.

In a glueing situation the two affine opens cover the scheme, and an object of the 2-fibre product of their deformation categories is glued to a deformation of the scheme itself.

def GluingSituation.glueDeformation (S : GluingSituation Λ k)
    (Q : TwoOpenDeformations (Λ := Λ) S.X S.U₁ S.U₂) :
    SchemeDeformationCategory (Λ := Λ) (k := k) S.X

Deformation.Examples.comparisonGlue_w, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverGlue.lean, line 404. The attribute's comment: “the compatibility of the two chart isomorphisms of the glueing with the comparison isomorphism of the datum, i.e. that the two of them are one morphism of the 2-fibre product; the equivalence itself is not proved here”.

The two chart isomorphisms of the glued deformation are compatible with the comparison isomorphism of the datum. This is the CategoryTheory.TwoFibreProductOver.Hom.w of the pair, that is, what makes Deformation.Examples.restrictGlueDeformationLeft and Deformation.Examples.restrictGlueDeformationRight the two components of a single morphism of the 2-fibre product. The source of Tag 0DYZ says only "we omit the verification".

theorem comparisonGlue_w :
    (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_left : U₁ ⊓ U₂ ≤ U₁)).map
        (restrictGlueDeformationLeftHom X U₁ U₂ Q hcover) ≫ Q.iso.hom =
      (restrictDeformationLEIso (glueDeformation X U₁ U₂ Q hcover)
            (inf_le_left : U₁ ⊓ U₂ ≤ U₁) ≪≫
          (restrictDeformationLEIso (glueDeformation X U₁ U₂ Q hcover)
            (inf_le_right : U₁ ⊓ U₂ ≤ U₂)).symm).hom ≫
        (openRestrictionLEFunctor (Λ := Λ) (k := k) (inf_le_right : U₁ ⊓ U₂ ≤ U₂)).map
          (restrictGlueDeformationRightHom X U₁ U₂ Q hcover)

Deformation.Examples.comparisonGlueHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverGlue.lean, line 453. The attribute's comment: “the comparison morphism from the comparison of the glued deformation to the datum, built from the two chart isomorphisms; it is an isomorphism, but only the morphism is constructed here, and the equivalence of Tag 0DYZ is not proved”.

Stacks 0DYZ, the comparison morphism out of the glueing. The two chart isomorphisms of the glued deformation are the two components of one morphism of the 2-fibre product from the comparison of the glued deformation to the datum it was glued from.

def comparisonGlueHom :
    (twoOpenComparisonFunctor (Λ := Λ) X U₁ U₂).obj (glueDeformation X U₁ U₂ Q hcover) ⟶ Q

Deformation.Examples.glueDeformationHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverGlue.lean, line 779. The attribute's comment: “the glueing construction of the proof on morphisms: a morphism of the 2-fibre product into the comparison of a deformation is glued to a morphism of deformations of X; the equivalence of Tag 0DYZ is not proved here”.

Stacks 0DYZ, the glueing quasi-inverse on morphisms. A morphism of the 2-fibre product from a datum Q to the comparison of a deformation P of X glues to a morphism from the deformation glued from Q to P. The source of Tag 0DYZ says only "we omit the verification".

def glueDeformationHom : glueDeformation X U₁ U₂ Q hcover ⟶ P

Deformation.Examples.twoOpenComparisonFunctor_map_glueDeformationHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverGlue.lean, line 801. The attribute's comment: “the compatibility of the glued morphism with the comparison morphism out of the glueing; the equivalence of Tag 0DYZ is not proved here”.

The triangle of the lifting problem commutes: the comparison of the glued morphism is the comparison morphism out of the glueing followed by the given morphism.

theorem twoOpenComparisonFunctor_map_glueDeformationHom :
    (twoOpenComparisonFunctor (Λ := Λ) X U₁ U₂).map (glueDeformationHom X U₁ U₂ Q hcover P g) =
      comparisonGlueHom X U₁ U₂ Q hcover ≫ g

Deformation.Examples.isSmooth_twoOpenComparisonBasedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverGlue.lean, line 860. The attribute's comment: “smoothness of the comparison morphism Def_X ⟶ Def_{U_1} ×_{Def_{U_12}} Def_{U_2}, which is what Tag 0DZN consumes; that the comparison morphism is an equivalence — the full assertion of 0DYZ — is not proved, and neither is the translation into the ring deformation categories Def_{P_i}”.

Stacks 0DYZ in the form Tag 0DZN uses it. If the two opens cover X then the comparison morphism Def_X ⟶ Def_{U₁} ×_{Def_{U₁ ⊓ U₂}} Def_{U₂} is smooth: a lifting problem is solved by glueing the datum over the smaller object of 𝒞_Λ to a deformation of X, glueing the given morphism to a morphism of deformations of X, and comparing the glued deformation with the datum by the two chart isomorphisms.

theorem isSmooth_twoOpenComparisonBasedFunctor (hcover : U₁ ⊔ U₂ = ⊤) :
    IsSmooth (twoOpenComparisonBasedFunctor (Λ := Λ) X U₁ U₂)

Deformation.Examples.GluingSituation.deformationCategories_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemesTwoOpenCoverRings.lean, line 357. The attribute's comment: “Def_X = Def_{P_1} ×_{Def_{P_12}} Def_{P_2} as an equivalence over 𝒞_Λ of deformation categories, with the ring deformation categories of Example 0DY1 and the restriction functors along U_12 ⊆ U_i”.

Stacks 0DYZ. In Situation 0DYY, Def_X and Def_{P₁} ×_{Def_{P₁₂}} Def_{P₂} are deformation categories, and the comparison functor between them is an equivalence of categories over 𝒞_Λ. Here Def_{P_i} is the deformation category of the k-algebra P_i of Example 0DY1, Def_X that of the scheme X of Example 0DY7, and the two legs of the 2-fibre product are the restriction functors Def_{P_i} ⟶ Def_{P₁₂} along U₁₂ ⊆ U_i.

theorem deformationCategories_equivalence :
    IsDeformationCategory.{u, u, u} (schemeDeformationCategoryProjection (Λ := Λ) (k := k) S.X) ∧
      IsDeformationCategory.{u, u, u} (ringChartDeformationsProjection S) ∧
      ∃ e : EquivalenceOver (schemeDeformationCategoryProjection (Λ := Λ) (k := k) S.X)
        (ringChartDeformationsProjection S), e.hom.functor = ringComparisonFunctor S

Sources

LeanDeformation.Examples.isCofiberedInGroupoids_chart · Deformation.Examples.FlatSchemeFamily · Deformation.Examples.FlatSchemeFamily.Hom · Deformation.Examples.FlatSchemeFamily.instCategory · Deformation.Examples.flatSchemeFamilyProjection · Deformation.Examples.flatSchemeFamilyProjection_cofiberedInGroupoids · Deformation.Examples.SchemeDeformationCategory · Deformation.Examples.SchemeDeformationCategory.Hom

Section93.10 Morphisms of Schemes #

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

Tag 0E3T, an example

Tag 0E3T in the Stacks Project.

Deformation.Examples.SchemeMorphismFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphisms.lean, line 68. The attribute's comment: “deformation_category_of_a_scheme_morphism”.

A flat family of morphisms of schemes over an object of 𝒞_Λ.

structure SchemeMorphismFamily (Λ : Type u) (k : Type v) [CommRing Λ] [Field k]
    [Algebra Λ k]

Deformation.Examples.SchemeMorphismFamily.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphisms.lean, line 94. The attribute's comment: “deformation_category_of_a_scheme_morphism”.

A cartesian morphism of flat families of morphisms of schemes, directed covariantly on the bases.

structure Hom (P Q : SchemeMorphismFamily.{u, v} Λ k)

Deformation.Examples.schemeMorphismFamilyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphisms.lean, line 133. The attribute's comment: “deformation_category_of_a_scheme_morphism”.

The functor sending a flat family of morphisms of schemes to its object of 𝒞_Λ.

def schemeMorphismFamilyFunctor :
    SchemeMorphismFamily.{u, v} Λ k ⥤ ArtinianLocalAlgCat.{u, v, v} Λ k

Deformation.Examples.schemeMorphismDeformationCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphisms.lean, line 183. The attribute's comment: “deformation_category_of_a_scheme_morphism”.

Deformations of a fixed morphism of schemes over the residue field.

abbrev schemeMorphismDeformationCategory {X Y : Scheme.{v}} (f : X ⟶ Y)
    (pX : X ⟶ baseSpec (residueFieldBase Λ k))
    (pY : Y ⟶ baseSpec (residueFieldBase Λ k))
    (hf : f ≫ pY = pX)

Deformation.Examples.schemeMorphismFamilyFunctor_cofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphisms.lean, line 298.

The category of flat families of morphisms of schemes is cofibered in groupoids over 𝒞_Λ.

theorem schemeMorphismFamilyFunctor_cofiberedInGroupoids
    {Λ : Type u} {k : Type v} [CommRing Λ] [Field k] [Algebra Λ k] :
    IsCofiberedInGroupoids (schemeMorphismFamilyFunctor.{u, v} (Λ := Λ) (k := k))

Tag 0E3U, a lemma

Tag 0E3U in the Stacks Project.

Deformation.Examples.isDeformationCategory_schemeMorphismDeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismsRimSchlessinger.lean, line 101. The attribute's comment: “the in-particular assertion only: granting (RS) for Example 0E3T as the hypothesis hRS, the deformation category Def_{X ⟶ Y} of a morphism of schemes X ⟶ Y over k is a deformation category. (RS) for Example 0E3T itself is NOT proved here”.

The second assertion of Stacks Tag 0E3U. Granting the Rim-Schlessinger condition for the category of all flat families of morphisms of schemes over 𝒞_Λ, the deformation category of a fixed morphism X ⟶ Y of schemes over the residue field is a deformation category: a predeformation category satisfying (RS).

theorem isDeformationCategory_schemeMorphismDeformationCategory
    (hRS : SatisfiesRS (schemeMorphismFamilyFunctor.{u, v} (Λ := Λ) (k := k)))
    {X Y : Scheme.{v}} (f : X ⟶ Y)
    (pX : X ⟶ baseSpec (residueFieldBase Λ k))
    (pY : Y ⟶ baseSpec (residueFieldBase Λ k))
    (hf : f ≫ pY = pX) :
    IsDeformationCategory (schemeMorphismDeformationCategoryProjection f pX pY hf)

Deformation.Examples.satisfiesRS_schemeMorphismFamilyFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismsRimSchlessingerSquares.lean, line 183. The attribute's comment: “condition (RS) for the category of all flat families of morphisms of schemes of Example 0E3T -- the first assertion -- with nothing assumed. The two gluing facts it rests on are the last assertion of Tag 07RV and the equivalence assertion of the closing paragraph of Tag 07RX, both proved in this repository: Stacks.Pushout.isPullback_of_isPushout_glued and Stacks.Pushout.isPushout_restrictions_of_flat. The pushout of spectra, the existence of the glued family, the flatness of its two structure morphisms and both halves of the universal property are proved as well. The in-particular assertion, that the deformation category of a fixed morphism of schemes over k is a deformation category, is Deformation.Examples.isDeformationCategory_schemeMorphismDeformationCategoryProjection”.

Stacks Project, Tag 0E3U, first assertion. The category of flat families of morphisms of schemes over 𝒞_Λ of Example 0E3T satisfies the Rim-Schlessinger condition (RS), with no hypothesis.

The fibre product of a cospan of families over a surjection of bases is glued twice over the one cocartesian square of spectra that the surjection produces: the sources are glued, the targets are glued, and the morphism between the two glued schemes is the descent of the two given morphisms along the pushout of the sources.

theorem satisfiesRS_schemeMorphismFamilyFunctor :
    SatisfiesRS (schemeMorphismFamilyFunctor.{u, v} (Λ := Λ) (k := k))

Deformation.Examples.isDeformationCategory_schemeMorphismDeformationCategoryProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismsRimSchlessingerUnconditional.lean, line 73. The attribute's comment: “the in-particular assertion, with nothing assumed: the deformation category Def_{X ⟶ Y} of a morphism of schemes X ⟶ Y over k is a deformation category, by the localization argument of Tag 06JC. Condition (RS) for the category of all flat families of morphisms of schemes of Example 0E3T -- the first assertion -- is Deformation.Examples.satisfiesRS_schemeMorphismFamilyFunctor, proved by gluing the sources and the targets over one cocartesian square of spectra”.

Stacks Project, Tag 0E3U, second assertion. The deformation category of a fixed morphism X ⟶ Y of schemes over the residue field is a deformation category: a predeformation category satisfying the Rim-Schlessinger condition (RS), with no hypothesis.

This is Deformation.Examples.isDeformationCategory_schemeMorphismDeformationCategory with its hypothesis supplied by Deformation.Examples.satisfiesRS_schemeMorphismFamilyFunctor.

theorem isDeformationCategory_schemeMorphismDeformationCategoryProjection {X Y : Scheme.{v}}
    (f : X ⟶ Y)
    (pX : X ⟶ baseSpec (residueFieldBase Λ k))
    (pY : Y ⟶ baseSpec (residueFieldBase Λ k))
    (hf : f ≫ pY = pX) :
    IsDeformationCategory (schemeMorphismDeformationCategoryProjection f pX pY hf)

Tag 0E3V, a lemma

Tag 0E3V in the Stacks Project.

Deformation.Examples.schemeMorphismTargetForgetful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 124. The attribute's comment: “the target-forgetting functor Def_{X ⟶ Y} ⟶ Def_Y, one half of the morphism of deformation categories Def_{X ⟶ Y} ⟶ Def_X × Def_Y of the source's proof”.

The functor from deformations of a morphism f : X ⟶ Y of schemes over the residue field to deformations of its target Y, keeping the family that deforms Y together with its identification of the fibre over the closed point and forgetting the family that deforms X.

def schemeMorphismTargetForgetful :
    schemeMorphismDeformationCategory f pX pY hf ⥤
      SchemeDeformationCategory (Λ := Λ) (k := k) (Over.mk pY)

Deformation.Examples.schemeMorphismTargetForgetful_comp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 163. The attribute's comment: “that the target-forgetting functor is a morphism of deformation categories over the base category”.

The target-forgetful functor commutes with the projections of the two deformation categories to 𝒞_Λ, so it is a morphism of categories over the base category.

theorem schemeMorphismTargetForgetful_comp_projection :
    schemeMorphismTargetForgetful f pX pY hf ⋙
        schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY) =
      schemeMorphismDeformationCategoryProjection f pX pY hf

Deformation.Examples.schemeMorphismSourceBased, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 203. The attribute's comment: “the source component of the morphism Def_{X → Y} → Def_X × Def_Y”.

The source-forgetful functor Def_{X ⟶ Y} ⟶ Def_X, as a morphism of categories over 𝒞_Λ.

def schemeMorphismSourceBased :
    BasedCategory.ofFunctor (schemeMorphismDeformationCategoryProjection f pX pY hf) ⥤ᵇ
      BasedCategory.ofFunctor
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX))

Deformation.Examples.schemeMorphismTargetBased, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 213. The attribute's comment: “the target component of the morphism Def_{X → Y} → Def_X × Def_Y”.

The target-forgetful functor Def_{X ⟶ Y} ⟶ Def_Y, as a morphism of categories over 𝒞_Λ.

def schemeMorphismTargetBased :
    BasedCategory.ofFunctor (schemeMorphismDeformationCategoryProjection f pX pY hf) ⥤ᵇ
      BasedCategory.ofFunctor
        (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY))

Deformation.Examples.schemeMorphismInfinitesimalPair, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 227. The attribute's comment: “the arrow Inf(Def_{X → Y}) → Inf(Def_X × Def_Y), as the pair of the maps induced on infinitesimal automorphisms by the two endpoint-forgetting 1-morphisms”.

Stacks 0E3V, the arrow Inf(Def_{X ⟶ Y}) → Inf(Def_X × Def_Y): the pair of the k-linear maps on infinitesimal automorphisms induced by the two endpoint-forgetting morphisms of deformation categories.

def schemeMorphismInfinitesimalPair
    (hM : SatisfiesRS (schemeMorphismDeformationCategoryProjection f pX pY hf))
    (hX : SatisfiesRS (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX)))
    (hY : SatisfiesRS (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)))
    {x₀ : schemeMorphismDeformationCategory f pX pY hf}
    (PM : ChosenPushforwardsAt (schemeMorphismDeformationCategoryProjection f pX pY hf) x₀)
    (QX : ChosenPushforwardsAt
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX))
      ((schemeMorphismSourceForgetful f pX pY hf).obj x₀))
    (QY : ChosenPushforwardsAt
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY))
      ((schemeMorphismTargetForgetful f pX pY hf).obj x₀)) :
    letI := naturalLocalizedTangentAddCommGroup PM hM
    letI := naturalLocalizedTangentModule PM hM
    letI := naturalLocalizedTangentAddCommGroup QX hX
    letI := naturalLocalizedTangentModule QX hX
    letI := naturalLocalizedTangentAddCommGroup QY hY
    letI := naturalLocalizedTangentModule QY hY
    localizedAutomorphismFunctorTangent PM →ₗ[k]
      localizedAutomorphismFunctorTangent QX × localizedAutomorphismFunctorTangent QY

Deformation.Examples.injective_schemeMorphismInfinitesimalPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 266. The attribute's comment: “exactness at the first spot: the arrow Inf(Def_{X → Y}) → Inf(Def_X × Def_Y) is injective”.

Stacks 0E3V, exactness at the first spot. The arrow Inf(Def_{X ⟶ Y}) → Inf(Def_X × Def_Y) is injective, so the sequence 0 → Inf(Def_{X ⟶ Y}) → Inf(Def_X × Def_Y) is exact: an infinitesimal automorphism of a deformation of f is a pair of infinitesimal automorphisms of the two endpoint deformations compatible with the arrow, and such a pair determines it.

theorem injective_schemeMorphismInfinitesimalPair
    (hM : SatisfiesRS (schemeMorphismDeformationCategoryProjection f pX pY hf))
    (hX : SatisfiesRS (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX)))
    (hY : SatisfiesRS (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)))
    {x₀ : schemeMorphismDeformationCategory f pX pY hf}
    (PM : ChosenPushforwardsAt (schemeMorphismDeformationCategoryProjection f pX pY hf) x₀)
    (QX : ChosenPushforwardsAt
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX))
      ((schemeMorphismSourceForgetful f pX pY hf).obj x₀))
    (QY : ChosenPushforwardsAt
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY))
      ((schemeMorphismTargetForgetful f pX pY hf).obj x₀)) :
    letI := naturalLocalizedTangentAddCommGroup PM hM
    letI := naturalLocalizedTangentModule PM hM
    letI := naturalLocalizedTangentAddCommGroup QX hX
    letI := naturalLocalizedTangentModule QX hX
    letI := naturalLocalizedTangentAddCommGroup QY hY
    letI := naturalLocalizedTangentModule QY hY
    Function.Injective (schemeMorphismInfinitesimalPair f pX pY hf hM hX hY PM QX QY)

Deformation.Examples.schemeMorphismTangentPair, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 296. The attribute's comment: “the arrow T Def_{X → Y} → T(Def_X × Def_Y), as the pair of the maps induced on tangent modules by the two endpoint-forgetting 1-morphisms”.

Stacks 0E3V, the arrow T Def_{X ⟶ Y} → T(Def_X × Def_Y): the pair of the k-linear maps on tangent modules induced by the two endpoint-forgetting morphisms of deformation categories.

def schemeMorphismTangentPair
    (hM : IsDeformationCategory.{u, u, u}
      (schemeMorphismDeformationCategoryProjection f pX pY hf))
    (hX : IsDeformationCategory.{u, u, u}
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX)))
    (hY : IsDeformationCategory.{u, u, u}
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)))
    (M : FGModuleCat.{u} k) :
    ↥(tangentModuleAt.{u, u, u}
        (BasedCategory.ofFunctor (schemeMorphismDeformationCategoryProjection f pX pY hf))
        hM M) →ₗ[k]
      ↥(tangentModuleAt.{u, u, u} (BasedCategory.ofFunctor
          (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX))) hX M) ×
        ↥(tangentModuleAt.{u, u, u} (BasedCategory.ofFunctor
          (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY))) hY M)

Deformation.Examples.exists_schemeMorphismTangentPair_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 357. The attribute's comment: “the image of the arrow T Def_{X → Y} → T(Def_X × Def_Y): a pair of first-order deformations of X and of Y is hit exactly when f deforms along it. The identification of the obstruction with a class in Ext^1(Lf^* NL_{Y/k}, O_X) is NOT proved”.

Stacks 0E3V, the image of the arrow T Def_{X ⟶ Y} → T(Def_X × Def_Y). A pair of first-order deformations X_ε of X and Y_ε of Y is in the image exactly when f deforms along it, that is, when some first-order deformation of f has the two given deformations as its endpoints up to isomorphism in the fibre. This is the content of the last paragraph of the source's proof; the identification of the obstruction to such a deformation with a class in Ext¹_{𝒪_X}(Lf^*NL_{Y/k}, 𝒪_X) is not proved here.

theorem exists_schemeMorphismTangentPair_eq_iff
    (hM : IsDeformationCategory.{u, u, u}
      (schemeMorphismDeformationCategoryProjection f pX pY hf))
    (hX : IsDeformationCategory.{u, u, u}
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX)))
    (hY : IsDeformationCategory.{u, u, u}
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)))
    (M : FGModuleCat.{u} k)
    (xε : (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX)).Fiber
      ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M))
    (yε : (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)).Fiber
      ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M)) :
    (∃ t, schemeMorphismTangentPair f pX pY hf hM hX hY M t =
        (tangentClassAt.{u, u, u} (BasedCategory.ofFunctor
            (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX))) hX M xε,
          tangentClassAt.{u, u, u} (BasedCategory.ofFunctor
            (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY))) hY M yε)) ↔
      ∃ mε : (schemeMorphismDeformationCategoryProjection f pX pY hf).Fiber
          ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M),
        IsIsomorphic ((fiberFunctor (schemeMorphismSourceBased f pX pY hf)
            ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M)).obj mε) xε ∧
          IsIsomorphic ((fiberFunctor (schemeMorphismTargetBased f pX pY hf)
            ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M)).obj mε) yε

Deformation.Examples.schemeMorphismDeformation_endpointArrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismEndpoints.lean, line 421. The attribute's comment: “PARTIAL. Of the six-term exact sequence this establishes: the arrow Inf(Def_{X → Y}) → Inf(Def_X × Def_Y) and the arrow T Def_{X → Y} → T(Def_X × Def_Y), both as the pairs of the maps induced by the source- and target-forgetting 1-morphisms Def_{X → Y} → Def_X and Def_{X → Y} → Def_Y; exactness at the FIRST spot, i.e. exactness of 0 → Inf(Def_{X → Y}) → Inf(Def_X × Def_Y); and the description of the IMAGE of T Def_{X → Y} → T(Def_X × Def_Y) as the pairs of first-order deformations of X and Y along which f deforms. NOT established: the terms Der_k(O_Y, f_O_X) and Ext^1(Lf^ NL_{Y/k}, O_X), the three arrows Inf(Def_X × Def_Y) → Der_k(O_Y, f_O_X), Der_k(O_Y, f_O_X) → T Def_{X → Y} and T(Def_X × Def_Y) → Ext^1(Lf^* NL_{Y/k}, O_X), and exactness at the second, third and fourth spots. Hypotheses carried rather than proved: condition (RS) for Example 0E3T, and that Def_X and Def_Y are deformation categories”.

Stacks 0E3V, the part of the six-term exact sequence that this file establishes.

For a morphism f : X ⟶ Y of schemes over k, the morphism of deformation categories Def_{X ⟶ Y} ⟶ Def_X × Def_Y of the source's proof induces two of the six arrows of the source's sequence, and the package records them together with what is proved about exactness:

the sequence 0 → Inf(Def_{X ⟶ Y}) → Inf(Def_X × Def_Y) is exact, i.e. the arrow on infinitesimal automorphisms is injective;

the arrow on tangent spaces is the pair of the maps induced by the two forgetful morphisms;

a pair of first-order deformations of X and of Y is in the image of that arrow exactly when f deforms along it.

The three remaining arrows of the source's sequence — the two involving Der_k(𝒪_Y, f_*𝒪_X) and the obstruction map into Ext¹_{𝒪_X}(Lf^*NL_{Y/k}, 𝒪_X) — and exactness at the second, third and fourth spots are not proved; see the implementation notes of this file.

The deformation hypothesis on Def_{X ⟶ Y} is supplied by Deformation.Examples.isDeformationCategory_schemeMorphismDeformationCategory from condition (RS) for the category of all flat families of morphisms of schemes.

theorem schemeMorphismDeformation_endpointArrows
    (hM : IsDeformationCategory.{u, u, u}
      (schemeMorphismDeformationCategoryProjection f pX pY hf))
    (hX : IsDeformationCategory.{u, u, u}
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX)))
    (hY : IsDeformationCategory.{u, u, u}
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)))
    {x₀ : schemeMorphismDeformationCategory f pX pY hf}
    (PM : ChosenPushforwardsAt (schemeMorphismDeformationCategoryProjection f pX pY hf) x₀)
    (QX : ChosenPushforwardsAt
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX))
      ((schemeMorphismSourceForgetful f pX pY hf).obj x₀))
    (QY : ChosenPushforwardsAt
      (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY))
      ((schemeMorphismTargetForgetful f pX pY hf).obj x₀))
    (M : FGModuleCat.{u} k) :
    letI := naturalLocalizedTangentAddCommGroup PM hM.satisfiesRS
    letI := naturalLocalizedTangentModule PM hM.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup QX hX.satisfiesRS
    letI := naturalLocalizedTangentModule QX hX.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup QY hY.satisfiesRS
    letI := naturalLocalizedTangentModule QY hY.satisfiesRS
    Function.Injective (schemeMorphismInfinitesimalPair f pX pY hf hM.satisfiesRS
        hX.satisfiesRS hY.satisfiesRS PM QX QY) ∧
      (∀ t, schemeMorphismTangentPair f pX pY hf hM hX hY M t =
        (tangentMapAt.{u, u, u} hM hX (schemeMorphismSourceBased f pX pY hf) M t,
          tangentMapAt.{u, u, u} hM hY (schemeMorphismTargetBased f pX pY hf) M t)) ∧
      ∀ (xε : (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX)).Fiber
          ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M))
        (yε : (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)).Fiber
          ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M)),
        (∃ t, schemeMorphismTangentPair f pX pY hf hM hX hY M t =
            (tangentClassAt.{u, u, u} (BasedCategory.ofFunctor
                (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX))) hX M xε,
              tangentClassAt.{u, u, u} (BasedCategory.ofFunctor
                (schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pY)))
                hY M yε)) ↔
          ∃ mε : (schemeMorphismDeformationCategoryProjection f pX pY hf).Fiber
              ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M),
            IsIsomorphic ((fiberFunctor (schemeMorphismSourceBased f pX pY hf)
                ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M)).obj mε) xε ∧
              IsIsomorphic ((fiberFunctor (schemeMorphismTargetBased f pX pY hf)
                ((squareZeroExtensionArtinian.{u, u, u} Λ k).obj M)).obj mε) yε

Deformation.Examples.schemeMorphismDeformation_sixTermExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismSixTermExact.lean, line 234. The attribute's comment: “the canonical exact sequence of k-vector spaces 0 -> Inf(Def_{X -> Y}) -> Inf(Def_X x Def_Y) -> Der_k(O_Y, f_O_X) -> T Def_{X -> Y} -> T(Def_X x Def_Y) -> Ext^1_{O_X}(Lf^ NL_{Y/k}, O_X) for a morphism of schemes f : X -> Y over k: its five k-linear maps and exactness at all five spots”.

Let f : X → Y be a morphism of schemes over k (Example 0DY7). There is a canonical exact sequence of k-vector spaces

0 → Inf(Def_{X → Y}) → Inf(Def_X × Def_Y) → Der_k(𝒪_Y, f_*𝒪_X) → T Def_{X → Y} → T(Def_X × Def_Y) → Ext¹_{𝒪_X}(Lf^*NL_{Y/k}, 𝒪_X).

The six terms are localizedAutomorphismFunctorTangent of the fixed pushforwards schemeMorphismTrivialPushforwards f pX pY hf (Inf(Def_{X → Y})), the product of those of schemeMorphismSourcePushforwards f pX pY hf and schemeMorphismTargetPushforwards f pX pY hf (Inf(Def_X × Def_Y)), schemeMorphismDerivations f pY (Der_k(𝒪_Y, f_*𝒪_X)), the tangent module of Def_{X → Y} over k[ε] (T Def_{X → Y}), the product of the tangent modules of Def_X and Def_Y over k[ε] (T(Def_X × Def_Y)), and schemeMorphismObstructionExt f pY (Ext¹_{𝒪_X}(Lf^*NL_{Y/k}, 𝒪_X)), each with its k-vector space structure. The products are the source's Def_X × Def_Y: for the 2-fibre product schemeEndpointsProduct pX pY over 𝒞_Λ (a deformation category, isDeformationCategory_schemeEndpointsProduct), the projections induce k-linear equivalences schemeEndpointsProductInfEquiv (Inf(Def\_X × Def\_Y) ≃ Inf(Def\_X) × Inf(Def\_Y)) and schemeEndpointsProductTangentEquiv (T(Def\_X × Def\_Y) ≃ T Def\_X × T Def\_Y), and the arrows a and d below are the maps induced by Def_{X → Y} → Def_X × Def_Y (schemeMorphismEndpointsBased) followed by these equivalences (schemeMorphismInfinitesimalPair'_canonical_eq, schemeMorphismTangentPair'_eq).

The five arrows are a = schemeMorphismInfinitesimalPair' and d = schemeMorphismTangentPair', induced by the endpoint-forgetting morphisms; b = schemeMorphismSixTermConjugationArrow, (α, β) ↦ the derivation by which β⁻¹ ∘ f' ∘ α differs from the trivial lift f' = f × id; c = schemeMorphismDerivationTangentLinearMap, D ↦ the class of D ⬝ f'; and e = schemeMorphismObstructionLinearMap, (X', Y') ↦ Push(Y') − Pull(X'), the obstruction of Tag 08U8. The statement: a is injective (exactness at Inf(Def_{X → Y})) and the sequence is exact at Inf(Def_X × Def_Y), Der_k(𝒪_Y, f_*𝒪_X), T Def_{X → Y} and T(Def_X × Def_Y).

theorem schemeMorphismDeformation_sixTermExact :
    letI := naturalLocalizedTangentAddCommGroup (schemeMorphismTrivialPushforwards f pX pY hf)
      (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY hf).satisfiesRS
    letI := naturalLocalizedTangentModule (schemeMorphismTrivialPushforwards f pX pY hf)
      (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY hf).satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup (schemeMorphismSourcePushforwards f pX pY
        hf) (isDeformationCategory_schemeDeformationCategoryProjection (Over.mk pX)).satisfiesRS
    letI := naturalLocalizedTangentModule (schemeMorphismSourcePushforwards f pX pY
        hf) (isDeformationCategory_schemeDeformationCategoryProjection (Over.mk pX)).satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup (schemeMorphismTargetPushforwards f pX pY
        hf) (isDeformationCategory_schemeDeformationCategoryProjection (Over.mk pY)).satisfiesRS
    letI := naturalLocalizedTangentModule (schemeMorphismTargetPushforwards f pX pY
        hf) (isDeformationCategory_schemeDeformationCategoryProjection (Over.mk pY)).satisfiesRS
    letI := schemeMorphismDerivationsModule f pY
      (SheafOfModules.unit (structureSheafRing X.toRingedSpace))
    letI := schemeMorphismObstructionExtModule f pY
    Function.Injective (schemeMorphismInfinitesimalPair' f pX pY hf
        (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY
        hf).satisfiesRS (schemeMorphismTrivialPushforwards f pX pY hf)
            (schemeMorphismSourcePushforwards f pX pY hf) (schemeMorphismTargetPushforwards f pX pY
            hf)) ∧
      Function.Exact (schemeMorphismInfinitesimalPair' f pX pY hf
          (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY
          hf).satisfiesRS (schemeMorphismTrivialPushforwards f pX pY hf)
              (schemeMorphismSourcePushforwards f pX pY hf) (schemeMorphismTargetPushforwards f pX
              pY hf)) (schemeMorphismSixTermConjugationArrow f pX pY hf) ∧
      Function.Exact (schemeMorphismSixTermConjugationArrow f pX pY hf)
        (schemeMorphismDerivationTangentLinearMap f pX pY hf) ∧
      Function.Exact (schemeMorphismDerivationTangentLinearMap f pX pY hf)
        (schemeMorphismTangentPair' f pX pY hf
            (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY
            hf) (FGModuleCat.of k (ULift.{u} k))) ∧
      Function.Exact (schemeMorphismTangentPair' f pX pY hf
            (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY
            hf) (FGModuleCat.of k (ULift.{u} k)))
        (schemeMorphismObstructionLinearMap f pX pY hf)

Tag 0E3W, a lemma

Tag 0E3W in the Stacks Project.

Deformation.Examples.isFiniteDimensionalDeformationCategory_schemeMorphismDeformationCategoryProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismsFiniteDimensional.lean, line 87. The attribute's comment: “for a morphism f : X -> Y of schemes over k with X and Y both proper over k, Inf(Def_{X -> Y}) and T Def_{X -> Y} are finite dimensional; stated as condition (4) of Deformation.IsFiniteDimensionalDeformationCategory: the tangent space, and the infinitesimal automorphisms at every point over k and every choice of pushforwards, are finite dimensional”.

Stacks Project, Tag 0E3W. In the setting of Tag 0E3V — a morphism f : X → Y of schemes over the field k — if X and Y are both proper over k, then Inf(Def_{X → Y}) and T Def_{X → Y} are finite dimensional.

The statement is condition (4) of Deformation.IsFiniteDimensionalDeformationCategory for the deformation category Def_{X → Y} of Example 0E3T: it is a deformation category, its tangent space T Def_{X → Y} (isomorphism classes over the dual numbers, with the vector space structure of Tag 06IH) is finite dimensional, and its infinitesimal automorphisms are finite dimensional at every point over k and every choice of pushforwards.

theorem isFiniteDimensionalDeformationCategory_schemeMorphismDeformationCategoryProjection
    [IsProper pX] [IsProper pY] :
    IsFiniteDimensionalDeformationCategory
      (schemeMorphismDeformationCategoryProjection f pX pY hf)

Tag 0ET6, a lemma

Tag 0ET6 in the Stacks Project.

Deformation.Examples.exists_hull_schemeMorphismIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismsHull.lean, line 120. The attribute's comment: “the functor of isomorphism classes of Def_{X -> Y} has a hull”. References: SGA 7 VI (4.9), “(a)”.

Stacks 0ET6, the hull. Let Λ be a complete local ring with residue field k and let f : X ⟶ Y be a morphism of proper k-schemes. Then the functor A ↦ Ob(Def_{X → Y}(A))/≅ of isomorphism classes of deformations of f has a hull: a versal formal object whose differential is bijective.

theorem exists_hull_schemeMorphismIsomorphismClasses (hΛ : IsClassical Λ k)
    [IsProper pX] [IsProper pY] :
    let G := isomorphismClasses
      (BasedCategory.ofFunctor (schemeMorphismDeformationCategoryProjection f pX pY hf))
      (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY
        hf).predeformation.cofibered
    ∃ ξ : FormalObject (CategoryOfElements.π G),
      IsHull (categoryOfElements_projection_isCofibered G) ξ

Deformation.Examples.isProrepresentableULift_schemeMorphismIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismsHull.lean, line 139. The attribute's comment: “if Der_k(O_X, O_X) = Der_k(O_Y, O_Y) = 0, the functor of isomorphism classes of Def_{X -> Y} is prorepresentable”.

Stacks 0ET6, prorepresentability. Let Λ be a complete local ring with residue field k and let f : X ⟶ Y be a morphism of proper k-schemes with Der_k(𝒪_X, 𝒪_X) = Der_k(𝒪_Y, 𝒪_Y) = 0. Then the functor A ↦ Ob(Def_{X → Y}(A))/≅ of isomorphism classes of deformations of f is prorepresentable.

theorem isProrepresentableULift_schemeMorphismIsomorphismClasses (hΛ : IsClassical Λ k)
    [IsProper pX] [IsProper pY]
    (hX : ∀ D : schemeMorphismDerivations (Λ := Λ) (k := k) (𝟙 X) pX, D = 0)
    (hY : ∀ D : schemeMorphismDerivations (Λ := Λ) (k := k) (𝟙 Y) pY, D = 0) :
    IsProrepresentableULift (isomorphismClasses
      (BasedCategory.ofFunctor (schemeMorphismDeformationCategoryProjection f pX pY hf))
      (isDeformationCategory_schemeMorphismDeformationCategoryProjection f pX pY
        hf).predeformation.cofibered)

Tag 0E3X, a lemma

Tag 0E3X in the Stacks Project.

Deformation.Examples.schemeMorphismSourceForgetful_comp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismSource.lean, line 221. The attribute's comment: “morphism of deformation categories”.

The source-forgetful functor commutes with the projections of the two deformation categories to 𝒞_Λ, so it is a morphism of categories over the base category: this is the morphism of deformation categories Def_{X ⟶ Y} ⟶ Def_X.

theorem schemeMorphismSourceForgetful_comp_projection :
    schemeMorphismSourceForgetful f pX pY hf ⋙
        schemeDeformationCategoryProjection (Λ := Λ) (k := k) (Over.mk pX) =
      Over.forget (schemeMorphismFamilySpecialFiber f pX pY hf) ⋙
        schemeMorphismFamilyFunctor

Deformation.Examples.schemeMorphismSourceForgetful_reflectsIsomorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismSource.lean, line 232. The attribute's comment: “reflects isomorphisms”.

The source-forgetful functor reflects isomorphisms: an arrow of deformations of f whose source component is invertible has invertible component on bases, and an arrow of flat families over an isomorphism of bases is an isomorphism.

instance schemeMorphismSourceForgetful_reflectsIsomorphisms :
    (schemeMorphismSourceForgetful f pX pY hf).ReflectsIsomorphisms

Deformation.Examples.schemeMorphismSourceForgetful_isEquivalence_of_specialFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SchemeMorphismSourceEquivalence.lean, line 123.

Let f : X ⟶ Y be a morphism of schemes over the residue field k such that the canonical map 𝒪_Y ⟶ f_*𝒪_X is an isomorphism and R¹f_*𝒪_X vanishes. Then the functor forgetting the target of a deformation of f is an equivalence from the deformation category of f to the deformation category of X.

theorem schemeMorphismSourceForgetful_isEquivalence_of_specialFibre
    (h0 : IsIso (C := Y.Modules) (Scheme.Modules.unitToPushforwardUnit f))
    (hR : IsZero (((Scheme.Modules.pushforward f).rightDerived 1).obj
      (SheafOfModules.unit X.ringCatSheaf))) :
    (schemeMorphismSourceForgetful f pX pY hf).IsEquivalence

Sources

LeanDeformation.Examples.SchemeMorphismFamily · Deformation.Examples.SchemeMorphismFamily.Hom · Deformation.Examples.schemeMorphismFamilyFunctor · Deformation.Examples.schemeMorphismDeformationCategory · Deformation.Examples.schemeMorphismFamilyFunctor_cofiberedInGroupoids · Deformation.Examples.isDeformationCategory_schemeMorphismDeformationCategory · Deformation.Examples.satisfiesRS_schemeMorphismFamilyFunctor · Deformation.Examples.isDeformationCategory_schemeMorphismDeformationCategoryProjection

Section93.11 Algebraic spaces #

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

Tag 0E3Z, an example

Tag 0E3Z in the Stacks Project.

Deformation.Examples.FlatAlgebraicSpaceFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 160. The attribute's comment: “the category ℱ: objects”.

Stacks 0E3Z. A flat family of algebraic spaces: an object of 𝒞_Λ together with an algebraic space over its spectrum, flat over it.

public structure FlatAlgebraicSpaceFamily

Deformation.Examples.FlatAlgebraicSpaceFamily.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 177. The attribute's comment: “the category ℱ: morphisms”.

Stacks 0E3Z. A morphism of flat families, covariant on coefficient algebras: a morphism of the coefficient algebras together with a cartesian morphism of spaces over it.

public structure Hom (P Q : FlatAlgebraicSpaceFamily B hΛ hSpec)

Deformation.Examples.FlatAlgebraicSpaceFamily.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 189. The attribute's comment: “the category ℱ”.

Stacks 0E3Z. Flat families of algebraic spaces and their cartesian morphisms form a category; composition pastes two cartesian squares.

public instance instCategory : Category (FlatAlgebraicSpaceFamily B hΛ hSpec)

Deformation.Examples.flatAlgebraicSpaceFamilyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 290. The attribute's comment: “the functor p”.

Stacks 0E3Z. Forget the space and retain the coefficient algebra.

public def flatAlgebraicSpaceFamilyFunctor :
    FlatAlgebraicSpaceFamily B hΛ hSpec ⥤ ArtinianLocalAlgCat.{u, u, u} Λ k

Deformation.Examples.flatAlgebraicSpaceFamilyFunctor_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 314. The attribute's comment: “p is cofibred in groupoids”.

Stacks 0E3Z. The projection from flat families of algebraic spaces to their coefficient algebras is cofibered in groupoids: the cocartesian lift of A ⟶ A' is the base change of the space along Spec A' ⟶ Spec A, which is flat because flatness of morphisms of algebraic spaces is stable under base change.

public theorem flatAlgebraicSpaceFamilyFunctor_isCofiberedInGroupoids :
    IsCofiberedInGroupoids (flatAlgebraicSpaceFamilyFunctor B hΛ hSpec)

Deformation.Examples.isFlat_of_over_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 339. The attribute's comment: “flatness of the special fibre”.

An algebraic space over the spectrum of the residue field is flat over it: the target of every étale chart is Spec k, over which any morphism is flat, and the atlas of Stacks 025Y supplies a surjective chart, so the one-chart form of Stacks 03MJ applies.

public theorem isFlat_of_over_residueField
    (X : (BigFppfOver B (Spec (.of Λ)) hΛ)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of Λ)) hΛ X)
    (toK : X ⟶ yoneda.obj (spaceBaseOver B hΛ hSpec (residueFieldBase Λ k))) :
    Space.IsFlat B (Spec (.of Λ)) hΛ toK

Deformation.Examples.spaceSpecialFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 364. The attribute's comment: “the object x₀”.

Stacks 0E3Z. An algebraic space X over the residue field, as the object (k, X) of the category of flat families.

public def spaceSpecialFiber (X : (BigFppfOver B (Spec (.of Λ)) hΛ)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of Λ)) hΛ X)
    (toK : X ⟶ yoneda.obj (spaceBaseOver B hΛ hSpec (residueFieldBase Λ k))) :
    FlatAlgebraicSpaceFamily B hΛ hSpec

Deformation.Examples.spaceDeformationProjection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Spaces.lean, line 378. The attribute's comment: “the deformation category of X”.

Stacks 0E3Z. The deformation category of an algebraic space X over the residue field, with its structure functor to 𝒞_Λ: its objects are flat families equipped with a cartesian morphism to (k, X).

public abbrev spaceDeformationProjection
    (X : (BigFppfOver B (Spec (.of Λ)) hΛ)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of Λ)) hΛ X)
    (toK : X ⟶ yoneda.obj (spaceBaseOver B hΛ hSpec (residueFieldBase Λ k))) :
    Over (spaceSpecialFiber B hΛ hSpec X hX toK) ⥤ ArtinianLocalAlgCat.{u, u, u} Λ k

Tag 0E40, a lemma

Tag 0E40 in the Stacks Project.

Deformation.Examples.satisfiesRS_flatAlgebraicSpaceFamilyFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesRimSchlessinger.lean, line 149. The attribute's comment: “condition (RS) for the category of flat families of algebraic spaces of Example 0E3Z”.

Stacks Project, Tag 0E40. The category of flat families of algebraic spaces over 𝒞_Λ of Example 0E3Z satisfies the Rim-Schlessinger condition (RS).

For a cospan X₁ ⟶ X ⟵ X₂ of flat families over A₁ ⟶ A ⟵ A₂ with A₂ ⟶ A surjective, the pushout of algebraic spaces X₂ ⨿_X X₁ (Stacks 07VX), with its morphism to the spectrum of A₁ ×_A A₂, is a flat family (Stacks 07W3, clause (2)) restricting to X₁ and X₂ (Stacks 07W0); it is a fibre product of flat families because any flat family over A₁ ×_A A₂ is the pushout of its two restrictions (the counit assertion of Stacks 07W3).

theorem satisfiesRS_flatAlgebraicSpaceFamilyFunctor :
    SatisfiesRS (flatAlgebraicSpaceFamilyFunctor B hΛ hSpec)

Deformation.Examples.isDeformationCategory_spaceDeformationProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesRimSchlessinger.lean, line 382. The attribute's comment: “the in-particular clause: the deformation category of an algebraic space over k is a deformation category”.

Stacks Project, Tag 0E40, the in-particular clause. The deformation category of an algebraic space X over the residue field k is a deformation category: a predeformation category satisfying (RS).

It is the category of flat families lying over the family (k, X), which lies over the residue field, a terminal object of 𝒞_Λ; condition (RS) for the category of all flat families is Deformation.Examples.satisfiesRS_flatAlgebraicSpaceFamilyFunctor.

theorem isDeformationCategory_spaceDeformationProjection
    (X : (BigFppfOver B (Spec (.of Λ)) hΛ)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of Λ)) hΛ X)
    (toK : X ⟶ yoneda.obj (spaceBaseOver B hΛ hSpec (residueFieldBase Λ k))) :
    IsDeformationCategory.{u, u, u} (spaceDeformationProjection B hΛ hSpec X hX toK)

Tag 0E41, a lemma

Tag 0E41 in the Stacks Project.

Deformation.Examples.spaceInfinitesimalAutomorphismGroupChain, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesInfinitesimalAutomorphisms.lean, line 97. The attribute's comment: “first display: for an algebraic space X over the field k, Inf(Def_X) = Ext^0(NL_{X/k}, O_X) = Hom(Omega_{X/k}, O_X) = Der_k(O_X, O_X), as three identifications at every point x0 over k and every pushforward x0 -> x_eps along a dual-number pair (06JS): Inf(Def_X) is isomorphic as a group to Der_k(O_X, O_X), Ext^0 out of the naive cotangent complex is k-linearly Hom(Omega_{X/k}, O_X), and Hom(Omega_{X/k}, O_X) is k-linearly Der_k(O_X, O_X), k acting through the structure morphism X -> Spec k. The second display, T Def_X = Ext^1(NL_{X/k}, O_X), is registered separately”.

The first display of [Stacks Project, Tag 0E41]. In Example 0E3Z, let X be an algebraic space over the field k. Then

Inf(𝓓_X) = Ext⁰_{𝒪_X}(NL_{X/k}, 𝒪_X) = Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X) = Der_k(𝒪_X, 𝒪_X),

given as the identifications of those four groups. Inf(𝓓_X) is the infinitesimal automorphism group Deformation.infinitesimalAutomorphismGroup of [Stacks Project, Tag 06JS] of the deformation category of X, a predeformation category (Deformation.Examples.isPredeformationCategory_spaceDeformationProjection), formed at an arbitrary point x₀ over k, an arbitrary pushforward i : x₀ ⟶ xε of it along a dual-number pair k → k[ε] → k — the automorphisms of the deformation X' of X over k[ε] (the trivial one, X ×_{Spec k} Spec k[ε]) which are the identity modulo ε.

k acts on 𝒪_X-modules, and so on Ext⁰, on Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X) and on Der_k(𝒪_X, 𝒪_X), through the pullback of functions along the structure morphism X ⟶ Spec k (Deformation.Examples.spaceResidueFieldRingHom).

The first component identifies Inf(𝓓_X) with Der_k(𝒪_X, 𝒪_X) as groups, composition of automorphisms corresponding to addition of derivations; through the other two it is Ext⁰_{𝒪_X}(NL_{X/k}, 𝒪_X).

The second is Ext⁰_{𝒪_X}(NL_{X/k}, 𝒪_X) = Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X), k-linearly, from H⁰(NL_{X/k}) = Ω_{X/k} (Stacks 0D0Y).

The third is Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X) = Der_k(𝒪_X, 𝒪_X), k-linearly, postcomposition with the universal derivation of Stacks 04CT, as Modules on Sites, Definition 04BN defines Ω.

def spaceInfinitesimalAutomorphismGroupChain
    [HasDerivedCategory.{w} (NaiveCotangentModules B (Spec (.of Λ)) hΛ (spaceOf B hΛ X hX))]
    {Aε : ArtinianLocalAlgCat.{u, u, u} Λ k}
    {x₀ : (spaceDeformationProjection B hΛ hSpec X hX toK).Fiber
      (residueFieldObject.{u, u, u} Λ k)}
    {xε : (spaceDeformationProjection B hΛ hSpec X hX toK).Fiber Aε}
    (g : residueFieldObject.{u, u, u} Λ k ⟶ Aε) (e : Aε ⟶ residueFieldObject.{u, u, u} Λ k)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1)
    (hi : (spaceDeformationProjection B hΛ hSpec X hX toK).IsHomLift g i) :
    letI := naiveCotangentModulesLinear B (Spec (.of Λ)) hΛ (X := spaceOf B hΛ X hX)
      (spaceResidueFieldRingHom B hΛ hSpec X hX toK)
    letI := modulesLinearOfRingHom B (Spec (.of Λ)) hΛ (X := spaceOf B hΛ X hX)
      (spaceResidueFieldRingHom B hΛ hSpec X hX toK)
    letI : Module k (SpaceDerivations B hΛ (spaceStructureMap B hΛ hSpec X hX toK)) :=
      derivationModuleOfRingHom B (Spec (.of Λ)) hΛ (X := spaceOf B hΛ X hX)
        (spaceResidueFieldRingHom B hΛ hSpec X hX toK)
        (spaceStructureMap B hΛ hSpec X hX toK) (spaceStructureModule B hΛ (spaceOf B hΛ X hX))
    (infinitesimalAutomorphismGroup
        (isPredeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK) g e hpair i hi ≃*
      Multiplicative (SpaceDerivations B hΛ (spaceStructureMap B hΛ hSpec X hX toK))) ×
    (DerivedCategory.Ext (DerivedCategory.Q.obj (naiveCotangentComplex B (Spec (.of Λ)) hΛ
        (spaceStructureMap B hΛ hSpec X hX toK)))
        ((DerivedCategory.singleFunctor _ 0).obj
          (naiveCotangentCoefficient B (Spec (.of Λ)) hΛ
            (spaceStructureModule B hΛ (spaceOf B hΛ X hX)))) 0 ≃ₗ[k]
      (sheafOfDifferentials B (Spec (.of Λ)) hΛ (spaceStructureMap B hΛ hSpec X hX toK) ⟶
        spaceStructureModule B hΛ (spaceOf B hΛ X hX))) ×
    ((sheafOfDifferentials B (Spec (.of Λ)) hΛ (spaceStructureMap B hΛ hSpec X hX toK) ⟶
        spaceStructureModule B hΛ (spaceOf B hΛ X hX)) ≃ₗ[k]
      SpaceDerivations B hΛ (spaceStructureMap B hΛ hSpec X hX toK))

Deformation.Examples.spaceInfinitesimalAutomorphismGroup_linearEquivDerivations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesInfinitesimalAutomorphismsLinear.lean, line 311. The attribute's comment: “first display, k-linear form: for an algebraic space X over the field k, Inf(Def_X) with the vector space structure of 06JV (addition is composition; c acts by pushforward along eps -> c eps, along every arrow over such a rescaling fixing the pushforward x0 -> x_eps) is k-linearly isomorphic to Der_k(O_X, O_X), k acting through the structure morphism X -> Spec k, by the first identification of the first display, at every point x0 over k and every pushforward along a dual-number pair”. References: SGA 3 II (3.14), “special case”.

The first display of [Stacks Project, Tag 0E41], k-linearly: Inf(𝓓_X) = Der_k(𝒪_X, 𝒪_X) as k-vector spaces. In Example 0E3Z, let X be an algebraic space over the field k. At every point x₀ of the deformation category of X over k, every pushforward i : x₀ ⟶ xε of it along a dual-number pair k → k[ε] → k and every predeformation-category structure, the infinitesimal automorphism group Inf(𝓓_X) of [Stacks Project, Tag 06JS] carries the k-vector-space structure of [Stacks Project, Tag 06JV]:

addition is composition of infinitesimal automorphisms;

a scalar c acts by pushforward along ε ↦ c ε: for every endomorphism s of the base which is ε ↦ c ε in a dual-number coordinate and every arrow j : xε ⟶ xε over s fixing i, c • a is the pushforward of a along j;

and the first identification of the first display, Deformation.Examples.spaceInfinitesimalAutomorphismGroupMulEquivDerivations, is a k-linear isomorphism onto Der_k(𝒪_X, 𝒪_X), k acting on derivations through the structure morphism X ⟶ Spec k. The remaining identifications of the display, Ext⁰_{𝒪_X}(NL_{X/k}, 𝒪_X) = Hom_{𝒪_X}(Ω_{X/k}, 𝒪_X) = Der_k(𝒪_X, 𝒪_X), are k-linear by Deformation.Examples.spaceInfinitesimalAutomorphismGroupChain.

theorem spaceInfinitesimalAutomorphismGroup_linearEquivDerivations :
    letI : Module k (SpaceDerivations B hΛ (spaceStructureMap B hΛ hSpec X hX toK)) :=
      derivationModuleOfRingHom B (Spec (.of Λ)) hΛ (X := spaceOf B hΛ X hX)
        (spaceResidueFieldRingHom B hΛ hSpec X hX toK)
        (spaceStructureMap B hΛ hSpec X hX toK) (spaceStructureModule B hΛ (spaceOf B hΛ X hX))
    ∃ A : AddCommGroup (Additive (infinitesimalAutomorphismGroup hp g e hpair i hi)),
      letI := A
      ∃ M : Module k (Additive (infinitesimalAutomorphismGroup hp g e hpair i hi)),
        letI := M
        (∀ a b : infinitesimalAutomorphismGroup hp g e hpair i hi,
          Additive.ofMul a + Additive.ofMul b = Additive.ofMul (a * b)) ∧
        (∀ (c : k) (s : Aε ⟶ Aε),
          (∃ φ : Aε ≃ₐ[Λ] DualNumber k,
            (∀ t : Aε, (φ t).1 = Aε.residueEquiv (IsLocalRing.residue Aε t)) ∧
            (∀ t : k, φ (s.hom (φ.symm (TrivSqZeroExt.inl t))) = TrivSqZeroExt.inl t) ∧
            φ (s.hom (φ.symm DualNumber.eps)) = c • DualNumber.eps) →
          ∀ (j : xε.1 ⟶ xε.1) (hj : (spaceDeformationProjection B hΛ hSpec X hX toK).IsHomLift s j),
            i ≫ j = i → ∀ a : infinitesimalAutomorphismGroup hp g e hpair i hi,
              ∃ b : infinitesimalAutomorphismGroup hp g e hpair i hi,
                b.val = pushforwardAutomorphismHom hp.cofibered s j hj a.val ∧
                  c • Additive.ofMul a = Additive.ofMul b) ∧
        ∃ E : Additive (infinitesimalAutomorphismGroup hp g e hpair i hi) ≃ₗ[k]
            SpaceDerivations B hΛ (spaceStructureMap B hΛ hSpec X hX toK),
          ∀ a : infinitesimalAutomorphismGroup hp g e hpair i hi,
            DFunLike.coe
              (F := Additive (infinitesimalAutomorphismGroup hp g e hpair i hi) ≃ₗ[k]
                SpaceDerivations B hΛ (spaceStructureMap B hΛ hSpec X hX toK)) E
              (Additive.ofMul a) =
            Multiplicative.toAdd
              (spaceInfinitesimalAutomorphismGroupMulEquivDerivations B hΛ hSpec X hX toK hpair i
                hp hi a)

Deformation.Examples.spaceTangentSpaceLinearEquivExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesTangentSpaceLinearEquivExt.lean, line 145. The attribute's comment: “second display: for an algebraic space X over the field k, T Def_X = Ext^1(NL_{X/k}, O_X) as k-vector spaces, from the tangent space of the deformation category of X (isomorphism classes of flat deformations of X over k[eps], with the canonical vector space structure of 06IH) onto Ext^1_{O_X}(NL_{X/k}, O_X) of the naive cotangent complex of 0D0V, k acting through the structure morphism X -> Spec k; a deformation goes to the 0GQ5 class of the extension 0 -> O_X -> O_X' -> O_X -> 0. The first display is registered separately”.

Stacks 0E41, second display. In Example 0E3Z let X be an algebraic space over k. Then T Def_X = Ext¹_{𝒪_X}(NL_{X/k}, 𝒪_X): the tangent space of the deformation category Def_X (the isomorphism classes of flat deformations of X over k[ε], with the vector-space structure of Stacks 06IH) is k-linearly isomorphic to Ext¹ of the naive cotangent complex NL_{X/k} of Stacks 0D0V into 𝒪_X (sections raised to the universe of NL_{X/k}, any model of the derived category), k acting through the structure morphism X ⟶ Spec k. A deformation X' goes to the class (Stacks 0GQ5) of the extension 0 ⟶ 𝒪_X ⟶ 𝒪_{X'} ⟶ 𝒪_X ⟶ 0 (Deformation.Examples.spaceTangentSpaceLinearEquivExtModel_apply).

def spaceTangentSpaceLinearEquivExt
    [HasDerivedCategory.{w} (Space.NaiveCotangentModules B (Spec (.of Λ)) hΛ (spaceOf B hΛ X hX))] :
    letI : Fact (IsPredeformationCategory
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK)).p) :=
      ⟨(isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π (isomorphismClasses
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX
          toK).predeformation.cofibered))) :=
      ⟨Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK)⟩
    letI := Space.naiveCotangentModulesLinear B (Spec (.of Λ)) hΛ (X := spaceOf B hΛ X hX)
      (spaceResidueFieldRingHom B hΛ hSpec X hX toK)
    artinianTangentSpace Λ k (isomorphismClasses
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX
          toK).predeformation.cofibered) ≃ₗ[k]
      DerivedCategory.Ext
        (DerivedCategory.Q.obj (Space.naiveCotangentComplex B (Spec (.of Λ)) hΛ
          (spaceStructureMap B hΛ hSpec X hX toK)))
        ((DerivedCategory.singleFunctor _ 0).obj
          (Space.naiveCotangentCoefficient B (Spec (.of Λ)) hΛ
            (spaceStructureModule B hΛ (spaceOf B hΛ X hX)))) 1

Tag 0E42, a lemma

Tag 0E42 in the Stacks Project.

Deformation.Examples.spaceInfinitesimalAutomorphisms_finiteDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesFiniteDimensional.lean, line 99. The attribute's comment: “infinitesimal automorphisms: for an algebraic space X proper over the field k, Inf(Def_X), with the vector space structure of 06JV (addition is composition; c acts by pushforward along eps -> c eps), is finite dimensional over k, at every point x0 over k and every pushforward x0 -> x_eps along a dual-number pair”.

Stacks 0E42, the infinitesimal automorphisms. In Example 0E3Z, let X be an algebraic space over the field k which is proper over k. Then Inf(𝓓_X) is a finite-dimensional k-vector space: at every point x₀ of 𝓓_X over k and every pushforward i : x₀ ⟶ xε of it along a dual-number pair k → Aε → k, the infinitesimal automorphism group of Stacks 06JS carries a k-vector-space structure

whose addition is composition of infinitesimal automorphisms, and

in which a scalar c acts by pushforward along ε ↦ c ε: for every endomorphism s of Aε which is ε ↦ c ε in a dual-number coordinate of Aε (and the identity on the residue field) and every arrow j : xε ⟶ xε over s fixing i, c • a is the pushforward of a along j,

and this vector space is finite dimensional. The predeformation-category structure of 𝓓_X is that of Stacks 0E40 (Deformation.Examples.isDeformationCategory_spaceDeformationProjection).

theorem spaceInfinitesimalAutomorphisms_finiteDimensional
    (hproper : Space.IsProper B (Spec (.of Λ)) hΛ toK)
    {Aε : ArtinianLocalAlgCat.{u, u, u} Λ k}
    {x₀ : (spaceDeformationProjection B hΛ hSpec X hX toK).Fiber
      (residueFieldObject.{u, u, u} Λ k)}
    {xε : (spaceDeformationProjection B hΛ hSpec X hX toK).Fiber Aε}
    (g : residueFieldObject.{u, u, u} Λ k ⟶ Aε) (e : Aε ⟶ residueFieldObject.{u, u, u} Λ k)
    (hpair : IsCanonicalDualNumberPair g e) (i : x₀.1 ⟶ xε.1)
    (hi : (spaceDeformationProjection B hΛ hSpec X hX toK).IsHomLift g i) :
    ∃ hA : AddCommGroup (infinitesimalAutomorphismGroup
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation g e
        hpair i hi),
      letI := hA
      ∃ hM : Module k (infinitesimalAutomorphismGroup
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation g e
        hpair i hi),
        letI := hM
        (∀ a b : (infinitesimalAutomorphismGroup
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation g e
        hpair i hi), a + b = a * b) ∧
        (∀ (c : k) (s : Aε ⟶ Aε),
            IsDualNumberScaling c s →
            s ≫ e = e →
            ∀ (j : xε.1 ⟶ xε.1)
                (hj : (spaceDeformationProjection B hΛ hSpec X hX toK).IsHomLift s j),
              i ≫ j = i → ∀ a : (infinitesimalAutomorphismGroup
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation g e
        hpair i hi),
                ∃ b : (infinitesimalAutomorphismGroup
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation g e
        hpair i hi),
                  b.val = pushforwardAutomorphismHom
                    (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX
                      toK).predeformation.cofibered s j hj a.val ∧ c • a = b) ∧
        FiniteDimensional k (infinitesimalAutomorphismGroup
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation g e
        hpair i hi)

Deformation.Examples.spaceTangentSpace_finiteDimensional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesTangentSpaceFinite.lean, line 55. The attribute's comment: “tangent space: for an algebraic space X proper over the field k, the tangent space T Def_X of its deformation category (isomorphism classes of flat deformations over k[eps], with the canonical vector space structure of 06IH) is finite dimensional over k. The clause on Inf(Def_X) is registered separately”.

Stacks 0E42, the tangent space. In Lemma 0E41, if the algebraic space X is proper over k, then T Def_X (with the vector-space structure of Stacks 06IH) is finite dimensional over k.

theorem spaceTangentSpace_finiteDimensional (hproper : Space.IsProper B (Spec (.of Λ)) hΛ toK) :
    letI : Fact (IsPredeformationCategory
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK)).p) :=
      ⟨(isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK).predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π (isomorphismClasses
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX
          toK).predeformation.cofibered))) :=
      ⟨Artin.schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX toK)⟩
    FiniteDimensional k (artinianTangentSpace Λ k (isomorphismClasses
        (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
        (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX
          toK).predeformation.cofibered))

Tag 0ET7, a lemma

Tag 0ET7 in the Stacks Project.

Deformation.Examples.exists_hull_spaceIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesHull.lean, line 102. The attribute's comment: “for a proper algebraic space X over k and Λ complete local with residue field k, the functor of isomorphism classes of Def_X has a hull”.

Stacks 0ET7, the hull. Let Λ be a complete local ring with residue field k and let X be a proper algebraic space over k. Then the functor A ↦ Ob(Def_X(A))/≅ of isomorphism classes of deformations of X has a hull: a versal formal object whose differential is bijective.

public theorem exists_hull_spaceIsomorphismClasses (hcl : IsClassical Λ k)
    (hproper : Space.IsProper B (Spec (.of Λ)) hΛ toK) :
    let G := isomorphismClasses
      (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
      (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX
        toK).predeformation.cofibered
    ∃ ξ : FormalObject (CategoryOfElements.π G),
      IsHull (categoryOfElements_projection_isCofibered G) ξ

Deformation.Examples.isProrepresentableULift_spaceIsomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/SpacesHull.lean, line 120. The attribute's comment: “if Der_k(O_X, O_X) = 0, the functor of isomorphism classes of Def_X is prorepresentable”.

Stacks 0ET7, prorepresentability. Let Λ be a complete local ring with residue field k and let X be a proper algebraic space over k with Der_k(𝒪_X, 𝒪_X) = 0. Then the functor A ↦ Ob(Def_X(A))/≅ of isomorphism classes of deformations of X is prorepresentable.

public theorem isProrepresentableULift_spaceIsomorphismClasses (hcl : IsClassical Λ k)
    (hproper : Space.IsProper B (Spec (.of Λ)) hΛ toK)
    (hDer : ∀ D : SpaceDerivations B hΛ (spaceStructureMap B hΛ hSpec X hX toK), D = 0) :
    IsProrepresentableULift (isomorphismClasses
      (BasedCategory.ofFunctor (spaceDeformationProjection B hΛ hSpec X hX toK))
      (isDeformationCategory_spaceDeformationProjection B hΛ hSpec X hX
        toK).predeformation.cofibered)

Sources

LeanDeformation.Examples.FlatAlgebraicSpaceFamily · Deformation.Examples.FlatAlgebraicSpaceFamily.Hom · Deformation.Examples.FlatAlgebraicSpaceFamily.instCategory · Deformation.Examples.flatAlgebraicSpaceFamilyFunctor · Deformation.Examples.flatAlgebraicSpaceFamilyFunctor_isCofiberedInGroupoids · Deformation.Examples.isFlat_of_over_residueField · Deformation.Examples.spaceSpecialFiber · Deformation.Examples.spaceDeformationProjection

Section93.12 Deformations of completions #

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

Tag 0DZ1, a lemma

Tag 0DZ1 in the Stacks Project.

Deformation.Examples.DerivedLift.exists_flat_lift_iff_exists_derived_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Tor/BaseChangeIndependence/DerivedLift.lean, line 481.

Over a nilpotent surjection, an A-flat module lifts flatly if and only if it admits a bounded-above derived lift.

public theorem exists_flat_lift_iff_exists_derived_lift
    (A' A P' : Type u) [CommRing A'] [CommRing A] [CommRing P']
    [Algebra A' A] [Algebra A' P']
    (hsurj : Function.Surjective (algebraMap A' A))
    (hnil : IsNilpotent (RingHom.ker (algebraMap A' A)))
    [Module.Flat A' P']
    (M : Type v) [AddCommGroup M] [Module (TensorProduct A' P' A) M]
    [Module A M] [IsScalarTower A (TensorProduct A' P' A) M]
    [Module.Flat A M] :
    (∃ (M' : Type (max u v)) (_ : AddCommGroup M')
      (_ : Module P' M') (_ : Module A' M') (_ : IsScalarTower A' P' M'),
      Module.Flat A' M' ∧
        Nonempty
          ((ModuleCat.extendScalars.{u, u, max u v}
              (algebraMap P' (TensorProduct A' P' A))).obj
                (ModuleCat.of.{max u v, u} P' M') ≅
            ModuleCat.of.{max u v, u} (TensorProduct A' P' A) (ULift.{u} M))) ↔
      ∃ (K : DerivedCategory.Minus (ModuleCat.{max u v} P')),
        Nonempty
          ((CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral.{u, v, u}
            (algebraMap P' (TensorProduct A' P' A))).functor.obj K.obj ≅
            (DerivedCategory.Q
              (C := ModuleCat.{max u v} (TensorProduct A' P' A))).obj
                ((CochainComplex.singleFunctor
                  (ModuleCat.{max u v} (TensorProduct A' P' A)) 0).obj
                    (ModuleCat.of.{max u v, u} (TensorProduct A' P' A)
                      (ULift.{u} M))))

Tag 0DZ2, a lemma

Tag 0DZ2 in the Stacks Project.

Deformation.HasFlatModuleLift.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FlatModuleLift.lean, line 280. The attribute's comment: “the implication (1) => (2) of 0DZ2, in full, at the source's hypotheses and with no hypothesis added. This is what the tag asserts in this library: the converse is FALSE at the source's hypotheses, a Stacks ERRATUM. The biconditional is refuted, at every universe, by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatement, and in the form that writes out every one of the source's hypotheses by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatementFaithful. Inside the forward implication nothing is restricted: it carries the source's own nilpotence hypothesis on the kernel of P' → P and is more general than the source in needing neither the Noetherian hypotheses, nor finiteness of M, nor the ideal J', nor the local liftability hypothesis, and every binder it does carry is used. A restricted converse — a finite M under a square-zero thickening P' → P — is proved in StacksFrontier.Deformation.FlatModuleLiftLocalization, whose clause records why the dévissage to the source's nilpotent thickening is not merely unavailable from 0DZ2's hypotheses but closed: the step it needs is Deformation.ObstructionIndependentOfLift and that statement is unsatisfiable, by Deformation.not_obstructionIndependentOfLift”.

Stacks 0DZ2, forward implication. In a commuting square of ring maps P' → Q', P' → P, Q' → Q, P → Q whose left vertical map p is surjective with nilpotent kernel and whose top map P' → Q' is flat, a flat module lift of a P-module M base-changes to a flat module lift of Q ⊗[P] M.

By Nakayama the lift N is generated over P' by a family indexed by M, so Q' ⊗[P'] N is a quotient of M →₀ Q' and can be presented in the universe of Q' and M, which is what HasFlatModuleLift demands of the witness.

This direction of Stacks 0DZ2 carries the source's own hypothesis on the kernel of P' → P — nilpotent, not square-zero — and uses none of the obstruction calculus, so it is faithful and in fact more general than the source: neither the Noetherian hypotheses, nor finiteness of M, nor the ideal J', nor the local liftability hypothesis is needed. The converse is the obstruction-theoretic half, and is exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift_of_isNilpotent_ker in StacksFrontier.Deformation.FlatModuleLiftLocalization.

public theorem HasFlatModuleLift.baseChange
    {A' : Type u₁} {P' : Type u₃} {P : Type u₄} {Q' : Type u₅} {Q : Type u₆}
    [CommRing A'] [CommRing P'] [CommRing P] [CommRing Q'] [CommRing Q]
    [Algebra A' P'] [Algebra P' Q'] [Algebra P Q]
    {p : P' →+* P} {q : Q' →+* Q}
    (hcomm : (algebraMap P Q).comp p = q.comp (algebraMap P' Q'))
    (hflat : Module.Flat P' Q')
    (hp : Function.Surjective p) (hnp : IsNilpotent (RingHom.ker p))
    (M : Type v) [AddCommGroup M] [Module P M]
    (h : HasFlatModuleLift (algebraMap A' P') p M) :
    HasFlatModuleLift ((algebraMap P' Q').comp (algebraMap A' P')) q (Q ⊗[P] M)

Deformation.exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift_of_isNilpotent_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FlatModuleLiftLocalization.lean, line 584. The attribute's comment: “a RESTRICTED form of 0DZ2, restricted by exactly two hypotheses: hzeroP, which asks the thickening P' → P to be square-zero rather than merely nilpotent, and Module.Finite P M, which asks M to be finite over P. NEITHER IS REMOVABLE, because the UNRESTRICTED statement is FALSE — a Stacks ERRATUM — so what 0DZ2 asserts in this library is the implication (1) => (2), registered on Deformation.HasFlatModuleLift.baseChange. It is refuted, at every universe, by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatement, and in the form that writes out every one of the source's hypotheses by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatementFaithful. That witness satisfies both of the hypotheses whose removal is at issue in the other direction: its ker(A' → A) = (t) has t³ = 0 and t² ≠ 0, so it is nilpotent and not square-zero, and its M IS finite over P. What follows is why each restriction is there. Corrected: M is assumed finite over P. The source's statement omits it, its own proof uses it — here we use that P is Noetherian and M finite, when invoking Stacks 0A6A to commute Ext² with the flat base change P → Q — and that step is FALSE without it, not merely unproved: for k countable, P = k[x, y], Q = k[[x, y]], A' = k[ε]/(ε²), J' = (x, y) and the non-finite A-flat module M = ⨁ₙ P/(xⁿ, yⁿ), the comparison Ext²_P(M, M ⊗_P IP) ⊗_P Q → Ext²_Q(M ⊗_P Q, (M ⊗_P Q) ⊗_Q IQ) is the multiplication map T ⊗_P Q → T of a copy of Q sitting inside the infinite product T that Ext out of an infinite direct sum produces, and Q ⊗_P Q → Q has a nonzero kernel. Nothing weaker will do either: over the Noetherian P that 0DZ2 assumes, the (-3)-pseudo-coherence that Stacks 087Q needs in degree 2 is equivalent to finiteness. The computation, and the Mayer–Vietoris identification of what a finiteness-free proof would still owe, are in the implementation notes of this file; the equivalence itself is not refuted for a non-finite M, only the source's proof of it. Also: the thickening P' → P is assumed square-zero rather than merely nilpotent, which is what the obstruction calculus of Stacks 0DYR needs in order to have an obstruction class at all. Those are the only two deviations: the kernel of A' → A itself is assumed only nilpotent, as in the source, and squareness of the second thickening Q' → Q is derived rather than assumed, by Deformation.sq_ker_algebraMap_tensorProduct_eq_bot_of_tower; so this statement is strictly stronger than the one registered on Deformation.exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift. The dévissage from the square-zero thickening to the source's nilpotent one is NOT available from 0DZ2's own hypotheses. The source's reduction is details omitted; with A'' = A'/I^{n-1} every hypothesis of the lemma transports to the stage A'' → A, including local liftability, which reduces along the already-proved forward direction, so the induction produces an A''-flat P''-lift M'' of M — and then needs the obstruction class of the square-zero step A' → A'' to be independent of which A''-flat P''-lift of M it is evaluated on. Grant that and the induction closes; it is false already for I³ = 0. All of this is now a Lean object rather than a paragraph: the tower of quotients is Deformation.squareZero_devissage, a lift across one step of it is a lift across the composite by Deformation.hasFlatModuleLift_comp, the generic step of the induction with its missing input named is Deformation.hasFlatModuleLift_of_obstructionIndependentOfLift, that input is Deformation.ObstructionIndependentOfLift, and it is UNSATISFIABLE — Deformation.not_obstructionIndependentOfLift, at every universe, by the elementary witness A' = ℤ/8, Q' = A'[ε]/(ε²), where the two lifts Q''/(ε) and Q''/(ε − 2) over Q'' = Q'/4Q' have the same reduction and only the first lifts. So the source's route to the nilpotent case is closed, not untried. In the shape the source's own k would take it: over A' = k[t]/(t³), P' = k[t, x]/(t³, x²), the module M = k has the A'-flat P'-lift P'/(x), while its A''-flat P''-lift P''/(x - t) has none, the two obstructions differing by the Yoneda square of the separating class in Ext¹_{k[x]/(x²)}(k, k); and that is a legitimate instance of 0DZ2, with Q' = P' and J' = P'. Selecting M'' instead by Q'' ⊗ M'' ≅ N'' would need base change to be surjective on isomorphism classes of lifts, i.e. Ext¹_P(M, M ⊗_P ĪP) to be J'-power torsion by Stacks 0A6A and 05EC, which fails already for a hypersurface M = P/(f). Full diagnosis in the implementation notes of this file”.

Stacks 0DZ2 with the source's local liftability hypothesis, at the source's nilpotence hypothesis. Let A' → A be a surjection of commutative rings with nilpotent kernel whose thickening P' → P is square-zero, let P' and Q' be flat A'-algebras with P' → Q' flat, let P = P' ⊗_{A'} A and Q = Q' ⊗_{A'} A with P Noetherian and P/J'P ≅ Q/J'Q for an ideal J' of P', and let N be the base change to Q of a P-module M finite over P and flat over A. If for every g ∈ J' the base change of M to the localization of P at the image of g has an A'-flat module lift over (P')_g, then M has an A'-flat lift to a P'-module if and only if N has an A'-flat lift to a Q'-module.

This is exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift with the hypothesis ker(A' → A)² = ⊥ dropped, so that the kernel of A' → A carries only the nilpotence the source assumes; what remains square-zero is the single thickening P' → P, squareness of Q' → Q being derived from it by Deformation.sq_ker_algebraMap_tensorProduct_eq_bot_of_tower.

Flatness of N over A is not assumed, in either form: N is isomorphic to Q ⊗_P M and M is A-flat, so flat_base_of_baseChangeEquiv supplies it. The source does not assume it either.

The localization of P at the image of g is realized as (P')_g ⊗_{A'} A, which IsLocalization.Away.tensorBaseChange identifies with it.

theorem exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift_of_isNilpotent_ker
    (A' A P' Q' : Type u) [CommRing A'] [CommRing A] [CommRing P'] [CommRing Q']
    [Algebra A' A] [Algebra A' P'] [Algebra A' Q'] [Algebra P' Q'] [IsScalarTower A' P' Q']
    [Module.Flat A' P'] [Module.Flat P' Q']
    (hsurjA : Function.Surjective (algebraMap A' A))
    (hnilA : IsNilpotent (RingHom.ker (algebraMap A' A)))
    (hzeroP : (RingHom.ker (algebraMap P' (TensorProduct A' P' A))) ^ 2 = ⊥)
    [Algebra (TensorProduct A' P' A) (TensorProduct A' Q' A)]
    [IsNoetherianRing (TensorProduct A' P' A)]
    (hcomm : (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A)).comp
        (algebraMap P' (TensorProduct A' P' A)) =
      (algebraMap Q' (TensorProduct A' Q' A)).comp (algebraMap P' Q'))
    (hflatPQ : Module.Flat (TensorProduct A' P' A) (TensorProduct A' Q' A))
    (J' : Ideal P')
    (hquot : Function.Bijective (Ideal.quotientMap
      ((J'.map (algebraMap P' (TensorProduct A' P' A))).map
        (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A)))
      (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A)) Ideal.le_comap_map))
    (M : Type u) [AddCommGroup M] [Module (TensorProduct A' P' A) M] [Module A M]
    [IsScalarTower A (TensorProduct A' P' A) M] [Module.Flat A M]
    [Module.Finite (TensorProduct A' P' A) M]
    (N : Type u) [AddCommGroup N] [Module (TensorProduct A' Q' A) N] [Module A N]
    [IsScalarTower A (TensorProduct A' Q' A) N]
    (hN : Nonempty ((ModuleCat.extendScalars.{u, u, u}
        (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A))).obj
          (ModuleCat.of (TensorProduct A' P' A) (ULift.{u} M)) ≅
      ModuleCat.of (TensorProduct A' Q' A) (ULift.{u} N)))
    (K : DerivedCategory (ModuleCat.{u} (TensorProduct A' P' A)))
    (hK : (DerivedCategory.TStructure.t
      (C := ModuleCat.{u} (TensorProduct A' P' A))).minus K)
    (eK : K ≅ DerivedCategory.Q.obj ((CochainComplex.singleFunctor
      (ModuleCat.{u} (TensorProduct A' P' A)) 0).obj
        (ModuleCat.of (TensorProduct A' P' A) (ULift.{u} M))))
    (hlocal : ∀ g ∈ J',
      letI : Algebra (TensorProduct A' P' A) (TensorProduct A' (Localization.Away g) A) :=
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom A' P' (Localization.Away g))
          (AlgHom.id A' A)).toRingHom.toAlgebra
      ∃ (L : Type u) (_ : AddCommGroup L) (_ : Module (Localization.Away g) L)
        (_ : Module A' L) (_ : IsScalarTower A' (Localization.Away g) L),
        Module.Flat A' L ∧ Nonempty
          ((ModuleCat.extendScalars.{u, u, u} (algebraMap (Localization.Away g)
              (TensorProduct A' (Localization.Away g) A))).obj
                (ModuleCat.of (Localization.Away g) L) ≅
            ModuleCat.of (TensorProduct A' (Localization.Away g) A)
              (ULift.{u} (TensorProduct (TensorProduct A' P' A)
                (TensorProduct A' (Localization.Away g) A) (ULift.{u} M))))) :
    (∃ (M' : Type u) (_ : AddCommGroup M') (_ : Module P' M') (_ : Module A' M')
        (_ : IsScalarTower A' P' M'), Module.Flat A' M' ∧
        Nonempty ((ModuleCat.extendScalars.{u, u, u}
            (algebraMap P' (TensorProduct A' P' A))).obj (ModuleCat.of P' M') ≅
          ModuleCat.of (TensorProduct A' P' A) (ULift.{u} M))) ↔
      (∃ (N' : Type u) (_ : AddCommGroup N') (_ : Module Q' N') (_ : Module A' N')
        (_ : IsScalarTower A' Q' N'), Module.Flat A' N' ∧
        Nonempty ((ModuleCat.extendScalars.{u, u, u}
            (algebraMap Q' (TensorProduct A' Q' A))).obj (ModuleCat.of Q' N') ≅
          ModuleCat.of (TensorProduct A' Q' A) (ULift.{u} N)))

Deformation.exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FlatModuleLiftLocalization.lean, line 716. The attribute's comment: “a RESTRICTED form of 0DZ2, restricted by hzeroA — the kernel of A' → A is assumed square-zero rather than merely nilpotent — and by Module.Finite P M. NEITHER IS REMOVABLE: the UNRESTRICTED statement is FALSE — a Stacks ERRATUM — so what 0DZ2 asserts in this library is the implication (1) => (2), registered on Deformation.HasFlatModuleLift.baseChange. It is refuted at every universe by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatement and, with every source hypothesis written out, by Deformation.Examples.ArtinSchreier.not_flatModuleLiftBaseChangeStatementFaithful, whose witness has a nilpotent non-square-zero ker(A' → A) and a finite M. Why each restriction is there: M is assumed finite over P — the source's statement omits it, its own proof uses it when invoking Stacks 0A6A to commute Ext² with the flat base change P → Q, and that step is false without it, by the counterexample written out in the implementation notes of this file; and the kernel of A' → A is assumed square-zero rather than merely nilpotent, which is what makes both the nilpotence of that kernel and squareness of the thickening P' → P theorems here rather than hypotheses. This is the weaker of the two registrations: exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift_of_isNilpotent_ker carries the source's nilpotence on that kernel and asks squareness only of the thickening P' → P, and the clause there records why the dévissage to the source's nilpotent thickening is not available from 0DZ2's own hypotheses”.

Stacks 0DZ2 with the source's local liftability hypothesis. Let A' → A be a surjection of commutative rings with square-zero kernel, let P' and Q' be flat A'-algebras with P' → Q' flat, let P = P' ⊗_{A'} A and Q = Q' ⊗_{A'} A with P Noetherian and P/J'P ≅ Q/J'Q for an ideal J' of P', and let N be the base change to Q of a P-module M finite over P and flat over A. If for every g ∈ J' the base change of M to the localization of P at the image of g has an A'-flat module lift over (P')_g, then M has an A'-flat lift to a P'-module if and only if N has an A'-flat lift to a Q'-module.

Flatness of N over A is not assumed here either; see exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift_of_isNilpotent_ker.

The localization of P at the image of g is realized as (P')_g ⊗_{A'} A, which IsLocalization.Away.tensorBaseChange identifies with it.

theorem exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift
    (A' A P' Q' : Type u) [CommRing A'] [CommRing A] [CommRing P'] [CommRing Q']
    [Algebra A' A] [Algebra A' P'] [Algebra A' Q'] [Algebra P' Q'] [IsScalarTower A' P' Q']
    [Module.Flat A' P'] [Module.Flat P' Q']
    (hsurjA : Function.Surjective (algebraMap A' A))
    (hzeroA : (RingHom.ker (algebraMap A' A)) ^ 2 = ⊥)
    [Algebra (TensorProduct A' P' A) (TensorProduct A' Q' A)]
    [IsNoetherianRing (TensorProduct A' P' A)]
    (hcomm : (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A)).comp
        (algebraMap P' (TensorProduct A' P' A)) =
      (algebraMap Q' (TensorProduct A' Q' A)).comp (algebraMap P' Q'))
    (hflatPQ : Module.Flat (TensorProduct A' P' A) (TensorProduct A' Q' A))
    (J' : Ideal P')
    (hquot : Function.Bijective (Ideal.quotientMap
      ((J'.map (algebraMap P' (TensorProduct A' P' A))).map
        (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A)))
      (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A)) Ideal.le_comap_map))
    (M : Type u) [AddCommGroup M] [Module (TensorProduct A' P' A) M] [Module A M]
    [IsScalarTower A (TensorProduct A' P' A) M] [Module.Flat A M]
    [Module.Finite (TensorProduct A' P' A) M]
    (N : Type u) [AddCommGroup N] [Module (TensorProduct A' Q' A) N] [Module A N]
    [IsScalarTower A (TensorProduct A' Q' A) N]
    (hN : Nonempty ((ModuleCat.extendScalars.{u, u, u}
        (algebraMap (TensorProduct A' P' A) (TensorProduct A' Q' A))).obj
          (ModuleCat.of (TensorProduct A' P' A) (ULift.{u} M)) ≅
      ModuleCat.of (TensorProduct A' Q' A) (ULift.{u} N)))
    (K : DerivedCategory (ModuleCat.{u} (TensorProduct A' P' A)))
    (hK : (DerivedCategory.TStructure.t
      (C := ModuleCat.{u} (TensorProduct A' P' A))).minus K)
    (eK : K ≅ DerivedCategory.Q.obj ((CochainComplex.singleFunctor
      (ModuleCat.{u} (TensorProduct A' P' A)) 0).obj
        (ModuleCat.of (TensorProduct A' P' A) (ULift.{u} M))))
    (hlocal : ∀ g ∈ J',
      letI : Algebra (TensorProduct A' P' A) (TensorProduct A' (Localization.Away g) A) :=
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom A' P' (Localization.Away g))
          (AlgHom.id A' A)).toRingHom.toAlgebra
      ∃ (L : Type u) (_ : AddCommGroup L) (_ : Module (Localization.Away g) L)
        (_ : Module A' L) (_ : IsScalarTower A' (Localization.Away g) L),
        Module.Flat A' L ∧ Nonempty
          ((ModuleCat.extendScalars.{u, u, u} (algebraMap (Localization.Away g)
              (TensorProduct A' (Localization.Away g) A))).obj
                (ModuleCat.of (Localization.Away g) L) ≅
            ModuleCat.of (TensorProduct A' (Localization.Away g) A)
              (ULift.{u} (TensorProduct (TensorProduct A' P' A)
                (TensorProduct A' (Localization.Away g) A) (ULift.{u} M))))) :
    (∃ (M' : Type u) (_ : AddCommGroup M') (_ : Module P' M') (_ : Module A' M')
        (_ : IsScalarTower A' P' M'), Module.Flat A' M' ∧
        Nonempty ((ModuleCat.extendScalars.{u, u, u}
            (algebraMap P' (TensorProduct A' P' A))).obj (ModuleCat.of P' M') ≅
          ModuleCat.of (TensorProduct A' P' A) (ULift.{u} M))) ↔
      (∃ (N' : Type u) (_ : AddCommGroup N') (_ : Module Q' N') (_ : Module A' N')
        (_ : IsScalarTower A' Q' N'), Module.Flat A' N' ∧
        Nonempty ((ModuleCat.extendScalars.{u, u, u}
            (algebraMap Q' (TensorProduct A' Q' A))).obj (ModuleCat.of Q' N') ≅
          ModuleCat.of (TensorProduct A' Q' A) (ULift.{u} N)))

Tag 0DZ3, a lemma

Tag 0DZ3 in the Stacks Project.

Deformation.hasFlatAlgebraLift_iff_hasFlatAlgebraLift_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FlatAlgebraLiftCompletionNilpotent.lean, line 348. The attribute's comment: “Spec(B) → Spec(A) being syntomic on the complement of V(𝔟) is read pointwise and affinely: for every prime 𝔮 not containing 𝔟 there is g ∉ 𝔮 with A → B_g syntomic, the characterization of Stacks 00SY and 01UE. B^∧ is AdicCompletion 𝔟 B. The published proof rests on Stacks 0DZ2, which is false at a nilpotent kernel; the proof here approximates a flat lift over the completed presentation by relation solutions over the polynomial presentation and corrects them one power of the kernel at a time (Artin-Rees plus Stacks 07M8 at every level). See the module docstring.”.

Stacks 0DZ3. Let A' → A be a surjective map of Noetherian rings with nilpotent kernel, let A → B be a finite type flat ring map and let 𝔟 ⊆ B be an ideal such that Spec(B) → Spec(A) is syntomic on the complement of V(𝔟). Then B has a flat lift to A' if and only if the 𝔟-adic completion B^∧ has a flat lift to A'.

Spec(B) → Spec(A) is syntomic at the point 𝔮 exactly when A → B_g is syntomic for some g ∉ 𝔮 (Stacks 00SY, 01UE); that is how the hypothesis hsyn reads the source's condition at every point 𝔮 of the complement of V(𝔟). The proof does not go through Stacks 0DZ2 (which is false at a nilpotent kernel); see the module documentation.

public theorem hasFlatAlgebraLift_iff_hasFlatAlgebraLift_adicCompletion
    (A' A B : Type u) [CommRing A'] [CommRing A] [CommRing B]
    [IsNoetherianRing A'] [IsNoetherianRing A] [Algebra A' A] [Algebra A B]
    (hsurjA : Function.Surjective (algebraMap A' A))
    (hnilA : IsNilpotent (RingHom.ker (algebraMap A' A)))
    [Algebra.FiniteType A B] [Module.Flat A B] (b : Ideal B)
    (hsyn : ∀ q : Ideal B, q.IsPrime → ¬ b ≤ q →
      ∃ g ∉ q, Algebra.Syntomic A (Localization.Away g)) :
    HasFlatAlgebraLift A' A B ↔ HasFlatAlgebraLift A' A (AdicCompletion b B)

Tag 0DZ4, a lemma

Tag 0DZ4 in the Stacks Project.

Deformation.Examples.exists_squareZeroAlgebraExtensionClassesCompletionEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CompletionFirstOrder.lean, line 1035.

Stacks 0DZ4. For a finite type algebra B over a field k which is smooth over k outside the zero set of an ideal J, and a finite B-module N, completion along J is a bijection from the isomorphism classes of square-zero extensions of B by N to those of B^ by N^, matching a class with its image exactly when the two extensions admit a k-algebra map of middle rings over B → B^ and over N → N^.

public theorem exists_squareZeroAlgebraExtensionClassesCompletionEquiv
    (k : Type uk) (B : Type uB) [Field k] [CommRing B] [Algebra k B]
    [Algebra.FiniteType k B] (J : Ideal B)
    (hsm : ∀ q : PrimeSpectrum B, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal)
    (N : Type uN) [AddCommGroup N] [Module B N] [Module.Finite B N] :
    ∃ e : SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB, uN,
        max uB uN} (algebraExtensionProblem k B N) ≃
      SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB, uN,
        max uB uN} (algebraExtensionProblem k (AdicCompletion J B) (AdicCompletion J N)),
      ∀ (X : (algebraExtensionProblem k B N).CompatibleExtension.{max uB uN})
        (Y : (algebraExtensionProblem k (AdicCompletion J B)
          (AdicCompletion J N)).CompatibleExtension.{max uB uN}),
        (∃ h : X.B' →ₐ[k] Y.B',
            (∀ z : X.B', Y.toB (h z) = algebraMap B (AdicCompletion J B) (X.toB z)) ∧
              ∀ n : N, h (kernelInclusion X n) =
                kernelInclusion Y (AdicCompletion.of J N n)) ↔
          e ⟦X⟧ = ⟦Y⟧

Tag 0DZ5, a lemma

Tag 0DZ5 in the Stacks Project.

Deformation.Examples.isSmooth_adicCompletionFunctorData_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CompletionSmooth.lean, line 457. The attribute's comment: “the first conclusion, smoothness, over an arbitrary base-compatible completion functor datum, and unconditionally: no hypothesis stands for Stacks 0DZ2, because only the square-zero case of Stacks 0DZ3 is consumed and that case is proved in StacksFrontier.Deformation.FlatModuleLiftBaseChangeAbstract. The second conclusion, the isomorphism on tangent spaces, is Deformation.Examples.bijective_differential_adicCompletionFunctorData over the same data. RESTRICTED in the same way as that declaration, to a datum satisfying Deformation.Examples.AdicCompletionFunctorData.IsBaseCompatible; at the canonical choice the conclusion is Deformation.Examples.isSmooth_adicCompletionFunctor”. References: SGA 7 VI (4.13), “(a), special case”.

Stacks 0DZ5, the smoothness conclusion. Let k be a field, P a finite type k-algebra, J ⊆ P an ideal such that Spec(P) → Spec(k) is smooth outside V(J), and P^ the J-adic completion. The completion functor 𝓓_P ⟶ 𝓓_{P^} of Stacks 0DYV is smooth.

The criterion of Stacks 0DYP reduces this to surjectivity of the differential, which is Deformation.Examples.bijective_differential_adicCompletionFunctorData, and to the correspondence of liftability, which is Deformation.Examples.lifts_adicCompletionFunctorData_unconditional.

theorem isSmooth_adicCompletionFunctorData_unconditional [Algebra.FiniteType k P]
    (F : AdicCompletionFunctorData (Λ := Λ) (k := k) P J) (hF : F.IsBaseCompatible)
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    IsSmooth F.functor

Deformation.Examples.bijective_differential_adicCompletionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CompletionSmooth.lean, line 512. The attribute's comment: “the second conclusion only: the functor induces an isomorphism on tangent spaces. The first conclusion, smoothness, is Deformation.Examples.isSmooth_adicCompletionFunctor”.

Stacks 0DZ5, the tangent-space conclusion. This is Deformation.Examples.bijective_differential_adicCompletionFunctorData specialized to the completion functor Deformation.Examples.adicCompletionFunctor of Stacks 0DYV, whose base-compatibility is Deformation.Examples.isBaseCompatible_adicCompletionFunctor; so no hypothesis on the functor remains.

theorem bijective_differential_adicCompletionFunctor [Algebra.FiniteType k P]
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    letI : IsNoetherianRing P := Algebra.FiniteType.isNoetherianRing k P
    Function.Bijective (differential (𝓕 := ringDeformationBasedCategory Λ k P)
      (𝓖 := ringDeformationBasedCategory Λ k (AdicCompletion J P))
      isCofiberedInGroupoids_ringDeformationProjection
      isCofiberedInGroupoids_ringDeformationProjection
      (adicCompletionFunctor (Λ := Λ) (k := k) P J).functor)

Deformation.Examples.isSmooth_adicCompletionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CompletionSmooth.lean, line 532. The attribute's comment: “the first conclusion, smoothness. The second conclusion, the isomorphism on tangent spaces, is Deformation.Examples.bijective_differential_adicCompletionFunctor”.

Stacks 0DZ5, the smoothness conclusion. This is Deformation.Examples.isSmooth_adicCompletionFunctorData_unconditional specialized to the completion functor Deformation.Examples.adicCompletionFunctor of Stacks 0DYV, whose base-compatibility is Deformation.Examples.isBaseCompatible_adicCompletionFunctor; so no hypothesis on the functor remains.

theorem isSmooth_adicCompletionFunctor [Algebra.FiniteType k P]
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    letI : IsNoetherianRing P := Algebra.FiniteType.isNoetherianRing k P
    IsSmooth (adicCompletionFunctor (Λ := Λ) (k := k) P J).functor

Deformation.Examples.bijective_differential_baseCompatibleAdicCompletionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CompletionSmooth.lean, line 568. The attribute's comment: “the second conclusion only: the functor induces an isomorphism on tangent spaces. Stated at the canonical base-compatible completion functor datum Deformation.Examples.baseCompatibleAdicCompletionFunctor rather than over an arbitrary datum, so there is no hypothesis on the functor; it is still RESTRICTED to a base-compatible datum. The first conclusion, smoothness, is proved over an arbitrary base-compatible datum by Deformation.Examples.isSmooth_adicCompletionFunctorData_unconditional, and at Deformation.Examples.adicCompletionFunctor by Deformation.Examples.isSmooth_adicCompletionFunctor”.

Stacks 0DZ5, the tangent-space conclusion, at the canonical base-compatible completion functor. This is Deformation.Examples.bijective_differential_adicCompletionFunctorData specialized to Deformation.Examples.baseCompatibleAdicCompletionFunctor, whose base-compatibility is its own second component; so no hypothesis on the functor remains.

theorem bijective_differential_baseCompatibleAdicCompletionFunctor
    [Algebra.FiniteType k P] [IsNoetherianRing P]
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    Function.Bijective (differential (𝓕 := ringDeformationBasedCategory Λ k P)
      (𝓖 := ringDeformationBasedCategory Λ k (AdicCompletion J P))
      isCofiberedInGroupoids_ringDeformationProjection
      isCofiberedInGroupoids_ringDeformationProjection
      (baseCompatibleAdicCompletionFunctor (Λ := Λ) (k := k) P J).1.functor)

Deformation.Examples.bijective_differential_adicCompletionFunctorData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CompletionTangentSpace.lean, line 360. The attribute's comment: “the second conclusion only: the functor induces an isomorphism on tangent spaces. The first conclusion, smoothness, is not proved here; granted the correspondence of liftability it is Deformation.Examples.isSmooth_adicCompletionFunctorData_of_lifts. RESTRICTED: the statement is for any completion functor datum of Stacks 0DYV which in addition satisfies Deformation.Examples.AdicCompletionFunctorData.IsBaseCompatible, and such data exist by Deformation.Examples.nonempty_isBaseCompatible_adicCompletionFunctorData; it is not for the arbitrary choice Deformation.Examples.adicCompletionFunctor, which satisfies only the clauses recorded in Stacks 0DYV. See the implementation notes”.

Stacks 0DZ5, the tangent-space conclusion. Let k be a field, P a finite type k-algebra, J ⊆ P an ideal such that Spec(P) → Spec(k) is smooth outside V(J), and P^ the J-adic completion. The completion functor 𝓓_P ⟶ 𝓓_{P^} of Stacks 0DYV induces a bijection on tangent spaces.

The proof is the source's: the family of extension classes of Stacks 0DY3 is a bijection of each tangent space with a first Ext group of the naive cotangent complex, by Deformation.Examples.bijective_tangentExtClass; the functor is compatible with those classes through the two comparison maps of Stacks 0GPV, by Deformation.Examples.squareZeroFiberExtClass_completion; and both comparison maps are bijective by Stacks 0DZ4.

public theorem bijective_differential_adicCompletionFunctorData
    [Algebra.FiniteType k P]
    (F : AdicCompletionFunctorData (Λ := Λ) (k := k) P J) (hF : F.IsBaseCompatible)
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    Function.Bijective (differential (𝓕 := ringDeformationBasedCategory Λ k P)
      (𝓖 := ringDeformationBasedCategory Λ k (AdicCompletion J P))
      isCofiberedInGroupoids_ringDeformationProjection
      isCofiberedInGroupoids_ringDeformationProjection F.functor)

Deformation.Examples.isSmooth_adicCompletionFunctorData_of_lifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/CompletionTangentSpace.lean, line 435. The attribute's comment: “the first conclusion, smoothness, GRANTED the hypothesis hlifts: that a deformation lifts along a small extension of its Artinian base whenever its completion does. That correspondence of liftability is the deformation-category reading of Stacks 0DZ3 and is NOT proved here, so this declaration is not the conclusion of the tag. The tag's other input, surjectivity of the differential, is supplied in full from Deformation.Examples.bijective_differential_adicCompletionFunctorData, and the reduction to the two inputs is Stacks 0DYP. RESTRICTED in the same way as that declaration, to a base-compatible completion functor datum. See the implementation notes”.

Stacks 0DZ5, the smoothness conclusion, granted the correspondence of liftability. Under the hypotheses of Stacks 0DZ5, the completion functor 𝓓_P ⟶ 𝓓_{P^} is smooth as soon as liftability of a deformation along a small extension of the Artinian base is implied by liftability of its completion.

That implication is the deformation-category reading of Stacks 0DZ3 and is the only input missing: the other half of the criterion of Stacks 0DYP, surjectivity of the differential, is Deformation.Examples.bijective_differential_adicCompletionFunctorData.

public theorem isSmooth_adicCompletionFunctorData_of_lifts
    [Algebra.FiniteType k P]
    (F : AdicCompletionFunctorData (Λ := Λ) (k := k) P J) (hF : F.IsBaseCompatible)
    (hsm : ∀ q : PrimeSpectrum P, ¬ J ≤ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal)
    (hlifts : ∀ ⦃B A : ArtinianLocalAlgCat.{u, w, w} Λ k⦄ (f : B ⟶ A),
      InfinitesimalLifting.IsSmallExtension (CommRingCat.ofHom f.hom.toRingHom) →
        ∀ x : (ringDeformationBasedCategory Λ k P).p.Fiber A,
          (∃ (y' : (ringDeformationBasedCategory Λ k (AdicCompletion J P)).obj)
              (g : y' ⟶ F.functor.obj x.1),
            (ringDeformationBasedCategory Λ k (AdicCompletion J P)).p.IsHomLift f g) →
            ∃ (x' : (ringDeformationBasedCategory Λ k P).obj) (h : x' ⟶ x.1),
              (ringDeformationBasedCategory Λ k P).p.IsHomLift f h) :
    IsSmooth F.functor

Sources

LeanDeformation.Examples.DerivedLift.exists_flat_lift_iff_exists_derived_lift · Deformation.HasFlatModuleLift.baseChange · Deformation.exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift_of_isNilpotent_ker · Deformation.exists_flat_lift_iff_exists_flat_lift_baseChange_of_localizationLift · Deformation.hasFlatAlgebraLift_iff_hasFlatAlgebraLift_adicCompletion · Deformation.Examples.exists_squareZeroAlgebraExtensionClassesCompletionEquiv · Deformation.Examples.isSmooth_adicCompletionFunctorData_unconditional · Deformation.Examples.bijective_differential_adicCompletionFunctor

Section93.13 Deformations of localizations #

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

Tag 0DZ7, a lemma

Tag 0DZ7 in the Stacks Project.

Deformation.hasFlatAlgebraLift_iff_hasFlatAlgebraLift_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/FlatAlgebraLiftLocalizationNilpotent.lean, line 335. The attribute's comment: “S⁻¹B is any C with IsLocalization S C. Spec(B) → Spec(A) being syntomic at the point 𝔮 is read affinely as ∃ g ∉ 𝔮, A → B_g syntomic, the characterization of Stacks 00SY and 01UE; S ∩ 𝔮 = ∅ is ∀ s ∈ S, s ∉ 𝔮. The published proof rests on Stacks 0DZ2, which is false; the proof here approximates a flat lift over the localized presentation by relation solutions over the polynomial presentation and corrects them one power of the kernel at a time (Artin-Rees plus Stacks 07M8 at every level). See the module docstring.”.

Stacks 0DZ7. Let A' → A be a surjective map of Noetherian rings with nilpotent kernel, let A → B be a finite type flat ring map and let S ⊆ B be a multiplicative subset such that if Spec(B) → Spec(A) is not syntomic at 𝔮, then S ∩ 𝔮 = ∅. Then B has a flat lift to A' if and only if S⁻¹B has a flat lift to A'.

Spec(B) → Spec(A) is syntomic at the point 𝔮 exactly when A → B_g is syntomic for some g ∉ 𝔮 (Stacks 00SY, 01UE); that is how the hypothesis hS reads the source's condition. The proof does not go through Stacks 0DZ2 (which is false); see the module documentation.

public theorem hasFlatAlgebraLift_iff_hasFlatAlgebraLift_localization
    (A' A B : Type u) [CommRing A'] [CommRing A] [CommRing B]
    [IsNoetherianRing A'] [IsNoetherianRing A] [Algebra A' A] [Algebra A B]
    (hsurjA : Function.Surjective (algebraMap A' A))
    (hnilA : IsNilpotent (RingHom.ker (algebraMap A' A)))
    [Algebra.FiniteType A B] [Module.Flat A B] (S : Submonoid B)
    (hS : ∀ q : Ideal B, q.IsPrime →
      (¬ ∃ g ∉ q, Algebra.Syntomic A (Localization.Away g)) → ∀ s ∈ S, s ∉ q)
    (C : Type u) [CommRing C] [Algebra B C] [IsLocalization S C] [Algebra A C]
    [IsScalarTower A B C] :
    HasFlatAlgebraLift A' A B ↔ HasFlatAlgebraLift A' A C

Tag 0DZ8, a lemma

Tag 0DZ8 in the Stacks Project.

Deformation.Examples.squareZeroAlgebraExtensionClassesLocalizationEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/LocalizationFirstOrder/ClassesLocalizationEquiv.lean, line 546. The attribute's comment: “localization equivalence”.

Stacks 0DZ8. If a multiplicative subset S of a finite type algebra B over a field k is disjoint from every prime in the non-smooth locus of B, then localization at S is a bijection from the isomorphism classes of square-zero extensions of B by N to those of square-zero extensions of S⁻¹B by S⁻¹N.

The companion lemma Deformation.Examples.squareZeroAlgebraExtensionClassesLocalizationEquiv_apply identifies the forward map with localization.

noncomputable def squareZeroAlgebraExtensionClassesLocalizationEquiv
    (k : Type uk) (B : Type uB) [Field k] [CommRing B] [Algebra k B]
    [Algebra.FiniteType k B] (S : Submonoid B)
    (hS : ∀ q : PrimeSpectrum B,
      ¬ Algebra.IsSmoothAt k q.asIdeal →
        Disjoint (S : Set B) (q.asIdeal : Set B))
    (N : Type uN) [AddCommGroup N] [Module B N] :
    SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB, uN,
        max uk (max uB uN)} (algebraExtensionProblem k B N) ≃
      SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uk, uk, uB,
        max uB uN, max uk (max uB uN)}
        (algebraExtensionProblem k (Localization S) (LocalizedModule S N))

Deformation.Examples.squareZeroAlgebraExtensionClassesLocalizationEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/LocalizationFirstOrder/ClassesLocalizationEquiv.lean, line 589. The attribute's comment: “forward map is localization”.

Stacks 0DZ8. The forward map of Deformation.Examples.squareZeroAlgebraExtensionClassesLocalizationEquiv is localization of an extension at the inverse image of S in its middle ring.

theorem squareZeroAlgebraExtensionClassesLocalizationEquiv_apply
    (k : Type uk) (B : Type uB) [Field k] [CommRing B] [Algebra k B]
    [Algebra.FiniteType k B] (S : Submonoid B)
    (hS : ∀ q : PrimeSpectrum B,
      ¬ Algebra.IsSmoothAt k q.asIdeal →
        Disjoint (S : Set B) (q.asIdeal : Set B))
    (N : Type uN) [AddCommGroup N] [Module B N]
    (X : (algebraExtensionProblem k B N).CompatibleExtension.{max uk (max uB uN)}) :
    ∃ Y : (algebraExtensionProblem k (Localization S)
        (LocalizedModule S N)).CompatibleExtension.{max uk (max uB uN)},
      squareZeroAlgebraExtensionClassesLocalizationEquiv k B S hS N
          (Quotient.mk
            (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
              (algebraExtensionProblem k B N)) X) =
        Quotient.mk
          (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
            (algebraExtensionProblem k (Localization S)
              (LocalizedModule S N))) Y ∧
      IsLocalizedExtension k B S N X Y

Deformation.Examples.IsLocalizedExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/LocalizationFirstOrder/LocalizedExtension.lean, line 346. The attribute's comment: “the localization relation between two extensions”.

Stacks 0DZ8. The extension Y of S⁻¹B is obtained from the extension X of B by localizing its middle ring at the inverse image of S: there is a map of the two middle rings which is such a localization, and which is compatible both with the quotient maps down to B and S⁻¹B and with the identifications of the two kernels with N and S⁻¹N.

def IsLocalizedExtension
    (k : Type uk) (B : Type uB) [Field k] [CommRing B] [Algebra k B]
    (S : Submonoid B) (N : Type uN) [AddCommGroup N] [Module B N]
    (X : (algebraExtensionProblem k B N).CompatibleExtension.{max uk (max uB uN)})
    (Y : (algebraExtensionProblem k (Localization S)
      (LocalizedModule S N)).CompatibleExtension.{max uk (max uB uN)}) : Prop

Tag 0DZ9, a lemma

Tag 0DZ9 in the Stacks Project.

Deformation.Examples.isSmooth_localizationFunctorData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/LocalizationSmooth.lean, line 268. The attribute's comment: “the first conclusion, smoothness: the functor of Stacks 0DYS is smooth. Under the tag's own hypotheses: (1) is Algebra.FiniteType k P and (2) is hsm, smoothness of Spec(P) → Spec(k) at every point of V(g) for every g of S. Stated for an arbitrary functor datum of Stacks 0DYS, with no extra hypothesis on the datum. The criterion of Stacks 0DYP reduces it to surjectivity of the differential, which is Deformation.Examples.bijective_differential_localizationFunctorData, and to the correspondence of liftability, which is proved here in Deformation.Examples.lifts_localizationFunctorData”.

Stacks 0DZ9, the smoothness conclusion. Let k be a field, P a finite type k-algebra and S ⊆ P a multiplicative subset such that Spec(P) → Spec(k) is smooth at every point of V(g) for every g ∈ S. The localization functor 𝓓_P ⟶ 𝓓_{S⁻¹P} of Stacks 0DYS is smooth.

theorem isSmooth_localizationFunctorData [Algebra.FiniteType k P]
    (F : LocalizationFunctorData (Λ := Λ) (k := k) S)
    (hsm : ∀ g ∈ S, ∀ q : PrimeSpectrum P, g ∈ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    IsSmooth F.functor

Deformation.Examples.isSmooth_localizationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/LocalizationSmooth.lean, line 285. The attribute's comment: “the first conclusion, smoothness, at the canonical localization functor Deformation.Examples.localizationFunctor of Stacks 0DYS. Under the tag's own hypotheses”.

Stacks 0DZ9, the smoothness conclusion, at the canonical localization functor. This is Deformation.Examples.isSmooth_localizationFunctorData specialized to Deformation.Examples.localizationFunctor, the functor datum built in the proof of Stacks 0DYS.

theorem isSmooth_localizationFunctor [Algebra.FiniteType k P]
    (hsm : ∀ g ∈ S, ∀ q : PrimeSpectrum P, g ∈ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    IsSmooth (localizationFunctor (Λ := Λ) (k := k) S).functor

Deformation.Examples.bijective_differential_localizationFunctorData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/LocalizationTangentSpace.lean, line 273. The attribute's comment: “the tangent-space assertion: the functor of Stacks 0DYS induces an isomorphism on tangent spaces. Under the tag's own hypotheses: (1) is Algebra.FiniteType k P and (2) is hsm, smoothness of Spec(P) → Spec(k) at every point of V(g) for every g of S. Stated for an arbitrary functor datum of Stacks 0DYS, with no extra hypothesis on the datum”.

Let k be a field, P a finite type k-algebra and S ⊆ P a multiplicative subset such that Spec(P) → Spec(k) is smooth at every point of V(g) for every g ∈ S. Then the localization functor 𝓓_P ⟶ 𝓓_{S⁻¹P} of Stacks 0DYS, given by any LocalizationFunctorData, induces a bijection on tangent spaces.

The proof is the source's: the family of extension classes of Stacks 0DY3 is a bijection of each tangent space with a first Ext group of the naive cotangent complex, by Deformation.Examples.bijective_tangentExtClass; the functor is compatible with those classes through the two comparison maps of Stacks 0GPV, by Deformation.Examples.squareZeroFiberExtClass_localization; the bijection of Stacks 0DZ8 is compatible with the same two maps, by Deformation.Examples.naiveCotangentExtOneMap_localizationCoefficientMap; and restriction along P → S⁻¹P is injective, by Stacks.Deformation.injective_naiveCotangentExtOneTowerMap_isLocalization.

public theorem bijective_differential_localizationFunctorData
    [Algebra.FiniteType k P]
    (F : LocalizationFunctorData (Λ := Λ) (k := k) S)
    (hsm : ∀ g ∈ S, ∀ q : PrimeSpectrum P, g ∈ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    Function.Bijective (differential (𝓕 := ringDeformationBasedCategory Λ k P)
      (𝓖 := ringDeformationBasedCategory Λ k (Localization S))
      isCofiberedInGroupoids_ringDeformationProjection
      isCofiberedInGroupoids_ringDeformationProjection F.functor)

Deformation.Examples.bijective_differential_localizationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Examples/Geometric/LocalizationTangentSpace.lean, line 332. The attribute's comment: “the tangent-space assertion: the functor induces an isomorphism on tangent spaces, at the canonical localization functor Deformation.Examples.localizationFunctor of Stacks 0DYS. Under the tag's own hypotheses”.

Under the hypotheses of Deformation.Examples.bijective_differential_localizationFunctorData, the canonical localization functor Deformation.Examples.localizationFunctor, the functor datum built in the proof of Stacks 0DYS, induces a bijection on tangent spaces.

public theorem bijective_differential_localizationFunctor [Algebra.FiniteType k P]
    (hsm : ∀ g ∈ S, ∀ q : PrimeSpectrum P, g ∈ q.asIdeal → Algebra.IsSmoothAt k q.asIdeal) :
    Function.Bijective (differential (𝓕 := ringDeformationBasedCategory Λ k P)
      (𝓖 := ringDeformationBasedCategory Λ k (Localization S))
      isCofiberedInGroupoids_ringDeformationProjection
      isCofiberedInGroupoids_ringDeformationProjection
      (localizationFunctor (Λ := Λ) (k := k) S).functor)

Sources

LeanDeformation.hasFlatAlgebraLift_iff_hasFlatAlgebraLift_localization · Deformation.Examples.squareZeroAlgebraExtensionClassesLocalizationEquiv · Deformation.Examples.squareZeroAlgebraExtensionClassesLocalizationEquiv_apply · Deformation.Examples.IsLocalizedExtension · Deformation.Examples.isSmooth_localizationFunctorData · Deformation.Examples.isSmooth_localizationFunctor · Deformation.Examples.bijective_differential_localizationFunctorData · Deformation.Examples.bijective_differential_localizationFunctor

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

93.4 Finite projective modules to 93.13 Deformations of…

Section93.4 Finite projective modules#

Tag 0D3I, an example

Tag 0DVP, a lemma

Tag 0DVQ, a lemma

Sources

Section93.5 Representations of a group#

Tag 0D3J, an example

Tag 0DVS, a lemma

Tag 0DVT, a lemma

Tag 0ET1, a lemma

Sources

Section93.6 Continuous representations#

Tag 0D3K, an example

Tag 0DVV, a lemma

Tag 0DVW, a lemma

Tag 0ET2, a lemma

Sources

Section93.7 Graded algebras#

Tag 0D3L, an example

Tag 0DVY, a lemma

Tag 0DVZ, a lemma

Tag 0ET3, a lemma

Sources

Section93.8 Rings#

Tag 0DY1, an example

Tag 0DY2, a lemma

Tag 0DY3, a lemma

Tag 0DZL, a lemma

Tag 0DY4, a lemma

Tag 0ET4, a lemma

Tag 0DYS, a lemma

Tag 0DYT, a lemma

Tag 0DYU, a lemma

Tag 0DYV, a lemma

Tag 0DY5, a lemma

Sources

Section93.9 Schemes#

Tag 0DY7, an example

Tag 0DY8, a lemma

Tag 0DY9, a lemma

Tag 0DYA, a lemma

Tag 0ET5, a lemma

Tag 0DYW, a lemma

Tag 0DYX, a lemma

Tag 0DZM, a lemma

Tag 0DYY, a situation

Tag 0DYZ, a lemma

Sources

Section93.10 Morphisms of Schemes#

Tag 0E3T, an example

Tag 0E3U, a lemma

Tag 0E3V, a lemma

Tag 0E3W, a lemma

Tag 0ET6, a lemma

Tag 0E3X, a lemma

Sources

Section93.11 Algebraic spaces#

Tag 0E3Z, an example

Tag 0E40, a lemma

Tag 0E41, a lemma

Tag 0E42, a lemma

Tag 0ET7, a lemma

Sources

Section93.12 Deformations of completions#

Tag 0DZ1, a lemma

Tag 0DZ2, a lemma

Tag 0DZ3, a lemma

Tag 0DZ4, a lemma

Tag 0DZ5, a lemma

Sources

Section93.13 Deformations of localizations#

Tag 0DZ7, a lemma

Tag 0DZ8, a lemma

Tag 0DZ9, a lemma

Sources

Section93.4 Finite projective modules #

Section93.5 Representations of a group #

Section93.6 Continuous representations #

Section93.7 Graded algebras #

Section93.8 Rings #

Section93.9 Schemes #

Section93.10 Morphisms of Schemes #

Section93.11 Algebraic spaces #

Section93.12 Deformations of completions #

Section93.13 Deformations of localizations #