90.16 Rim-Schlessinger… to 90.29 Change of residue field

Section90.16 Rim-Schlessinger conditions and deformation categories#

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

Tag 06J2, a definition

Tag 06J2 in the Stacks Project.

Deformation.SatisfiesRS, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/Basic.lean, line 70. References: SGA 7 VI (2.5).

Condition (RS): every cospan over a cospan of Artinian local algebras whose second morphism is surjective has a pullback cone which remains a pullback cone in the base.

public abbrev SatisfiesRS {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ
  k] {F : Type u₁} [Category.{v₁} F] (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) : Prop
Tag 06J3, a lemma

Tag 06J3 in the Stacks Project.

Deformation.isLimit_of_map_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/Basic.lean, line 87.

Under condition (RS), a square over a pullback square is a pullback square when the second morphism in the base cospan is surjective.

public theorem isLimit_of_map_isLimit
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : SatisfiesRS p)
    {x₁ x₂ x : F} (f₁ : x₁ ⟶ x) (f₂ : x₂ ⟶ x)
    (c : PullbackCone f₁ f₂)
    (hsurj : Function.Surjective (p.map f₂).hom)
    (hc : Nonempty (IsLimit (c.map p))) :
    Nonempty (IsLimit c)
Tag 06J4, a lemma

Tag 06J4 in the Stacks Project.

Deformation.satisfiesRS_of_small_extensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/SmallExtensionCriterion.lean, line 225.

Stacks Project, Tag 06J4. To verify condition (RS) for a category cofibered in groupoids, it suffices to consider cospans whose second base morphism is a small extension.

public theorem satisfiesRS_of_small_extensions
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : IsCofiberedInGroupoids p)
    (hsmall : ∀ {x₁ x₂ x : F} (f₁ : x₁ ⟶ x) (f₂ : x₂ ⟶ x),
      InfinitesimalLifting.IsSmallExtension
          (CommRingCat.ofHom (p.map f₂).hom.toRingHom) →
        ∃ c : PullbackCone f₁ f₂,
          (Nonempty (IsLimit c) ∧ Nonempty (IsLimit (c.map p)))) :
    SatisfiesRS p
Tag 06J5, a lemma

Tag 06J5 in the Stacks Project.

Deformation.satisfiesRS_iff_comparison_isEquivalence_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/ComparisonEquivalence.lean, line 634. The attribute's comment: “surjective maps”. References: SGA 7 VI (2.6(b)), “homogeneous criterion”.

Stacks Project, Tag 06J5. Condition (RS) holds precisely when the canonical functor from the fibre over a pullback to the 2-fibre product of fibres is an equivalence for every square whose second map is surjective.

theorem satisfiesRS_iff_comparison_isEquivalence_of_surjective
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (hp : IsCofiberedInGroupoids p) :
    SatisfiesRS p ↔
      ∀ {P A₁ A₂ A : ArtinianLocalAlgCat.{u, v, w} Λ k}
        (p₁ : P ⟶ A₁) (p₂ : P ⟶ A₂) (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A)
        (hP : IsPullback p₁ p₂ f₁ f₂)
        (hf₂ : Function.Surjective f₂.hom)
        (P₁ : PushforwardChoice p p₁) (P₂ : PushforwardChoice p p₂)
        (F₁ : PushforwardChoice p f₁) (F₂ : PushforwardChoice p f₂)
        (Qp₁ : PushforwardFunctor P₁) (Qp₂ : PushforwardFunctor P₂)
        (Qf₁ : PushforwardFunctor F₁) (Qf₂ : PushforwardFunctor F₂),
        (squareComparisonFunctor p hp p₁ p₂ f₁ f₂ hP hf₂
          P₁ P₂ F₁ F₂ Qp₁ Qp₂ Qf₁ Qf₂).toFunctor.IsEquivalence

Deformation.satisfiesRS_iff_comparison_isEquivalence_of_smallExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/ComparisonEquivalence.lean, line 661. The attribute's comment: “small extensions”. References: SGA 7 VI (2.6(b)), “small extensions”.

Stacks Project, Tag 06J5. It is enough to test the comparison functor on squares whose second map is a small extension.

theorem satisfiesRS_iff_comparison_isEquivalence_of_smallExtension
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (hp : IsCofiberedInGroupoids p) :
    SatisfiesRS p ↔
      ∀ {P A₁ A₂ A : ArtinianLocalAlgCat.{u, v, w} Λ k}
        (p₁ : P ⟶ A₁) (p₂ : P ⟶ A₂) (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A)
        (hP : IsPullback p₁ p₂ f₁ f₂)
        (hsmall : InfinitesimalLifting.IsSmallExtension
          (CommRingCat.ofHom f₂.hom.toRingHom))
        (P₁ : PushforwardChoice p p₁) (P₂ : PushforwardChoice p p₂)
        (F₁ : PushforwardChoice p f₁) (F₂ : PushforwardChoice p f₂)
        (Qp₁ : PushforwardFunctor P₁) (Qp₂ : PushforwardFunctor P₂)
        (Qf₁ : PushforwardFunctor F₁) (Qf₂ : PushforwardFunctor F₂),
        (squareComparisonFunctor p hp p₁ p₂ f₁ f₂ hP
          hsmall.2.2.2.2.1 P₁ P₂ F₁ F₂ Qp₁ Qp₂ Qf₁ Qf₂).toFunctor.IsEquivalence
Tag 06J6, a remark

Tag 06J6 in the Stacks Project.

Deformation.satisfiesRS_elementsProjection_iff_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/SetValuedRS.lean, line 135.

Stacks Project, Tag 06J6. For a set-valued functor F on the category of Artinian local Λ-algebras, condition (RS) for the associated category cofibered in sets holds exactly when the canonical map F(A₁ ×_A A₂) → F(A₁) ×_{F(A)} F(A₂) is bijective for every fibre-product square whose second map is surjective; this is Schlessinger's condition (H4).

theorem satisfiesRS_elementsProjection_iff_bijective
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (G : ArtinianLocalAlgCat.{u, v, w} Λ k ⥤ Type t) :
    SatisfiesRS (Functor.Elements.π G) ↔
      ∀ {P A₁ A₂ A : ArtinianLocalAlgCat.{u, v, w} Λ k}
        (p₁ : P ⟶ A₁) (p₂ : P ⟶ A₂) (f₁ : A₁ ⟶ A) (f₂ : A₂ ⟶ A)
        (hP : IsPullback p₁ p₂ f₁ f₂), Function.Surjective f₂.hom →
          Function.Bijective (fibreProductComparison G p₁ p₂ f₁ f₂ hP.w.symm)
Tag 06J7, a lemma

Tag 06J7 in the Stacks Project.

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

Condition (RS) implies Schlessinger's condition (S1).

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

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

Condition (RS) implies Schlessinger's condition (S2).

public theorem schlessingerConditionS2_of_satisfiesRS
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : SatisfiesRS p) :
    SchlessingerConditionS2 p
Tag 06J8, a lemma

Tag 06J8 in the Stacks Project.

Deformation.associatedSatisfiesRS_iff_gluingClassesInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/AutomorphismLifting.lean, line 702. The attribute's comment: “conditions (1) and (2)”. References: SGA 7 VI (2.7), “(i) <=> injectivity”.

For a category cofibered in groupoids satisfying (RS), the associated functor of isomorphism classes satisfies (RS) exactly when the comparison on isomorphism classes of gluing data is injective.

theorem associatedSatisfiesRS_iff_gluingClassesInjective
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (hp : SatisfiesRS p) :
    SatisfiesRS (CategoryOfElements.π
        (isomorphismClassesData (BasedCategory.ofFunctor p) hp.1).classes) ↔
      IsInjectiveOnGluingClasses p

Deformation.gluingClassesInjective_iff_automorphismsLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/AutomorphismLifting.lean, line 713. The attribute's comment: “conditions (2) and (3)”. References: SGA 7 VI (2.7), “inj <=> aut surjective”.

For a category cofibered in groupoids, injectivity on isomorphism classes of gluing data is equivalent to lifting automorphisms along every surjection of Artinian local algebras.

theorem gluingClassesInjective_iff_automorphismsLift
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (hp : IsCofiberedInGroupoids p) :
    IsInjectiveOnGluingClasses p ↔
      (∀ {A' A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : A' ⟶ A),
        Function.Surjective f.hom → AutomorphismsLiftAlong p f)

Deformation.automorphismsLift_iff_smallExtensions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/AutomorphismLifting.lean, line 764. The attribute's comment: “conditions (3) and (4)”. References: SGA 7 VI (2.7), “(ii) vs surjections”.

For a category cofibered in groupoids, automorphisms lift along every surjection of Artinian local algebras exactly when they lift along every small extension.

theorem automorphismsLift_iff_smallExtensions
    (p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k) (hp : IsCofiberedInGroupoids p) :
    (∀ {A' A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : A' ⟶ A),
      Function.Surjective f.hom → AutomorphismsLiftAlong p f) ↔
      (∀ {A' A : ArtinianLocalAlgCat.{u, v, w} Λ k} (f : A' ⟶ A),
        InfinitesimalLifting.IsSmallExtension
          (CommRingCat.ofHom f.hom.toRingHom) → AutomorphismsLiftAlong p f)
Tag 06J9, a definition

Tag 06J9 in the Stacks Project.

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

A predeformation category over 𝒞_Λ satisfying condition (RS).

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

Declarations registered for the tag:

Tag 06JA, a remark

Tag 06JA in the Stacks Project.

Deformation.IsDeformationFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/Basic.lean, line 150. The attribute's comment: “deformation_functor”.

A set-valued functor is a deformation functor if its value at the residue field is a singleton and its associated cofibered set satisfies (RS).

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

Deformation.isDeformationCategory_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/Basic.lean, line 159. The attribute's comment: “deformation_functor”.

A functor is a deformation functor exactly when its associated cofibered set is a deformation category.

public theorem isDeformationCategory_iff
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t) :
    IsDeformationCategory (CategoryOfElements.π F) ↔
      IsDeformationFunctor F

Declarations registered for the tag:

Tag 06JB, an example

Tag 06JB in the Stacks Project.

Deformation.restrictedCoyoneda_isPredeformationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/Prorepresentable.lean, line 47. The attribute's comment: “singleton value at the residue field”.

Stacks Project, Tag 06JB. A functor represented by a complete local algebra takes the residue-field object to a one-element set.

theorem restrictedCoyoneda_isPredeformationFunctor
    (R : CompleteLocalAlgCat.{u, max v w, w} Λ k) :
    IsPredeformationFunctor (restrictedCoyoneda R)

Deformation.restrictedCoyoneda_satisfiesRS, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/Prorepresentable.lean, line 85. The attribute's comment: “the (RS) property”.

Stacks Project, Tag 06JB. A functor represented by a complete local algebra satisfies (RS), since maps out of the representing object preserve the relevant fibre products.

theorem restrictedCoyoneda_satisfiesRS
    (R : CompleteLocalAlgCat.{u, max v w, w} Λ k) :
    SatisfiesRS (Functor.Elements.π (restrictedCoyoneda R))

Deformation.isDeformationFunctor_of_isProrepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessingerCategory/Prorepresentable.lean, line 214. The attribute's comment: “prorepresentable implies deformation”.

Stacks Project, Tag 06JB. Every prorepresentable functor on Artinian local algebras is a deformation functor.

theorem isDeformationFunctor_of_isProrepresentable
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type (max v w))
    (hF : IsProrepresentable F) :
    IsDeformationFunctor F
Tag 06JC, a lemma

Tag 06JC in the Stacks Project.

Deformation.satisfiesRS_objectsOverFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/Basic.lean, line 185. The attribute's comment: “Rim-Schlessinger condition”.

The category localized at an object of the special fibre inherits the Rim–Schlessinger condition.

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

Deformation.isDeformationCategory_objectsOverFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/Basic.lean, line 247. The attribute's comment: “deformation category”.

The category localized at an object of the special fibre is a deformation category when the original category satisfies the Rim–Schlessinger condition.

public theorem isDeformationCategory_objectsOverFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : SatisfiesRS p)
    (x : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    IsDeformationCategory
      (objectsOverFunctor p x.1)
Tag 06L4, a lemma

Tag 06L4 in the Stacks Project.

Deformation.satisfiesRS_twoFibreProductOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RimSchlessinger/TwoFibreProduct.lean, line 286.

A 2-fibre product of categories satisfying condition (RS) again satisfies condition (RS).

theorem satisfiesRS_twoFibreProductOver
    {Lambda : Type u} {k : Type w} [CommRing Lambda] [Field k] [Algebra Lambda k]
    {H : Type u₁} [Category.{v₁} H]
    {G : Type u₂} [Category.{v₂} G]
    {F : Type u₃} [Category.{v₃} F]
    (pH : H ⥤ ArtinianLocalAlgCat.{u, v, w} Lambda k)
    (pG : G ⥤ ArtinianLocalAlgCat.{u, v, w} Lambda k)
    (pF : F ⥤ ArtinianLocalAlgCat.{u, v, w} Lambda k)
    (f : H ⥤ F) (g : G ⥤ F)
    (hf : f ⋙ pF = pH) (hg : g ⋙ pF = pG)
    (hH : SatisfiesRS pH)
    (hG : SatisfiesRS pG)
    (hF : SatisfiesRS pF) :
    SatisfiesRS
      (TwoFibreProductOver.structureFunctor pH pG pF f g)
Sources
LeanDeformation.SatisfiesRS · Deformation.isLimit_of_map_isLimit · Deformation.satisfiesRS_of_small_extensions · Deformation.satisfiesRS_iff_comparison_isEquivalence_of_surjective · Deformation.satisfiesRS_iff_comparison_isEquivalence_of_smallExtension · Deformation.satisfiesRS_elementsProjection_iff_bijective · Deformation.schlessingerConditionS1_of_satisfiesRS · Deformation.schlessingerConditionS2_of_satisfiesRS

Section90.17 Lifts of objects#

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

Tag 06JE, a definition

Tag 06JE in the Stacks Project.

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

The category of lifts of x along f. Its objects are arrows to x lying over f; its arrows are commuting triangles whose remaining side lies over the identity.

public structure Lift
    {C : Type u} [Category.{v} C] {F : Type uF} [Category.{vF} F]
    (p : F ⥤ C) {A' A : C} (f : A' ⟶ A) (x : p.Fiber A)

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

A morphism of lifts is a morphism over the identity which makes the triangle of lifting arrows commute.

public structure Lift.Hom
    {C : Type u} [Category.{v} C] {F : Type uF} [Category.{vF} F]
    {p : F ⥤ C} {A' A : C} {f : A' ⟶ A} {x : p.Fiber A}
    (a b : Lift p f x)

Deformation.LiftClasses, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Lift.lean, line 131. The attribute's comment: “the set of lifts”.

The set of isomorphism classes of lifts of x along f.

public abbrev LiftClasses
    {C : Type u} [Category.{v} C] {F : Type uF} [Category.{vF} F]
    (p : F ⥤ C) {A' A : C} (f : A' ⟶ A) (x : p.Fiber A)
Tag 06JF, a remark

Tag 06JF in the Stacks Project.

Deformation.Lift.over, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Lift.lean, line 141. The attribute's comment: “the category of lifts named by the source object”.

The category of lifts of x to an object A' of the base category given together with its morphism to A: the lifts of x along that morphism, which the name leaves implicit.

public abbrev Lift.over
    {C : Type u} [Category.{v} C] {F : Type uF} [Category.{vF} F]
    (p : F ⥤ C) {A : C} (A' : Over A) (x : p.Fiber A)

Deformation.LiftClasses.over, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Lift.lean, line 149. The attribute's comment: “the set of lifts named by the source object”.

The set of isomorphism classes of lifts of x to an object A' of the base category given together with its morphism to A, that morphism being left implicit.

public abbrev LiftClasses.over
    {C : Type u} [Category.{v} C] {F : Type uF} [Category.{vF} F]
    (p : F ⥤ C) {A : C} (A' : Over A) (x : p.Fiber A)
Tag 06JG, a remark

Tag 06JG in the Stacks Project.

Deformation.liftClassesEquivObjectsOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/TangentSpaceOfLifts.lean, line 128. The attribute's comment: “lifts as localized isomorphism classes”.

A lift of x₀ along a square-zero augmentation is an object of the localized category over x₀ in the source fibre, up to isomorphism.

public noncomputable def liftClassesEquivObjectsOver
    (hp : IsCofiberedInGroupoids p)
    {A : ArtinianLocalAlgCat.{u, w, w} Λ k}
    (e : A ⟶ residueFieldObject Λ k)
    (x₀ : p.Fiber (residueFieldObject Λ k)) :
    let q := objectsOverFunctor p x₀.1
    let hq := (isPredeformationCategory_objectsOverFunctor p hp x₀).cofibered
    { comparison : LiftClasses p e x₀ ≃
        (isomorphismClasses (BasedCategory.ofFunctor q) hq).obj A //
      ∀ a : Lift p e x₀, comparison (ThinSkeleton.mk a) =
        classOf (BasedCategory.ofFunctor q) hq
          (⟨Over.mk a.hom,
            IsHomLift.domain_eq p e a.hom⟩ : q.Fiber A) }

Deformation.liftClassesTangentSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/TangentSpaceOfLifts.lean, line 227. The attribute's comment: “tangent-space tensor identification”.

Under (S2), the lifts to k[V] are the tangent space of the category localized at x₀, tensored with V, as vector spaces.

public noncomputable def liftClassesTangentSpace
    (hp : IsCofiberedInGroupoids p)
    (hS2 : SchlessingerConditionS2 p)
    (x₀ : p.Fiber (residueFieldObject Λ k))
    (V : FGModuleCat.{w} k)
    (e : (squareZeroExtensionArtinian Λ k).obj V ⟶ residueFieldObject Λ k) :
    LiftTangentSpaceData p hp hS2 x₀ V e

Deformation.liftClassesTangentSpace_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/TangentSpaceOfLifts.lean, line 288. The attribute's comment: “naturality in the vector space”.

The tensor identification of lifts commutes with every linear map of finite-dimensional vector spaces, using the induced map on localized lifts.

public theorem liftClassesTangentSpace_naturality
    (hp : IsCofiberedInGroupoids p)
    (hS2 : SchlessingerConditionS2 p)
    (x₀ : p.Fiber (residueFieldObject Λ k))
    (V W : FGModuleCat.{w} k)
    (eV : (squareZeroExtensionArtinian Λ k).obj V ⟶ residueFieldObject Λ k)
    (eW : (squareZeroExtensionArtinian Λ k).obj W ⟶ residueFieldObject Λ k)
    (f : V ⟶ W) :
    let q := objectsOverFunctor p x₀.1
    let hpq := isPredeformationCategory_objectsOverFunctor p hp x₀
    let H := isomorphismClasses (BasedCategory.ofFunctor q) hpq.cofibered
    let DV := liftClassesTangentSpace p hp hS2 x₀ V eV
    let DW := liftClassesTangentSpace p hp hS2 x₀ W eW
    letI : Fact (IsPredeformationCategory (BasedCategory.ofFunctor q).p) := ⟨hpq⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π H)) := ⟨DV.associatedS2⟩
    letI : AddCommGroup (artinianTangentSpace Λ k H) :=
      associatedTangentSpaceAddCommGroupUnlifted (BasedCategory.ofFunctor q)
    letI : Module k (artinianTangentSpace Λ k H) :=
      associatedTangentSpaceModuleUnlifted (BasedCategory.ofFunctor q)
    ∀ z : TensorProduct k (artinianTangentSpace Λ k H) V,
      (liftClassesEquivObjectsOver p hp eW x₀).1
          (DW.equiv (TensorProduct.map
            (LinearMap.id : artinianTangentSpace Λ k H →ₗ[k]
              artinianTangentSpace Λ k H) f.hom.hom z)) =
        H.map ((squareZeroExtensionArtinian Λ k).map f)
          ((liftClassesEquivObjectsOver p hp eV x₀).1 (DV.equiv z))
Tag 06JH, a remark

Tag 06JH in the Stacks Project.

Deformation.liftClassesProdEquivPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Lift.lean, line 698. The attribute's comment: “product_bijection”.

Isomorphism classes of lifts to a fibre product are in bijection with pairs of isomorphism classes of lifts to the two factors when one structural map is surjective.

public theorem liftClassesProdEquivPullback
    {Λ : Type*} {k : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat Λ k)
    (hRS : SatisfiesRS p)
    {A₁ A₂ A : ArtinianLocalAlgCat Λ k}
    {f₁ : A₁ ⟶ A} {f₂ : A₂ ⟶ A}
    (c : PullbackCone f₁ f₂) (hc : IsLimit c)
    (hsurj : Function.Surjective f₁.hom ∨ Function.Surjective f₂.hom)
    (x : p.Fiber A) :
    Nonempty (LiftProductEquiv p c x)

Deformation.liftClassesEquivOfFixedLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Lift.lean, line 950. The attribute's comment: “fixed_lift_bijection”.

After fixing a lift over the first factor, pushing along the second projection gives a bijection from lifts of the fixed object to lifts over the second factor.

public theorem liftClassesEquivOfFixedLift
    {Λ : Type*} {k : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat Λ k)
    (hRS : SatisfiesRS p)
    {A₁ A₂ A : ArtinianLocalAlgCat Λ k}
    {f₁ : A₁ ⟶ A} {f₂ : A₂ ⟶ A}
    (c : PullbackCone f₁ f₂) (hc : IsLimit c)
    (hsurj : Function.Surjective f₁.hom ∨ Function.Surjective f₂.hom)
    (x : p.Fiber A) (a₁ : Lift p f₁ x) :
    Nonempty (FixedLiftEquiv p c x a₁)

Deformation.liftClassesEquivProdOfCompositePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Lift.lean, line 1047. The attribute's comment: “composite_square_bijection”.

Let left be a fibre square of a surjection g : A₁' ⟶ A₁ and the first projection of right. Isomorphism classes of lifts of the source of a₁ along left.fst ≫ g are in bijection with pairs of isomorphism classes of lifts of it along g and along right.fst.

public theorem liftClassesEquivProdOfCompositePullback
    {Λ : Type*} {k : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat Λ k)
    (hRS : SatisfiesRS p)
    {A₁' A₁ A₂ A : ArtinianLocalAlgCat Λ k}
    {f₁ : A₁ ⟶ A} {f₂ : A₂ ⟶ A} {g : A₁' ⟶ A₁}
    (right : PullbackCone f₁ f₂)
    (left : PullbackCone g right.fst)
    (hleft : IsLimit left)
    (hg : Function.Surjective g.hom)
    (x : p.Fiber A) (a₁ : Lift p f₁ x) :
    Nonempty (LiftClasses p (left.fst ≫ g) (liftSourceFiber a₁) ≃
      LiftClasses p g (liftSourceFiber a₁) ×
        LiftClasses p right.fst (liftSourceFiber a₁))

Deformation.liftClassesEquivOuterProdOfCompositePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Lift.lean, line 1071. The attribute's comment: “composite_square_bijection”.

Let right be a fibre square of f₁ and f₂ with f₁ surjective, and left a fibre square of a surjection g : A₁' ⟶ A₁ and the first projection of right. Isomorphism classes of lifts of the source of a₁ along left.fst ≫ g are in bijection with pairs of an isomorphism class of lifts of it along g and an isomorphism class of lifts of x along f₂.

public theorem liftClassesEquivOuterProdOfCompositePullback
    {Λ : Type*} {k : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat Λ k)
    (hRS : SatisfiesRS p)
    {A₁' A₁ A₂ A : ArtinianLocalAlgCat Λ k}
    {f₁ : A₁ ⟶ A} {f₂ : A₂ ⟶ A} {g : A₁' ⟶ A₁}
    (right : PullbackCone f₁ f₂)
    (hright : IsLimit right)
    (left : PullbackCone g right.fst)
    (hleft : IsLimit left)
    (hg : Function.Surjective g.hom)
    (hf₁ : Function.Surjective f₁.hom)
    (x : p.Fiber A) (a₁ : Lift p f₁ x) :
    Nonempty (LiftClasses p (left.fst ≫ g) (liftSourceFiber a₁) ≃
      LiftClasses p g (liftSourceFiber a₁) × LiftClasses p f₂ x)
Tag 06JI, a lemma

Tag 06JI in the Stacks Project.

Deformation.liftAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Action/FreeTransitive.lean, line 63. The attribute's comment: “action”.

Stacks Project, Tag 06JI. The canonical additive action of tangent vectors tensored with the infinitesimal kernel on the classes of lifts.

public noncomputable def liftAction
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsDeformationCategory 𝓕.p)
    {A' A : ArtinianLocalAlgCat.{u, w, w} Λ k}
    (f : A' ⟶ A) (hf : Function.Surjective f.hom)
    (hann : ∀ a : A', a ∈ maximalIdeal A' →
      ∀ i : RingHom.ker f.hom.toRingHom, a * (i : A') = 0)
    (x : 𝓕.p.Fiber A) :
    letI : Module k (RingHom.ker f.hom.toRingHom) := kernelModule f hann
    let hS2 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓕 h𝓕.predeformation.cofibered
      (schlessingerConditionS2_of_satisfiesRS h𝓕.satisfiesRS)
      (.inl h𝓕.predeformation)
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨h𝓕.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))) := ⟨hS2⟩
    AddAction
      (TensorProduct k
        (artinianTangentSpace Λ k
          (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))
        (RingHom.ker f.hom.toRingHom))
      (LiftClasses 𝓕.p f x)

Deformation.liftDifference_isPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Action/FreeTransitive.lean, line 182. The attribute's comment: “difference is canonical pushforward”.

Stacks Project, Tag 06JI. The infinitesimal difference of any two lifts is exactly the canonical tangent coordinate of the cocartesian pushforward of their fibre product along (a₁, a₂) ↦ (ā₁, a₂ - a₁).

public theorem liftDifference_isPushforward
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsDeformationCategory 𝓕.p)
    {A' A : ArtinianLocalAlgCat.{u, w, w} Λ k}
    (f : A' ⟶ A) (hf : Function.Surjective f.hom)
    (hann : ∀ a : A', a ∈ maximalIdeal A' →
      ∀ i : RingHom.ker f.hom.toRingHom, a * (i : A') = 0)
    (x : 𝓕.p.Fiber A) :
    letI : Module k (RingHom.ker f.hom.toRingHom) := kernelModule f hann
    let hS2 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓕 h𝓕.predeformation.cofibered
      (schlessingerConditionS2_of_satisfiesRS h𝓕.satisfiesRS)
      (.inl h𝓕.predeformation)
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨h𝓕.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))) := ⟨hS2⟩
    ∀ a b : LiftClasses 𝓕.p f x,
      IsPushforwardDifference 𝓕 h𝓕 f hf hann x a b
        (liftDifference 𝓕 h𝓕 f hf hann x a b)

Deformation.liftAction_difference, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Action/FreeTransitive.lean, line 253. The attribute's comment: “difference characterization”.

Stacks Project, Tag 06JI. The action is the unique lift whose infinitesimal difference from the given lift is the prescribed tangent vector.

public theorem liftAction_difference
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsDeformationCategory 𝓕.p)
    {A' A : ArtinianLocalAlgCat.{u, w, w} Λ k}
    (f : A' ⟶ A) (hf : Function.Surjective f.hom)
    (hann : ∀ a : A', a ∈ maximalIdeal A' →
      ∀ i : RingHom.ker f.hom.toRingHom, a * (i : A') = 0)
    (x : 𝓕.p.Fiber A) :
    letI : Module k (RingHom.ker f.hom.toRingHom) := kernelModule f hann
    let hS2 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓕 h𝓕.predeformation.cofibered
      (schlessingerConditionS2_of_satisfiesRS h𝓕.satisfiesRS)
      (.inl h𝓕.predeformation)
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨h𝓕.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))) := ⟨hS2⟩
    letI := liftAction 𝓕 h𝓕 f hf hann x
    ∀ (a : LiftClasses 𝓕.p f x)
      (t : TensorProduct k
        (artinianTangentSpace Λ k
          (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))
        (RingHom.ker f.hom.toRingHom)),
      liftDifference 𝓕 h𝓕 f hf hann x a (t +ᵥ a) = t

Deformation.liftAction_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Action/FreeTransitive.lean, line 293. The attribute's comment: “free and transitive”.

Stacks Project, Tag 06JI. From any fixed lift, addition of tangent vectors is a bijection onto all isomorphism classes of lifts; equivalently, the action is free and transitive.

public theorem liftAction_bijective
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsDeformationCategory 𝓕.p)
    {A' A : ArtinianLocalAlgCat.{u, w, w} Λ k}
    (f : A' ⟶ A) (hf : Function.Surjective f.hom)
    (hann : ∀ a : A', a ∈ maximalIdeal A' →
      ∀ i : RingHom.ker f.hom.toRingHom, a * (i : A') = 0)
    (x : 𝓕.p.Fiber A) :
    letI : Module k (RingHom.ker f.hom.toRingHom) := kernelModule f hann
    let hS2 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓕 h𝓕.predeformation.cofibered
      (schlessingerConditionS2_of_satisfiesRS h𝓕.satisfiesRS)
      (.inl h𝓕.predeformation)
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨h𝓕.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))) := ⟨hS2⟩
    letI := liftAction 𝓕 h𝓕 f hf hann x
    ∀ a : LiftClasses 𝓕.p f x,
      Function.Bijective
        (fun t : TensorProduct k
          (artinianTangentSpace Λ k
            (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))
          (RingHom.ker f.hom.toRingHom) => t +ᵥ a)
Tag 06TA, an equation

Tag 06TA in the Stacks Project.

Deformation.liftClassesEquivSquareZeroPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/SquareZeroPullback.lean, line 658.

The canonical difference isomorphism A' ×_A A' ≅ A' ×_k k[I] induces a bijection of lifts of x over these two objects, compatible with pushforward of each representative. The presentation coord of k[I] respects its Λ-algebra map and its chosen residue-field identification, as required for an identification in 𝒞_Λ.

public theorem liftClassesEquivSquareZeroPullback
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : IsDeformationCategory p)
    {A' A S K P Q : ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (f : A' ⟶ A) (_hf : Function.Surjective f.hom)
    (hann : ∀ a : A', a ∈ IsLocalRing.maximalIdeal A' →
      ∀ i : RingHom.ker f.hom.toRingHom, a * (i : A') = 0)
    [Module k (RingHom.ker f.hom.toRingHom)]
    [Module kᵐᵒᵖ (RingHom.ker f.hom.toRingHom)]
    [IsCentralScalar k (RingHom.ker f.hom.toRingHom)]
    (hmodule : ∀ (a : A') (i : RingHom.ker f.hom.toRingHom),
      (A'.residueEquiv (IsLocalRing.residue A' a)) • i = a • i)
    (coord : S ≃+* TrivSqZeroExt k (RingHom.ker f.hom.toRingHom))
    (hcoordΛ : ∀ a : Λ, coord (algebraMap Λ S a) =
      TrivSqZeroExt.inl (algebraMap Λ k a))
    (hcoordResidue : ∀ s : S,
      (coord s).fst = S.residueEquiv (IsLocalRing.residue S s))
    (hK : K ≅ residueFieldObject.{u, v, w} Λ k)
    (rA : A' ⟶ K) (rS : S ⟶ K)
    (p₁ p₂ : P ⟶ A') (hP : IsPullback p₁ p₂ f f)
    (q₁ : Q ⟶ A') (q₂ : Q ⟶ S) (hQ : IsPullback q₁ q₂ rA rS)
    (x : p.Fiber A) :
    Nonempty (DifferenceLiftEquiv p f rA rS p₁ p₂ q₁ q₂ coord x)
Tag 06TB, an equation

Tag 06TB in the Stacks Project.

Declarations registered for the tag:

Tag 06TC, an equation

Tag 06TC in the Stacks Project.

Deformation.liftClassesEquivProdOfResiduePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/CompositeProjection.lean, line 178.

For a composite of two fibre squares, lifts over the outer pullback are identified with a lift over the inner factor and a lift over the other outer factor, via the two projections.

public theorem liftClassesEquivProdOfResiduePullback
    {Λ : Type*} {k : Type*} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type uF} [Category.{vF} F]
    (p : F ⥤ ArtinianLocalAlgCat Λ k)
    (hp : IsDeformationCategory p)
    {A₁' A₁ A₂ A : ArtinianLocalAlgCat Λ k}
    {f₁ : A₁ ⟶ A} {f₂ : A₂ ⟶ A} {g : A₁' ⟶ A₁}
    (right : PullbackCone f₁ f₂) (hright : IsLimit right)
    (left : PullbackCone g right.fst) (hleft : IsLimit left)
    (hg : Function.Surjective g.hom)
    (hf₁ : Function.Surjective f₁.hom)
    (x₀ : p.Fiber A) (a₁ : Lift p f₁ x₀) :
    Nonempty (LiftProjectionEquiv p right left x₀ a₁)
Tag 06JJ, a remark

Tag 06JJ in the Stacks Project.

Deformation.mapLiftClasses_vadd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Action/Functoriality.lean, line 289.

Stacks Project, Tag 06JJ. The map on lift classes commutes with the torsor actions, with tangent vectors mapped by the differential tensored with the identity of the kernel.

public theorem mapLiftClasses_vadd
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (𝓕 : BasedCategory.{vF, uF} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (𝓖 : BasedCategory.{vG, uG} (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (h𝓕 : IsDeformationCategory 𝓕.p)
    (h𝓖 : IsDeformationCategory 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖)
    {A' A : ArtinianLocalAlgCat.{u, w, w} Λ k}
    (f : A' ⟶ A) (hf : Function.Surjective f.hom)
    (hann : ∀ a : A', a ∈ maximalIdeal A' →
      ∀ i : RingHom.ker f.hom.toRingHom, a * (i : A') = 0)
    (x : 𝓕.p.Fiber A) :
    letI : Module k (RingHom.ker f.hom.toRingHom) := kernelModule f hann
    let hS2𝓕 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓕 h𝓕.predeformation.cofibered
      (schlessingerConditionS2_of_satisfiesRS h𝓕.satisfiesRS)
      (.inl h𝓕.predeformation)
    let hS2𝓖 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓖 h𝓖.predeformation.cofibered
      (schlessingerConditionS2_of_satisfiesRS h𝓖.satisfiesRS)
      (.inl h𝓖.predeformation)
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨h𝓕.predeformation⟩
    letI : Fact (IsPredeformationCategory 𝓖.p) := ⟨h𝓖.predeformation⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))) := ⟨hS2𝓕⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓖 h𝓖.predeformation.cofibered))) := ⟨hS2𝓖⟩
    letI := liftAction 𝓕 h𝓕 f hf hann x
    letI := liftAction 𝓖 h𝓖 f hf hann ((fiberFunctor φ A).obj x)
    let dφ := IsLinearMap.mk' (differential h𝓕.predeformation.cofibered
      h𝓖.predeformation.cofibered φ)
      (differential_isLinearMap 𝓕 𝓖 h𝓕.predeformation h𝓖.predeformation hS2𝓕 hS2𝓖 φ)
    ∀ (a : LiftClasses 𝓕.p f x)
      (t : TensorProduct k
        (artinianTangentSpace Λ k
          (isomorphismClasses 𝓕 h𝓕.predeformation.cofibered))
        (RingHom.ker f.hom.toRingHom)),
      mapLiftClasses φ f x (t +ᵥ a) =
        (TensorProduct.map dφ (LinearMap.id :
          RingHom.ker f.hom.toRingHom →ₗ[k] RingHom.ker f.hom.toRingHom) t) +ᵥ
          mapLiftClasses φ f x a
Sources
LeanDeformation.Lift · Deformation.Lift.Hom · Deformation.LiftClasses · Deformation.Lift.over · Deformation.LiftClasses.over · Deformation.liftClassesEquivObjectsOver · Deformation.liftClassesTangentSpace · Deformation.liftClassesTangentSpace_naturality

Section90.18 Schlessinger's theorem on prorepresentable functors#

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

Tag 06JL, a lemma

Tag 06JL in the Stacks Project.

Deformation.isIso_of_isSmooth_of_tangent_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Smoothness/TangentIsomorphism.lean, line 410.

Stacks Project, Tag 06JL. A smooth morphism of deformation functors whose differential is bijective is an isomorphism.

public theorem isIso_of_isSmooth_of_tangent_bijective
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F G : ArtinianLocalAlgCat.{u, w, w} Λ k ⥤ Type t}
    (hF : IsDeformationFunctor F)
    (hG : IsDeformationFunctor G)
    (φ : F ⟶ G)
    (hφ : IsSmooth (elementsBasedFunctor φ))
    (hdφ : Function.Bijective
      (φ.app (augmentedDualNumbers (Λ := Λ) (k := k)))) :
    IsIso φ
Tag 06JM, a theorem

Tag 06JM in the Stacks Project.

Deformation.isProrepresentable_iff_isDeformationFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Schlessinger/Prorepresentable.lean, line 1216. References: SGA 7 VI (2.18).

Schlessinger's theorem. A set-valued functor on the category of Artinian local Λ-algebras with residue field k is prorepresentable exactly when it is a deformation functor, its tangent space is a finite-dimensional k-vector space, and the canonical map from the Λ-derivations of k to that tangent space is injective.

public theorem isProrepresentable_iff_isDeformationFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [IsNoetherianRing Λ]
    [Field k] [Algebra Λ k] [Module.Finite Λ k]
    (F : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type (max v w)) :
    IsProrepresentable F ↔
      ∃ hF : IsDeformationFunctor F,
        let p := CategoryOfElements.π F
        let 𝓕 := BasedCategory.ofFunctor p
        let hD := (isDeformationCategory_iff F).2 hF
        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 := tangentSpaceArtinian Λ k
          (isomorphismClasses 𝓕 hD.predeformation.cofibered)
        letI : AddCommGroup T := associatedTangentSpaceAddCommGroup 𝓕
        letI : Module k T := associatedTangentSpaceModule 𝓕
        FiniteDimensional k T ∧
          Function.Injective (derivationToTangentSpace p hD.predeformation)
Sources
LeanDeformation.isIso_of_isSmooth_of_tangent_bijective · Deformation.isProrepresentable_iff_isDeformationFunctor

Section90.19 Infinitesimal automorphisms#

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

Tag 06JP, a definition

Tag 06JP in the Stacks Project.

Deformation.relativeInfinitesimalAutomorphisms, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Object.lean, line 162.

The group of infinitesimal automorphisms of x' relative to x along f : x' ⟶ x: the kernel of the canonical homomorphism between the two fibre automorphism groups.

public noncomputable def relativeInfinitesimalAutomorphisms
    (hp : IsCofiberedInGroupoids p) (g : A' ⟶ A) (f : x'.1 ⟶ x.1)
    (hf : p.IsHomLift g f) : Subgroup (Aut x')
Tag 06JQ, a definition

Tag 06JQ in the Stacks Project.

Deformation.infinitesimalAutomorphisms, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Object.lean, line 273. The attribute's comment: “infinitesimal automorphism group”.

The group of infinitesimal automorphisms at a point, for a chosen pushforward along the constant inclusion into the dual numbers.

public noncomputable abbrev infinitesimalAutomorphisms
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    {A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k}
    {x₀ : p.Fiber A₀} {xε : p.Fiber Aε}
    (hp : IsCofiberedInGroupoids p)
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i) : Subgroup (Aut xε)

Deformation.existsUnique_retraction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Object.lean, line 346. The attribute's comment: “unique map back”.

A chosen pushforward along the constant inclusion into the dual numbers has a unique retraction, without a restriction on the image of that retraction in the base.

public theorem existsUnique_retraction
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    {A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k}
    {x₀ : p.Fiber A₀} {xε : p.Fiber Aε}
    (hp : IsCofiberedInGroupoids p)
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i) :
    ∃! r : xε.1 ⟶ x₀.1, i ≫ r = 𝟙 x₀.1
Tag 06JR, a remark

Tag 06JR in the Stacks Project.

Deformation.existsUnique_pushforwardIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 26. The attribute's comment: “canonical isomorphism of pushforwards”.

Pushforwards of isomorphic objects along the same arrow have a unique isomorphism commuting with their structure maps.

public theorem existsUnique_pushforwardIso
    {F : Type u₁} [Category.{v₁} F]
    {C : Type u₂} [Category.{v₂} C] {p : F ⥤ C}
    {A₀ A : C} {x₀ y₀ : p.Fiber A₀} {x y : p.Fiber A}
    (hp : IsCofiberedInGroupoids p)
    (g : A₀ ⟶ A) (h₀ : x₀ ≅ y₀)
    (i : x₀.1 ⟶ x.1) (hi : p.IsHomLift g i)
    (j : y₀.1 ⟶ y.1) (hj : p.IsHomLift g j) :
    ∃! h : x ≅ y, i ≫ h.hom.val = h₀.hom.val ≫ j

Deformation.existsUnique_infinitesimalAutomorphismsEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 172. The attribute's comment: “invariance under isomorphism of the original object”.

An isomorphism of the original objects canonically identifies their infinitesimal automorphism groups, by conjugation through the unique comparison of their pushforwards.

public theorem existsUnique_infinitesimalAutomorphismsEquiv
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    {A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k}
    {x₀ y₀ : p.Fiber A₀} {xε yε : p.Fiber Aε}
    (hp : IsCofiberedInGroupoids p)
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀)
    (hpair : IsCanonicalDualNumberPair g e)
    (h₀ : x₀ ≅ y₀)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i)
    (j : y₀.1 ⟶ yε.1) (hj : p.IsHomLift g j) :
    ∃! φ : infinitesimalAutomorphisms hp g e hpair i hi ≃*
        infinitesimalAutomorphisms hp g e hpair j hj,
      ∃ h : xε ≅ yε,
        (i ≫ h.hom.val = h₀.hom.val ≫ j) ∧
        (∀ a, (φ a).1 = h.conjAut a.1)

Deformation.existsUnique_infinitesimalAutomorphismAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 207. The attribute's comment: “action of automorphisms of the original object”.

The automorphism group of the original object acts on its infinitesimal automorphism group by conjugation through pushed-forward automorphisms.

public theorem existsUnique_infinitesimalAutomorphismAction
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    {A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k}
    {x₀ : p.Fiber A₀} {xε : p.Fiber Aε}
    (hp : IsCofiberedInGroupoids p)
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i) :
    ∃! ρ : Aut x₀ →* MulAut
        (infinitesimalAutomorphisms hp g e hpair i hi),
      ∀ (a : Aut x₀)
        (b : infinitesimalAutomorphisms hp g e hpair i hi),
        ((ρ a) b).1 =
          (pushforwardAutomorphism hp g i hi a).asIso.conjAut b.1
Tag 06JS, a remark

Tag 06JS in the Stacks Project.

Deformation.subsingleton_aut_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 274. The attribute's comment: “automorphisms_at_a_point”.

The automorphism group of an object over the residue field in a predeformation category is trivial.

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

Deformation.infinitesimalAutomorphisms_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 285. The attribute's comment: “automorphisms_at_a_point”.

Every automorphism of a pushforward to the dual numbers is infinitesimal.

public theorem infinitesimalAutomorphisms_eq_top
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (hp : IsPredeformationCategory p)
    {Aε : ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (x₀ : p.Fiber (residueFieldObject Λ k)) (xε : p.Fiber Aε)
    (g : residueFieldObject Λ k ⟶ Aε)
    (e : Aε ⟶ residueFieldObject Λ k)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i) :
    infinitesimalAutomorphisms hp.cofibered g e hpair i hi = ⊤

Deformation.existsUnique_pointIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 312. The attribute's comment: “independence_of_point”.

Any two points over the residue field in a predeformation category have exactly one isomorphism between them.

public theorem existsUnique_pointIso
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (hp : IsPredeformationCategory p)
    (x₀ y₀ : p.Fiber (residueFieldObject.{u, v, w} Λ k)) :
    ∃! _ : x₀ ≅ y₀, True

Deformation.existsUnique_infinitesimalAutomorphismsEquiv_of_isPredeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 328. The attribute's comment: “independence_of_point”.

The unique isomorphism of points induces the canonical group isomorphism on infinitesimal automorphisms. Its action is conjugation by any compatible isomorphism between chosen pushforwards to the dual numbers.

public theorem existsUnique_infinitesimalAutomorphismsEquiv_of_isPredeformationCategory
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (hp : IsPredeformationCategory p)
    {Aε : ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (g : residueFieldObject.{u, v, w} Λ k ⟶ Aε)
    (e : Aε ⟶ residueFieldObject.{u, v, w} Λ k)
    (hpair : IsCanonicalDualNumberPair g e)
    (x₀ y₀ : p.Fiber (residueFieldObject.{u, v, w} Λ k))
    (xε yε : p.Fiber Aε)
    (iₓ : x₀.1 ⟶ xε.1) (hiₓ : p.IsHomLift g iₓ)
    (iᵧ : y₀.1 ⟶ yε.1) (hiᵧ : p.IsHomLift g iᵧ) :
    ∃! φ : ↥(infinitesimalAutomorphisms hp.cofibered g e hpair iₓ hiₓ) ≃*
        ↥(infinitesimalAutomorphisms hp.cofibered g e hpair iᵧ hiᵧ),
      ∀ (f : x₀ ≅ y₀) (j : xε ≅ yε),
        (iₓ ≫ j.hom.val = f.hom.val ≫ iᵧ) →
          ∀ a, (φ a).val.asIso.hom.val = j.inv.val ≫ a.val.asIso.hom.val ≫ j.hom.val

Deformation.infinitesimalAutomorphismGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 425. The attribute's comment: “infinitesimal_automorphisms_of_predeformation_category”.

The infinitesimal automorphism group of a predeformation category, formed using a chosen object over the residue field and its pushforward to the dual numbers.

public noncomputable abbrev infinitesimalAutomorphismGroup
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (hp : IsPredeformationCategory p)
    {Aε : ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    {x₀ : p.Fiber (residueFieldObject Λ k)} {xε : p.Fiber Aε}
    (g : residueFieldObject Λ k ⟶ Aε)
    (e : Aε ⟶ residueFieldObject Λ k)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i) : Type _

Deformation.infinitesimalAutomorphismGroup_uniqueEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Independence.lean, line 442. The attribute's comment: “infinitesimal_automorphisms_of_predeformation_category”.

Changing the chosen object over the residue field, and its pushforward, gives a unique identification of infinitesimal automorphism groups. On automorphisms it is conjugation by the isomorphism between the pushforwards.

public theorem infinitesimalAutomorphismGroup_uniqueEquiv
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (hp : IsPredeformationCategory p)
    {Aε : ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    {x₀ y₀ : p.Fiber (residueFieldObject Λ k)}
    {xε yε : p.Fiber Aε}
    (g : residueFieldObject Λ k ⟶ Aε)
    (e : Aε ⟶ residueFieldObject Λ k)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i)
    (j : y₀.1 ⟶ yε.1) (hj : p.IsHomLift g j) :
    ∃! E : infinitesimalAutomorphismGroup hp g e hpair i hi ≃*
        infinitesimalAutomorphismGroup hp g e hpair j hj,
      ∃ (f₀ : x₀ ≅ y₀) (fε : xε ≅ yε),
        f₀.hom.val ≫ j = i ≫ fε.hom.val ∧
        (∀ a, (E a).val = fε.conjAut a.val)

Deformation.infinitesimalAutomorphismGroup_objectsOverFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Basic/Localization.lean, line 225. The attribute's comment: “infinitesimal_automorphisms_of_localization”.

Infinitesimal automorphisms of objects over x₀ are the infinitesimal automorphisms of x₀.

public theorem infinitesimalAutomorphismGroup_objectsOverFunctor
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    (hp : IsPredeformationCategory p)
    {Aε : ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    {x₀ : p.Fiber (residueFieldObject Λ k)} {xε : p.Fiber Aε}
    (g : residueFieldObject Λ k ⟶ Aε)
    (e : Aε ⟶ residueFieldObject Λ k)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i)
    {y₀ : (objectsOverFunctor p x₀.1).Fiber
      (residueFieldObject Λ k)}
    {yε : (objectsOverFunctor p x₀.1).Fiber Aε}
    (j : y₀.1 ⟶ yε.1)
    (hj : (objectsOverFunctor p x₀.1).IsHomLift g j)
    (h₀ : y₀.1.left = x₀.1) (hε : yε.1.left = xε.1)
    (h₀hom : y₀.1.hom = eqToHom h₀)
    (hεhom : yε.1.hom = eqToHom hε ≫
      (canonicalRetraction hp.cofibered g e hpair.split i hi).1)
    (hjleft : j.left ≫ eqToHom hε = eqToHom h₀ ≫ i) :
    ∃! E :
      infinitesimalAutomorphismGroup
        (isPredeformationCategory_objectsOverFunctor p hp.cofibered x₀)
        g e hpair j hj ≃* infinitesimalAutomorphismGroup hp g e hpair i hi,
      ∀ a, (E a).val.asIso.hom.val =
        eqToHom hε.symm ≫ a.val.asIso.hom.val.left ≫ eqToHom hε
Tag 06JT, a definition

Tag 06JT in the Stacks Project.

Deformation.automorphismFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Functor.lean, line 338.

The automorphism functor of x: at f : p.obj x ⟶ V it is the type of automorphisms over V of the chosen pushforward f_* x.

public noncomputable def automorphismFunctor
    {F : Type u₁} [Category.{v₁} F] {C : Type u₂} [Category.{v₂} C]
    {p : F ⥤ C} {x : F} (P : ChosenPushforwardsAt p x) : Under (p.obj x) ⥤ Type v₁
Tag 06JU, a lemma

Tag 06JU in the Stacks Project.

Deformation.automorphismFunctor_satisfiesRS, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/AutomorphismFunctorRS.lean, line 69.

The automorphism functor of an object in a category cofibered in groupoids satisfying (RS) itself satisfies (RS).

public theorem automorphismFunctor_satisfiesRS
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    (hp : SatisfiesRS p) (x : F)
    (P : ChosenPushforwardsAt p x) :
    SatisfiesRSUnder (p.obj x) (automorphismFunctor P)
Tag 06JV, a lemma

Tag 06JV in the Stacks Project.

Deformation.exists_naturalLocalizedAutomorphismTangentVectorSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/TangentVectorSpace.lean, line 879. The attribute's comment: “part (1)”. References: SGA 7 VI (2.6(c)), “Aut(1_ε) k-structure”.

Stacks Project, Tag 06JV (1). On the tangent space at the identity of the automorphism functor of x, addition is composition of automorphisms and scalar multiplication is induced by the canonical scaling of the dual-number coordinate; in particular composition there is commutative.

public theorem exists_naturalLocalizedAutomorphismTangentVectorSpace
    (hp : SatisfiesRS p) :
    ∃ V : AddCommGroup (localizedAutomorphismFunctorTangent P),
      letI := V
      ∃ M : Module k (localizedAutomorphismFunctorTangent P),
        letI := M
        (∀ a b, localizedTangentEquivKernel P (a + b) =
          localizedTangentEquivKernel P a * localizedTangentEquivKernel P b) ∧
        (∀ (c : k) a, (localizedTangentEquivKernel P (c • a)).1 =
          P.transportAutHom (tangentScaling c) (localizedTangentEquivKernel P a).1)

Deformation.existsUnique_localizedTangentAutomorphismLinearEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/TangentVectorSpace.lean, line 1020. The attribute's comment: “part (2)”.

Stacks Project, Tag 06JV (2). Pushforward to the special fibre canonically identifies the tangent spaces at the identity of the two automorphism functors. The comparison is conjugation by the unique isomorphism of dual-number pushforwards lying over the identity of the dual-number ring.

public theorem existsUnique_localizedTangentAutomorphismLinearEquiv
    (_hbase : p.obj x₀ = residueFieldObject.{u, v, w} Λ k)
    (P : ChosenPushforwardsAt p x)
    (Q : ChosenPushforwardsAt p x₀) :
    letI := naturalLocalizedTangentAddCommGroup P hp
    letI := naturalLocalizedTangentModule P hp
    letI := naturalLocalizedTangentAddCommGroup Q hp
    letI := naturalLocalizedTangentModule Q hp
    let U₀ := specialFibreUnder (p := p) (x := x)
    let Uε := dualNumbersUnder (p := p) (x := x)
    let V₀ := specialFibreUnder (p := p) (x := x₀)
    let Vε := dualNumbersUnder (p := p) (x := x₀)
    ∃! E : localizedAutomorphismFunctorTangent P ≃ₗ[k]
        localizedAutomorphismFunctorTangent Q,
      ∃ (H₀ : (P.obj U₀).1 ≅ (Q.obj V₀).1)
          (Hε : (P.obj Uε).1 ≅ (Q.obj Vε).1),
        (P.inclusion U₀ ≫ H₀.hom = j ≫ Q.inclusion V₀) ∧
        (P.inclusion Uε ≫ Hε.hom = j ≫ Q.inclusion Vε) ∧
        (∀ t : Uε.right,
          (eqToHom (P.obj Uε).2.symm ≫ p.map Hε.hom ≫
            eqToHom (Q.obj Vε).2).hom t = t) ∧
        (∀ a, (localizedTangentEquivKernel P a).1.asIso.hom.val ≫ Hε.hom =
          Hε.hom ≫ (localizedTangentEquivKernel Q (E a)).1.asIso.hom.val)
Tag 06JW, a remark

Tag 06JW in the Stacks Project.

Deformation.relativeInfinitesimalAutomorphismsEquivIdentityLifts, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/IdentityLifts.lean, line 92. The attribute's comment: “relative identity lifts”.

Relative infinitesimal automorphisms are precisely lifts of the identity automorphism along the given morphism.

public noncomputable def relativeInfinitesimalAutomorphismsEquivIdentityLifts
    {F : Type u₁} [Category.{v₁} F] {C : Type u} [Category.{v} C]
    {p : F ⥤ C} {A' A : C} {x' : p.Fiber A'} {x : p.Fiber A}
    (hp : IsCofiberedInGroupoids p)
    (g : A' ⟶ A) (f : x'.1 ⟶ x.1) (hf : p.IsHomLift g f) :
    relativeInfinitesimalAutomorphisms hp g f hf ≃
      identityAutomorphismLifts hp g f hf

Deformation.infinitesimalAutomorphismsEquivIdentityLifts, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/IdentityLifts.lean, line 122. The attribute's comment: “dual-number identity lifts”.

Infinitesimal automorphisms at a residue-field object are lifts of its identity automorphism to the dual numbers.

public noncomputable def infinitesimalAutomorphismsEquivIdentityLifts
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    {A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k}
    {x₀ : p.Fiber A₀} {xε : p.Fiber Aε}
    (hp : IsCofiberedInGroupoids p)
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀)
    (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i) :
    let r := canonicalRetraction hp g e hpair.split i hi
    infinitesimalAutomorphisms hp g e hpair i hi ≃
      identityAutomorphismLifts hp e r.1 r.2.1

Deformation.infinitesimalAutomorphisms_eq_tangentFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/IdentityLifts.lean, line 141. The attribute's comment: “tangent fibre at the identity”.

At a point over the residue field, infinitesimal automorphisms are the fibre over the identity of the automorphism functor at the dual numbers.

public theorem infinitesimalAutomorphisms_eq_tangentFiber
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, v, w} Λ k}
    {x : F} (hp : IsCofiberedInGroupoids p)
    (P : ChosenPushforwardsAt p x)
    {A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k}
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀)
    (hpair : IsCanonicalDualNumberPair g e)
    (hbase : p.obj x = A₀) :
    let U₀ : Under (p.obj x) := Under.mk (eqToHom hbase)
    let Uε : Under (p.obj x) := Under.mk (eqToHom hbase ≫ g)
    let j : U₀ ⟶ Uε := Under.homMk g (by simp [U₀, Uε])
    let r : Uε ⟶ U₀ := Under.homMk e (by simp [U₀, Uε, hpair.split])
    infinitesimalAutomorphisms hp g e hpair (P.map j)
      (P.map_isHomLift j) = MonoidHom.ker (P.transportAutHom r)

Deformation.infinitesimalAutomorphismsEquivTangentSpaceAtIdentity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/IdentityLifts.lean, line 724. The attribute's comment: “tangent space at the identity”.

Infinitesimal automorphisms at a residue-field object are the tangent space at the identity of its automorphism functor.

public noncomputable def infinitesimalAutomorphismsEquivTangentSpaceAtIdentity
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {F : Type u₁} [Category.{v₁} F]
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k}
    {x : F}
    (hp : IsCofiberedInGroupoids p)
    (P : ChosenPushforwardsAt p x)
    (hbase : p.obj x = residueFieldObject.{u, v, w} Λ k)
    (Aε : ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (g : residueFieldObject.{u, v, w} Λ k ⟶ Aε)
    (e : Aε ⟶ residueFieldObject.{u, v, w} Λ k)
    (hpair : IsCanonicalDualNumberPair g e) :
    let U₀ : Under (p.obj x) := Under.mk (eqToHom hbase)
    let Uε : Under (p.obj x) := Under.mk (eqToHom hbase ≫ g)
    let j : U₀ ⟶ Uε := Under.homMk g (by simp [U₀, Uε])
    let baseChange := residueAlgebrasToUnder.{u, v, w} Λ k ⋙
      Under.map (eqToHom hbase)
    let AutFunctor := baseChange ⋙ automorphismFunctor P
    let q := CategoryOfElements.π AutFunctor
    let k₀ := residueFieldObject.{w, v, w} k k
    let identityPoint : q.Fiber k₀ :=
      ⟨AutFunctor.elementsMk k₀ (1 : Aut (P.obj (baseChange.obj k₀))), rfl⟩
    (infinitesimalAutomorphisms hp g e hpair (P.map j)
      (P.map_isHomLift j)) ≃
    tangentSpaceAtPoint q
        (automorphismFunctorCategory_isCofiberedInGroupoids P baseChange)
        identityPoint
Tag 06JX, a lemma

Tag 06JX in the Stacks Project.

Deformation.exists_naturalLocalizedAutomorphismTangentVectorSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/TangentVectorSpace.lean, line 879. The attribute's comment: “Inf_{x_0}(F) as the tangent space, with addition composition”. References: SGA 7 VI (2.6(c)), “Aut(1_ε) k-structure”.

Stacks Project, Tag 06JV (1). On the tangent space at the identity of the automorphism functor of x, addition is composition of automorphisms and scalar multiplication is induced by the canonical scaling of the dual-number coordinate; in particular composition there is commutative.

public theorem exists_naturalLocalizedAutomorphismTangentVectorSpace
    (hp : SatisfiesRS p) :
    ∃ V : AddCommGroup (localizedAutomorphismFunctorTangent P),
      letI := V
      ∃ M : Module k (localizedAutomorphismFunctorTangent P),
        letI := M
        (∀ a b, localizedTangentEquivKernel P (a + b) =
          localizedTangentEquivKernel P a * localizedTangentEquivKernel P b) ∧
        (∀ (c : k) a, (localizedTangentEquivKernel P (c • a)).1 =
          P.transportAutHom (tangentScaling c) (localizedTangentEquivKernel P a).1)
Tag 07W6, a lemma

Tag 07W6 in the Stacks Project.

Deformation.inducedInfinitesimalLinearMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Morphism.lean, line 542. The attribute's comment: “the induced k-linear map, as a construction”.

Stacks Project, Tag 07W6. A morphism of categories cofibered in groupoids over 𝒞_Λ satisfying (RS) induces a k-linear map on infinitesimal automorphisms at a point.

public noncomputable def inducedInfinitesimalLinearMap (hp : SatisfiesRS (Φ ⋙ q))
    (hq : SatisfiesRS q) :
    letI := naturalLocalizedTangentAddCommGroup P hp
    letI := naturalLocalizedTangentModule P hp
    letI := naturalLocalizedTangentAddCommGroup Q hq
    letI := naturalLocalizedTangentModule Q hq
    localizedAutomorphismFunctorTangent P →ₗ[k] localizedAutomorphismFunctorTangent Q

Deformation.exists_inducedInfinitesimalLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Morphism.lean, line 606. The attribute's comment: “the morphism presented as a functor commuting with the two projections, with the map pinned by the dual-number comparison”.

Stacks Project, Tag 07W6. Presented with a morphism as a functor commuting with the two projections: it induces a k-linear map on infinitesimal automorphisms, pinned by the comparison of dual-number pushforwards.

public theorem exists_inducedInfinitesimalLinearMap
    {p : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k} (hw : Φ ⋙ q = p) (hp : SatisfiesRS p)
    (hq : SatisfiesRS q) (P : ChosenPushforwardsAt p x₀)
    (Q : ChosenPushforwardsAt q (Φ.obj x₀)) :
    letI := naturalLocalizedTangentAddCommGroup P hp
    letI := naturalLocalizedTangentModule P hp
    letI := naturalLocalizedTangentAddCommGroup Q hq
    letI := naturalLocalizedTangentModule Q hq
    ∃ T : localizedAutomorphismFunctorTangent P →ₗ[k] localizedAutomorphismFunctorTangent Q,
      ∃ H : (Q.obj (dualNumbersUnder (p := q) (x := Φ.obj x₀))).1 ⟶
          Φ.obj (P.obj (dualNumbersUnder (p := p) (x := x₀))).1,
        q.IsHomLift (𝟙 (dualNumbersUnder (p := q) (x := Φ.obj x₀)).right) H ∧
          Q.inclusion (dualNumbersUnder (p := q) (x := Φ.obj x₀)) ≫ H =
            Φ.map (P.inclusion (dualNumbersUnder (p := p) (x := x₀))) ∧
          ∀ a, (localizedTangentEquivKernel Q (T a)).1.asIso.hom.val ≫ H =
            H ≫ Φ.map (localizedTangentEquivKernel P a).1.asIso.hom.val
Tag 06JY, a lemma

Tag 06JY in the Stacks Project.

Deformation.exists_localizedTangentEquiv_infinitesimalAutomorphismKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/TangentTensorAction.lean, line 76. The attribute's comment: “the two descriptions of the acting group”.

Stacks Project, Tag 06JY. The two descriptions of the acting group agree: for a morphism j : y ⟶ y₀ of a category cofibered in groupoids over 𝒞_Λ satisfying (RS) whose target lies over the residue field, the k-vector space T_{id_{y₀}} Aut(y) is linearly isomorphic to T_{id_{y₀}} Aut(y₀), and the latter is the group Inf_{y₀}(𝓕) of infinitesimal automorphisms of the dual-number pushforward of y₀ by an equivalence taking addition to composition. Tensoring with the kernel therefore gives the same space either way.

public theorem exists_localizedTangentEquiv_infinitesimalAutomorphismKernel
    (hrs : SatisfiesRS p) {y y₀ : F} (j : y ⟶ y₀)
    (hbase : p.obj y₀ = residueFieldObject.{u, w, w} Λ k)
    (P : ChosenPushforwardsAt p y) (Q : ChosenPushforwardsAt p y₀) :
    letI := naturalLocalizedTangentAddCommGroup P hrs
    letI := naturalLocalizedTangentModule P hrs
    letI := naturalLocalizedTangentAddCommGroup Q hrs
    letI := naturalLocalizedTangentModule Q hrs
    ∃ (_ : localizedAutomorphismFunctorTangent P ≃ₗ[k]
        localizedAutomorphismFunctorTangent Q)
      (G : localizedAutomorphismFunctorTangent Q ≃
        infinitesimalAutomorphismKernel Q (tangentReduction (p := p) (x := y₀))),
      ∀ a b, G (a + b) = G a * G b

Deformation.exists_freeTransitiveAction_tangentTensor_relativeInfinitesimalAutomorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/TangentTensorSplit.lean, line 777. The attribute's comment: “the free and transitive action”.

For a category cofibered in groupoids over 𝒞_Λ satisfying (RS) and a morphism φ : x' ⟶ x lying over a surjection g : A' → A whose kernel I is annihilated by the maximal ideal of A', the group Inf(x'/x) of infinitesimal automorphisms of x' over x carries a free and transitive action by T_{id_{x₀}} Aut(x') ⊗_k I.

public theorem exists_freeTransitiveAction_tangentTensor_relativeInfinitesimalAutomorphisms
    (hrs : SatisfiesRS p) {A' A : ArtinianLocalAlgCat.{u, w, w} Λ k}
    {x' : p.Fiber A'} {x : p.Fiber A}
    (g : A' ⟶ A) (φ : x'.1 ⟶ x.1) (hφ : p.IsHomLift g φ)
    (hg : Function.Surjective g.hom)
    (hann : ∀ a : A', a ∈ maximalIdeal A' →
      ∀ i : RingHom.ker g.hom.toRingHom, a * (i : A') = 0)
    {x₀ : p.Fiber (residueFieldObject.{u, w, w} Λ k)}
    (ψ₀ : x.1 ⟶ x₀.1) (hψ₀ : p.IsHomLift (residueMorphism A) ψ₀)
    (P : ChosenPushforwardsAt p x'.1) :
    letI : Module k (RingHom.ker g.hom.toRingHom) := kernelModule g hann
    letI := naturalLocalizedTangentAddCommGroup P hrs
    letI := naturalLocalizedTangentModule P hrs
    ∃ act : TensorProduct k (localizedAutomorphismFunctorTangent P)
          (RingHom.ker g.hom.toRingHom) →
        ↥(relativeInfinitesimalAutomorphisms hrs.1 g φ hφ) →
        ↥(relativeInfinitesimalAutomorphisms hrs.1 g φ hφ),
      (∀ s, act 0 s = s) ∧
      (∀ t u s, act (t + u) s = act t (act u s)) ∧
      (∀ s t, act t s = s → t = 0) ∧
      (∀ s s', ∃ t, act t s = s') ∧
      (∀ s, Function.Bijective fun t => act t s)
Tag 06JZ, a lemma

Tag 06JZ in the Stacks Project.

Deformation.relativeInfinitesimalAutomorphisms_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/Vanishing.lean, line 884.

Let 𝓕 be a category cofibered in groupoids over 𝒞_Λ satisfying (RS), let x' ⟶ x be a morphism of 𝓕 lying over a surjection, and let x₀ be a pushforward of x to the special fibre. If the infinitesimal automorphisms of x₀ vanish, then so do the infinitesimal automorphisms of x' over x.

theorem relativeInfinitesimalAutomorphisms_eq_bot
    (hrs : SatisfiesRS p)
    {B A A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k}
    {x' : p.Fiber B} {x : p.Fiber A} {x₀ : p.Fiber A₀} {xε : p.Fiber Aε}
    (g : B ⟶ A) (f : x'.1 ⟶ x.1) (hf : p.IsHomLift g f)
    (hg : Function.Surjective g.hom)
    (g₀ : A ⟶ A₀) (f₀ : x.1 ⟶ x₀.1) (hf₀ : p.IsHomLift g₀ f₀)
    (i : A₀ ⟶ Aε) (e : Aε ⟶ A₀)
    (hpair : IsCanonicalDualNumberPair i e)
    (fi : x₀.1 ⟶ xε.1) (hfi : p.IsHomLift i fi)
    (htriv : infinitesimalAutomorphisms hrs.1 i e hpair fi hfi = ⊥) :
    relativeInfinitesimalAutomorphisms hrs.1 g f hf = ⊥
Tag 06K0, a lemma

Tag 06K0 in the Stacks Project.

Deformation.infinitesimalAutomorphisms_eq_bot_iff_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/EquivalenceCriterion.lean, line 208.

Stacks 06K0. For a category cofibered in groupoids over 𝒞_Λ satisfying (RS) and an object x₀ of the fibre over the residue field, the infinitesimal automorphisms of x₀ vanish exactly when the canonical morphism ℱ_{x₀} ⟶ ℱ̄_{x₀} to the functor of fibrewise isomorphism classes is an equivalence.

theorem infinitesimalAutomorphisms_eq_bot_iff_isEquivalence (hrs : SatisfiesRS p)
    {A₀ Aε : ArtinianLocalAlgCat.{u, v, w} Λ k} {x₀ : p.Fiber A₀} {xε : p.Fiber Aε}
    (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
    (i : x₀.1 ⟶ xε.1) (hi : p.IsHomLift g i) :
    infinitesimalAutomorphisms hrs.1 g e hpair i hi = ⊥ ↔
      (toIsomorphismClasses (pointLocalization p x₀.1)
        (isCofiberedInGroupoids_objectsOverFunctor hrs.1
          (maximalIdeal_eq_bot_of_isCanonicalDualNumberPair hpair)
            x₀)).toFunctor.IsEquivalence
Sources
LeanDeformation.relativeInfinitesimalAutomorphisms · Deformation.infinitesimalAutomorphisms · Deformation.existsUnique_retraction · Deformation.existsUnique_pushforwardIso · Deformation.existsUnique_infinitesimalAutomorphismsEquiv · Deformation.existsUnique_infinitesimalAutomorphismAction · Deformation.subsingleton_aut_residueField · Deformation.infinitesimalAutomorphisms_eq_top

Section90.20 Applications#

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

Tag 06L5, a lemma

Tag 06L5 in the Stacks Project.

Deformation.boundaryLinearMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductBoundaryLinear.lean, line 495. The attribute's comment: “part (2), the boundary map Inf(ℱ) → T𝒲 of the six-term exact sequence, as a k-linear map of the vector spaces of Tag 06IH”.

Stacks Project, Tag 06L5, part (2): the boundary map δ : Inf(ℱ) → T𝒲 of the six-term sequence, as a k-linear map, at an arbitrary coordinate module. At the rank-one module this is the third map of the six-term exact sequence of the 2-fibre product.

This is the form of δ that the sequence of k-vector spaces asks for; Deformation.boundaryFun, of which it is the linear reading, is a map of sets.

public noncomputable def boundaryLinearMap
    (pF : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k) (f : H ⥤ F) (g : G ⥤ F)
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF)
    {y₀ : H} {z₀ : G} (hzy : (g ⋙ pF).obj z₀ = (f ⋙ pF).obj y₀)
    {cmp : f.obj y₀ ≅ g.obj z₀}
    (hcmp : pF.IsHomLift (𝟙 ((f ⋙ pF).obj y₀)) cmp.hom)
    (PH : ChosenPushforwardsAt (f ⋙ pF) y₀) (PG : ChosenPushforwardsAt (g ⋙ pF) z₀)
    (PF : ChosenPushforwardsAt pF (f.obj y₀)) (M : FGModuleCat.{max v w} k) :
    ↥((infinitesimalAutomorphismLinearLift PF hF.satisfiesRS).functor.obj M) →ₗ[k]
      ↥((productTangentLift.{u, v, w} pF f g hH hG hF).obj M)

Deformation.isDeformationCategory_twoFibreProductOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductDeformation.lean, line 260. The attribute's comment: “part (1)”.

Stacks Project, Tag 06L5, part (1). The 2-fibre product 𝒲 = ℋ ×_ℱ 𝒢 of two 1-morphisms of deformation categories over 𝒞_Λ is again a deformation category.

Condition (RS) is Tag 06L4, and it carries the cofibered-in-groupoids condition with it; the special fibre 𝒲(k) has a unique isomorphism class because ℋ(k), 𝒢(k) and ℱ(k) do.

theorem isDeformationCategory_twoFibreProductOver
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {H : Type u₁} [Category.{v₁} H]
    {G : Type u₂} [Category.{v₂} G]
    {F : Type u₃} [Category.{v₃} F]
    (pH : H ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (pG : G ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (pF : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (f : H ⥤ F) (g : G ⥤ F)
    (hf : f ⋙ pF = pH) (hg : g ⋙ pF = pG)
    (hH : IsDeformationCategory pH)
    (hG : IsDeformationCategory pG)
    (hF : IsDeformationCategory pF) :
    IsDeformationCategory (TwoFibreProductOver.structureFunctor pH pG pF f g)

Deformation.injective_infProjPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductInfRow.lean, line 302. The attribute's comment: “part (2), the map Inf(𝒲) → Inf(ℋ) ⊕ Inf(𝒢) of the six-term exact sequence and the injectivity of it asserted at the first spot”.

Stacks Project, Tag 06L5, part (2): exactness at Inf(𝒲). The map a : Inf(𝒲) → Inf(ℋ) ⊕ Inf(𝒢) of the six-term sequence is injective, which is the 0 → at its source.

This is the source's "injectivity of the first map comes from the fact that f × g : 𝒲 → ℋ × 𝒢 is faithful": the induced map on infinitesimal automorphisms is conjugation by the comparison of dual-number pushforwards (Deformation.inducedInfinitesimalLinearMap_apply), so a tangent vector in the kernel of both components is an automorphism of a pushforward of w₀ whose two projections are identities, and a self-arrow of the 2-fibre product is determined by its two components (CategoryTheory.TwoFibreProductOver.Hom.ext').

public theorem injective_infProjPair
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF)
    {w₀ : TwoFibreProductOver (f ⋙ pF) (g ⋙ pF) pF f g}
    (PW : ChosenPushforwardsAt
      (TwoFibreProductOver.structureFunctor (f ⋙ pF) (g ⋙ pF) pF f g) w₀)
    (QH : ChosenPushforwardsAt (f ⋙ pF) w₀.x)
    (QG : ChosenPushforwardsAt (g ⋙ pF) w₀.y) :
    letI := naturalLocalizedTangentAddCommGroup PW
      (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF).satisfiesRS
    letI := naturalLocalizedTangentModule PW
      (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF).satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup QH hH.satisfiesRS
    letI := naturalLocalizedTangentModule QH hH.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup QG hG.satisfiesRS
    letI := naturalLocalizedTangentModule QG hG.satisfiesRS
    Function.Injective (infProjPair.{u, v, w} pF f g hH hG hF PW QH QG)

Deformation.exact_infProjPair_infLegDiff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductInfRow.lean, line 743. The attribute's comment: “part (2), exactness at Inf(ℋ) ⊕ Inf(𝒢) of the six-term exact sequence”.

Stacks Project, Tag 06L5, part (2): exactness at Inf(ℋ) ⊕ Inf(𝒢). In the Inf-row

Inf(𝒲) → Inf(ℋ) ⊕ Inf(𝒢) → Inf(ℱ)

of the six-term sequence of the 2-fibre product 𝒲 = ℋ ×_ℱ 𝒢, the kernel of the difference of the two outer legs is the image of the pair of the two projections.

This is the source's "if (β, γ) map to the same element of Inf_{x₀}(ℱ) then (β, γ) defines an automorphism of w'₀ = (k[ε], y'₀, z'₀, c' ∘ b')". Each of the five maps in sight is conjugation by a comparison of chosen pushforwards (Deformation.inducedInfinitesimalLinearMapOfEq_spec_iso, Deformation.canonicalLocalizedTangentAutomorphismLinearEquiv_spec), and Deformation.pushforwardIso_eq_comparison_comp identifies the composite of those comparisons with the comparison isomorphism carried by the chosen pushforward of w₀. The two halves are then the two readings of one square: the comparison square of a self-arrow of that pushforward gives the vanishing of the composite (Deformation.eq_of_conjugation), and conversely a pair with equal images satisfies that square (Deformation.square_of_conjugation), hence defines a self-arrow, which is automatically infinitesimal because the special fibre of 𝒲 is thin (Deformation.ker_transportAutHom_eq_top_of_isThin).

public theorem exact_infProjPair_infLegDiff
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF)
    {w₀ : TwoFibreProductOver (f ⋙ pF) (g ⋙ pF) pF f g}
    (PW : ChosenPushforwardsAt
      (TwoFibreProductOver.structureFunctor (f ⋙ pF) (g ⋙ pF) pF f g) w₀)
    (QH : ChosenPushforwardsAt (f ⋙ pF) w₀.x)
    (QG : ChosenPushforwardsAt (g ⋙ pF) w₀.y)
    (PF : ChosenPushforwardsAt pF (f.obj w₀.x))
    (PF' : ChosenPushforwardsAt pF (g.obj w₀.y))
    (hw₀ : (f ⋙ pF).obj w₀.x = residueFieldObject.{u, v, w} Λ k) :
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w} PW
      (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF).satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w} PW
      (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF).satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₁, v₁} QH hH.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₁, v₁} QH hH.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₂, v₂} QG hG.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₂, v₂} QG hG.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₃, v₃} PF hF.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₃, v₃} PF hF.satisfiesRS
    Function.Exact (infProjPair.{u, v, w} pF f g hH hG hF PW QH QG)
      (infLegDiff.{u, v, w} pF f g hH hG hF QH QG PF PF' hw₀)

Deformation.exact_boundaryLinearMap_tangentProjPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductSelfExact.lean, line 280. The attribute's comment: “part (2), exactness at T𝒲 of the six-term exact sequence, for the k-linear boundary map Inf(ℱ) → T𝒲 and the map T𝒲 → Tℋ ⊕ T𝒢”.

Stacks Project, Tag 06L5, part (2), for the k-linear boundary map: exactness at T𝒲. The kernel of c : T𝒲 → Tℋ ⊕ T𝒢 is the image of the k-linear boundary map δ : Inf(ℱ) → T𝒲.

That the composite vanishes is Deformation.tangentProjPair_boundaryFun_eq_zero, which holds for every automorphism of x'₀. Conversely an element of the kernel is the class of a quadruple (k[M], y'₀, z'₀, c' ∘ α ∘ b') by Deformation.exists_aut_boundaryObject_tangentClassAt_eq, and that α is in the image of the linear lift because Deformation.ker_transportAutHom_squareZeroUnderRed_eq_top makes the lift's value all of the automorphisms of the pushforward, transport along Deformation.squareZeroCrossUnderIso matching the two normalizations of the square-zero extension.

This is the statement of part (2) at T𝒲: both of its maps are k-linear maps of the vector spaces of Tag 06IH, and it carries neither the splitting of k ⟶ k[M] nor the hypothesis that the basepoint lies over the residue field that the set-level Deformation.exact_boundaryFun_tangentProjPair needs.

public theorem exact_boundaryLinearMap_tangentProjPair
    (pF : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k) (f : H ⥤ F) (g : G ⥤ F)
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF)
    {y₀ : H} {z₀ : G} (hzy : (g ⋙ pF).obj z₀ = (f ⋙ pF).obj y₀)
    {cmp : f.obj y₀ ≅ g.obj z₀}
    (hcmp : pF.IsHomLift (𝟙 ((f ⋙ pF).obj y₀)) cmp.hom)
    (PH : ChosenPushforwardsAt (f ⋙ pF) y₀) (PG : ChosenPushforwardsAt (g ⋙ pF) z₀)
    (PF : ChosenPushforwardsAt pF (f.obj y₀)) (M : FGModuleCat.{max v w} k) :
    Function.Exact (boundaryLinearMap.{u, v, w} pF f g hH hG hF hzy hcmp PH PG PF M)
      (tangentProjPair.{u, v, w} pF f g hH hG hF M)

Deformation.exact_tangentProjPair_tangentLegDiff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductSixTermExact.lean, line 329. The attribute's comment: “part (2), the tangent row T𝒲 → Tℋ ⊕ T𝒢 → Tℱ of the six-term exact sequence and its exactness at Tℋ ⊕ T𝒢”.

In the tangent row T𝒲 → Tℋ ⊕ T𝒢 → Tℱ of the six-term sequence of the 2-fibre product 𝒲 = ℋ ×_ℱ 𝒢, the kernel of the difference of the two outer legs is the image of the pair of the two projections.

public theorem exact_tangentProjPair_tangentLegDiff
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF) (M : FGModuleCat.{max v w} k) :
    Function.Exact (tangentProjPair.{u, v, w} pF f g hH hG hF M)
      (tangentLegDiff.{u, v, w} pF f g hH hG hF M)

Deformation.tangentProjPair_boundaryFun_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductSixTermExact.lean, line 550. The attribute's comment: “part (2), that the boundary map of the six-term exact sequence lands in the kernel of T𝒲 → Tℋ ⊕ T𝒢”.

The boundary map δ : Aut(x'₀) → T𝒲 of the six-term sequence lands in the kernel of the map c : T𝒲 → Tℋ ⊕ T𝒢.

public theorem tangentProjPair_boundaryFun_eq_zero
    (pF : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k) (f : H ⥤ F) (g : G ⥤ F)
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF)
    {y₀ : H} {z₀ : G} (hzy : (g ⋙ pF).obj z₀ = (f ⋙ pF).obj y₀)
    {cmp : f.obj y₀ ≅ g.obj z₀}
    (hcmp : pF.IsHomLift (𝟙 ((f ⋙ pF).obj y₀)) cmp.hom)
    (PH : ChosenPushforwardsAt (f ⋙ pF) y₀) (PG : ChosenPushforwardsAt (g ⋙ pF) z₀)
    (PF : ChosenPushforwardsAt pF (f.obj y₀)) (M : FGModuleCat.{max v w} k)
    (α : Aut (PF.obj (squareZeroCrossUnder.{u, v, w} ((f ⋙ pF).obj y₀) M))) :
    tangentProjPair.{u, v, w} pF f g hH hG hF M
        (boundaryFun.{u, v, w} f g hzy hcmp PH PG PF hF.predeformation.cofibered
          (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF).predeformation
          (tangentConditionS2.{u, v, w}
            (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF)) M α) = 0

Deformation.exact_infLegDiff_infBoundaryLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductSixTermFull/SixTerm.lean, line 94. The attribute's comment: “part (2), exactness at Inf(ℱ) of the six-term exact sequence, for the map Inf(ℋ) ⊕ Inf(𝒢) → Inf(ℱ) and the boundary map Inf(ℱ) → T𝒲”.

Stacks Project, Tag 06L5, part (2): exactness at Inf(ℱ). In the six-term sequence of the 2-fibre product 𝒲 = ℋ ×_ℱ 𝒢, the kernel of the boundary map δ : Inf(ℱ) → T𝒲 is the image of the difference b : Inf(ℋ) ⊕ Inf(𝒢) → Inf(ℱ) of the two outer legs.

This is the source's "if α gives the trivial deformation (k[ε], y'₀, z'₀, c' ∘ α ∘ b') of w₀, then the isomorphism w'₀ → δ(α) produces a pair (β, γ) which is a preimage of α", together with its converse. The class of the quadruple δ(α) vanishes exactly when α satisfies the boundary square for some pair of automorphisms of y'₀ and z'₀ (Deformation.tangentClassAt_boundaryObject_eq_zero_iff), and the boundary square says exactly that α is the value of b on the pair those automorphisms define (Deformation.eq_comp_inv_iff_boundary_square): the two maps b is the difference of are conjugation by the comparisons of Tag 07W6 and Tag 06JV (2) at the dual numbers, and the three transports Deformation.transportAut_comp_boundaryCompareFst, Deformation.map_cross_comp_boundaryCompareSnd and Deformation.transportAut_comp_boundaryCompareSnd carry those conjugations to the re-based square-zero extension at which δ is built.

Every automorphism of a chosen pushforward to the dual numbers is infinitesimal, the special fibre of a predeformation category being thin (Deformation.ker_transportAutHom_eq_top_of_isThin), so the pair of automorphisms the square produces does come from Inf(ℋ) ⊕ Inf(𝒢). The sign the source defers is absorbed by reading the difference as -c(g(γ)) + f(β); the two orders agree because the tangent space is an abelian group.

public theorem exact_infLegDiff_infBoundaryLinearMap
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF)
    {w₀ : TwoFibreProductOver (f ⋙ pF) (g ⋙ pF) pF f g}
    (PW : ChosenPushforwardsAt
      (TwoFibreProductOver.structureFunctor (f ⋙ pF) (g ⋙ pF) pF f g) w₀)
    (QH : ChosenPushforwardsAt (f ⋙ pF) w₀.x)
    (QG : ChosenPushforwardsAt (g ⋙ pF) w₀.y)
    (PF : ChosenPushforwardsAt pF (f.obj w₀.x))
    (PF' : ChosenPushforwardsAt pF (g.obj w₀.y))
    (hw₀ : (f ⋙ pF).obj w₀.x = residueFieldObject.{u, v, w} Λ k) :
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₁, v₁} QH hH.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₁, v₁} QH hH.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₂, v₂} QG hG.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₂, v₂} QG hG.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₃, v₃} PF hF.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₃, v₃} PF hF.satisfiesRS
    Function.Exact (infLegDiff.{u, v, w} pF f g hH hG hF QH QG PF PF' hw₀)
      (infBoundaryLinearMap.{u, v, w} pF f g hH hG hF QH QG PF)

Deformation.twoFibreProduct_sixTermExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductSixTermFull/SixTerm.lean, line 350. The attribute's comment: “part (2), the six-term exact sequence 0 → Inf(𝒲) → Inf(ℋ) ⊕ Inf(𝒢) → Inf(ℱ) → T𝒲 → Tℋ ⊕ T𝒢 → Tℱ of a 2-fibre product of deformation categories, with its five k-linear maps and the exactness at all five of its spots: at Inf(𝒲), at Inf(ℋ) ⊕ Inf(𝒢), at Inf(ℱ), at T𝒲 and at Tℋ ⊕ T𝒢”.

Stacks Project, Tag 06L5, part (2): the six-term sequence

0 → Inf(𝒲) → Inf(ℋ) ⊕ Inf(𝒢) → Inf(ℱ) → T𝒲 → Tℋ ⊕ T𝒢 → Tℱ

of the 2-fibre product 𝒲 = ℋ ×_ℱ 𝒢 of deformation categories, with all five of its k-linear maps and the exactness at every one of its five spots in one statement.

The five conjuncts are, in order: injectivity of a at Inf(𝒲) (the source's 0 →, Deformation.injective_infProjPair), exactness at Inf(ℋ) ⊕ Inf(𝒢) (Deformation.exact_infProjPair_infLegDiff), exactness at Inf(ℱ) (Deformation.exact_infLegDiff_infBoundaryLinearMap), exactness at T𝒲 (Deformation.exact_boundaryLinearMap_tangentProjPair, read through the model bridge of Deformation.infBoundaryLinearMap) and exactness at Tℋ ⊕ T𝒢 (Deformation.exact_tangentProjPair_tangentLegDiff).

The basepoints are the images of one object w₀ of 𝒲, as in the source's "let x₀, y₀, z₀ be the image of w₀", and the tangent terms are taken at the rank-one coordinate module, at which they are the tangent spaces of Tag 06IH.

public theorem twoFibreProduct_sixTermExact
    (hH : IsDeformationCategory.{u, v, w} (f ⋙ pF))
    (hG : IsDeformationCategory.{u, v, w} (g ⋙ pF))
    (hF : IsDeformationCategory.{u, v, w} pF)
    {w₀ : TwoFibreProductOver (f ⋙ pF) (g ⋙ pF) pF f g}
    (PW : ChosenPushforwardsAt
      (TwoFibreProductOver.structureFunctor (f ⋙ pF) (g ⋙ pF) pF f g) w₀)
    (QH : ChosenPushforwardsAt (f ⋙ pF) w₀.x)
    (QG : ChosenPushforwardsAt (g ⋙ pF) w₀.y)
    (PF : ChosenPushforwardsAt pF (f.obj w₀.x))
    (PF' : ChosenPushforwardsAt pF (g.obj w₀.y))
    (hw₀ : (f ⋙ pF).obj w₀.x = residueFieldObject.{u, v, w} Λ k) :
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w} PW
      (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF).satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w} PW
      (isDeformationCategory_productBased.{u, v, w} pF f g hH hG hF).satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₁, v₁} QH hH.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₁, v₁} QH hH.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₂, v₂} QG hG.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₂, v₂} QG hG.satisfiesRS
    letI := naturalLocalizedTangentAddCommGroup.{u, v, w, u₃, v₃} PF hF.satisfiesRS
    letI := naturalLocalizedTangentModule.{u, v, w, u₃, v₃} PF hF.satisfiesRS
    Function.Injective (infProjPair.{u, v, w} pF f g hH hG hF PW QH QG) ∧
      Function.Exact (infProjPair.{u, v, w} pF f g hH hG hF PW QH QG)
          (infLegDiff.{u, v, w} pF f g hH hG hF QH QG PF PF' hw₀) ∧
        Function.Exact (infLegDiff.{u, v, w} pF f g hH hG hF QH QG PF PF' hw₀)
            (infBoundaryLinearMap.{u, v, w} pF f g hH hG hF QH QG PF) ∧
          Function.Exact (infBoundaryLinearMap.{u, v, w} pF f g hH hG hF QH QG PF)
              (tangentProjPair.{u, v, w} pF f g hH hG hF (FGModuleCat.of k (ULift.{v} k))) ∧
            Function.Exact
              (tangentProjPair.{u, v, w} pF f g hH hG hF (FGModuleCat.of k (ULift.{v} k)))
              (tangentLegDiff.{u, v, w} pF f g hH hG hF (FGModuleCat.of k (ULift.{v} k)))
Tag 0DYN, a lemma

Tag 0DYN in the Stacks Project.

Deformation.mapTwoFibreProductBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductBaseChangeSmooth.lean, line 191. The attribute's comment: “the canonical functor between the two 2-fibre products”.

The canonical functor over 𝒞_Λ from the 2-fibre product of ℋ₁ and ℋ₂ over 𝒢 to their 2-fibre product over ℱ, for a morphism q : 𝒢 → ℱ: it keeps both components and applies q to the comparison isomorphism.

public def mapTwoFibreProductBaseChange
    (p₁ : BasedFunctor 𝓗₁ 𝓖) (p₂ : BasedFunctor 𝓗₂ 𝓖) (q : BasedFunctor 𝓖 𝓕) :
    BasedFunctor (twoFibreProductBasedCategory p₁ p₂)
      (twoFibreProductBasedCategory (BasedFunctor.comp p₁ q) (BasedFunctor.comp p₂ q))

Deformation.isSmooth_mapTwoFibreProductBaseChange', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductBaseChangeSmooth.lean, line 538. The attribute's comment: “smoothness”.

Let p₁ : ℋ₁ → 𝒢, p₂ : ℋ₂ → 𝒢 and q : 𝒢 → ℱ be morphisms of categories cofibered in groupoids over 𝒞_Λ. Assume that ℱ and 𝒢 are deformation categories, that T𝒢 → Tℱ is injective, and that Inf(𝒢) → Inf(ℱ) is surjective. Then ℋ₁ ×_𝒢 ℋ₂ → ℋ₁ ×_ℱ ℋ₂ is smooth.

public theorem isSmooth_mapTwoFibreProductBaseChange'
    (p₁ : BasedFunctor 𝓗₁ 𝓖) (p₂ : BasedFunctor 𝓗₂ 𝓖) (q : BasedFunctor 𝓖 𝓕)
    (h𝓗₁ : IsCofiberedInGroupoids 𝓗₁.p) (h𝓗₂ : IsCofiberedInGroupoids 𝓗₂.p)
    (h𝓖 : IsDeformationCategory 𝓖.p) (h𝓕 : IsDeformationCategory 𝓕.p)
    (htangent : Function.Injective
      (differential h𝓖.predeformation.cofibered h𝓕.predeformation.cofibered q))
    {z₀ : 𝓖.p.Fiber (residueFieldObject.{u, w, w} Λ k)}
    (PG : ChosenPushforwardsAt 𝓖.p z₀.1) (PF : ChosenPushforwardsAt 𝓕.p (q.obj z₀.1))
    (hinf :
      letI := naturalLocalizedTangentAddCommGroup PG h𝓖.satisfiesRS
      letI := naturalLocalizedTangentModule PG h𝓖.satisfiesRS
      letI := naturalLocalizedTangentAddCommGroup PF h𝓕.satisfiesRS
      letI := naturalLocalizedTangentModule PF h𝓕.satisfiesRS
      Function.Surjective (inducedInfinitesimalLinearMapOfEq q.toFunctor q.w
        h𝓖.satisfiesRS h𝓕.satisfiesRS PG PF)) :
    IsSmooth (mapTwoFibreProductBaseChange p₁ p₂ q)
Tag 0DYP, a lemma

Tag 0DYP in the Stacks Project.

Deformation.isSmooth_iff_differential_surjective_and_lifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Smoothness/Criterion.lean, line 115.

Surjectivity of the differential and preservation of the existence of lifts across small extensions characterize smoothness.

public theorem isSmooth_iff_differential_surjective_and_lifts
    (h𝓕 : IsDeformationCategory 𝓕.p)
    (h𝓖 : IsDeformationCategory 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖) :
    IsSmooth φ ↔
      (Function.Surjective
        (differential h𝓕.predeformation.cofibered
          h𝓖.predeformation.cofibered φ) ∧
       ∀ ⦃B A : ArtinianLocalAlgCat.{u, w, w} Λ k⦄
         (f : B ⟶ A),
         InfinitesimalLifting.IsSmallExtension
           (CommRingCat.ofHom f.hom.toRingHom) →
         ∀ (x : 𝓕.p.Fiber A),
           (∃ (y' : 𝓖.obj) (g : y' ⟶ φ.obj x.1),
             𝓖.p.IsHomLift f g) →
           (∃ (x' : 𝓕.obj) (h : x' ⟶ x.1),
             𝓕.p.IsHomLift f h))
Tag 0E3R, a lemma

Tag 0E3R in the Stacks Project.

Deformation.isSmooth_of_differential_surjective_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/LiftsOfObjects/Smoothness/Composite.lean, line 45.

Stacks Project, Tag 0E3R. A morphism of deformation categories is smooth if its differential is surjective and its composite with another morphism is smooth.

public theorem isSmooth_of_differential_surjective_of_comp
    {𝓕 : BasedCategory.{v₁, u₁} (ArtinianLocalAlgCat.{u, w, w} Λ k)}
    {𝓖 : BasedCategory.{v₂, u₂} (ArtinianLocalAlgCat.{u, w, w} Λ k)}
    {𝓗 : BasedCategory.{v₃, u₃} (ArtinianLocalAlgCat.{u, w, w} Λ k)}
    (h𝓕 : IsDeformationCategory 𝓕.p)
    (h𝓖 : IsDeformationCategory 𝓖.p)
    (φ : BasedFunctor 𝓕 𝓖) (ψ : BasedFunctor 𝓖 𝓗)
    (hd : Function.Surjective
      (differential h𝓕.predeformation.cofibered
        h𝓖.predeformation.cofibered φ))
    (hsmooth : IsSmooth (BasedFunctor.comp φ ψ)) :
    IsSmooth φ
Sources
LeanDeformation.boundaryLinearMap · Deformation.isDeformationCategory_twoFibreProductOver · Deformation.injective_infProjPair · Deformation.exact_infProjPair_infLegDiff · Deformation.exact_boundaryLinearMap_tangentProjPair · Deformation.exact_tangentProjPair_tangentLegDiff · Deformation.tangentProjPair_boundaryFun_eq_zero · Deformation.exact_infLegDiff_infBoundaryLinearMap

Section90.21 Groupoids in functors on an arbitrary category#

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

Tag 06K3, a definition

Tag 06K3 in the Stacks Project.

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

A groupoid in functors on C: functors of objects and arrows with natural source, target, and composition maps which give a groupoid after evaluation at every object of C.

structure GroupoidInFunctors (C : Type u) [Category.{v} C]

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

A morphism of groupoids in functors.

structure Hom {C : Type u} [Category.{v} C]
    (G H : GroupoidInFunctors C)
Tag 06K4, a remark

Tag 06K4 in the Stacks Project.

Deformation.GroupoidInFunctors.evaluationEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/EvaluationEquivalence.lean, line 557.

A groupoid in functors on C is the same data as a functor C ⥤ Grpd, and a morphism of groupoids in functors is the same data as a morphism of the associated functors: evaluation is an equivalence of categories.

noncomputable def evaluationEquivalence :
    GroupoidInFunctors.{u, v, w} C ≌ (C ⥤ Grpd.{w, w})
Tag 06K5, a remark

Tag 06K5 in the Stacks Project.

Deformation.existsUnique_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Basic.lean, line 540. The attribute's comment: “identity”.

Pointwise identities uniquely assemble into a natural transformation from objects to arrows.

public theorem existsUnique_identity {C : Type u} [Category.{v} C]
    (G : GroupoidInFunctors.{u, v, w} C) :
    ∃! e : G.objects ⟶ G.arrows,
      ∀ (T : C) (x : G.Evaluation T), e.app T x = G.identity T x

Deformation.existsUnique_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Basic.lean, line 558. The attribute's comment: “inverse”.

Pointwise inverses uniquely assemble into a natural transformation of the arrow functor.

public theorem existsUnique_inverse {C : Type u} [Category.{v} C]
    (G : GroupoidInFunctors.{u, v, w} C) :
    ∃! i : G.arrows ⟶ G.arrows,
      ∀ (T : C) (a : G.arrows.obj T), i.app T a = inverseArrow G T a
Tag 06K6, a definition

Tag 06K6 in the Stacks Project.

Deformation.IsRepresentable, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Basic.lean, line 622.

A groupoid in functors is representable if it is isomorphic to one presented by covariant representable functors of objects and arrows, and the pushout of the two morphisms representing source and target exists.

public def IsRepresentable {C : Type u} [Category.{v} C] (G : GroupoidInFunctors.{u,
  v, max w v} C) : Prop
Tag 06K9, a definition

Tag 06K9 in the Stacks Project.

Deformation.GroupoidInFunctors.restrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/BaseCategory.lean, line 74.

Restriction of a groupoid in functors along a functor of source categories. The restriction (U, R, s, t, c)|_{C'} of a groupoid in functors to a subcategory C' ⊆ C is the case where the functor is the inclusion of C'.

public def restrict {C : Type u} {D : Type v} [Category.{w} C] [Category.{x} D]
    (G : GroupoidInFunctors.{v, x, y} D) (F : C ⥤ D) :
    GroupoidInFunctors.{u, w, y} C
Tag 06KA, a remark

Tag 06KA in the Stacks Project.

Deformation.GroupoidInFunctors.restrict_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Restriction.lean, line 57. The attribute's comment: “source”.

The source of a restriction is the source of the original groupoid in functors, whiskered by the restricting functor.

public theorem restrict_source : (G.restrict F).source = F.whiskerLeft G.source

Deformation.GroupoidInFunctors.restrict_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Restriction.lean, line 62. The attribute's comment: “target”.

The target of a restriction is the target of the original groupoid in functors, whiskered by the restricting functor.

public theorem restrict_target : (G.restrict F).target = F.whiskerLeft G.target

Deformation.GroupoidInFunctors.restrict_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Restriction.lean, line 67. The attribute's comment: “composition”.

The composition of a restriction is the composition of the original groupoid in functors, whiskered by the restricting functor.

public theorem restrict_comp : (G.restrict F).comp = F.whiskerLeft G.comp
Tag 06KB, a definition

Tag 06KB in the Stacks Project.

Deformation.evaluationFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Basic.lean, line 712. The attribute's comment: “evaluation functor”.

The covariant functor of groupoids obtained by evaluating a groupoid in functors at each object of the base category.

public noncomputable def evaluationFunctor {C : Type u} [Category.{v} C]
    (G : GroupoidInFunctors.{u, v, w} C) : C ⥤ Cat.{w, w}

Deformation.quotientMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Basic.lean, line 781. The attribute's comment: “quotient morphism”.

The canonical quotient map from the category of elements of the object functor to the Grothendieck construction of the evaluated groupoids.

public noncomputable def quotientMorphism {C : Type u} [Category.{v} C]
    (G : GroupoidInFunctors.{u, v, w} C) :
    G.objects.Elements ⥤ Grothendieck (evaluationFunctor G)

Deformation.quotientProjection_cofibered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Basic.lean, line 987. The attribute's comment: “cofibered property”. References: SGA 7 VI (1.1(a)), “groupoid in functors”.

The projection of the Grothendieck construction of a groupoid in functors is cofibered in groupoids.

public theorem quotientProjection_cofibered {C : Type u} [Category.{v} C]
    (G : GroupoidInFunctors.{u, v, w} C) :
    IsCofiberedInGroupoids
      (Grothendieck.forget (evaluationFunctor G))

Declarations registered for the tag:

Sources
LeanDeformation.GroupoidInFunctors · Deformation.GroupoidInFunctors.Hom · Deformation.GroupoidInFunctors.evaluationEquivalence · Deformation.existsUnique_identity · Deformation.existsUnique_inverse · Deformation.IsRepresentable · Deformation.GroupoidInFunctors.restrict · Deformation.GroupoidInFunctors.restrict_source

Section90.22 Groupoids in functors on the base category#

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

Tag 06KD, a definition

Tag 06KD in the Stacks Project.

Deformation.GroupoidInFunctors.IsProrepresentable, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/BaseCategory.lean, line 102. References: SGA 7 VI (2.13), “prorepresentable”.

A groupoid in functors on Artinian local Λ-algebras is prorepresentable if it is isomorphic to the restriction of a representable groupoid in functors on Noetherian complete local Λ-algebras.

public abbrev GroupoidInFunctors.IsProrepresentable {Λ : Type u} {k : Type w} [CommRing Λ]
    [Field k] [Algebra Λ k]
    (G : GroupoidInFunctors.{_, v, max v z}
      (ArtinianLocalAlgCat.{u, v, w} Λ k)) : Prop
Tag 06KE, a definition

Tag 06KE in the Stacks Project.

Deformation.GroupoidInFunctors.completion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/Completion.lean, line 887.

Completion of a groupoid in functors on Artinian local algebras.

public noncomputable def completion {Λ : Type u} {k : Type w} [CommRing Λ]
    [Field k] [Algebra Λ k]
    (G : GroupoidInFunctors.{_, v, max v z}
      (ArtinianLocalAlgCat.{u, v, w} Λ k)) :
    GroupoidInFunctors.{_, v, max v z}
      (CompleteLocalAlgCat.{u, v, w} Λ k)
Tag 06KF, a remark

Tag 06KF in the Stacks Project.

Deformation.GroupoidInFunctors.completionRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/CompletionRestrict.lean, line 43. The attribute's comment: “completion_restrict”.

The canonical isomorphism from a completed groupoid, restricted back to Artinian local algebras, to the original groupoid. Its two components are the completion--restriction counits.

public noncomputable def completionRestrictIso
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (G : GroupoidInFunctors.{_, v, max v z}
      (ArtinianLocalAlgCat.{u, v, w} Λ k)) :
    { e : GroupoidInFunctors.restrict
          (GroupoidInFunctors.completion G)
          (artinianToComplete (Λ := Λ) (k := k)) ≅ G //
      e.hom.mapObjects =
        (cofiberedCompletionAdjunction
          (Λ := Λ) (k := k)).counit.app G.objects ∧
      e.hom.mapArrows =
        (cofiberedCompletionAdjunction
          (Λ := Λ) (k := k)).counit.app G.arrows }

Deformation.GroupoidInFunctors.completionRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/RestrictCompletion.lean, line 158. The attribute's comment: “restrict_completion”.

The canonical groupoid isomorphism from the completion of a restricted limit-preserving groupoid to the original groupoid.

public noncomputable def completionRestrictionIso
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (G : GroupoidInFunctors.{_, v, max v z}
      (CompleteLocalAlgCat.{u, v, w} Λ k))
    [PreservesLimits G.objects] [PreservesLimits G.arrows] :
    { i : GroupoidInFunctors.completion
        (GroupoidInFunctors.restrict G
          (artinianToComplete (Λ := Λ) (k := k))) ≅ G //
      i.inv.mapObjects =
        (cofiberedCompletionAdjunction (Λ := Λ) (k := k)).unit.app
          G.objects ∧
      i.inv.mapArrows =
        (cofiberedCompletionAdjunction (Λ := Λ) (k := k)).unit.app
          G.arrows }
Tag 06KG, a lemma

Tag 06KG in the Stacks Project.

Deformation.GroupoidInFunctors.isProrepresentable_iff_isRepresentable_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/Prorepresentable.lean, line 461. The attribute's comment: “part (1)”.

A groupoid in functors on Artinian local algebras is prorepresentable if and only if its completion is representable on complete local algebras.

public theorem isProrepresentable_iff_isRepresentable_completion
    (G : GroupoidInFunctors.{_, v, max v z}
      (ArtinianLocalAlgCat.{u, v, w} Λ k)) :
    GroupoidInFunctors.IsProrepresentable G ↔
      IsRepresentable (GroupoidInFunctors.completion G)

Deformation.GroupoidInFunctors.isProrepresentable_iff_objects_arrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Formal/Groupoid/Prorepresentable.lean, line 500. The attribute's comment: “part (2)”.

A groupoid in functors is prorepresentable if and only if both its object and arrow functors are prorepresentable.

public theorem isProrepresentable_iff_objects_arrows
    (G : GroupoidInFunctors.{_, v, v}
      (ArtinianLocalAlgCat.{u, v, w} Λ k)) :
    GroupoidInFunctors.IsProrepresentable G ↔
      (_root_.Deformation.IsProrepresentable G.objects ∧
        _root_.Deformation.IsProrepresentable G.arrows)
Sources
LeanDeformation.GroupoidInFunctors.IsProrepresentable · Deformation.GroupoidInFunctors.completion · Deformation.GroupoidInFunctors.completionRestrictIso · Deformation.GroupoidInFunctors.completionRestrictionIso · Deformation.GroupoidInFunctors.isProrepresentable_iff_isRepresentable_completion · Deformation.GroupoidInFunctors.isProrepresentable_iff_objects_arrows

Section90.23 Smooth groupoids in functors on the base category#

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

Tag 06KI, a definition

Tag 06KI in the Stacks Project.

Deformation.GroupoidInFunctors.IsSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Smooth.lean, line 55.

A groupoid in functors is smooth when both its source and target morphisms are smooth.

public abbrev GroupoidInFunctors.IsSmooth (G : GroupoidInFunctors
  (ArtinianLocalAlgCat.{u, v, w} Λ k)) : Prop
Tag 06KJ, a remark

Tag 06KJ in the Stacks Project.

Deformation.smooth_groupoid_quotient_not_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/SmoothWarning.lean, line 247. The attribute's comment: “smooth groupoid with nonsmooth quotient category”.

A smooth groupoid in functors can have a quotient category that is not smooth over the base.

public theorem smooth_groupoid_quotient_not_smooth :
    ∃ G : GroupoidInFunctors (ArtinianLocalAlgCat.{0, 0, 0} ℚ ℚ),
      GroupoidInFunctors.IsSmooth G ∧
        ¬ IsSmooth (quotientProjectionBasedFunctor G)

Declarations registered for the tag:

Tag 06KL, a lemma

Tag 06KL in the Stacks Project.

Deformation.isSmooth_iff_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Smooth.lean, line 411. The attribute's comment: “smooth groupoid iff smooth source”.

A groupoid in functors is smooth exactly when its source morphism is smooth.

public theorem isSmooth_iff_source
    (G : GroupoidInFunctors (ArtinianLocalAlgCat.{u, v, w} Λ k)) :
      GroupoidInFunctors.IsSmooth G ↔
      Deformation.IsSmooth (elementsBasedFunctor G.source)

Deformation.source_isSmooth_iff_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Smooth.lean, line 419. The attribute's comment: “smooth source iff smooth target”.

Smoothness of the source and target morphisms of a groupoid in functors are equivalent.

public theorem source_isSmooth_iff_target
    (G : GroupoidInFunctors (ArtinianLocalAlgCat.{u, v, w} Λ k)) :
    Deformation.IsSmooth (elementsBasedFunctor G.source) ↔
      Deformation.IsSmooth (elementsBasedFunctor G.target)

Deformation.source_isSmooth_iff_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Groupoid/Smooth.lean, line 427. The attribute's comment: “smooth source iff smooth quotient morphism”.

The source morphism is smooth exactly when the quotient morphism is smooth.

public theorem source_isSmooth_iff_quotient
    (G : GroupoidInFunctors (ArtinianLocalAlgCat.{u, v, w} Λ k)) :
    Deformation.IsSmooth (elementsBasedFunctor G.source) ↔
      Deformation.IsSmooth (quotientBasedFunctor G)
Sources
LeanDeformation.GroupoidInFunctors.IsSmooth · Deformation.smooth_groupoid_quotient_not_smooth · isSmooth_iff_source · source_isSmooth_iff_quotient · Deformation.isSmooth_iff_source · Deformation.source_isSmooth_iff_target · Deformation.source_isSmooth_iff_quotient

Section90.24 Deformation categories as quotients of groupoids in functors#

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

Tag 06KT, a lemma

Tag 06KT in the Stacks Project.

Deformation.quotient_satisfiesRS, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/RimSchlessinger.lean, line 150.

The quotient of a smooth groupoid in functors whose object and arrow functors satisfy condition (RS) also satisfies condition (RS).

public theorem quotient_satisfiesRS
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (G : GroupoidInFunctors (ArtinianLocalAlgCat.{u, v, w} Λ k))
    (hG : GroupoidInFunctors.IsSmooth G)
    (hU : SatisfiesRS (Functor.Elements.π G.objects))
    (hR : SatisfiesRS (Functor.Elements.π G.arrows)) :
    SatisfiesRS (Grothendieck.forget (evaluationFunctor G))
Tag 06KU, a lemma

Tag 06KU in the Stacks Project.

Deformation.quotient_isDeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/DeformationCategory.lean, line 123. The attribute's comment: “quotient_deformation_category”.

The quotient of a smooth groupoid of deformation functors is a deformation category.

public theorem quotient_isDeformationCategory
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (G : GroupoidInFunctors.{_, _, t} (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hG : GroupoidInFunctors.IsSmooth G)
    (hU : IsDeformationFunctor G.objects)
    (hR : IsDeformationFunctor G.arrows) :
    IsDeformationCategory (Grothendieck.forget (evaluationFunctor G))

Deformation.quotientInfinitesimalBoundary_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/InfinitesimalAutomorphisms.lean, line 807. The attribute's comment: “part (3): Inf([U/R]) = Ker(ds ⊕ dt : TR → TU ⊕ TU), as the exactness of 0 → Inf([U/R]) → TR → TU ⊕ TU. The two differentials are the maps on tangent modules induced by s and t at an arbitrary coordinate module M, and Inf([U/R]) is the value at M of the k-linear lift of the infinitesimal automorphisms of the image in [U/R] of a point y₀ of U, taken with an arbitrary choice PF of pushforwards there. No hypothesis is carried beyond the tag's own: G smooth, U and R deformation functors”.

Stacks Project, Tag 06KU, part (3). Let (U, R, s, t, c) be a smooth groupoid in functors on 𝒞_Λ whose functors of objects and of arrows are deformation functors. Then the space of infinitesimal automorphisms of the quotient is the kernel of the differential of the source-and-target map,

Inf([U/R]) = Ker(ds ⊕ dt : TR → TU ⊕ TU),

in the form of the exact sequence of k-vector spaces

0 → Inf([U/R]) → TR → TU ⊕ TU:

the boundary map is injective and its image is the kernel of the pair of the two differentials.

The identification is the one of Tag 06L6 part (2) for the quotient morphism q : U → [U/R], whose self 2-fibre product U ×_{q, [U/R], q} U is the arrow functor: an arrow of the groupoid over A with source x and target y is an isomorphism over A between the images of x and of y in the quotient, and that comparison is an equivalence on every strict fibre, hence an isomorphism of tangent modules.

public theorem quotientInfinitesimalBoundary_exact
    (hG : GroupoidInFunctors.IsSmooth G)
    (hU : IsDeformationFunctor.{u, v, w} G.objects)
    (hR : IsDeformationFunctor.{u, v, w} G.arrows) {y₀ : G.objects.Elements}
    (PF : ChosenPushforwardsAt (Grothendieck.forget (evaluationFunctor G))
      ((quotientMorphism G).obj y₀))
    (M : FGModuleCat.{max v w} k) :
    Function.Injective (quotientInfinitesimalBoundary.{u, v, w, t} G hG hU hR PF M) ∧
      Function.Exact (quotientInfinitesimalBoundary.{u, v, w, t} G hG hU hR PF M)
        (LinearMap.prod
          (tangentMapAt.{u, v, w} (arrowsBasedDeformationCategory G hR)
            (objectsBasedDeformationCategory G hU) (elementsBasedFunctor G.source) M)
          (tangentMapAt.{u, v, w} (arrowsBasedDeformationCategory G hR)
            (objectsBasedDeformationCategory G hU)
            (elementsBasedFunctor G.target) M))

Deformation.quotientTangentEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/TangentSpace.lean, line 144. The attribute's comment: “quotient_tangent_space”.

The canonical tangent space of a smooth quotient is the cokernel of the source-minus-target differential.

public noncomputable def quotientTangentEquiv
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (G : GroupoidInFunctors (ArtinianLocalAlgCat.{u, w, w} Λ k))
    (hG : GroupoidInFunctors.IsSmooth G)
    (hU : IsDeformationFunctor G.objects)
    (hR : IsDeformationFunctor G.arrows) :
    let 𝓡 := BasedCategory.ofFunctor (Functor.Elements.π G.arrows)
    let 𝓤 := BasedCategory.ofFunctor (Functor.Elements.π G.objects)
    let 𝓠 := BasedCategory.ofFunctor (Grothendieck.forget (evaluationFunctor G))
    let h𝓡 := ((isDeformationCategory_iff G.arrows).2 hR).predeformation
    let h𝓤 := ((isDeformationCategory_iff G.objects).2 hU).predeformation
    let h𝓠 := quotient_isPredeformationCategory G hU hR
    let s2𝓡 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓡 h𝓡.cofibered (schlessingerConditionS2_of_satisfiesRS hR.2) (Or.inl h𝓡)
    let s2𝓤 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓤 h𝓤.cofibered (schlessingerConditionS2_of_satisfiesRS hU.2) (Or.inl h𝓤)
    let s2𝓠 := schlessingerConditionS2_of_isIsomorphismClasses
      𝓠 h𝓠.cofibered
      (schlessingerConditionS2_of_satisfiesRS (quotient_satisfiesRS G hG hU.2 hR.2))
      (Or.inl h𝓠)
    letI : Fact (IsPredeformationCategory 𝓡.p) := ⟨h𝓡⟩
    letI : Fact (IsPredeformationCategory 𝓤.p) := ⟨h𝓤⟩
    letI : Fact (IsPredeformationCategory 𝓠.p) := ⟨h𝓠⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓡 h𝓡.cofibered))) := ⟨s2𝓡⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓤 h𝓤.cofibered))) := ⟨s2𝓤⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓠 h𝓠.cofibered))) := ⟨s2𝓠⟩
    let TR := artinianTangentSpace Λ k (isomorphismClasses 𝓡 h𝓡.cofibered)
    let TU := artinianTangentSpace Λ k (isomorphismClasses 𝓤 h𝓤.cofibered)
    let TQ := artinianTangentSpace Λ k (isomorphismClasses 𝓠 h𝓠.cofibered)
    let ds : TR →ₗ[k] TU := IsLinearMap.mk'
      (differential h𝓡.cofibered h𝓤.cofibered (elementsBasedFunctor G.source))
      (differential_isLinearMap 𝓡 𝓤 h𝓡 h𝓤 s2𝓡 s2𝓤 (elementsBasedFunctor G.source))
    let dt : TR →ₗ[k] TU := IsLinearMap.mk'
      (differential h𝓡.cofibered h𝓤.cofibered (elementsBasedFunctor G.target))
      (differential_isLinearMap 𝓡 𝓤 h𝓡 h𝓤 s2𝓡 s2𝓤 (elementsBasedFunctor G.target))
    let dq : TU →ₗ[k] TQ := IsLinearMap.mk'
      (differential h𝓤.cofibered h𝓠.cofibered
        (⟨quotientMorphism G, quotientMorphism_over G⟩ : BasedFunctor 𝓤 𝓠))
      (differential_isLinearMap 𝓤 𝓠 h𝓤 h𝓠 s2𝓤 s2𝓠
        (⟨quotientMorphism G, quotientMorphism_over G⟩ : BasedFunctor 𝓤 𝓠))
    { e : (TU ⧸ LinearMap.range (ds - dt)) ≃ₗ[k] TQ //
      ∀ x : TU, e (Submodule.Quotient.mk x) = dq x }
Sources
LeanDeformation.quotient_satisfiesRS · Deformation.quotient_isDeformationCategory · Deformation.quotientInfinitesimalBoundary_exact · Deformation.quotientTangentEquiv

Section90.25 Presentations of categories cofibered in groupoids#

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

Tag 06KX, a definition

Tag 06KX in the Stacks Project.

Deformation.Presentation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Presentation.lean, line 44.

An equivalence over C from the quotient of G to a category over C. When the latter is cofibered in groupoids, this is a presentation in the sense of Stacks Project, Tag 06KX.

public abbrev Presentation {C : Type u} [Category.{v} C] (G : GroupoidInFunctors.{u, v, w} C)
    {F : Type u₁} [Category.{v₁} F] (p : F ⥤ C)
Tag 06KY, a lemma

Tag 06KY in the Stacks Project.

Deformation.presentationGroupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Groupoid.lean, line 1108.

A morphism from a set-valued functor to a category cofibered in groupoids canonically produces a groupoid in functors, whose arrows are the two-fibre product with source, target, and composition given by the second, first, and first-and-last projections respectively.

noncomputable def presentationGroupoid
    (hp : IsCofiberedInGroupoids p) : PresentationGroupoid p U f over
Tag 06KZ, a lemma

Tag 06KZ in the Stacks Project.

Deformation.presentationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Morphism.lean, line 593. The attribute's comment: “natural morphism”.

The canonical morphism from the quotient of a presentation to the category being presented, together with its compatibility with the projection and the original presentation functor.

noncomputable def presentationMorphism :
    {g : Grothendieck (evaluationFunctor P.toGroupoidInFunctors) ⥤ F //
      (g ⋙ p = Grothendieck.forget
        (evaluationFunctor P.toGroupoidInFunctors)) ∧
      ((uliftElementsEquivalence U).functor ⋙
        quotientMorphism P.toGroupoidInFunctors ⋙ g = f)}

Deformation.presentationMorphism_full, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Morphism.lean, line 609. The attribute's comment: “full”.

The morphism from a presentation quotient is full.

theorem presentationMorphism_full
    (hp : IsCofiberedInGroupoids p) :
    (presentationMorphism p U f over P).1.Full

Deformation.presentationMorphism_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Morphism.lean, line 616. The attribute's comment: “faithful”.

The morphism from a presentation quotient is faithful.

theorem presentationMorphism_faithful :
    (presentationMorphism p U f over P).1.Faithful

Deformation.presentationMorphism_isEquivalence_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Morphism.lean, line 623. The attribute's comment: “equivalence criterion”.

The quotient morphism is an equivalence exactly when the original presentation functor is essentially surjective.

theorem presentationMorphism_isEquivalence_iff
    (hp : IsCofiberedInGroupoids p) :
    (presentationMorphism p U f over P).1.IsEquivalence ↔ f.EssSurj
Sources
LeanDeformation.Presentation · Deformation.presentationGroupoid · Deformation.presentationMorphism · Deformation.presentationMorphism_full · Deformation.presentationMorphism_faithful · Deformation.presentationMorphism_isEquivalence_iff

Section90.26 Presentations of deformation categories#

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

Tag 06L1, a lemma

Tag 06L1 in the Stacks Project.

Deformation.presentationMorphism_isEquivalence_of_isSmooth_of_fiber_essSurj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/QuotientEquivalence.lean, line 44. The attribute's comment: “quotient_equivalence”.

The canonical quotient morphism associated to a smooth presentation is an equivalence if the presentation is essentially surjective over the residue field.

theorem presentationMorphism_isEquivalence_of_isSmooth_of_fiber_essSurj
    (hp : IsCofiberedInGroupoids p)
    (hf : IsSmooth f)
    (h₀ : (fiberFunctor f (residueFieldObject Λ k)).EssSurj) :
    (presentationMorphism p U f.toFunctor f.w
      (presentationGroupoid p U f.toFunctor f.w hp)).1.IsEquivalence

Deformation.isSmooth_presentationGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Smooth.lean, line 546. The attribute's comment: “smooth_groupoid”.

A smooth presentation has a smooth associated groupoid in functors.

This is one of the two covering declarations of Stacks 06L1; the other is the equivalence criterion for the quotient morphism, Deformation.presentationMorphism_isEquivalence_of_isSmooth_of_fiber_essSurj. See the implementation notes.

theorem isSmooth_presentationGroupoid
    (hp : IsCofiberedInGroupoids p)
    (hf : IsSmooth f) :
    GroupoidInFunctors.IsSmooth
      ((presentationGroupoid p U f.toFunctor f.w hp).toGroupoidInFunctors)
Tag 06L6, a lemma

Tag 06L6 in the Stacks Project.

Deformation.isDeformationFunctor_twoFibreProductOver_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductDeformation.lean, line 373. The attribute's comment: “part (1), that the 2-fibre product is a deformation functor; the exact sequence 0 → Inf(ℱ) → T(U ×_{f,ℱ,f} U) → TU ⊕ TU of part (2) is not covered”.

Stacks Project, Tag 06L6, part (1). Let U : 𝒞_Λ → Sets be a deformation functor, ℱ a deformation category and f : U → ℱ a 1-morphism of categories cofibered in groupoids over 𝒞_Λ. Then 𝒲 = U ×_{f, ℱ, f} U is a deformation functor: it is a deformation category, and every one of its infinitesimal automorphism groups vanishes, which by Tag 06K0 is exactly the statement that it is cofibered in setoids, i.e. that it is a functor.

The deformation-category half is Tag 06L5 part (1), Deformation.isDeformationCategory_twoFibreProductOver, read through Deformation.isDeformationCategory_iff for the two outer legs. The vanishing is the source's "the fact that Inf(U) = (0)": the fibres of the category of elements of a set-valued functor are thin (Deformation.elementsFiber_isThin), hence so are the fibres of the 2-fibre product (Deformation.isThin_fibre_twoFibreProductOver), and over a thin fibre there is no room for a nontrivial automorphism at all.

The cofibered-in-groupoids witness is quantified over rather than taken from the first component because Deformation.IsCofiberedInGroupoids is a proposition, so the infinitesimal automorphism group does not depend on which witness is supplied.

theorem isDeformationFunctor_twoFibreProductOver_self
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    (U : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t)
    {F : Type u₃} [Category.{v₃} F]
    (pF : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (f : U.Elements ⥤ F)
    (hf : f ⋙ pF = CategoryOfElements.π U)
    (hU : IsDeformationFunctor U)
    (hF : IsDeformationCategory pF) :
    let p𝒲 := TwoFibreProductOver.structureFunctor
      (CategoryOfElements.π U) (CategoryOfElements.π U) pF f f
    IsDeformationCategory p𝒲 ∧
      ∀ (hcof : IsCofiberedInGroupoids p𝒲)
        {A₀ Aε : ArtinianLocalAlgCat.{u, max v w, w} Λ k}
        {w₀ : p𝒲.Fiber A₀} {wε : p𝒲.Fiber Aε}
        (g : A₀ ⟶ Aε) (e : Aε ⟶ A₀) (hpair : IsCanonicalDualNumberPair g e)
        (i : w₀.1 ⟶ wε.1) (hi : p𝒲.IsHomLift g i),
        infinitesimalAutomorphisms hcof g e hpair i hi = ⊥

Deformation.exact_selfBoundaryLinearMap_tangentProjPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Applications/TwoFibreProductSelfExact.lean, line 384. The attribute's comment: “part (2), the exact sequence of k-vector spaces 0 → Inf(ℱ) → T(U ×_{f,ℱ,f} U) → TU ⊕ TU”.

Stacks Project, Tag 06L6, part (2). Let U : 𝒞_Λ → Sets be a deformation functor, ℱ a deformation category and f : U → ℱ a 1-morphism of categories cofibered in groupoids over 𝒞_Λ. Then the tangent space of 𝒲 = U ×_{f, ℱ, f} U fits into an exact sequence of k-vector spaces

0 → Inf(ℱ) → T𝒲 → TU ⊕ TU,

where the first map is the k-linear boundary map δ of the six-term sequence and the second is the pair of the maps induced by the two projections. Exactness at Inf(ℱ) is injectivity of δ and exactness at T𝒲 is the kernel-equals-image statement; both maps are k-linear, and the three terms are the k-vector spaces of Tag 06IH, taken at an arbitrary coordinate module.

Exactness at T𝒲 is part (2) of Tag 06L5 for the two legs (Deformation.exact_boundaryLinearMap_tangentProjPair). Exactness at Inf(ℱ) is what the self 2-fibre product adds, and it is the source's Inf(U) = (0): the fibres of the category of elements of a set-valued functor are thin (Deformation.isThin_fiber_comp_elementsProjection), so an isomorphism between two quadruples (k[M], y'₀, y'₀, c' ∘ α ∘ b') has both components the identity and its comparison square reads α = α'.

public theorem exact_selfBoundaryLinearMap_tangentProjPair
    (U : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type t)
    (pF : F ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k) (f : U.Elements ⥤ F)
    (hf : f ⋙ pF = CategoryOfElements.π U) (hU : IsDeformationFunctor.{u, v, w} U)
    (hF : IsDeformationCategory.{u, v, w} pF) {y₀ : U.Elements}
    (PH : ChosenPushforwardsAt (f ⋙ pF) y₀) (PF : ChosenPushforwardsAt pF (f.obj y₀))
    (M : FGModuleCat.{max v w} k) :
    Function.Injective (selfBoundaryLinearMap.{u, v, w} pF U f
        (isDeformationCategory_comp_of_isDeformationFunctor.{u, v, w} U pF f hf hU) hF PH PF M) ∧
      Function.Exact
        (selfBoundaryLinearMap.{u, v, w} pF U f
          (isDeformationCategory_comp_of_isDeformationFunctor.{u, v, w} U pF f hf hU) hF PH PF M)
        (tangentProjPair.{u, v, w} pF f f
          (isDeformationCategory_comp_of_isDeformationFunctor.{u, v, w} U pF f hf hU)
          (isDeformationCategory_comp_of_isDeformationFunctor.{u, v, w} U pF f hf hU) hF M)
Tag 06L7, a lemma

Tag 06L7 in the Stacks Project.

Deformation.isProrepresentable_presentationGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Prorepresentable.lean, line 402. The attribute's comment: “the hom-set universe of ℱ is at most that of 𝒞_Λ: the base is written ArtinianLocalAlgCat.{u, max v v₃ w, w} with v₃ the hom-set universe of ℱ, because the criterion of 06KG part (2) is available only at value universe equal to the hom-set universe”.

Let ℱ be a deformation category, let U : 𝒞_Λ → Sets be a prorepresentable functor and let f : U → ℱ be a 1-morphism of categories cofibered in groupoids. Let (U, R, s, t, c) be the groupoid in functors on 𝒞_Λ constructed from f in Stacks 06KY. If dim_k Inf(ℱ) < ∞, then (U, R, s, t, c) is prorepresentable.

The finite-dimensionality hypothesis is read at one basepoint y₀ of U and one choice PF of pushforwards there.

public theorem isProrepresentable_presentationGroupoid
    (hU : IsProrepresentable U) (hF : IsDeformationCategory.{u, max v v₃, w} pF)
    {y₀ : U.Elements} (PF : ChosenPushforwardsAt pF (f.obj y₀))
    (hInf : FiniteDimensional k
      ↥((infinitesimalAutomorphismLinearLift.{u, max v v₃, w} PF hF.satisfiesRS).functor.obj
        (FGModuleCat.of k (ULift.{max v v₃} k)))) :
    GroupoidInFunctors.IsProrepresentable
      ((presentationGroupoid pF U f hover hF.predeformation.cofibered).toGroupoidInFunctors)
Tag 06L8, a theorem

Tag 06L8 in the Stacks Project.

Deformation.hasSmoothPresentation_iff_isFiniteDimensionalDeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Criteria.lean, line 532. The attribute's comment: “the tag in full: ℱ admits a presentation by a smooth prorepresentable groupoid in functors on 𝒞_Λ iff (1) ℱ is a deformation category, (2) dim_k Tℱ is finite and (3) dim_k Inf(ℱ) is finite. Both directions, at the general universes of the chapter: ℱ has hom-set universe v and the base is ArtinianLocalAlgCat.{u, max v w, w}, with no universe equation imposed. The standing hypothesis of the source that ℱ be cofibered in groupoids is not carried: it is part of condition (1) on one side, and on the other it is derived from the presentation by Deformation.isCofiberedInGroupoids_of_equivalenceOver. The forward direction goes through Stacks 06L2 rather than through the construction of Stacks 06L8 itself, which Deformation.exists_isSmooth_isProrepresentable_presentation carries at the restricted universe”. References: SGA 7 VI (2.12), “more general”.

Stacks Project, Tag 06L8. Let ℱ be a category cofibered in groupoids over 𝒞_Λ. Then ℱ admits a presentation by a smooth prorepresentable groupoid in functors on 𝒞_Λ if and only if ℱ is a deformation category, dim_k Tℱ is finite and dim_k Inf(ℱ) is finite.

The direction from the three conditions to a presentation is Tag 06L2, whose minimal presentation is in particular a smooth prorepresentable one; the converse is Deformation.isFiniteDimensionalDeformationCategory_of_hasSmoothPresentation, which is parts (1), (2) and (3) of Tag 06KU transported along the presentation. Being cofibered in groupoids is not a hypothesis here: it is part of condition (1) on one side and a consequence of the presentation on the other.

theorem hasSmoothPresentation_iff_isFiniteDimensionalDeformationCategory [IsNoetherianRing Λ]
    [Module.Finite Λ k] :
    HasSmoothPresentation.{u, v, w} p ↔ IsFiniteDimensionalDeformationCategory.{u, v, w} p

Deformation.exists_isSmooth_isProrepresentable_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Existence.lean, line 155. The attribute's comment: “the construction of the tag's existence direction: (1)(2)(3) ⟹ ℱ admits a presentation by a smooth prorepresentable groupoid in functors on 𝒞_Λ, built as the source builds it, from a versal formal object and the groupoid in functors of 06KY. Only that direction, and only when the hom-set universe of ℱ equals that of k, the restriction 06L7 carries here. The tag in full — the biconditional, at the general universes, both directions — is Deformation.hasSmoothPresentation_iff_isFiniteDimensionalDeformationCategory, whose existence direction goes through 06L2 instead and whose converse direction is Deformation.isFiniteDimensionalDeformationCategory_of_hasSmoothPresentation, proved from part (3) of 06KU, Inf([U/R]) = Ker(ds ⊕ dt), which the library now has as Deformation.quotientInfinitesimalBoundary_exact”.

Stacks Project, Tag 06L8, the existence direction. A category ℱ cofibered in groupoids over 𝒞_Λ which is a deformation category and whose tangent space and space of infinitesimal automorphisms are finite-dimensional over k has a presentation by a smooth prorepresentable groupoid in functors on 𝒞_Λ.

The proof of the source. Condition (RS) gives (S1) and (S2) by Tag 06J7, so Schlessinger's existence theorem, Tag 06IW, produces a versal formal object ξ over a complete local algebra R from the finite-dimensionality of the tangent space. Put U = R̲|_{𝒞_Λ}; the associated morphism ξ̲ : U → ℱ of Tag 06HC is smooth, which is what versality of ξ says, and the groupoid in functors (U, R, s, t, c) built from it is the one of Tag 06KY. Tag 06L1 makes it smooth and its quotient morphism an equivalence — the quotient morphism is an equivalence because ξ̲ is essentially surjective, which follows from smoothness together with essential surjectivity on the special fibre, and the latter holds because the special fibre of ℱ is equivalent to a point. Tag 06L7 makes it prorepresentable from the finite-dimensionality of the infinitesimal automorphisms.

theorem exists_isSmooth_isProrepresentable_presentation
    (p : F ⥤ ArtinianLocalAlgCat.{u, w, w} Λ k)
    (hp : IsDeformationCategory.{u, w, w} p)
    (hT : FiniteDimensional k
      ↥(tangentModuleAt.{u, w, w} (BasedCategory.ofFunctor p) hp
        (FGModuleCat.of k (ULift.{w} k))))
    (hInf : ∀ (x : F) (P : ChosenPushforwardsAt p x),
      p.obj x = residueFieldObject.{u, w, w} Λ k →
      FiniteDimensional k
        ↥((infinitesimalAutomorphismLinearLift.{u, w, w} P hp.satisfiesRS).functor.obj
          (FGModuleCat.of k (ULift.{w} k)))) :
    ∃ G : GroupoidInFunctors.{_, w, w} (ArtinianLocalAlgCat.{u, w, w} Λ k),
      GroupoidInFunctors.IsSmooth G ∧
        GroupoidInFunctors.IsProrepresentable.{u, w, w, w} G ∧
          Nonempty (Presentation G p)
Sources
LeanDeformation.presentationMorphism_isEquivalence_of_isSmooth_of_fiber_essSurj · Deformation.isSmooth_presentationGroupoid · Deformation.isDeformationFunctor_twoFibreProductOver_self · Deformation.exact_selfBoundaryLinearMap_tangentProjPair · Deformation.isProrepresentable_presentationGroupoid · Deformation.hasSmoothPresentation_iff_isFiniteDimensionalDeformationCategory · Deformation.exists_isSmooth_isProrepresentable_presentation

Section90.27 Remarks regarding minimality#

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

Tag 06KM, a definition

Tag 06KM in the Stacks Project.

Deformation.GroupoidInFunctors.IsNormalized, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Minimality.lean, line 65. The attribute's comment: “normalized”. References: SGA 7 VI (2.11), “normalized”.

Stacks Project, Tag 06KM, part (1). A smooth prorepresentable groupoid in functors (U, R, s, t, c) is normalized when the groupoid (U(k[ε]), R(k[ε]), s, t, c) obtained by evaluating at the dual numbers k[ε] is totally disconnected: there are no arrows between distinct objects.

Total disconnection is stated here in the equivalent pointwise form: every element of R(k[ε]), i.e. every arrow of the evaluated groupoid, has equal source and target.

public abbrev IsNormalized (G : GroupoidInFunctors
  (ArtinianLocalAlgCat.{u, max v w, w} Λ k)) : Prop

Deformation.GroupoidInFunctors.IsMinimal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Minimality.lean, line 92. The attribute's comment: “minimal”.

Stacks Project, Tag 06KM, part (2). A smooth prorepresentable groupoid in functors (U, R, s, t, c) is minimal when the quotient morphism U → [U/R] is given by a minimal versal formal object of [U/R].

Here p : [U/R] ⥤ 𝒞_Λ is the structure morphism of the quotient category, realized as Grothendieck.forget (evaluationFunctor G), and the data asserted to exist are:

  • ξ, a formal object of [U/R], required by the first conjunct to be minimal versal (IsMinimalVersal, Tag 06T4): this is the source's "minimal versal formal object of [U/R]";
  • pushforwards, a choice of cocartesian pushforwards in [U/R]. This is the auxiliary data needed to build the morphism ξ^# associated to ξ (associatedMorphism, Tag 06HC), which goes from the category of elements of restrictedCoyoneda ξ.base to [U/R]; "the morphism given by ξ" means ξ^#;
  • e, an equivalence from the category of elements of the object functor U to that of restrictedCoyoneda ξ.base. The second conjunct, e.functor ⋙ π = π, says that e commutes with the projections to 𝒞_Λ, i.e. that it is an equivalence over 𝒞_Λ; it is this that lets ξ^# be read as a morphism e.functor ⋙ ξ^# out of U;
  • the third conjunct: a natural isomorphism α from quotientMorphism G, which is the quotient morphism U → [U/R], to e.functor ⋙ ξ^#, every component of which lies over an identity arrow of 𝒞_Λ (Functor.IsHomLift p (𝟙 X.1)). Being isomorphic by such a vertical natural isomorphism is the sense in which U → [U/R] is given by ξ.
public def IsMinimal
    (G : GroupoidInFunctors.{_, max v w, max (max v w) z}
      (ArtinianLocalAlgCat.{u, max v w, w} Λ k)) : Prop

Deformation.GroupoidInFunctors.exists_isMinimalVersal_of_isMinimal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Minimality.lean, line 114. The attribute's comment: “minimal: the quotient has a minimal versal formal object”.

Stacks Project, Tag 06KM, part (2). A minimal groupoid in functors has a minimal versal formal object of its quotient: the object ξ whose associated morphism the quotient morphism U → [U/R] is given by. This states the first conjunct of IsMinimal on its own, so that the content of part (2) is available as a theorem and not only inside the definition.

public theorem exists_isMinimalVersal_of_isMinimal
    {G : GroupoidInFunctors.{_, max v w, max (max v w) z}
      (ArtinianLocalAlgCat.{u, max v w, w} Λ k)}
    (hG : IsMinimal.{u, v, w, z} G) :
    ∃ ξ : FormalObject (Grothendieck.forget (evaluationFunctor G)),
      IsMinimalVersal (quotientProjection_cofibered G) ξ

Deformation.GroupoidInFunctors.exists_quotientMorphism_iso_associatedMorphism_of_isMinimal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Minimality.lean, line 128. The attribute's comment: “minimal: the quotient morphism is the one associated to that object”.

Stacks Project, Tag 06KM, part (2). For a minimal groupoid in functors, the quotient morphism U → [U/R] is, up to a vertical natural isomorphism and the equivalence prorepresenting U, the morphism associated to a minimal versal formal object of [U/R]. This is part (2) in full, stated as a theorem.

public theorem exists_quotientMorphism_iso_associatedMorphism_of_isMinimal
    {G : GroupoidInFunctors.{_, max v w, max (max v w) z}
      (ArtinianLocalAlgCat.{u, max v w, w} Λ k)}
    (hG : IsMinimal.{u, v, w, z} G) :
    ∃ (ξ : FormalObject (Grothendieck.forget (evaluationFunctor G)))
      (pushforwards : ChosenPushforwards (Grothendieck.forget (evaluationFunctor G)))
      (e : G.objects.Elements ≌ (restrictedCoyoneda ξ.base).Elements),
      IsMinimalVersal (quotientProjection_cofibered G) ξ ∧
      (e.functor ⋙ CategoryOfElements.π (restrictedCoyoneda ξ.base) =
        CategoryOfElements.π G.objects) ∧
      Nonempty
        { α : quotientMorphism G ≅
            e.functor ⋙ (associatedMorphism (quotientProjection_cofibered G) ξ
              pushforwards).toBasedFunctor.toFunctor //
          ∀ X : G.objects.Elements,
            CategoryTheory.Functor.IsHomLift
              (Grothendieck.forget (evaluationFunctor G)) (𝟙 X.1) (α.hom.app X) }
Tag 06KN, a lemma

Tag 06KN in the Stacks Project.

Deformation.GroupoidInFunctors.isNormalized_iff_bijective_quotientDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/Minimality.lean, line 717. The attribute's comment: “part (1): normalized iff isomorphism on tangent spaces”.

A groupoid in functors is normalized precisely when the quotient morphism U → [U/R] induces an isomorphism on tangent spaces.

public theorem isNormalized_iff_bijective_quotientDifferential
    (G : GroupoidInFunctors (ArtinianLocalAlgCat.{u, max v w, w} Λ k)) :
    IsNormalized.{u, v, w} G ↔ Function.Bijective (quotientDifferential.{u, v, w} G)

Deformation.GroupoidInFunctors.isMinimal_iff_quotientDifferential_ker_le_derivationRange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/Minimality.lean, line 852. The attribute's comment: “part (2): minimal iff the kernel of the differential lies in the image of Der”.

A smooth prorepresentable groupoid in functors is minimal precisely when the kernel of the differential of U → [U/R] is contained in the image of the canonical map Der_Λ(k, k) → TU.

public theorem isMinimal_iff_quotientDifferential_ker_le_derivationRange
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hpro : IsProrepresentable G) (hsmooth : IsSmooth G) :
    IsMinimal.{u, v, w, v} G ↔
      ∀ x : tangentSpaceArtinian.{u, w, v} Λ k
          (isomorphismClasses (BasedCategory.ofFunctor (CategoryOfElements.π G.objects))
            (categoryOfElements_projection_isCofibered G.objects)),
        quotientDifferential.{u, v, w} G x =
            quotientDifferential.{u, v, w} G
              (derivationToTangentSpace (CategoryOfElements.π G.objects)
                (objects_isPredeformationCategory_of_isProrepresentable G hpro) 0) →
          x ∈ Set.range (derivationToTangentSpace (CategoryOfElements.π G.objects)
            (objects_isPredeformationCategory_of_isProrepresentable G hpro))
Tag 06KP, a lemma

Tag 06KP in the Stacks Project.

Deformation.isIso_of_tangentSpace_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Predeformation/ProrepresentableEndomorphism.lean, line 60.

Stacks Project, Tag 06KP. An endomorphism of a prorepresentable functor on Artinian local Λ-algebras whose differential — its component at the dual numbers — is bijective is an isomorphism.

theorem isIso_of_tangentSpace_bijective
    (U : ArtinianLocalAlgCat.{u, max v w, w} Λ k ⥤ Type (max v w))
    (hU : IsProrepresentable U) (φ : U ⟶ U)
    (hφ : Function.Bijective (φ.app (artinianDualNumbers Λ k))) :
    IsIso φ
Tag 06KQ, a lemma

Tag 06KQ in the Stacks Project.

Deformation.GroupoidInFunctors.isIso_quotientMap_of_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/MinimalAutoequivalence.lean, line 485. The attribute's comment: “equivalence taken as induced by an endomorphism of the groupoid, and the conclusion read as strict isomorphism of categories. Neither is the source's reading, so this is an auxiliary and not the tag's covering declaration: the tag is carried outright by Deformation.GroupoidInFunctors.exists_isIso_hom_of_isEquivalence_endo, which takes an arbitrary 1-morphism of the quotients over 𝒞_Λ whose functor is an equivalence of categories and concludes that it is isomorphic to the one induced by an isomorphism of groupoids in functors. What this auxiliary adds is that the induced functor is then an isomorphism of categories on the nose, which is stronger than the source's conclusion and not invariant under isomorphism of functors”.

Stacks Project, Tag 06KQ. Let (U, R, s, t, c) be a minimal smooth prorepresentable groupoid in functors on 𝒞_Λ. An equivalence [U/R] → [U/R] of categories cofibered in groupoids induced by an endomorphism of the groupoid is an isomorphism of categories.

public theorem isIso_quotientMap_of_isEquivalence [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hpro : IsProrepresentable G) (hsmooth : IsSmooth G) (hmin : IsMinimal.{u, v, w, v} G)
    (f : G ⟶ G) [(quotientMap f).IsEquivalence] :
    IsIso (quotientMap f).toCatHom

Deformation.GroupoidInFunctors.exists_isIso_hom_of_isEquivalence_endo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/MinimalEquivalence.lean, line 257.

Stacks Project, Tag 06KQ. Let (U, R, s, t, c) be a minimal smooth prorepresentable groupoid in functors on 𝒞_Λ. A 1-morphism [U/R] → [U/R] over 𝒞_Λ whose functor is an equivalence of categories is an isomorphism: it is isomorphic to the functor induced by an isomorphism of groupoids in functors, and therefore has a two-sided inverse 1-morphism over 𝒞_Λ up to 2-isomorphism, by Deformation.GroupoidInFunctors.exists_inverse_morphismOver_of_isIso.

The 1-morphism is realised by a morphism F of groupoids in functors, which is the assertion opening the source proof and is Deformation.GroupoidInFunctors.exists_hom_of_morphismOver; the functor induced by F is then an equivalence, so F is an isomorphism by Deformation.GroupoidInFunctors.isIso_of_quotientMap_isEquivalence, which is the differential argument of the source proof.

theorem exists_isIso_hom_of_isEquivalence_endo [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hpro : IsProrepresentable G) (hsmooth : IsSmooth G) (hmin : IsMinimal.{u, v, w, v} G)
    (Φ : StacksRepresentableCFG.MorphismOver
      (Grothendieck.forget (evaluationFunctor G))
      (Grothendieck.forget (evaluationFunctor G))) [Φ.functor.IsEquivalence] :
    ∃ F : G ⟶ G, IsIso F ∧ Nonempty (quotientMap F ≅ Φ.functor)
Tag 06KR, a lemma

Tag 06KR in the Stacks Project.

Deformation.GroupoidInFunctors.isIso_quotientMap_of_quotientMaps_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/MinimalEquivalence.lean, line 142. The attribute's comment: “equivalence and quasi-inverse taken as induced by morphisms of groupoids, and the conclusion read as strict isomorphism of categories. Neither is the source's reading, so this is an auxiliary and not the tag's covering declaration: the tag is carried outright by Deformation.GroupoidInFunctors.exists_isIso_hom_of_isEquivalence below, which takes an arbitrary 1-morphism of the quotients over 𝒞_Λ whose functor is an equivalence of categories. What this auxiliary adds is that the induced functor is then an isomorphism of categories on the nose, which is stronger than the source's conclusion and not invariant under isomorphism of functors”.

An equivalence [U/R] → [U'/R'] of minimal smooth prorepresentable quotients induced by a morphism of groupoids in functors, and admitting a quasi-inverse induced by one in the opposite direction, induces an isomorphism of categories on the nose.

public theorem isIso_quotientMap_of_quotientMaps_isEquivalence
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hproG : IsProrepresentable G) (hsmoothG : IsSmooth G) (hminG : IsMinimal.{u, v, w, v} G)
    (hproH : IsProrepresentable H) (hsmoothH : IsSmooth H) (hminH : IsMinimal.{u, v, w, v} H)
    (F : G ⟶ H) (F' : H ⟶ G)
    [(quotientMap F).IsEquivalence] [(quotientMap F').IsEquivalence] :
    IsIso (quotientMap F).toCatHom

Deformation.GroupoidInFunctors.exists_isIso_hom_of_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/GroupoidQuotient/MinimalEquivalence.lean, line 279.

Stacks Project, Tag 06KR. Let (U, R, s, t, c) and (U', R', s', t', c') be minimal smooth prorepresentable groupoids in functors on 𝒞_Λ. A 1-morphism [U/R] → [U'/R'] over 𝒞_Λ whose functor is an equivalence of categories is an isomorphism: it is isomorphic to the functor induced by an isomorphism of groupoids in functors, and therefore has a two-sided inverse 1-morphism over 𝒞_Λ up to 2-isomorphism, by Deformation.GroupoidInFunctors.exists_inverse_morphismOver_of_isIso.

This is the source's proof: a quasi-inverse of the given 1-morphism, corrected to lie over 𝒞_Λ by Deformation.GroupoidInFunctors.inverseMorphismOver, is realised by a morphism of groupoids in functors in the opposite direction, and the two composites are autoequivalences of the two quotients, hence isomorphisms by Tag 06KQ.

theorem exists_isIso_hom_of_isEquivalence [IsNoetherianRing Λ] [Module.Finite Λ k]
    (hproG : IsProrepresentable G) (hsmoothG : IsSmooth G) (hminG : IsMinimal.{u, v, w, v} G)
    (hproH : IsProrepresentable H) (hsmoothH : IsSmooth H) (hminH : IsMinimal.{u, v, w, v} H)
    (Φ : StacksRepresentableCFG.MorphismOver
      (Grothendieck.forget (evaluationFunctor G))
      (Grothendieck.forget (evaluationFunctor H))) [Φ.functor.IsEquivalence] :
    ∃ F : G ⟶ H, IsIso F ∧ Nonempty (quotientMap F ≅ Φ.functor)
Tag 06L2, a lemma

Tag 06L2 in the Stacks Project.

Deformation.exists_minimalPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/MinimalPresentation.lean, line 567.

Stacks Project, Tag 06L2. Let ℱ be a deformation category over 𝒞_Λ with dim_k Tℱ < ∞ and dim_k Inf(ℱ) < ∞. Then there is a minimal versal formal object ξ of ℱ, say over R, and, with U = R̲|_{𝒞_Λ} and f = ξ : U → ℱ the associated morphism, the groupoid in functors (U, R, s, t, c) constructed from f in Tag 06KY is a minimal smooth prorepresentable groupoid in functors on 𝒞_Λ with [U/R] → ℱ an equivalence.

The two Fact instances carry no content beyond hp; they make Tag 06IH's canonical k-vector space structure on the tangent space available, so that the finite dimensionality of Tℱ can be stated.

public theorem exists_minimalPresentation [IsNoetherianRing Λ] [Module.Finite Λ k]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v v₃ w, w} Λ k)
    (hp : IsDeformationCategory.{u, max v v₃, w} p)
    [h𝓕 : Fact (IsPredeformationCategory.{u, max v v₃, w} (BasedCategory.ofFunctor p).p)]
    [Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses (BasedCategory.ofFunctor p) h𝓕.out.cofibered)))]
    [FiniteDimensional k (tangentSpaceArtinian.{u, w, max v v₃} Λ k
      (isomorphismClasses (BasedCategory.ofFunctor p) h𝓕.out.cofibered))]
    (hInf : ∀ (x : F) (_hbase : p.obj x = residueFieldObject.{u, max v v₃, w} Λ k)
      (PF : ChosenPushforwardsAt p x), FiniteDimensional k
        ↥((infinitesimalAutomorphismLinearLift.{u, max v v₃, w} PF hp.satisfiesRS).functor.obj
          (FGModuleCat.of k (ULift.{max v v₃} k)))) :
    Nonempty (MinimalPresentation.{u, v, w, u₃, v₃} p hp.predeformation.cofibered)
Tag 06L3, a lemma

Tag 06L3 in the Stacks Project.

Deformation.GroupoidInFunctors.nonempty_iso_of_presentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/MinimalUniqueness.lean, line 104. The attribute's comment: “the statement is specialised to third universe max v w, that is IsMinimal.{u, v, w, v}, which is where Stacks 06KR and the Stacks 06KQ under it are fixed; IsNoetherianRing Λ and Module.Finite Λ k are the chapter's standing assumptions on Λ, which Stacks 06KQ consumes”.

Stacks Project, Tag 06L3. Let ℱ be a category cofibered in groupoids over 𝒞_Λ. If ℱ admits presentations by minimal smooth prorepresentable groupoids in functors (U, R, s, t, c) and (U', R', s', t', c'), then the two are isomorphic.

The two presentations compose to an equivalence [U/R] → [U'/R'] over 𝒞_Λ. Both its forward and its backward 1-morphism of quotients is induced, up to isomorphism of functors, by a morphism of groupoids in functors, so the forward morphism induces an equivalence of the quotients whose quasi-inverse is induced as well, and it is therefore an isomorphism by Tag 06KR.

public theorem nonempty_iso_of_presentations [IsNoetherianRing Λ] [Module.Finite Λ k]
    {ℱ : Type u₁} [Category.{v₁} ℱ] (p : ℱ ⥤ ArtinianLocalAlgCat.{u, max v w, w} Λ k)
    (hp : Deformation.IsCofiberedInGroupoids p)
    (G H : GroupoidInFunctors.{_, max v w, max v w}
      (ArtinianLocalAlgCat.{u, max v w, w} Λ k))
    (hGpro : IsProrepresentable G) (hGsmooth : IsSmooth G) (hGmin : IsMinimal.{u, v, w, v} G)
    (hGpres : Deformation.Presentation G p)
    (hHpro : IsProrepresentable H) (hHsmooth : IsSmooth H) (hHmin : IsMinimal.{u, v, w, v} H)
    (hHpres : Deformation.Presentation H p) :
    Nonempty (G ≅ H)
Tag 06TE, a theorem

Tag 06TE in the Stacks Project.

Deformation.hasNormalizedPresentation_iff_hasMinimalPresentation_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Criteria.lean, line 560. The attribute's comment: “the separability clause of the tag: when k' ⊂ k is separable, condition (1), a normalized smooth prorepresentable presentation, is equivalent to the other three. Proved outright. Separability is read as Algebra.IsSeparable (residueImageField Λ k) k, and the equivalence of (1) with conditions (2), (3), (4) is this equivalence with (3) together with the equivalence of (2), (3), (4) in Deformation.hasSmoothPresentation_tfae; the four-way equivalence is assembled as Deformation.tfae_of_isSeparable”.

Stacks Project, Tag 06TE, the separable case. When k is separable over the image field of Λ the residue field carries no nonzero Λ-derivation, so a minimal smooth prorepresentable presentation is normalized and conditions (1) and (3) agree.

theorem hasNormalizedPresentation_iff_hasMinimalPresentation_of_isSeparable
    [IsNoetherianRing Λ] [Module.Finite Λ k]
    [Algebra.IsSeparable (residueImageField Λ k) k] :
    HasNormalizedPresentation.{u, v, w} p ↔ HasMinimalPresentation.{u, v, w} p

Deformation.hasSmoothPresentation_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Criteria.lean, line 595. The attribute's comment: “the tag: for ℱ cofibered in groupoids over 𝒞_Λ, conditions (2) a smooth prorepresentable presentation, (3) a minimal one, and (4) ℱ a deformation category with dim_k Tℱ and dim_k Inf(ℱ) finite, are equivalent and implied by (1) a normalized one, and all four are equivalent when k' ⊂ k is separable. Delivered outright and with no carried hypothesis: (1) ⟹ (3), (3) ⟹ (2), (4) ⟹ (3), (2) ⟹ (4) — the last from Deformation.hasSmoothPresentation_iff_isFiniteDimensionalDeformationCategory, Stacks 06L8 — and (3) ⟺ (1) whenever Der_Λ(k, k) vanishes. Nothing is assumed: this theorem takes no hypothesis beyond the chapter's standing IsNoetherianRing Λ and Module.Finite Λ k, and the vanishing of Der_Λ(k, k) is the antecedent of the fourth conjunct, which is proved outright as an implication. Separability of k' ⊂ k supplies that vanishing, by Deformation.derivation_eq_zero_of_residueImageField_separable, so the fourth conjunct is at least as strong as the source's separable clause; that clause itself, as the four-way equivalence, is Deformation.tfae_of_isSeparable, also carrying this tag. The final uniqueness clause of the tag is not here: it is Stacks 06L3, carried by this tag's add_to_stacks on Deformation.GroupoidInFunctors.nonempty_iso_of_presentations, and it too is delivered outright — the realisation of a 1-morphism of quotients by a morphism of groupoids in functors, which that proof attributes to Definition 06KB, is proved as Deformation.GroupoidInFunctors.exists_hom_of_morphismOver. No part of this tag is conditional. The statement is specialised to a hom-set universe of ℱ equal to the value universe v of the groupoids in functors, which is where Stacks 06L2 and Stacks 06L3 meet”.

Stacks Project, Tag 06TE. Conditions (2), (3) and (4) are equivalent, and (1) implies them; when the residue field carries no nonzero Λ-derivation all four are equivalent.

The implications are (1) implies (3) and (3) implies (2), from Tag 06KN and the definitions, (4) implies (3), from Tag 06L2, and (2) implies (4), from Tag 06L8; the equivalence of (1) and (3) under hzero is the other half of Tag 06KN.

theorem hasSmoothPresentation_tfae [IsNoetherianRing Λ] [Module.Finite Λ k] :
    (HasNormalizedPresentation.{u, v, w} p → HasMinimalPresentation.{u, v, w} p) ∧
      (HasSmoothPresentation.{u, v, w} p ↔ HasMinimalPresentation.{u, v, w} p) ∧
      (HasSmoothPresentation.{u, v, w} p ↔
        IsFiniteDimensionalDeformationCategory.{u, v, w} p) ∧
      ((∀ δ : Derivation Λ k k, δ = 0) →
        (HasNormalizedPresentation.{u, v, w} p ↔ HasMinimalPresentation.{u, v, w} p))

Deformation.tfae_of_isSeparable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/CofiberedPresentation/Criteria.lean, line 629. The attribute's comment: “the tag's final equivalence, assembled: under separability of k' ⊂ k the four conditions (1) a normalized smooth prorepresentable presentation, (2) a smooth prorepresentable one, (3) a minimal one, and (4) ℱ a deformation category with dim_k Tℱ and dim_k Inf(ℱ) finite are all equivalent. Proved outright, with no carried hypothesis. Separability is read as Algebra.IsSeparable (residueImageField Λ k) k. The statement is specialised to a hom-set universe of ℱ equal to the value universe v of the groupoids in functors, which is where Stacks 06L2 and Stacks 06L3 meet. The uniqueness clause of the tag is separate and is also delivered outright: see this tag's add_to_stacks on Deformation.GroupoidInFunctors.nonempty_iso_of_presentations”.

Stacks Project, Tag 06TE, the four-way equivalence under separability. When k is separable over the image field of Λ, a category cofibered in groupoids over 𝒞_Λ admits a presentation by a normalized smooth prorepresentable groupoid in functors if and only if it admits one by a smooth prorepresentable groupoid in functors, if and only if it admits one by a minimal smooth prorepresentable groupoid in functors, if and only if it is a deformation category whose tangent space and whose space of infinitesimal automorphisms are finite dimensional over k.

The cycle is (1) implies (3) by Tag 06KN, (3) implies (2) by the definitions, (2) implies (4) by Tag 06L8, and (4) implies (1) by Tag 06L2 followed by the separable half of Tag 06KN.

theorem tfae_of_isSeparable [IsNoetherianRing Λ] [Module.Finite Λ k]
    [Algebra.IsSeparable (residueImageField Λ k) k] :
    List.TFAE [HasNormalizedPresentation.{u, v, w} p, HasSmoothPresentation.{u, v, w} p,
      HasMinimalPresentation.{u, v, w} p,
      IsFiniteDimensionalDeformationCategory.{u, v, w} p]

Declarations registered for the tag:

  • Deformation.GroupoidInFunctors.nonempty_iso_of_presentations, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/CofiberedPresentation/Criteria.lean, line 646 (StacksFrontier): “the final uniqueness clause of the tag: the minimal smooth prorepresentable groupoids in functors which present a given category cofibered in groupoids over 𝒞_Λ are unique up to isomorphism. This is Stacks 06L3, delivered outright: the realisation it rests on — that a 1-morphism of quotients over 𝒞_Λ is, up to isomorphism of functors, the one induced by a morphism of groupoids in functors, the step the source proof attributes to Definition 06KB — is proved as Deformation.GroupoidInFunctors.exists_hom_of_morphismOver, for a prorepresentable source and a smooth target, which both presentations here supply. No part of Stacks 06TE is conditional; for the equivalence of the four conditions see Deformation.hasSmoothPresentation_tfae and Deformation.tfae_of_isSeparable”.
Sources
LeanDeformation.GroupoidInFunctors.IsNormalized · Deformation.GroupoidInFunctors.IsMinimal · Deformation.GroupoidInFunctors.exists_isMinimalVersal_of_isMinimal · Deformation.GroupoidInFunctors.exists_quotientMorphism_iso_associatedMorphism_of_isMinimal · Deformation.GroupoidInFunctors.isNormalized_iff_bijective_quotientDifferential · Deformation.GroupoidInFunctors.isMinimal_iff_quotientDifferential_ker_le_derivationRange · Deformation.isIso_of_tangentSpace_bijective · Deformation.GroupoidInFunctors.isIso_quotientMap_of_isEquivalence

Section90.28 Uniqueness of versal rings#

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

Tag 0DQB, a lemma

Tag 0DQB in the Stacks Project.

Deformation.CompleteLocalAlgCat.formallyHomotopic_refl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalRing.lean, line 765. The attribute's comment: “reflexivity”.

Stacks Project, Tag 0DQB. Every morphism of complete local Λ-algebras is formally homotopic to itself: take the homotopy in no variables.

theorem formallyHomotopic_refl (f : R ⟶ S) : FormallyHomotopic f f

Deformation.CompleteLocalAlgCat.formallyHomotopic_symm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalRing.lean, line 802. The attribute's comment: “symmetry”.

Stacks Project, Tag 0DQB. Formal homotopy is symmetric: substituting the homotopy into itself gives an automorphism of the power series ring exchanging the two specializations.

theorem formallyHomotopic_symm {f g : R ⟶ S}
    (h : FormallyHomotopic f g) : FormallyHomotopic g f

Deformation.CompleteLocalAlgCat.formallyHomotopic_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalRing.lean, line 864. The attribute's comment: “transitivity”.

Stacks Project, Tag 0DQB. Formal homotopy is transitive: concatenating the variables of two homotopies and substituting the first into the second gives a homotopy between the outer two morphisms.

theorem formallyHomotopic_trans {f g h : R ⟶ S}
    (hfg : FormallyHomotopic f g) (hgh : FormallyHomotopic g h) :
    FormallyHomotopic f h

Deformation.CompleteLocalAlgCat.formallyHomotopic_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalRing.lean, line 1062.

Stacks Project, Tag 0DQB. Formal homotopy is an equivalence relation on each set of morphisms of \widehat{\mathcal C}_Λ.

theorem formallyHomotopic_equivalence :
    Equivalence (α := R ⟶ S) FormallyHomotopic
Tag 0DQC, a lemma

Tag 0DQC in the Stacks Project.

Deformation.formallyHomotopic_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalRing.lean, line 358.

Postcomposing two formally homotopic maps with the same morphism preserves their formal homotopy.

theorem formallyHomotopic_comp
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {R S S' : CompleteLocalAlgCat.{u, v, w} Λ k}
    {f₁ f₂ : R ⟶ S} (hf : FormallyHomotopic f₁ f₂) (g : S ⟶ S') :
    FormallyHomotopic (f₁ ≫ g) (f₂ ≫ g)
Tag 0DQD, a lemma

Tag 0DQD in the Stacks Project.

Deformation.formallyHomotopic_of_isVersal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalRing/Uniqueness.lean, line 694.

Stacks Project, Tag 0DQD. Let ℱ be a deformation category over 𝒞_Λ whose tangent space and infinitesimal automorphisms are finite-dimensional over k. Let ξ be a versal formal object lying over R, and let η be a formal object lying over S. Then any two maps f, g : R → S with f_*ξ ≅ η ≅ g_*ξ are formally homotopic.

theorem formallyHomotopic_of_isVersal
    (p : F ⥤ ArtinianLocalAlgCat.{u, max v v₃ w, w} Λ k)
    (hp : IsDeformationCategory.{u, max v v₃, w} p)
    (_hT : FiniteDimensional k
      ↥(tangentModuleAt.{u, max v v₃, w} (BasedCategory.ofFunctor p) hp
        (FGModuleCat.of k (ULift.{max v v₃} k))))
    (hInf : ∀ (x : F) (P : ChosenPushforwardsAt p x),
      p.obj x = residueFieldObject.{u, max v v₃, w} Λ k →
      FiniteDimensional k
        ↥((infinitesimalAutomorphismLinearLift.{u, max v v₃, w} P hp.satisfiesRS).functor.obj
          (FGModuleCat.of k (ULift.{max v v₃} k))))
    (ξ η : FormalObject p) (hξ : IsVersal hp.predeformation.cofibered ξ)
    (f g : ξ.base ⟶ η.base)
    (hf : ∃ a : ξ ⟶ η, a.base = f) (hg : ∃ a : ξ ⟶ η, a.base = g) :
    CompleteLocalAlgCat.FormallyHomotopic f g
Tag 0DQE, a lemma

Tag 0DQE in the Stacks Project.

Deformation.Ideal.map_eq_of_formallyHomotopic_of_mem_minimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalRing.lean, line 327.

Formally homotopic morphisms of Noetherian complete local algebras extend a minimal prime of the source to the same ideal of the target.

theorem map_eq_of_formallyHomotopic_of_mem_minimalPrimes
    {Λ : Type u} {k : Type w} [CommRing Λ] [Field k] [Algebra Λ k]
    {R S : CompleteLocalAlgCat.{u, v, w} Λ k} (f₁ f₂ : R ⟶ S)
    (hf : FormallyHomotopic f₁ f₂) (p : Ideal R) (hp : p ∈ minimalPrimes R) :
    p.map f₁.hom.toRingHom = p.map f₂.hom.toRingHom
Sources
LeanDeformation.CompleteLocalAlgCat.formallyHomotopic_refl · Deformation.CompleteLocalAlgCat.formallyHomotopic_symm · Deformation.CompleteLocalAlgCat.formallyHomotopic_trans · Deformation.CompleteLocalAlgCat.formallyHomotopic_equivalence · Deformation.formallyHomotopic_comp · Deformation.formallyHomotopic_of_isVersal · Deformation.Ideal.map_eq_of_formallyHomotopic_of_mem_minimalPrimes

Section90.29 Change of residue field#

Section 90.29 of the Stacks Project, Tag 07W7. 7 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07W8, a situation

Tag 07W8 in the Stacks Project.

Deformation.ChangeOfFieldsSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Basic.lean, line 104. The attribute's comment: “the standing situation”.

Stacks Project, Tag 07W8. The standing finite tower of fields over the Noetherian base ring Λ.

public structure ChangeOfFieldsSituation

Deformation.comparisonFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Basic.lean, line 340. The attribute's comment: “the comparison functor”.

Stacks Project, Tag 07W8. The canonical comparison functor sending B to B ×_l k, with its prescribed algebra, residue and morphism maps.

public noncomputable def comparisonFunctor
    (S : ChangeOfFieldsSituation.{u, v, w}) :
    ComparisonFunctor.{u, v, w, x} S

Deformation.changeOfFieldsProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Basic.lean, line 454. The attribute's comment: “the associated projection”.

Stacks Project, Tag 07W8. The projection p_{l/k} : F_{l/k} ⟶ 𝒞_{Λ,l} associated to p : F ⟶ 𝒞_{Λ,k}.

public def changeOfFieldsProjection (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k) :
    ChangeOfFieldsCategory S p ⥤
      ArtinianLocalAlgCat.{u, x, w} S.Λ S.l

Deformation.changeOfFieldsFiberInclusion_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Basic.lean, line 494. The attribute's comment: “the fibers”.

Stacks Project, Tag 07W8. The canonical fiber inclusion is an equivalence. This fixes the identification of the changed fiber with the original fiber over B ×_l k, rather than merely asserting existence of an unspecified equivalence.

public theorem changeOfFieldsFiberInclusion_isEquivalence
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)
    (hp : IsCofiberedInGroupoids p)
    (B : ArtinianLocalAlgCat.{u, x, w} S.Λ S.l) :
    (changeOfFieldsFiberInclusion S p B).IsEquivalence

Deformation.changeOfFieldsProjection_isCofiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Basic.lean, line 582. The attribute's comment: “cofibered in groupoids”.

Stacks Project, Tag 07W8. The projection obtained by change of residue field is cofibered in groupoids whenever the original projection is.

public theorem changeOfFieldsProjection_isCofiberedInGroupoids
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)
    (hp : IsCofiberedInGroupoids p) :
    IsCofiberedInGroupoids (changeOfFieldsProjection S p)
Tag 07W9, an equation

Tag 07W9 in the Stacks Project.

Declarations registered for the tag:

Tag 07WA, a lemma

Tag 07WA in the Stacks Project.

Deformation.changeOfFieldsIsoClassMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Basic.lean, line 720. The attribute's comment: “isomorphism_classes”.

The canonical fiber inclusion induces a bijection on isomorphism classes, without restricting the universe of the total category.

public theorem changeOfFieldsIsoClassMap_bijective
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)
    (hp : IsCofiberedInGroupoids p)
    (B : ArtinianLocalAlgCat.{u, x, w} S.Λ S.l) :
    Function.Bijective (changeOfFieldsIsoClassMap S p B)

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

Naturality of the canonical identification on representative classes: a coCartesian pushforward and the change-of-fields fiber inclusion commute on isomorphism classes. This formulation allows the total category to live in an arbitrary universe.

public theorem changeOfFieldsIsoClassMap_naturality
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)
    (hp : IsCofiberedInGroupoids p)
    {B C : ArtinianLocalAlgCat.{u, x, w} S.Λ S.l}
    (f : B ⟶ C)
    (a : p.Fiber ((comparisonFunctor S).functor.obj B)) :
    letI : p.op.IsFibered := hp.isFibered
    letI : (changeOfFieldsProjection S p).op.IsFibered :=
      (changeOfFieldsProjection_isCofiberedInGroupoids S p hp).isFibered
    let a' : p.Fiber ((comparisonFunctor S).functor.obj C) :=
      ⟨(CategoryTheory.Functor.pullbackFiber p.op
        (⟨Opposite.op a.1, congrArg Opposite.op a.2⟩ :
          p.op.Fiber (Opposite.op ((comparisonFunctor S).functor.obj B)))
        ((comparisonFunctor S).functor.map f).op).1.unop,
        congrArg Opposite.unop (CategoryTheory.Functor.pullbackFiber p.op
          (⟨Opposite.op a.1, congrArg Opposite.op a.2⟩ :
            p.op.Fiber (Opposite.op ((comparisonFunctor S).functor.obj B)))
          ((comparisonFunctor S).functor.map f).op).2⟩
    (changeOfFieldsProjection S p).op.isoClassPresheaf.map f.op.op
      (CategoryTheory.Functor.isoClassMk (changeOfFieldsProjection S p).op
        (⟨Opposite.op ((changeOfFieldsFiberInclusion S p B).obj a).1,
          congrArg Opposite.op ((changeOfFieldsFiberInclusion S p B).obj a).2⟩ :
          (changeOfFieldsProjection S p).op.Fiber (Opposite.op B))) =
      CategoryTheory.Functor.isoClassMk (changeOfFieldsProjection S p).op
        (⟨Opposite.op ((changeOfFieldsFiberInclusion S p C).obj a').1,
          congrArg Opposite.op ((changeOfFieldsFiberInclusion S p C).obj a').2⟩ :
          (changeOfFieldsProjection S p).op.Fiber (Opposite.op C))

Deformation.changeOfFieldsProjection_isPredeformationCategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Basic.lean, line 1025. The attribute's comment: “predeformation”.

Changing the residue field of a predeformation category along k → l again gives a predeformation category.

public theorem changeOfFieldsProjection_isPredeformationCategory
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max (max x w) v, v} S.Λ S.k)
    (hp : IsPredeformationCategory.{u, max x w, v, z, y} p) :
    IsPredeformationCategory
      (changeOfFieldsProjection.{u, v, w, max x w, y, z} S p)

Deformation.schlessingerConditionS1_changeOfFields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/ChangeOfFieldsConditionS2.lean, line 688. The attribute's comment: “condition (S1)”.

A change of residue field preserves Schlessinger's condition (S1).

public theorem schlessingerConditionS1_changeOfFields
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)
    (hS1 : SchlessingerConditionS1 p) :
    SchlessingerConditionS1
      (changeOfFieldsProjection S p)

Deformation.schlessingerConditionS2_changeOfFields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/ChangeOfFieldsConditionS2.lean, line 707. The attribute's comment: “condition (S2)”.

A change of residue field preserves Schlessinger's condition (S2) for a functor cofibered in groupoids.

public theorem schlessingerConditionS2_changeOfFields
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)
    (hp : IsCofiberedInGroupoids p)
    (hS2 : SchlessingerConditionS2 p) :
    SchlessingerConditionS2
      (changeOfFieldsProjection S p)

Deformation.changeOfFieldsProjection_satisfiesRS, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/ChangeOfFieldsConditionS2.lean, line 881. The attribute's comment: “condition (RS)”.

A change of residue field preserves the Rim-Schlessinger condition (RS).

public theorem changeOfFieldsProjection_satisfiesRS
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)
    (hp : SatisfiesRS p) :
    SatisfiesRS (changeOfFieldsProjection S p)
Tag 07WB, a lemma

Tag 07WB in the Stacks Project.

Deformation.tangentSpaceChangeOfFields, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/ChangeOfFieldsTangentSpace.lean, line 1567.

public noncomputable def tangentSpaceChangeOfFields
    (S : ChangeOfFieldsSituation.{u, v, v})
    (𝓕 : BasedCategory.{z, y} (ArtinianLocalAlgCat.{u, v, v} S.Λ S.k))
    (hp : IsPredeformationCategory 𝓕.p)
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 hp.cofibered))) :
    let q := changeOfFieldsProjection.{u, v, v, v, y, z} S 𝓕.p
    let hq := changeOfFieldsProjection_isPredeformationCategory
      S 𝓕.p hp
    let 𝓖 : BasedCategory.{max v z, max (max u (v + 1)) y}
        (ArtinianLocalAlgCat.{u, v, v} S.Λ S.l) :=
      ⟨ChangeOfFieldsCategory S 𝓕.p, inferInstance, q⟩
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hp⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses
        𝓕 hp.cofibered))) := ⟨hS2⟩
    letI : Fact (IsPredeformationCategory 𝓖.p) := ⟨hq⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses
        𝓖 hq.cofibered))) :=
      ⟨associatedSchlessingerConditionS2_changeOfFields S 𝓕 hp hS2⟩
    letI : AddCommGroup (artinianTangentSpace S.Λ S.k
      (isomorphismClasses 𝓕 hp.cofibered)) :=
      associatedTangentSpaceAddCommGroupUnlifted 𝓕
    letI : Module S.k (artinianTangentSpace S.Λ S.k
      (isomorphismClasses 𝓕 hp.cofibered)) :=
      associatedTangentSpaceModuleUnlifted 𝓕
    letI : AddCommGroup (artinianTangentSpace S.Λ S.l
      (isomorphismClasses 𝓖 hq.cofibered)) :=
      associatedTangentSpaceAddCommGroupUnlifted 𝓖
    letI : Module S.l (artinianTangentSpace S.Λ S.l
      (isomorphismClasses 𝓖 hq.cofibered)) :=
      associatedTangentSpaceModuleUnlifted 𝓖
    TensorProduct S.k S.l
      (artinianTangentSpace S.Λ S.k
        (isomorphismClasses 𝓕 hp.cofibered)) ≃ₗ[S.l]
      artinianTangentSpace S.Λ S.l
        (isomorphismClasses 𝓖 hq.cofibered)

Deformation.tangentSpaceChangeOfFields_tmul_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/ChangeOfFieldsTangentSpace.lean, line 1859. The attribute's comment: “canonical pure-tensor formula”.

The scalar-extension equivalence sends a tangent vector tensored with 1 to its image under the canonical map on square-zero extensions and the change-of-field identification of fibrewise isomorphism classes.

public theorem tangentSpaceChangeOfFields_tmul_one
    (S : ChangeOfFieldsSituation.{u, v, v})
    (𝓕 : BasedCategory.{z, y} (ArtinianLocalAlgCat.{u, v, v} S.Λ S.k))
    (hp : IsPredeformationCategory 𝓕.p)
    (hS2 : SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses 𝓕 hp.cofibered))) :
    let q := changeOfFieldsProjection.{u, v, v, v, y, z} S 𝓕.p
    let hq := changeOfFieldsProjection_isPredeformationCategory
      S 𝓕.p hp
    let 𝓖 : BasedCategory.{max v z, max (max u (v + 1)) y}
        (ArtinianLocalAlgCat.{u, v, v} S.Λ S.l) :=
      ⟨ChangeOfFieldsCategory S 𝓕.p, inferInstance, q⟩
    let A := (artinianSquareZeroExtensionFunctor S.Λ S.k).obj
      (FGModuleCat.of S.k S.k)
    let B := (artinianSquareZeroExtensionFunctor S.Λ S.l).obj
      (FGModuleCat.of S.l S.l)
    let C := (comparisonFunctor S).functor.obj B
    let j : A ⟶ C := (canonicalDualNumberInclusion S).val
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hp⟩
    letI : Fact (SchlessingerConditionS2
      (CategoryOfElements.π (isomorphismClasses
        𝓕 hp.cofibered))) := ⟨hS2⟩
    letI : AddCommGroup (artinianTangentSpace S.Λ S.k
      (isomorphismClasses 𝓕 hp.cofibered)) :=
      associatedTangentSpaceAddCommGroupUnlifted 𝓕
    letI : Module S.k (artinianTangentSpace S.Λ S.k
      (isomorphismClasses 𝓕 hp.cofibered)) :=
      associatedTangentSpaceModuleUnlifted 𝓕
    ∀ (t : artinianTangentSpace S.Λ S.k
        (isomorphismClasses 𝓕 hp.cofibered)),
      (tangentSpaceChangeOfFields S 𝓕 hp hS2) (1 ⊗ₜ[S.k] t) =
        cast (isomorphismClasses_obj 𝓖 hq.cofibered B).symm
          (changeOfFieldsIsoClassMap S 𝓕.p B
            (cast (isomorphismClasses_obj 𝓕 hp.cofibered C)
              ((isomorphismClasses 𝓕 hp.cofibered).map j t)))
Tag 07WC, a lemma

Tag 07WC in the Stacks Project.

Deformation.existsUnique_infinitesimalAutomorphismsChangeOfFields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/InfinitesimalAutomorphism/ChangeOfFields.lean, line 1765.

Stacks Project, Tag 07WC. For a deformation category over the residue field k, the space of infinitesimal automorphisms extends by scalars along k → l to the space of infinitesimal automorphisms of the change of residue field. The equivalence is pinned by its action on dual-number automorphisms, read through a comparison of pushforwards whose base morphism has the prescribed pullback coordinates.

public theorem existsUnique_infinitesimalAutomorphismsChangeOfFields
    (S : Deformation.ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ Deformation.ArtinianLocalAlgCat.{u, max v w, v} S.Λ S.k)
    (hp : Deformation.IsDeformationCategory p)
    (x₀ : p.Fiber (residueFieldObject.{u, w, v} S.Λ S.k))
    (P : ChosenPushforwardsAt p x₀.1)
    (xₗ : (Deformation.changeOfFieldsProjection S p).Fiber
      (residueFieldObject.{u, v, w} S.Λ S.l))
    (Q : ChosenPushforwardsAt
      (Deformation.changeOfFieldsProjection S p) xₗ.1) :
    let hq := changeOfFieldsProjection_satisfiesRS
      S p hp.satisfiesRS
    letI : AddCommGroup (localizedAutomorphismFunctorTangent P) :=
      naturalLocalizedTangentAddCommGroup P hp.satisfiesRS
    letI : Module S.k (localizedAutomorphismFunctorTangent P) :=
      naturalLocalizedTangentModule P hp.satisfiesRS
    letI : AddCommGroup (localizedAutomorphismFunctorTangent Q) :=
      naturalLocalizedTangentAddCommGroup Q hq
    letI : Module S.l (localizedAutomorphismFunctorTangent Q) :=
      naturalLocalizedTangentModule Q hq
    let Uε := dualNumbersUnder (p := p) (x := x₀.1)
    let Vε := dualNumbersUnder
      (p := Deformation.changeOfFieldsProjection S p) (x := xₗ.1)
    ∃! E : TensorProduct S.k S.l
        (localizedAutomorphismFunctorTangent P) ≃ₗ[S.l]
        localizedAutomorphismFunctorTangent Q,
      ∃ (j : x₀.1 ⟶ xₗ.1.fst) (h : (P.obj Uε).1 ⟶ (Q.obj Vε).1.fst),
        let b : Uε.right ⟶
            (Deformation.comparisonFunctor.{u, v, w, max v w} S).functor.obj Vε.right :=
          eqToHom (P.obj Uε).2.symm ≫ p.map h ≫ (Q.obj Vε).1.iso.hom ≫
            (Deformation.comparisonFunctor.{u, v, w, max v w} S).functor.map (eqToHom (Q.obj Vε).2)
        (P.inclusion Uε ≫ h = j ≫ (Q.inclusion Vε).fst) ∧
        (∀ a : Uε.right,
          ((((Deformation.comparisonFunctor.{u, v, w, max v w} S).pullbackEquiv
              Vε.right) (b.hom a)).val.1).fst = algebraMap S.k S.l a.fst ∧
          ((((Deformation.comparisonFunctor.{u, v, w, max v w} S).pullbackEquiv
              Vε.right) (b.hom a)).val.1).snd =
            ULift.up (algebraMap S.k S.l a.snd.down) ∧
          (((Deformation.comparisonFunctor.{u, v, w, max v w} S).pullbackEquiv
              Vε.right) (b.hom a)).val.2 = a.fst) ∧
        (∀ t : localizedAutomorphismFunctorTangent P,
          (localizedTangentEquivKernel P t).1.asIso.hom.val ≫ h =
            h ≫ (localizedTangentEquivKernel Q
              (E (1 ⊗ₜ[S.k] t))).1.asIso.hom.val.fst)
Tag 07WD, a lemma

Tag 07WD in the Stacks Project.

Deformation.isSmooth_changeOfFields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ResidueField/Comparison.lean, line 329.

Stacks Project, Tag 07WD. A smooth morphism of categories over the Artinian algebras with residue field k remains smooth after changing the residue field to l.

public theorem isSmooth_changeOfFields
    (S : ChangeOfFieldsSituation.{u, v, w})
    {𝓕 : BasedCategory.{v₁, u₁}
      (ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)}
    {𝓖 : BasedCategory.{v₂, u₂}
      (ArtinianLocalAlgCat.{u, max x v, v} S.Λ S.k)}
    (φ : BasedFunctor 𝓕 𝓖) (hφ : IsSmooth φ) :
    IsSmooth (changeOfFieldsBasedFunctor S φ)
Tag 0DQF, a lemma

Tag 0DQF in the Stacks Project.

Deformation.exists_versal_formalObject_changeOfFields, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/VersalObject/ChangeOfFields.lean, line 1022.

Stacks Project, Tag 0DQF. For a versal formal object ξ of a category cofibered in groupoids over 𝒞_{Λ,k}, there is a Noetherian complete local Λ-algebra with residue field l, receiving a local Λ-algebra map from the base of ξ which is formally smooth for its maximal-ideal-adic topology and induces the extension l/k on residue fields, and carrying a versal formal object of the change-of-residue-field category.

public theorem exists_versal_formalObject_changeOfFields
    (S : ChangeOfFieldsSituation.{u, v, w})
    {F : Type y} [Category.{z} F]
    (p : F ⥤ ArtinianLocalAlgCat.{u, max x v w, v} S.Λ S.k)
    (hp : IsCofiberedInGroupoids p)
    (ξ : FormalObject p)
    (hξ : IsVersal hp ξ) :
    ∃ (T : CompleteLocalAlgCat.{u, max x v w, w} S.Λ S.l)
      (f : ξ.base →ₐ[S.Λ] T),
      IsLocalHom f.toRingHom ∧
        (∀ a : ξ.base,
          T.residueEquiv (residue T (f a)) =
            algebraMap S.k S.l (ξ.base.residueEquiv (residue ξ.base a))) ∧
        RingHom.FormallySmoothNAdic.{max x v w} f.toRingHom (maximalIdeal T) ∧
        ∃ ξ' : FormalObject
            (changeOfFieldsProjection.{u, v, w, max x v w} S p),
          ξ'.base = T ∧
            IsVersal (changeOfFieldsProjection_isCofiberedInGroupoids S p hp) ξ'
Sources
LeanDeformation.ChangeOfFieldsSituation · Deformation.comparisonFunctor · Deformation.changeOfFieldsProjection · Deformation.changeOfFieldsFiberInclusion_isEquivalence · Deformation.changeOfFieldsProjection_isCofiberedInGroupoids · comparisonFunctor · Deformation.changeOfFieldsIsoClassMap_bijective · Deformation.changeOfFieldsIsoClassMap_naturality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.