98.21 Infinitesimal deformations to 98.26 Algebraic spaces in the…

Section98.21 Infinitesimal deformations#

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

Tag 07Y7, a lemma

Tag 07Y7 in the Stacks Project.

Deformation.Artin.liftFunctorOfPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 348. The attribute's comment: “the functor”.

The canonical functor on lifts attached to a commutative square c ≫ a = d ≫ b in the base and a morphism F(x)|_V ⟶ y out of the chosen pullback.

public noncomputable def liftFunctorOfPullback (p : X ⥤ C) (q : Y ⥤ C)
    (hq : q.IsFiberedInGroupoids) (F : X ⥤ Y) (hF : F ⋙ q = p)
    {U' U V' V : C} (a : U' ⟶ U) (b : V ⟶ U) (c : V' ⟶ U') (d : V' ⟶ V)
    (hsq : c ≫ a = d ≫ b) (x : X) (hx : p.obj x = U)
    (y : Y) (hy : q.obj y = V) (e : q.ChoiceOfPullbacks)
    (φ : (e.pullbackFunctor b).obj (imageFiber p q F hF x hx) ⟶ ⟨y, hy⟩) :
    LiftFunctor p q F a b c d x hx y hy
      (pullbackComparison p q hq F hF b x hx y hy e φ)

Deformation.Artin.liftFunctor_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 418. The attribute's comment: “uniqueness”.

Two functors on lifts with cartesian comparison arrows over the same square are uniquely isomorphic by an isomorphism commuting with their comparison arrows.

public theorem liftFunctor_unique (p : X ⥤ C) (q : Y ⥤ C)
    (hq : q.IsFiberedInGroupoids) (F : X ⥤ Y)
    {U' U V' V : C} (a : U' ⟶ U) (b : V ⟶ U) (c : V' ⟶ U') (d : V' ⟶ V)
    (x : X) (hx : p.obj x = U) (y : Y) (hy : q.obj y = V)
    (φ : y ⟶ F.obj x)
    (L M : LiftFunctor p q F a b c d x hx y hy φ) :
    ∃! η : L.toFunctor ≅ M.toFunctor,
      ∀ t : Lift p a x hx,
        (η.hom.app t).1.1 ≫ M.comparison t = L.comparison t

Deformation.Artin.liftFunctor_comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 506. The attribute's comment: “compatibility with composition”.

The functor on lifts induced by a composite of morphisms of fibred groupoids is canonically isomorphic to the composite of the two functors on lifts. The second morphism acts over the identity square at the target of the first. At every lift, the isomorphism is the unique vertical morphism commuting with the two cartesian comparison arrows.

public noncomputable def liftFunctor_comp
    {Z : Type*} [Category Z]
    (p : X ⥤ C) (q : Y ⥤ C) (r : Z ⥤ C)
    (_hq : q.IsFiberedInGroupoids) (hr : r.IsFiberedInGroupoids)
    (F : X ⥤ Y) (G : Y ⥤ Z)
    (_hF : F ⋙ q = p) (hG : G ⋙ r = q)
    {U' U V' V : C} (a : U' ⟶ U) (b : V ⟶ U)
    (c : V' ⟶ U') (d : V' ⟶ V)
    (_hsq : c ≫ a = d ≫ b)
    (x : X) (hx : p.obj x = U)
    (y : Y) (hy : q.obj y = V)
    (z : Z) (hz : r.obj z = V)
    (φ : y ⟶ F.obj x) (ψ : z ⟶ G.obj y)
    (_hφ : q.IsHomLift b φ) (_hψ : r.IsHomLift (𝟙 V) ψ)
    (L : LiftFunctor p q F a b c d x hx y hy φ)
    (M : LiftFunctor q r G d (𝟙 V) (𝟙 V') d y hy z hz ψ)
    (N : LiftFunctor p r (F ⋙ G) a b c d x hx z hz (ψ ≫ G.map φ)) :
    {η : L.toFunctor ⋙ M.toFunctor ≅ N.toFunctor //
      ∀ t : Lift p a x hx,
        (η.hom.app t).1.1 ≫ N.comparison t =
          M.comparison (L.toFunctor.obj t) ≫ G.map (L.comparison t)}

Deformation.Artin.liftOutFunctorOfPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/InfinitesimalLiftOut.lean, line 424. The attribute's comment: “the functor, on the source's Lift(x, A'), lifts out of the base”.

Stacks 07Y7. Let F : X ⥤ Y be a 1-morphism of categories fibred in groupoids over C, let b ≫ a = d ≫ c be a commutative square of the base with a : U ⟶ U', b : V ⟶ U, c : V' ⟶ U' and d : V ⟶ V', let x lie over U, let y lie over V, and let φ be a morphism F(x)|_V ⟶ y of the fibre over V. Then there is a canonical functor from the lifts of x along a to the lifts of y along d: a lift x ⟶ x' is carried to the chosen pullback of F x' along c, whose structure arrow out of y is the factorization of y ⟶ F x ⟶ F x' through that cartesian arrow.

Over the big fppf site this is the source's Lift(x, A') ⟶ Lift(y, B') for the commutative diagram of S-algebras with rows A' ⟶ A, B' ⟶ B and columns A' ⟶ B', A ⟶ B.

public noncomputable def liftOutFunctorOfPullback (p : X ⥤ C) (q : Y ⥤ C)
    (hq : q.IsFiberedInGroupoids) (F : X ⥤ Y) (hF : F ⋙ q = p)
    {U U' V V' : C} (a : U ⟶ U') (b : V ⟶ U) (c : V' ⟶ U') (d : V ⟶ V')
    (hsq : b ≫ a = d ≫ c) (x : X) (hx : p.obj x = U)
    (y : Y) (hy : q.obj y = V) (e : q.ChoiceOfPullbacks)
    (φ : (e.pullbackFunctor b).obj (imageFiber p q F hF x hx) ⟶ ⟨y, hy⟩) :
    LiftOutFunctor p q F a b c d x hx y hy
      (pullbackComparison p q hq F hF b x hx y hy e φ)

Deformation.Artin.liftOutFunctor_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/InfinitesimalLiftOut.lean, line 554. The attribute's comment: “uniqueness, on the source's Lift(x, A'), lifts out of the base”.

Two constructions satisfying the cartesian-square specification are uniquely isomorphic by an isomorphism commuting with their comparison maps. In particular, the direct functor for a composite of morphisms of fibred groupoids agrees canonically with the composite of the induced lift functors.

public theorem liftOutFunctor_unique (p : X ⥤ C) (q : Y ⥤ C) (F : X ⥤ Y)
    {U U' V V' : C} (a : U ⟶ U') (b : V ⟶ U) (c : V' ⟶ U') (d : V ⟶ V')
    (x : X) (hx : p.obj x = U) (y : Y) (hy : q.obj y = V)
    (φ : y ⟶ F.obj x)
    (L M : LiftOutFunctor p q F a b c d x hx y hy φ) :
    ∃! η : L.toFunctor ≅ M.toFunctor,
      ∀ t : LiftOut p a x hx,
        (η.hom.app t).1.right ≫ M.comparison t = L.comparison t

Deformation.Artin.liftFunctorOfHom_comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/InfinitesimalLiftOut.lean, line 767. The attribute's comment: “compatibility with composition, on the source's Lift(x, A'), lifts out of the base”.

Stacks 07Y7, compatibility with composition. The construction is compatible with composition of 1-morphisms of categories fibred in groupoids: the functor on lifts induced by F and φ, followed by the functor on lifts induced by G and ψ over the identity square at d, is canonically isomorphic to the functor on lifts induced by F ⋙ G and the composite arrow ψ ≫ G φ, by the unique isomorphism commuting with the cartesian comparison arrows.

All three functors here are built, not assumed to satisfy the specification: each is, by definition, a functor Deformation.Artin.liftOutFunctorOfPullback builds from the datum Deformation.Artin.pullbackDatum attaches to the given arrow. The source's data are covered because a morphism out of the chosen pullback gives such an arrow, by Deformation.Artin.pullbackComparison and Deformation.Artin.pullbackComparison_isHomLift.

public noncomputable def liftFunctorOfHom_comp {Z : Type*} [Category Z]
    (p : X ⥤ C) (q : Y ⥤ C) (r : Z ⥤ C)
    (hq : q.IsFiberedInGroupoids) (hr : r.IsFiberedInGroupoids)
    (F : X ⥤ Y) (G : Y ⥤ Z) (hF : F ⋙ q = p) (hG : G ⋙ r = q)
    {U U' V V' : C} (a : U ⟶ U') (b : V ⟶ U) (c : V' ⟶ U') (d : V ⟶ V')
    (hsq : b ≫ a = d ≫ c) (x : X) (hx : p.obj x = U)
    (y : Y) (hy : q.obj y = V) (z : Z) (hz : r.obj z = V)
    (eY : q.ChoiceOfPullbacks) (eZ : r.ChoiceOfPullbacks)
    (φ : y ⟶ F.obj x) (hφ : q.IsHomLift b φ)
    (ψ : z ⟶ G.obj y) (hψ : r.IsHomLift (𝟙 V) ψ) :
    {η : (liftFunctorOfHom p q hq F hF a b c d hsq x hx y hy eY φ hφ).toFunctor ⋙
          (liftFunctorOfHom q r hr G hG d (𝟙 V) (𝟙 V') d (id_comp_square d) y hy z hz
            eZ ψ hψ).toFunctor ≅
        (liftFunctorOfHom p r hr (F ⋙ G) (comp_over_base hF hG) a b c d hsq x hx z hz eZ
          (ψ ≫ G.map φ)
          (comp_comparison_isHomLift q r F G hG b x y z φ hφ ψ hψ)).toFunctor //
      ∀ t : LiftOut p a x hx,
        (η.hom.app t).1.right ≫
            (liftFunctorOfHom p r hr (F ⋙ G) (comp_over_base hF hG) a b c d hsq x hx z hz eZ
              (ψ ≫ G.map φ)
              (comp_comparison_isHomLift q r F G hG b x y z φ hφ ψ hψ)).comparison t =
          (liftFunctorOfHom q r hr G hG d (𝟙 V) (𝟙 V') d (id_comp_square d) y hy z hz
              eZ ψ hψ).comparison
            ((liftFunctorOfHom p q hq F hF a b c d hsq x hx y hy eY φ hφ).toFunctor.obj t) ≫
            G.map ((liftFunctorOfHom p q hq F hF a b c d hsq x hx y hy eY φ hφ).comparison t)}

Tag 07Y9, a lemma

Tag 07Y9 in the Stacks Project.

Deformation.Artin.exists_infComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/ActionOnLifts/InfComparison.lean, line 760. The attribute's comment: “part (1), the comparison of Inf_x(I) with Inf(x'/x)”.

Stacks 07Y9 part (1). For 𝒳 satisfying (RS*), a deformation situation A' → A with square-zero kernel I whose source lies in the chosen site, and a lift x' of x over Spec A', the value of the A-linear functor Inf_x at I is isomorphic, as a group, to the infinitesimal automorphisms of x'.

public noncomputable def exists_infComparison (hRS : SatisfiesRSStar B S hS p hp)
    (Inf : InfinitesimalAutomorphismFunctorData A B S hS toS hA p x hx hp)
    (A' : Type u) [CommRing A'] (hA' : B.Contains (Spec (.of A')))
    (toS' : B.obj hA' ⟶ B.obj hS) (q : A' →+* A) (hq : Function.Surjective q)
    (hsq : RingHom.ker q ^ 2 = ⊥)
    (g : algebraOver A B S hS toS hA ⟶ (Over.mk toS' : BigFppfOver B S hS))
    (hg : B.inclusion.map g.left = Spec.map (CommRingCat.ofHom q))
    (x' : (Under.post p).Fiber (Under.mk (eqToHom hx ≫ g))) :
    InfComparisonData A B S hS toS hA p x hx hp Inf A' hA' toS' q hq hsq g x'

Deformation.Artin.exists_actionOnLifts, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/ActionOnLifts/LiftAction.lean, line 547. The attribute's comment: “part (2)(b), the action of T_x(I) on the lifts over A'”.

Stacks 07Y9 part (2)(b). The difference-transport action of the tangent module T_x(I) on the isomorphism classes of lifts of x over a square-zero deformation A' → A with kernel I. Every orbit map is bijective, so the action is simply transitive whenever there is a lift.

public noncomputable def exists_actionOnLifts
    (hp : p.IsFiberedInGroupoids)
    (hRS : SatisfiesRSStar B S hS p hp)
    (A' : Type u) [CommRing A']
    (hA' : B.Contains (Spec (.of A')))
    (toS' : B.obj hA' ⟶ B.obj hS)
    (q : A' →+* A)
    (hq : Function.Surjective q)
    (hsq : (RingHom.ker q) ^ 2 = ⊥)
    (g : algebraOver A B S hS toS hA ⟶
      (Over.mk toS' : BigFppfOver B S hS))
    (hg : B.inclusion.map g.left = Spec.map (CommRingCat.ofHom q)) :
    ActionOnLiftsData A B S hS toS hA p x hx
      (tangentFunctor A B S hS toS hA p x hx hp hRS)
      A' hA' toS' q hq hsq g

Deformation.Artin.exists_infinitesimalAutomorphismFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/AutomorphismFunctor.lean, line 902. The attribute's comment: “part (1), the A-linear functor Inf_x on trivial square-zero extensions”.

For 𝒳 satisfying (RS*), the infinitesimal automorphisms of the trivial deformations of x over the trivial square-zero extensions A[M] are the underlying sets of an A-linear functor of M.

public theorem exists_infinitesimalAutomorphismFunctor (hRS : SatisfiesRSStar B S hS p hp) :
    Nonempty (InfinitesimalAutomorphismFunctorData A B S hS toS hA p x hx hp)

Deformation.Artin.exists_tangentFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TangentFunctor.lean, line 1356. The attribute's comment: “part (2)(a), the A-linear tangent functor T_x”.

Stacks 07Y9 part (2)(a), the tangent functor. For 𝒳 satisfying (RS*), the isomorphism classes of lifts of x over the trivial square-zero extensions A[M] are the underlying sets of an A-linear functor of M.

public theorem exists_tangentFunctor (hp : p.IsFiberedInGroupoids)
    (hRS : SatisfiesRSStar B S hS p hp) :
    Nonempty (TangentFunctorData A B S hS toS hA p x hx)

Tag 07YA, a remark

Tag 07YA in the Stacks Project.

Deformation.Artin.isLinearMap_tangentBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/BaseChangeLinear.lean, line 473. The attribute's comment: “the A-linear map T_x(M) → T_y(N)”.

Remark 07YA for the tangent functor. For a ring map f : A ⟶ C, the restriction y = x|_{Spec C} and an f-semilinear map M ⟶ N of coefficients, the induced map T_x(M) ⟶ T_y(N) is A-linear, where T_y(N) is viewed as an A-module by restriction of scalars along f.

public theorem isLinearMap_tangentBaseChangeMap {M : SiteModule A B} {N : SiteModule C B}
    (ψ : M.obj ⟶ (ModuleCat.restrictScalars f).obj N.obj) :
    letI : Module A ((Ty.functor.obj N : Type (max (u + 1) v w))) := Module.compHom _ f
    IsLinearMap A
      (tangentBaseChangeMap f B S hS toS hA toSC hC hf p x y hx hy φ₀ hφ₀ hp Tx Ty ψ)

Deformation.Artin.isLinearMap_infBaseChangeMap_tangentBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/DeformationSituationMorphism.lean, line 389. The attribute's comment: “the A-linear maps Inf_x(M) → Inf_y(N) and T_x(M) → T_y(N) induced by pullback”.

Stacks 07YA, the maps. Let 𝒳 satisfy (RS*), let f : A ⟶ C be a map of S-algebras, y = x|_{Spec C} (the arrow φ₀ : y ⟶ x over Spec C ⟶ Spec A), M an A-module, N a C-module and ψ : M ⟶ N an A-linear map. The pullback functor on lifts along Spec C[N] ⟶ Spec A[M] induces maps Inf_x(M) ⟶ Inf_y(N) and T_x(M) ⟶ T_y(N) on the functors of Stacks 07Y9, and both are A-linear (with A acting on the targets through f). That the maps are induced by the pullback functor is the transition relation each of them realizes: Deformation.Artin.IsSiteInfinitesimalAutomorphismBaseChange and Deformation.Artin.IsSiteSquareZeroLiftBaseChange. The statement holds for every choice of the functors Inf_x, Inf_y, T_x, T_y of Stacks 07Y9.

public theorem isLinearMap_infBaseChangeMap_tangentBaseChangeMap
    (hRS : SatisfiesRSStar B S hS p hp)
    (Tx : TangentFunctorData A B S hS toS hA p x hx)
    (Ty : TangentFunctorData C B S hS toSC hC p y hy)
    {M : SiteModule A B} {N : SiteModule C B}
    (ψ : M.obj ⟶ (ModuleCat.restrictScalars f).obj N.obj) :
    letI : Module A (Inf'.functor.obj N : Type w) := Module.compHom _ f
    letI : Module A ((Ty.functor.obj N : Type (max (u + 1) v w))) := Module.compHom _ f
    IsLinearMap A (infBaseChangeMap f B S hS toS hA toSC hC hf p x y hx hy φ₀ hφ₀ hp Inf Inf'
        ψ) ∧
      (∀ a, IsSiteInfinitesimalAutomorphismBaseChange B S hS toS hA toSC hC p x y hx hy φ₀ f ψ hp
        (Inf.autEquiv M a)
        (Inf'.autEquiv N (infBaseChangeMap f B S hS toS hA toSC hC hf p x y hx hy φ₀ hφ₀ hp
          Inf Inf' ψ a))) ∧
      IsLinearMap A (tangentBaseChangeMap f B S hS toS hA toSC hC hf p x y hx hy φ₀ hφ₀ hp
        Tx Ty ψ) ∧
      (∀ a, IsSiteSquareZeroLiftBaseChange B S hS toS hA toSC hC p x y hx hy φ₀ f ψ
        (Tx.liftEquiv M a)
        (Ty.liftEquiv N (tangentBaseChangeMap f B S hS toS hA toSC hC hf p x y hx hy φ₀ hφ₀ hp
          Tx Ty ψ a)))

Deformation.Artin.infComparison_restrict_and_action_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/DeformationSituationMorphism.lean, line 703. The attribute's comment: “the two commutative squares for a morphism of deformation situations”.

Stacks 07YA, the two squares. Let 𝒳 satisfy (RS*) and let (y, C' → C) ⟶ (x, A' → A) be a morphism of deformation situations: f' : A' → C' over f : A → C, compatibly with the structure morphisms to S, and φ₀ : y ⟶ x over Spec C ⟶ Spec A. Let I = Ker(A' → A), J = Ker(C' → C), with the map I ⟶ J induced by f'.

• For a lift x' of x to A' and its restriction y' to C' (any lift of y with an arrow y' ⟶ x' over Spec C' ⟶ Spec A' compatible with φ₀), the square Inf_x(I) ⟶ Inf(x'/x) ⟶ Inf(y'/y) = Inf_x(I) ⟶ Inf_y(J) ⟶ Inf(y'/y) commutes.
• The square T_x(I) × Lift(x, A') ⟶ Lift(x, A') ⟶ Lift(y, C') = T_x(I) × Lift(x, A') ⟶ T_y(J) × Lift(y, C') ⟶ Lift(y, C') commutes.

The horizontal maps are the comparisons and the actions of Stacks 07Y9, the vertical ones the maps of Remark 07YA and the pullback of lifts along Spec C' ⟶ Spec A'. All the data of Stacks 07Y9 (the functors Inf, T, the comparisons and the actions) are arbitrary: each is pinned by its geometric difference, which is what the proof restricts.

public theorem infComparison_restrict_and_action_restrict (hRS : SatisfiesRSStar B S hS p hp)
    (Infx : InfinitesimalAutomorphismFunctorData A B S hS toS hA p x hx hp)
    (Infy : InfinitesimalAutomorphismFunctorData C B S hS toSC hC p y hy hp)
    (x' : (Under.post p).Fiber (Under.mk (eqToHom hx ≫ gA)))
    (y' : (Under.post p).Fiber (Under.mk (eqToHom hy ≫ gC)))
    (φ : y'.1.right ⟶ x'.1.right)
    (hφ : p.IsHomLift (deformationSituationMap B S hS hA' toS' hC' toSC' f' hf') φ)
    (hφc : y'.1.hom ≫ φ = φ₀ ≫ x'.1.hom)
    (Cx : InfComparisonData A B S hS toS hA p x hx hp Infx A' hA' toS' q hq hsq gA x')
    (Cy : InfComparisonData C B S hS toSC hC p y hy hp Infy C' hC' toSC' qC hqC hsqC gC y')
    (Tx : TangentFunctorData A B S hS toS hA p x hx)
    (Ty : TangentFunctorData C B S hS toSC hC p y hy)
    (Dx : ActionOnLiftsData A B S hS toS hA p x hx Tx A' hA' toS' q hq hsq gA)
    (Dy : ActionOnLiftsData C B S hS toSC hC p y hy Ty C' hC' toSC' qC hqC hsqC gC) :
    letI : Module A (RingHom.ker q) := Stacks.Smooth.kerModule hq hsq
    letI : Module C (RingHom.ker qC) := Stacks.Smooth.kerModule hqC hsqC
    (∀ a : (Infx.functor.obj ⟨ModuleCat.of A (RingHom.ker q), Cx.kernelIsSiteModule⟩ : Type w),
      Cy.equiv (infBaseChangeMap f B S hS toS hA toSC hC
          (specMap_comp_eq_of_deformationSituation f B S hS toS hA toSC hC hA' toS' q gA hgA hC'
          toSC' qC gC hgC f' hff hf') p x y hx hy φ₀ hφ₀ hp Infx Infy
          (M := ⟨ModuleCat.of A (RingHom.ker q), Cx.kernelIsSiteModule⟩)
          (N := ⟨ModuleCat.of C (RingHom.ker qC), Cy.kernelIsSiteModule⟩)
          (kernelBaseChange hq hsq hqC hsqC hff) a) =
        liftEndRestrict p hp φ₀ φ hφ hφc (Cx.equiv a)) ∧
    (∀ (a : (Tx.functor.obj ⟨ModuleCat.of A (RingHom.ker q), Dx.kernelIsSiteModule⟩ : Type _))
      (z : liftClassesOver A B S hS toS hA p x hx gA),
      liftClassesRestrict p hp φ₀ _ hφ₀
          (algebraOverMap_comp_deformationSituation f B S hS toS hA toSC hC hA' toS' q gA hgA
            hC' toSC' qC gC hgC f' hff hf') (Dx.action a z) =
        Dy.action (tangentBaseChangeMap f B S hS toS hA toSC hC
          (specMap_comp_eq_of_deformationSituation f B S hS toS hA toSC hC hA' toS' q gA hgA hC'
          toSC' qC gC hgC f' hff hf') p x y hx hy φ₀ hφ₀ hp Tx Ty
          (M := ⟨ModuleCat.of A (RingHom.ker q), Dx.kernelIsSiteModule⟩)
          (N := ⟨ModuleCat.of C (RingHom.ker qC), Dy.kernelIsSiteModule⟩)
          (kernelBaseChange hq hsq hqC hsqC hff) a)
          (liftClassesRestrict p hp φ₀ _ hφ₀
            (algebraOverMap_comp_deformationSituation f B S hS toS hA toSC hC hA' toS' q gA hgA
              hC' toSC' qC gC hgC f' hff hf') z))

Deformation.Artin.existsUnique_infAutBaseChangeHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/InfAutBaseChangeMap.lean, line 672. The attribute's comment: “the companion A-linear map Inf_x(M) -> Inf_y(N) along a ring map A -> C, and its uniqueness. The relation Deformation.Artin.IsInfinitesimalAutomorphismBaseChange, its single-valuedness and its bijectivity at a bijective map of coefficients are in the library, but without a map realizing it all of them would be conditional: the relation asks for a cartesian arrow between the two TRIVIAL lifts, and the pullback of the trivial lift of x along Spec C[N] -> Spec A[M] is only isomorphic to the trivial lift of y, not equal to it. What is added is that arrow -- Deformation.Artin.trivialLiftComparison, built from the presentation of each trivial lift as a pullback along the retraction Spec A[M] -> Spec A -- the conjugation by it, and the A-linearity of the resulting map, which is the remark's assertion. CARRIED, as an extra hypothesis the source does not make: x and y are Deformation.Artin.ChartedObjects, so Spec A -> S and Spec C -> S factor through a fixed affine open Spec L of S -- inherited from Deformation.Artin.IsInfinitesimalAutomorphismBaseChange, the relation this realizes; the geometric half is chart-free, as Deformation.Artin.underFiberConjugate. (RS*) is needed only for uniqueness, through the commutativity of the infinitesimal automorphisms; the two functors Inf_x, Inf_y are arbitrary members of Deformation.Artin.InfinitesimalAutomorphismFunctorData. NOT COVERED: the two commuting squares of the source, for which see the note on Deformation.Artin.existsUnique_tangentBaseChange”.

Stacks 07YA on infinitesimal automorphisms. Let x be an object of a category fibred in groupoids over the big fppf site of S lying over Spec A, let A ⟶ C be a ring map and let y ⟶ x be a morphism lying over Spec C ⟶ Spec A, so that y = x|_{Spec C}. For M ∈ Mod_A, N ∈ Mod_C and an A-linear map M ⟶ N there is exactly one A-linear map Inf_x(M) ⟶ Inf_y(N) carrying each infinitesimal automorphism of the trivial lift of x over Spec A[M] to its conjugate along a cartesian arrow over Spec C[N] ⟶ Spec A[M].

x and y are Deformation.Artin.ChartedObjects, so each of Spec A ⟶ S, Spec C ⟶ S factors through a fixed affine open Spec Λ ⊆ S: that is an extra hypothesis, which the source does not make. It is inherited from Deformation.Artin.IsInfinitesimalAutomorphismBaseChange, the relation on infinitesimal automorphisms that this theorem realizes, and it is what makes the result directly usable by the Stacks 07YT statements that take a map realizing that relation as a hypothesis. The geometric content is chart-free: the comparison of the trivial lifts and the conjugation along it are Deformation.Artin.underFiberConjugate, stated for an arbitrary category fibred in groupoids and an arbitrary commuting square of its base.

(RS) is used only for the uniqueness half. The two functors enter as arbitrary members of Deformation.Artin.InfinitesimalAutomorphismFunctorData rather than as the ones Stacks 07Y9 (1) produces from (RS).

NOT COVERED: the two commuting squares of the source; see the note on Deformation.Artin.existsUnique_tangentBaseChange.

public theorem existsUnique_infAutBaseChangeHom (hRS : SatisfiesRSStar B S hS p hp)
    {M : SiteModule P.ring B} {N : SiteModule Q.ring B}
    (ψ : M.obj ⟶ (ModuleCat.restrictScalars f).obj N.obj) :
    ∃! σ : ↥(F.functor.obj M) →ₛₗ[f] ↥(G.functor.obj N),
      ∀ θ, IsInfinitesimalAutomorphismBaseChange hp h f ψ (F.autEquiv M θ)
        (G.autEquiv N (σ θ))

Deformation.Artin.existsUnique_tangentBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/TangentPullback.lean, line 291. The attribute's comment: “tangent_base_change”.

Stacks 07YA on tangent modules. Let x be an object over Spec A of a category fibred in groupoids over the big fppf site of S, let f : A ⟶ C be a homomorphism of S-algebras and let y ⟶ x be a morphism lying over Spec C ⟶ Spec A, so that y = x|_{Spec C}. For M ∈ Mod_A, N ∈ Mod_C and an A-linear map M ⟶ N there is exactly one A-linear map T_x(M) ⟶ T_y(N) — written as an f-semilinear map — carrying each class of lifts of x over Spec A[M] to the class of its pullback along Spec C[N] ⟶ Spec A[M].

The tangent functors T_x, T_y are arbitrary members of Deformation.Artin.TangentFunctorData, which (RS*) supplies by Stacks 07Y9 (2)(a).

public theorem existsUnique_tangentBaseChange {M : SiteModule A B} {N : SiteModule C B}
    (ψ : M.obj ⟶ (ModuleCat.restrictScalars f).obj N.obj) :
    ∃! τ : ↥(F.functor.obj M) →ₛₗ[f] ↥(G.functor.obj N),
      ∀ z, G.liftEquiv N (τ z) = liftClassPullback f hf hp φ hφ ψ (F.liftEquiv M z)

Declarations registered for the tag:

• Deformation.Artin.liftFunctorOfPullback, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 607 (StacksFrontier): “pullback_of_lifts”.
• Deformation.Artin.liftFunctor_unique, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 608 (StacksFrontier): “pullback_of_lifts”.

Tag 07YB, a remark

Tag 07YB in the Stacks Project.

Deformation.Artin.compositionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 801. The attribute's comment: “composition_map”.

Composition with relative infinitesimal automorphisms on both sides of a morphism of lifts.

public noncomputable def compositionMap
    (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x) :
    ((infinitesimalAutomorphisms hp t₁ × (t₁ ⟶ t₂)) ×
      infinitesimalAutomorphisms hp t₂) → (t₁ ⟶ t₂)

Deformation.Artin.leftCompositionAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 859. The attribute's comment: “groupoid_actions”.

The left action of relative infinitesimal automorphisms of the source lift on morphisms of lifts, by inverse precomposition.

public noncomputable def leftCompositionAction
    (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x)
    (a : infinitesimalAutomorphisms hp t₁) (f : t₁ ⟶ t₂) : t₁ ⟶ t₂

Deformation.Artin.rightCompositionAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 868. The attribute's comment: “groupoid_actions”.

The right action of relative infinitesimal automorphisms of the target lift on morphisms of lifts, by inverse postcomposition.

public noncomputable def rightCompositionAction
    (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x)
    (f : t₁ ⟶ t₂) (b : infinitesimalAutomorphisms hp t₂) : t₁ ⟶ t₂

Deformation.Artin.leftComposition_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 992. The attribute's comment: “groupoid_actions”.

The identity automorphism acts trivially on the left.

public theorem leftComposition_one (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x) (f : t₁ ⟶ t₂) :
    leftCompositionAction hp t₁ t₂ 1 f = f

Deformation.Artin.leftComposition_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 1000. The attribute's comment: “groupoid_actions”.

The left action is compatible with multiplication of automorphisms.

public theorem leftComposition_mul (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x)
    (a b : infinitesimalAutomorphisms hp t₁) (f : t₁ ⟶ t₂) :
    leftCompositionAction hp t₁ t₂ (a * b) f =
      leftCompositionAction hp t₁ t₂ a (leftCompositionAction hp t₁ t₂ b f)

Deformation.Artin.rightComposition_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 1012. The attribute's comment: “groupoid_actions”.

The identity automorphism acts trivially on the right.

public theorem rightComposition_one (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x) (f : t₁ ⟶ t₂) :
    rightCompositionAction hp t₁ t₂ f 1 = f

Deformation.Artin.rightComposition_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 1020. The attribute's comment: “groupoid_actions”.

The right action is compatible with multiplication of automorphisms.

public theorem rightComposition_mul (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x)
    (a b : infinitesimalAutomorphisms hp t₂) (f : t₁ ⟶ t₂) :
    rightCompositionAction hp t₁ t₂ (rightCompositionAction hp t₁ t₂ f a) b =
      rightCompositionAction hp t₁ t₂ f (a * b)

Deformation.Artin.leftComposition_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 1042. The attribute's comment: “groupoid_actions”.

At each morphism of lifts, the orbit map for the left action is a bijection.

public theorem leftComposition_bijective
    (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x)
    (f : t₁ ⟶ t₂) :
    Function.Bijective (fun a : infinitesimalAutomorphisms hp t₁ =>
      leftCompositionAction hp t₁ t₂ a f)

Deformation.Artin.rightComposition_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 1062. The attribute's comment: “groupoid_actions”.

At each morphism of lifts, the orbit map for the right action is a bijection.

public theorem rightComposition_bijective
    (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x)
    (f : t₁ ⟶ t₂) :
    Function.Bijective (fun b : infinitesimalAutomorphisms hp t₂ =>
      rightCompositionAction hp t₁ t₂ f b)

Deformation.Artin.InfComparisonData.actions_agree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/ActionOnLiftsRestriction.lean, line 440. The attribute's comment: “actions on Mor(x', x'') agree via Inf(x'/x) = Inf_x(I) = Inf(x''/x)”.

Stacks 07YB. Let 𝒳 satisfy (RS*), let (x, A' → A) be a deformation situation with kernel I, and let x', x'' be lifts of x to Spec A'. Composition gives a map Inf(x'/x) × Mor(x', x'') × Inf(x''/x) → Mor(x', x''), and since the lifts form a groupoid it defines, at every morphism, simply transitive actions of Inf(x'/x) (by precomposition) and of Inf(x''/x) (by postcomposition). Let C' and C'' be the comparisons of Stacks 07Y9, Inf_x(I) ≅ Inf(x'/x) and Inf_x(I) ≅ Inf(x''/x). Then the two actions agree via these identifications: C'(a) ≫ f = f ≫ C''(a) for every a ∈ Inf_x(I) and every morphism f : x' ⟶ x''. In particular Inf_x(I) acts on Mor(x', x''), and the action is simply transitive as soon as Mor(x', x'') is nonempty: every orbit map is a bijection.

The agreement holds for every pair of comparisons in the sense of Deformation.Artin.InfComparisonData, which pins a comparison geometrically. The proof shows that this pin determines the comparison and is natural for isomorphisms of lifts (Deformation.Artin.IsGeometricInfDifference.conj), using (RS*) and the commutativity of Inf(x'/x) and of Inf_x(I).

public theorem InfComparisonData.actions_agree (hRS : SatisfiesRSStar B S hS p hp)
    (Inf : InfinitesimalAutomorphismFunctorData A B S hS toS hA p x hx hp)
    (A' : Type u) [CommRing A'] (hA' : B.Contains (Spec (.of A')))
    (toS' : B.obj hA' ⟶ B.obj hS) (q : A' →+* A) (hq : Function.Surjective q)
    (hsq : RingHom.ker q ^ 2 = ⊥)
    (g : algebraOver A B S hS toS hA ⟶ (Over.mk toS' : BigFppfOver B S hS))
    (hg : B.inclusion.map g.left = Spec.map (CommRingCat.ofHom q))
    {x' x'' : (Under.post p).Fiber (Under.mk (eqToHom hx ≫ g))}
    (C' : InfComparisonData A B S hS toS hA p x hx hp Inf A' hA' toS' q hq hsq g x')
    (C'' : InfComparisonData A B S hS toS hA p x hx hp Inf A' hA' toS' q hq hsq g x'') :
    letI := Stacks.Smooth.kerModule hq hsq
    (∀ f : x' ⟶ x'', Function.Bijective (fun α : x' ⟶ x' => α ≫ f)) ∧
      (∀ f : x' ⟶ x'', Function.Bijective (fun β : x'' ⟶ x'' => f ≫ β)) ∧
      (∀ (a : Inf.functor.obj ⟨ModuleCat.of A (RingHom.ker q), C'.kernelIsSiteModule⟩)
        (f : x' ⟶ x''), C'.equiv a ≫ f = f ≫ C''.equiv a) ∧
      (∀ f : x' ⟶ x'', C'.equiv 0 ≫ f = f) ∧
      (∀ (a b : Inf.functor.obj ⟨ModuleCat.of A (RingHom.ker q), C'.kernelIsSiteModule⟩)
        (f : x' ⟶ x''), C'.equiv (a + b) ≫ f = C'.equiv a ≫ C'.equiv b ≫ f) ∧
      (∀ f : x' ⟶ x'', Function.Bijective
        (fun a : Inf.functor.obj ⟨ModuleCat.of A (RingHom.ker q), C'.kernelIsSiteModule⟩ =>
          C'.equiv a ≫ f))

Deformation.Artin.infinitesimalAutTransport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/LiftCompositionActions.lean, line 143. The attribute's comment: “actions_agree”.

The identification of the two groups of relative infinitesimal automorphisms. A morphism of lifts identifies the relative infinitesimal automorphisms of its source with those of its target, by conjugation.

public noncomputable def infinitesimalAutTransport
    (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x) (f : t₁ ⟶ t₂) :
    infinitesimalAutomorphisms hp t₁ ≃* infinitesimalAutomorphisms hp t₂

Deformation.Artin.leftCompositionAction_eq_rightCompositionAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/LiftCompositionActions.lean, line 199. The attribute's comment: “actions_agree”.

The two actions agree. The left action of a relative infinitesimal automorphism of the source lift on a morphism of lifts is the right action, on the same morphism, of the corresponding relative infinitesimal automorphism of the target lift.

public theorem leftCompositionAction_eq_rightCompositionAction
    (hp : Deformation.IsCofiberedInGroupoids p)
    (t₁ t₂ : Deformation.Lift p g x)
    (a : infinitesimalAutomorphisms hp t₁) (f : t₁ ⟶ t₂) :
    leftCompositionAction hp t₁ t₂ a f =
      rightCompositionAction hp t₁ t₂ f (infinitesimalAutTransport hp t₁ t₂ f a)

Tag 07YE, a remark

Tag 07YE in the Stacks Project.

Deformation.Artin.IsShortExactSequence, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 626. The attribute's comment: “short_exact_sequence_of_deformation_situations”.

A composable triple of deformation situations is short exact if its kernel sequence 0 → I₃ → I₂ → I₁ → 0 is exact. The maps of situations run in the opposite direction to the ring homomorphisms f₂₁ : A₂' → A₁' and f₃₂ : A₃' → A₂'.

public abbrev IsShortExactSequence {A₁ : Type u₁} {A₂ : Type u₂} {A₃ : Type u₃} {A : Type u}
    [CommRing A₁] [CommRing A₂] [CommRing A₃] [CommRing A]
    (q₁ : A₁ →+* A) (q₂ : A₂ →+* A) (q₃ : A₃ →+* A)
    (f₂₁ : A₂ →+* A₁) (f₃₂ : A₃ →+* A₂) : Prop

Deformation.Artin.exists_factorization_through_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 639. The attribute's comment: “factorization_through_a”.

The composite A₃' → A₂' → A₁' in a short exact sequence of deformation situations factors through their common quotient A.

public theorem exists_factorization_through_base
    {A₁ : Type u₁} {A₂ : Type u₂} {A₃ : Type u₃} {A : Type u}
    [CommRing A₁] [CommRing A₂] [CommRing A₃] [CommRing A]
    (q₁ : A₁ →+* A) (q₂ : A₂ →+* A) (q₃ : A₃ →+* A)
    (f₂₁ : A₂ →+* A₁) (f₃₂ : A₃ →+* A₂)
    (h : IsShortExactSequence q₁ q₂ q₃ f₂₁ f₃₂) :
    ∃ g : A →+* A₁, g.comp q₃ = f₂₁.comp f₃₂

Deformation.Artin.splitExtensionRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal.lean, line 689. The attribute's comment: “canonical_isomorphism”.

The canonical isomorphism A₁ = A[I₁]. In a short exact sequence of deformation situations, the splitting of q₁ produced by exists_factorization_through_base exhibits A₁ as the trivial square-zero extension of A by its kernel I₁ = ker q₁.

noncomputable def splitExtensionRingEquiv
    {A₁ : Type u₁} {A₂ : Type u₂} {A₃ : Type u₃} {A : Type u}
    [CommRing A₁] [CommRing A₂] [CommRing A₃] [CommRing A]
    {q₁ : A₁ →+* A} {q₂ : A₂ →+* A} {q₃ : A₃ →+* A}
    {f₂₁ : A₂ →+* A₁} {f₃₂ : A₃ →+* A₂}
    (h : IsShortExactSequence q₁ q₂ q₃ f₂₁ f₃₂) :
    letI := kerModule q₁ h.1
    letI : Module Aᵐᵒᵖ (RingHom.ker q₁) :=
      Module.compHom _ (RingHom.fromOpposite (RingHom.id A) fun _ _ => Commute.all _ _)
    letI : IsCentralScalar A (RingHom.ker q₁) := ⟨fun _ _ => rfl⟩
    A₁ ≃+* TrivSqZeroExt A (RingHom.ker q₁)

Tag 0DNN, a lemma

Tag 0DNN in the Stacks Project.

Deformation.Artin.injective_twoFibreInfProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/Functoriality/InfTransportSixTerm.lean, line 578. The attribute's comment: “exactness of the six-term sequence at Inf_w(M), i.e. injectivity of Inf_w(M) → Inf_x(M) ⊕ Inf_z(M), which is what exactness of 0 → Inf_w(M) → ⋯ says (see exact_zero_iff_injective). Also constructed in this module, and used to state that map, are the four functoriality maps of Remark 07YA out of the 2-fibre product and out of 𝒳 (infLinearMapOfOneMorphism, tangentLinearMapOfOneMorphism) and the zeros of Inf_x(M) and T_x(M) (autEquiv_zero, liftEquiv_zero). The sequence with all five of its maps and the exactness at all five of its places is Deformation.Artin.twoFibre_sixTermExact in StacksFrontier.Deformation.Artin.Infinitesimal.TwoFibreInfExact.”.

Exactness of the six-term sequence of Stacks 0DNN at Inf_w(M): an infinitesimal automorphism of the trivial deformation of w is determined by its two components. Each component is read off through the comparison of the trivial deformation of the component with the image of the trivial deformation of w, and that comparison is invertible because the lifts form a category fibred in groupoids; a morphism of the 2-fibre product is determined by its two components.

public theorem injective_twoFibreInfProj (A : Type u) [CommRing A] (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) (toS : Spec (.of A) ⟶ S)
    (hA : B.Contains (Spec (.of A)))
    {𝒳 : Type v₁} [Category.{w₁} 𝒳] {𝒵 : Type v₂} [Category.{w₂} 𝒵]
    {𝒴 : Type v₃} [Category.{w₃} 𝒴]
    (p𝒳 : 𝒳 ⥤ BigFppfOver B S hS) (p𝒵 : 𝒵 ⥤ BigFppfOver B S hS)
    (p𝒴 : 𝒴 ⥤ BigFppfOver B S hS) (P : 𝒳 ⥤ 𝒴) (Q : 𝒵 ⥤ 𝒴)
    (hP : P ⋙ p𝒴 = p𝒳) (hQ : Q ⋙ p𝒴 = p𝒵)
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒵 : p𝒵.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (w : TwoFibreProductOver p𝒳 p𝒵 p𝒴 P Q)
    (hw : (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q).obj w = algebraOver A B S hS toS hA)
    (InfW : InfinitesimalAutomorphismFunctorData A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
        (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ))
    (InfX : InfinitesimalAutomorphismFunctorData A B S hS toS hA p𝒳 w.x (w.hx.trans hw) h𝒳)
    (InfZ : InfinitesimalAutomorphismFunctorData A B S hS toS hA p𝒵 w.y (w.hy.trans hw) h𝒵)
    (M : SiteModule A B) :
    Function.Injective (LinearMap.prod
        (infLinearMapOfOneMorphism A B S hS toS hA
            (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒳 (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴
              P Q) TwoFibreProductOver.fst_comp_eq w hw (TwoFibreProductOver.isFiberedInGroupoids p𝒳
              p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ) h𝒳
            InfW InfX M)
        (infLinearMapOfOneMorphism A B S hS toS hA
            (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒵 (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴
              P Q) TwoFibreProductOver.snd_comp_eq w hw (TwoFibreProductOver.isFiberedInGroupoids p𝒳
              p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ) h𝒵
            InfW InfZ M))

Deformation.Artin.twoFibreInfSideMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TwoFibreBoundary.lean, line 581. The attribute's comment: “the map Inf_z(M) → Inf_y(M) of the six-term sequence -- the map of Remark 07YA induced by q, followed by the transport along the comparison isomorphism of w. The sequence and its exactness are Deformation.Artin.twoFibre_sixTermExact.”.

The 𝒵-side map Inf_z(M) ⟶ Inf_y(M) of the six-term sequence of Stacks 0DNN: the map induced by q on infinitesimal automorphisms, followed by the identification of the invariants of q z with those of y = p x along the comparison isomorphism of w.

public def twoFibreInfSideMap
    (InfZ : InfinitesimalAutomorphismFunctorData A B S hS toS hA p𝒵 w.y
      (twoFibreSndOver A B S hS toS hA w hw) h𝒵)
    (InfY' : InfinitesimalAutomorphismFunctorData A B S hS toS hA p𝒴 (P.obj w.x)
      (twoFibreFstImageOver A B S hS toS hA hP w hw) h𝒴)
    (M : SiteModule A B) : InfZ.functor.obj M →ₗ[A] InfY'.functor.obj M

Deformation.Artin.twoFibreTangentSideMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TwoFibreBoundary.lean, line 612. The attribute's comment: “the map T_z(M) → T_y(M) of the six-term sequence -- the map of Remark 07YA induced by q, followed by the transport along the comparison isomorphism of w. The sequence and its exactness are Deformation.Artin.twoFibre_sixTermExact.”.

The 𝒵-side map T_z(M) ⟶ T_y(M) of the six-term sequence of Stacks 0DNN: the map induced by q on tangent spaces, followed by the identification of the invariants of q z with those of y = p x along the comparison isomorphism of w.

public def twoFibreTangentSideMap
    (TZ : TangentFunctorData A B S hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS hA w hw))
    (TY : TangentFunctorData A B S hS toS hA p𝒴 (P.obj w.x)
      (twoFibreFstImageOver A B S hS toS hA hP w hw))
    (M : SiteModule A B) : TZ.functor.obj M →ₗ[A] TY.functor.obj M

Deformation.Artin.boundaryLinearMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TwoFibreBoundary.lean, line 675. The attribute's comment: “the boundary map δ : Inf_y(M) → T_w(M) of the six-term sequence, as an A-linear map: an automorphism α of the trivial deformation y' of y = p x over A[M] is sent to the deformation (x', z', p x' → y' --α--> y' → q z') of w, exactly as in the source. The sequence and its exactness at all five places are Deformation.Artin.twoFibre_sixTermExact.”.

The boundary map δ : Inf_y(M) ⟶ T_w(M) of Stacks 0DNN, as an A-linear map.

public def boundaryLinearMap (M : SiteModule A B) :
    InfY.functor.obj M →ₗ[A] TW.functor.obj M

Deformation.Artin.tangentProj_twoFibreBoundaryMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TwoFibreBoundary.lean, line 733. The attribute's comment: “one inclusion of exactness at T_w(M): the composite Inf_y(M) → T_w(M) → T_x(M) ⊕ T_z(M) of the six-term sequence is zero, the two components of δ(α) being by construction the trivial deformations of x and of z. The exactness assertion itself is Deformation.Artin.exact_boundary_tangentProj, and the whole sequence is Deformation.Artin.twoFibre_sixTermExact.”.

The six-term sequence of Stacks 0DNN is a complex at T_w(M): the boundary map followed by the pair of projections to the tangent spaces of x and of z is zero, because the two components of δ(α) are the trivial deformations.

public theorem tangentProj_twoFibreBoundaryMap_eq_zero
    (TX : TangentFunctorData A B S hS toS hA p𝒳 w.x (twoFibreFstOver A B S hS toS hA w hw))
    (TZ : TangentFunctorData A B S hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS hA w hw))
    (M : SiteModule A B) (α : InfY.functor.obj M) :
    LinearMap.prod
        (tangentLinearMapOfOneMorphism A B S hS toS hA
          (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒳
          (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 P Q) TwoFibreProductOver.fst_comp_eq w hw TW TX
          h𝒳 M)
        (tangentLinearMapOfOneMorphism A B S hS toS hA
          (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒵
          (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 P Q) TwoFibreProductOver.snd_comp_eq w hw TW TZ
          h𝒵 M)
        (boundaryLinearMap A B S hS toS hA hP hQ h𝒳 h𝒵 h𝒴 w hw InfY TW M α) = 0

Deformation.Artin.twoFibre_sixTermExact_of_satisfiesRSStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/TwoFibreSixTerm.lean, line 61.

Stacks 0DNN. Let P : 𝒳 ⟶ 𝒴 and Q : 𝒵 ⟶ 𝒴 be 1-morphisms of categories fibred in groupoids over the big fppf site of S, and assume 𝒳, 𝒴, 𝒵 satisfy (RS*). Let w be an object of 𝒲 = 𝒳 ×_𝒴 𝒵 over Spec A, with components x, z and y = P x. For every A-module M the six-term sequence

0 ⟶ Inf_w(M) ⟶ Inf_x(M) ⊕ Inf_z(M) ⟶ Inf_y(M) --δ--> T_w(M) ⟶ T_x(M) ⊕ T_z(M) ⟶ T_y(M)

of A-modules is exact. Here Inf_? and T_? are the A-linear functors that (RS*) produces (Stacks 07Y9), for w through (RS*) for 𝒲 (Stacks 0CXQ); the horizontal maps are those of Remark 07YA and δ is Deformation.Artin.boundaryLinearMap. Exactness is stated as injectivity of the first map together with four Function.Exacts.

public theorem twoFibre_sixTermExact_of_satisfiesRSStar
    (hRS𝒳 : SatisfiesRSStar B S hS p𝒳 h𝒳) (hRS𝒵 : SatisfiesRSStar B S hS p𝒵 h𝒵)
    (hRS𝒴 : SatisfiesRSStar B S hS p𝒴 h𝒴) (M : SiteModule A B) :
    Function.Injective (LinearMap.prod (infLinearMapOfOneMorphism A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒳 (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 P Q)
      TwoFibreProductOver.fst_comp_eq w hw (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳
      h𝒵 h𝒴 hP hQ) h𝒳 (infinitesimalAutomorphismFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒳 w.x (twoFibreFstOver A B S hS toS hA w
      hw) h𝒳 hRS𝒳) M) (infLinearMapOfOneMorphism A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒵 (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 P Q)
      TwoFibreProductOver.snd_comp_eq w hw (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳
      h𝒵 h𝒴 hP hQ) h𝒵 (infinitesimalAutomorphismFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS hA w
      hw) h𝒵 hRS𝒵) M)) ∧ Function.Exact (LinearMap.prod (infLinearMapOfOneMorphism A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒳 (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 P Q)
      TwoFibreProductOver.fst_comp_eq w hw (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳
      h𝒵 h𝒴 hP hQ) h𝒳 (infinitesimalAutomorphismFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒳 w.x (twoFibreFstOver A B S hS toS hA w
      hw) h𝒳 hRS𝒳) M) (infLinearMapOfOneMorphism A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒵 (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 P Q)
      TwoFibreProductOver.snd_comp_eq w hw (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳
      h𝒵 h𝒴 hP hQ) h𝒵 (infinitesimalAutomorphismFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS hA w
      hw) h𝒵 hRS𝒵) M)) (LinearMap.coprod (infLinearMapOfOneMorphism A B S hS toS hA p𝒳 p𝒴 P hP w.x
      (twoFibreFstOver A B S hS toS hA w hw) h𝒳 h𝒴 (infinitesimalAutomorphismFunctor A B S hS toS hA
      p𝒳 w.x (twoFibreFstOver A B S hS toS hA w hw) h𝒳 hRS𝒳) (infinitesimalAutomorphismFunctor A B S
      hS toS hA p𝒴 (P.obj w.x) (twoFibreFstImageOver A B S hS toS hA hP w hw) h𝒴 hRS𝒴) M)
      (-(twoFibreInfSideMap A B S hS toS hA hP hQ h𝒵 h𝒴 w hw (infinitesimalAutomorphismFunctor A B S
      hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS hA w hw) h𝒵 hRS𝒵)
      (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒴 (P.obj w.x) (twoFibreFstImageOver A B S
      hS toS hA hP w hw) h𝒴 hRS𝒴) M))) ∧ Function.Exact (LinearMap.coprod (infLinearMapOfOneMorphism
      A B S hS toS hA p𝒳 p𝒴 P hP w.x (twoFibreFstOver A B S hS toS hA w hw) h𝒳 h𝒴
      (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒳 w.x (twoFibreFstOver A B S hS toS hA w
      hw) h𝒳 hRS𝒳) (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒴 (P.obj w.x)
      (twoFibreFstImageOver A B S hS toS hA hP w hw) h𝒴 hRS𝒴) M) (-(twoFibreInfSideMap A B S hS toS
      hA hP hQ h𝒵 h𝒴 w hw (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒵 w.y (twoFibreSndOver
      A B S hS toS hA w hw) h𝒵 hRS𝒵) (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒴 (P.obj
      w.x) (twoFibreFstImageOver A B S hS toS hA hP w hw) h𝒴 hRS𝒴) M))) (boundaryLinearMap A B S hS
      toS hA hP hQ h𝒳 h𝒵 h𝒴 w hw (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒴 (P.obj w.x)
      (twoFibreFstImageOver A B S hS toS hA hP w hw) h𝒴 hRS𝒴) (tangentFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵)) M) ∧
      Function.Exact (boundaryLinearMap A B S hS toS hA hP hQ h𝒳 h𝒵 h𝒴 w hw
      (infinitesimalAutomorphismFunctor A B S hS toS hA p𝒴 (P.obj w.x) (twoFibreFstImageOver A B S
      hS toS hA hP w hw) h𝒴 hRS𝒴) (tangentFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵)) M)
      (LinearMap.prod (tangentLinearMapOfOneMorphism A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒳 (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 P Q)
      TwoFibreProductOver.fst_comp_eq w hw (tangentFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (tangentFunctor A B S hS toS hA p𝒳 w.x (twoFibreFstOver A B S hS toS hA w hw) h𝒳 hRS𝒳) h𝒳 M)
      (tangentLinearMapOfOneMorphism A B S hS toS hA (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴
      P Q) p𝒵 (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 P Q) TwoFibreProductOver.snd_comp_eq w hw
      (tangentFunctor A B S hS toS hA (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (tangentFunctor A B S hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS hA w hw) h𝒵 hRS𝒵) h𝒵 M))
      ∧ Function.Exact (LinearMap.prod (tangentLinearMapOfOneMorphism A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) p𝒳 (TwoFibreProductOver.fst p𝒳 p𝒵 p𝒴 P Q)
      TwoFibreProductOver.fst_comp_eq w hw (tangentFunctor A B S hS toS hA
      (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (tangentFunctor A B S hS toS hA p𝒳 w.x (twoFibreFstOver A B S hS toS hA w hw) h𝒳 hRS𝒳) h𝒳 M)
      (tangentLinearMapOfOneMorphism A B S hS toS hA (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴
      P Q) p𝒵 (TwoFibreProductOver.snd p𝒳 p𝒵 p𝒴 P Q) TwoFibreProductOver.snd_comp_eq w hw
      (tangentFunctor A B S hS toS hA (TwoFibreProductOver.structureFunctor p𝒳 p𝒵 p𝒴 P Q) w hw
      (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒵 p𝒴 P Q h𝒳 h𝒵 h𝒴 hP hQ)
      (twoFibreProductOver_satisfiesRSStar B S hS p𝒳 p𝒴 p𝒵 P Q h𝒳 h𝒴 h𝒵 hP hQ hRS𝒳 hRS𝒴 hRS𝒵))
      (tangentFunctor A B S hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS hA w hw) h𝒵 hRS𝒵) h𝒵 M))
      (LinearMap.coprod (tangentLinearMapOfOneMorphism A B S hS toS hA p𝒳 p𝒴 P hP w.x
      (twoFibreFstOver A B S hS toS hA w hw) (tangentFunctor A B S hS toS hA p𝒳 w.x (twoFibreFstOver
      A B S hS toS hA w hw) h𝒳 hRS𝒳) (tangentFunctor A B S hS toS hA p𝒴 (P.obj w.x)
      (twoFibreFstImageOver A B S hS toS hA hP w hw) h𝒴 hRS𝒴) h𝒴 M) (-(twoFibreTangentSideMap A B S
      hS toS hA hP hQ h𝒴 w hw (tangentFunctor A B S hS toS hA p𝒵 w.y (twoFibreSndOver A B S hS toS
      hA w hw) h𝒵 hRS𝒵) (tangentFunctor A B S hS toS hA p𝒴 (P.obj w.x) (twoFibreFstImageOver A B S
      hS toS hA hP w hw) h𝒴 hRS𝒴) M)))

Tag 0D18, a remark

Tag 0D18 in the Stacks Project.

Deformation.Artin.tangentSpace_deformationCategory_linearEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/DeformationSpaceComparison.lean, line 995. The attribute's comment: “tangent spaces”.

Stacks Project, Tag 0D18, tangent spaces. For a category fibred in groupoids over the big fppf site of a locally Noetherian scheme satisfying (RS*), the tangent space of the deformation category of a finite-type field-valued point is the value of the tangent functor of Tag 07Y9 at the rank-one vector space. Both sides carry the unique linear structure compatible with finite products (Tag 06I6), and the identification carries the class of a deformation to the class of the corresponding lift.

public theorem tangentSpace_deformationCategory_linearEquiv
    (B : BigFppfSite.{u}) (S : Scheme.{u}) [IsLocallyNoetherian S] (hS : B.Contains S)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ S) (toS : Spec (.of k) ⟶ S)
    (hk : B.Contains (Spec (.of k)))
    (hfin : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hqc : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    {X : Type v} [Category.{w} X] (p : X ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hRS : SatisfiesRSStar B S hS p hp) (x₀ : X)
    (hx₀ : (p ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hx : p.obj x₀ = algebraOver k B S hS toS hk) :
    let D := predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀
    let 𝓕 := BasedCategory.ofFunctor D.projection
    let hD : Deformation.IsDeformationCategory D.projection :=
      isDeformationCategory_predeformationCategory_of_satisfiesRSStar B S hS p hp hRS iΛ x₀
        hx₀ hfin hqc
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses 𝓕 hD.predeformation.cofibered))) :=
      ⟨schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory 𝓕 hD⟩
    let M : SiteModule k B := (fgSiteModule B hk).obj (FGModuleCat.of k k)
    let L := tangentFunctor k B S hS toS hk p x₀ hx hp hRS
    ∃ e : artinianTangentSpace Λ k (isomorphismClasses 𝓕 hD.predeformation.cofibered) ≃ₗ[k]
        L.functor.obj M,
      ∀ z : D.projection.Fiber ((artinianSquareZeroExtensionFunctor Λ k).obj
          (FGModuleCat.of k k)),
        ∃ y : (Under.post p).Fiber
            (Under.mk (eqToHom hx ≫ squareZeroArrow k B S hS toS hk M)),
          L.liftEquiv M (e (classOf 𝓕 hD.predeformation.cofibered z)) = Quotient.mk _ y ∧
            ∃ (η : y.1.right ≅ (D.objects z.1).point)
              (hbase : p.obj y.1.right = p.obj (D.objects z.1).point),
              p.map η.hom = eqToHom hbase ∧
                y.1.hom ≫ η.hom = (D.objects z.1).arrow

Deformation.Artin.infinitesimalAutomorphisms_deformationCategory_linearEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/DeformationSpaceComparison.lean, line 1417. The attribute's comment: “infinitesimal automorphisms”.

Stacks Project, Tag 0D18, infinitesimal automorphisms. For a category fibred in groupoids over the big fppf site of a locally Noetherian scheme satisfying (RS*), the infinitesimal automorphisms of the deformation category of a finite-type field-valued point are the value of the infinitesimal automorphism functor of Tag 07Y9 at the rank-one vector space, by a k-linear equivalence carrying an automorphism to the endomorphism of the trivial deformation given by the same arrow.

public theorem infinitesimalAutomorphisms_deformationCategory_linearEquiv
    (B : BigFppfSite.{u}) (S : Scheme.{u}) [IsLocallyNoetherian S] (hS : B.Contains S)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ S) (toS : Spec (.of k) ⟶ S)
    (hk : B.Contains (Spec (.of k)))
    (hfin : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hqc : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    {X : Type v} [Category.{w} X] (p : X ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hRS : SatisfiesRSStar B S hS p hp) (x₀ : X)
    (hx₀ : (p ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hx : p.obj x₀ = algebraOver k B S hS toS hk) :
    let D := predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀
    let hD : Deformation.IsDeformationCategory D.projection :=
      isDeformationCategory_predeformationCategory_of_satisfiesRSStar B S hS p hp hRS iΛ x₀
        hx₀ hfin hqc
    let A₀ := (artinianSquareZeroExtensionFunctor Λ k).obj (FGModuleCat.of k PUnit.{u + 1})
    let Aε := (artinianSquareZeroExtensionFunctor Λ k).obj (FGModuleCat.of k k)
    let g : A₀ ⟶ Aε := (artinianSquareZeroExtensionFunctor Λ k).map 0
    let e : Aε ⟶ A₀ := (artinianSquareZeroExtensionFunctor Λ k).map 0
    let M : SiteModule k B := (fgSiteModule B hk).obj (FGModuleCat.of k k)
    let L := infinitesimalAutomorphismFunctor k B S hS toS hk p x₀ hx hp hRS
    let t := trivialDeformation k B S hS toS hk p x₀ hx hp M
    ∃ (hge : g ≫ e = 𝟙 A₀) (z₀ : D.projection.Fiber A₀) (zε : D.projection.Fiber Aε)
      (i : z₀.1 ⟶ zε.1) (hi : D.projection.IsHomLift g i)
      (η : (D.objects zε.1).point ≅ t.1.right),
      let G := ↥(infinitesimalAutomorphismsAlongSplitPair hD.predeformation.cofibered g e hge
        i hi)
      (D.objects zε.1).arrow ≫ η.hom = t.1.hom ∧
        ∃ hA : AddCommGroup G,
          letI : AddCommGroup G := hA
          ∃ hM : Module k G,
            letI : Module k G := hM
            ∃ E : G ≃ₗ[k] (L.functor.obj M : Type w),
              ∀ a : G, (L.autEquiv M (E a)).1.right =
                η.inv ≫ (D.morphisms zε.1 zε.1 a.val.asIso.hom.val).arrow ≫ η.hom

Deformation.Artin.localizedAutomorphismTangent_deformationCategory_linearEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/InfinitesimalAutomorphismsComparison.lean, line 120. The attribute's comment: “infinitesimal automorphisms”.

Stacks Project, Tag 0D18, infinitesimal automorphisms. For a category fibred in groupoids over the big fppf site of a locally Noetherian scheme satisfying (RS*), the infinitesimal automorphisms of the deformation category of a finite-type field-valued point x₀, with their natural vector space structure of Tag 06JX, are the value at the rank-one vector space of the infinitesimal automorphism functor of Tag 07Y9: there is a k-linear equivalence E, which is conjugation by any isomorphism η of the object underlying the dual-number pushforward with the trivial deformation of x₀ that is compatible with the arrows out of x₀ and lies over the comparison of the two presentations of the dual numbers; such an η exists.

public theorem localizedAutomorphismTangent_deformationCategory_linearEquiv
    (B : BigFppfSite.{u}) (S : Scheme.{u}) [IsLocallyNoetherian S] (hS : B.Contains S)
    {Λ k : Type u} [CommRing Λ] [Field k] [Algebra Λ k]
    (iΛ : Spec (.of Λ) ⟶ S) (toS : Spec (.of k) ⟶ S)
    (hk : B.Contains (Spec (.of k)))
    (hfin : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hqc : QuasiCompact (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    {X : Type v} [Category.{w} X] (p : X ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hRS : SatisfiesRSStar B S hS p hp) (x₀ : X)
    (hx₀ : (p ⋙ Over.post B.inclusion).obj x₀ =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ k)) ≫ iΛ))
    (hx : p.obj x₀ = algebraOver k B S hS toS hk)
    (y : (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection.Fiber
      (residueFieldObject.{u, u, u} Λ k))
    (P : ChosenPushforwardsAt
      (predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀).projection y.1) :
    let D := predeformationCategory iΛ (p ⋙ Over.post B.inclusion) x₀ hx₀
    let hD : Deformation.IsDeformationCategory D.projection :=
      isDeformationCategory_predeformationCategory_of_satisfiesRSStar B S hS p hp hRS iΛ x₀
        hx₀ hfin hqc
    letI := naturalLocalizedTangentAddCommGroup P hD.satisfiesRS
    letI := naturalLocalizedTangentModule P hD.satisfiesRS
    let M : SiteModule k B := (fgSiteModule B hk).obj (FGModuleCat.of k k)
    let L := infinitesimalAutomorphismFunctor k B S hS toS hk p x₀ hx hp hRS
    let t := trivialDeformation k B S hS toS hk p x₀ hx hp M
    let yε := P.obj (dualNumbersUnder (p := D.projection) (x := y.1))
    let IsCompatible : ((D.objects yε.1).point ≅ t.1.right) → Prop := fun η =>
      (D.objects yε.1).arrow ≫ η.hom = t.1.hom ∧
        eqToHom (congrArg Over.left (D.objects yε.1).base).symm ≫
            ((p ⋙ Over.post B.inclusion).map η.hom).left ≫ eqToHom (congrArg Over.left
              (trivialDeformation_right_post B S hS iΛ toS hk p hp x₀ hx₀ hx
                (FGModuleCat.of k k))) =
            Spec.map (CommRingCat.ofHom (CategoryTheory.inv
              (dualNumbersUnderHom (p := D.projection) (x := y.1)) ≫
                eqToHom (yε.2.symm.trans (D.object_projection yε.1))).hom.toRingHom)
    ∃ E : localizedAutomorphismFunctorTangent P ≃ₗ[k] (L.functor.obj M : Type w),
      (∃ η, IsCompatible η) ∧
        ∀ η, IsCompatible η → ∀ a, (L.autEquiv M (E a)).1.right =
          η.inv ≫ (D.morphisms yε.1 yε.1 (localizedTangentEquivKernel P a).1.asIso.hom.1).arrow ≫
            η.hom

Tag 07YC, a remark

Tag 07YC in the Stacks Project.

Deformation.Artin.canonicalDeformationElement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/CanonicalElement.lean, line 151. The attribute's comment: “canonical_deformation_element”.

Stacks 07YC. The canonical element of T_x(Ω_{A/Λ}) attached to the universal derivation d : A → Ω_{A/Λ}.

public def canonicalDeformationElement (baseMap : Spec (.of Λ) ⟶ S)
    (baseFactorization :
      Spec.map (CommRingCat.ofHom (algebraMap Λ A)) ≫ baseMap = toS) :
    CanonicalDeformationData Λ A B S hS toS hA p x hx hp hRS hΩ

Deformation.Artin.canonicalTangentMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/CanonicalElement.lean, line 259. The attribute's comment: “the tangent-space map”.

Stacks 07YC. The map on tangent spaces induced by the family x over Spec A: a Λ-derivation of A with values in k, written as an A-linear map Ω_{A/Λ} → k, carries the canonical element to an element of T_x(k).

public def canonicalTangentMap (θ : Ω[A⁄Λ] →ₗ[A] k) :
    (tangentFunctor A B S hS toS hA p x hx hp hRS).functor.obj
      (⟨ModuleCat.of A k, hk⟩ : SiteModule A B)

Deformation.Artin.canonicalTangentMap_eq_familyTangentMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/CanonicalElementInducedTangentMap.lean, line 743. The attribute's comment: “the canonical element gives the tangent map T𝓕_{U,k,u₀} ⟶ T𝓕_{𝒳,k,x₀} induced by x: θ ↦ T_x(θ)(x_can)”.

Stacks 07YC: the canonical element produces the map on tangent spaces induced by x.

Let 𝒳 be a category fibred in groupoids over the big fppf site of a locally Noetherian S, satisfying (RS*), let Spec Λ ⊂ S be an affine open through which U = Spec A ⟶ S factors, with A of finite type over Λ, let x be an object of 𝒳 over U, and let k be the residue field of a finite type point u₀ of U, with x₀ = x|_{u₀}. Then:

• T_x(k) is the tangent space of 𝓕_{𝒳,k,x₀}: the k-linear identification e below is the one of Stacks 0D18 composed with the (RS*) identification T_x(k) = T_{x₀}(k) across A[k] = A ×_k k[k], pinned down by sending the class of a deformation to the class of the corresponding lift;
• T𝓕_{U,k,u₀} = Der_Λ(A, k) = Hom_A(Ω_{A/Λ}, k) (Stacks 06IC), by Deformation.Artin.derivationTangentEquiv;
• through these identifications the map on tangent spaces T𝓕_{U,k,u₀} ⟶ T𝓕_{𝒳,k,x₀} induced by the object x over U (Deformation.Artin.familyTangentMap) is θ ↦ T_x(θ)(x_can).

The field k is only required to be an A-algebra with Spec k ⟶ U of finite type, which includes the residue field at a finite type point. The containments of the spectra of the square-zero extensions in the chosen big site are size conditions on the site.

public theorem canonicalTangentMap_eq_familyTangentMap [IsLocallyNoetherian S]
    [IsOpenImmersion baseMap] [Algebra.FiniteType Λ A]
    (hpt : LocallyOfFiniteType (Spec.map (CommRingCat.ofHom (algebraMap A k)))) :
    letI : p.IsFibered := hp.isFibered
    let x₀ := (familyMorphism A B S hS toS hA p x hx hp).obj (residuePoint A k B S hS toS hA hAk)
    let D := predeformationCategory baseMap (p ⋙ Over.post B.inclusion) x₀
      (familyMorphism_residuePoint_base Λ A k B S hS toS hA hAk baseMap baseFactorization p x hx
        hp)
    let 𝓕 := BasedCategory.ofFunctor D.projection
    let hD : IsDeformationCategory D.projection :=
      isDeformationCategory_predeformationCategory_of_satisfiesRSStar B S hS p hp hRS baseMap x₀
        (familyMorphism_residuePoint_base Λ A k B S hS toS hA hAk baseMap baseFactorization p x
          hx hp)
        (residue_locallyOfFiniteType Λ A k S toS baseMap baseFactorization hpt)
        (residue_quasiCompact Λ k S baseMap)
    letI : Fact (IsPredeformationCategory 𝓕.p) := ⟨hD.predeformation⟩
    letI : Fact (SchlessingerConditionS2 (CategoryOfElements.π
      (isomorphismClasses 𝓕 hD.predeformation.cofibered))) :=
      ⟨schlessingerConditionS2_isomorphismClasses_of_isDeformationCategory 𝓕 hD⟩
    let M : SiteModule k B := ⟨ModuleCat.of k k, hkk⟩
    let L := tangentFunctor k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk p
      x₀ (familyMorphism_residuePoint_obj A k B S hS toS hA hAk p x hx hp) hp hRS
    ∃ e : artinianTangentSpace Λ k (isomorphismClasses 𝓕 hD.predeformation.cofibered) ≃ₗ[k]
        ((tangentFunctor A B S hS toS hA p x hx hp hRS).functor.obj
          (⟨ModuleCat.of A k, hk⟩ : SiteModule A B) : Type max (u + 1) v w),
      (∀ z : D.projection.Fiber ((artinianSquareZeroExtensionFunctor Λ k).obj
          (FGModuleCat.of k k)),
        ∃ y : (Under.post p).Fiber (Under.mk (eqToHom
            (familyMorphism_residuePoint_obj A k B S hS toS hA hAk p x hx hp) ≫
              squareZeroArrow k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS)
                hAk M)),
          L.liftEquiv M (residueTangentEquiv A k B S hS toS hA p x hx hp hRS hk hAk hkk
              (e (classOf 𝓕 hD.predeformation.cofibered z))) = Quotient.mk _ y ∧
            ∃ (η : y.1.right ≅ (D.objects z.1).point)
              (hbase : p.obj y.1.right = p.obj (D.objects z.1).point),
              p.map η.hom = eqToHom hbase ∧ y.1.hom ≫ η.hom = (D.objects z.1).arrow) ∧
      ∀ θ : Ω[A⁄Λ] →ₗ[A] k,
        e (familyTangentMap Λ A k B S hS toS hA hAk baseMap baseFactorization p x hx hp
            (derivationTangentEquiv Λ A k B S hS toS hA hAk baseMap baseFactorization θ)) =
          (tangentFunctor A B S hS toS hA p x hx hp hRS).functor.map
            (⟨ModuleCat.ofHom θ⟩ : differentialsSiteModule Λ A B hΩ ⟶
              (⟨ModuleCat.of A k, hk⟩ : SiteModule A B))
            (canonicalDeformationElement Λ A B S hS toS hA p x hx hp hRS hΩ baseMap
              baseFactorization).element

Deformation.Artin.residueSquareZeroRing_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/CanonicalElementTangentSpace.lean, line 251. The attribute's comment: “the fibre product A[k] = A ×_k k[k]”.

Stacks 07YC: the square A[k] = A ×_k k[k]. For a ring map A ⟶ k to a field, the trivial square-zero extension A[k] is the fibre product of A and k[k] over k. The orientation is the one in which condition (RS*) reads a square: the pullback corner is A[k], and the square-zero surjection is the projection k[k] ⟶ k appearing as the fourth map.

This is Deformation.Artin.squareZeroRingBaseMap_isPullback at the residue map, with Deformation.Artin.coeffCompare — the identity of k, comparing the two module structures the A-algebra k puts on itself — as the semilinear bijection of coefficients.

public theorem residueSquareZeroRing_isPullback :
    IsPullback (CommRingCat.ofHom (TrivSqZeroExt.fstHom A A (ModuleCat.of A k)).toRingHom)
      (CommRingCat.ofHom (squareZeroRingBaseMap (algebraMap A k) (coeffCompare A k)
        (coeffCompare_smul A k)))
      (CommRingCat.ofHom (algebraMap A k))
      (CommRingCat.ofHom (TrivSqZeroExt.fstHom k k (ModuleCat.of k k)).toRingHom)

Deformation.Artin.residueTangentEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/CanonicalElementTangentSpace.lean, line 430. The attribute's comment: “T_x(k) is the tangent space of the deformation functor at the residue field”.

Stacks 07YC: T_x(k) is the tangent space at the residue field. By (RS*) and the square A[k] = A ×_k k[k], the tangent module T_x(k) of x at the coefficient module k is the tangent module T_{x₀}(k) of the restriction x₀ = x|_{Spec k} at the rank-one k-vector space, which by Stacks 0D18 is the tangent space of the deformation category 𝓕_{𝒳,k,x₀}.

This is an identification of k-vector spaces: on the left the structure Deformation.Artin.residueTangentModule that the A-linear tangent functor of Stacks 07Y9 puts on its value at the algebra coefficient k, on the right the structure the rank-one k-vector space gives the value of the tangent functor over k, which is the one Stacks 0D18 transports from the deformation category. Additivity is Deformation.Artin.residueTangentBaseChange_map_add and the scalar action is Deformation.Artin.residueTangentBaseChange_map_smul.

The identification itself is the (RS*) comparison of lift classes Deformation.Artin.canonicalFieldBaseChangeEquiv transported along the identifications T_x(M) = Lift(x, A[M]) of the tangent functor data of Stacks 07Y9 on both sides, which is Deformation.Artin.tangentBaseChangeEquiv at the residue map.

public def residueTangentEquiv :
    letI : p.IsFibered := hp.isFibered
    ((tangentFunctor A B S hS toS hA p x hx hp hRS).functor.obj
        (⟨ModuleCat.of A k, hk⟩ : SiteModule A B) : Type max (u + 1) v w) ≃ₗ[k]
      ((tangentFunctor k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk p
          (((Functor.chosenPullbacks p).pullbackFunctor
            (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
              (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj
                ⟨x, hx⟩).1
          (((Functor.chosenPullbacks p).pullbackFunctor
            (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
              (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj
                ⟨x, hx⟩).2
          hp hRS).functor.obj
        (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B) : Type max (u + 1) v w)

Deformation.Artin.canonicalTangentMapRestrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Infinitesimal/CanonicalElementTangentSpace.lean, line 509. The attribute's comment: “θ ↦ T_x(θ)(x_can) in T_x(k) = T𝓕_{𝒳,k,x₀}”.

Stacks 07YC: the canonical element produces the map on tangent spaces. A tangent vector of Spec A at the point with residue field k — that is, an element of Der_Λ(A, k) = Hom_A(Ω_{A/Λ}, k), the identification being Stacks 00RO (KaehlerDifferential.linearMapEquivDerivation) — is carried to T_x(θ)(x_can), read in T_{x₀}(k), which is the tangent space T𝓕_{𝒳,k,x₀} by Stacks 0D18.

public def canonicalTangentMapRestrict (θ : Ω[A⁄Λ] →ₗ[A] k) :
    letI : p.IsFibered := hp.isFibered
    ((tangentFunctor k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk p
        (((Functor.chosenPullbacks p).pullbackFunctor
          (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
            (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj ⟨x, hx⟩).1
        (((Functor.chosenPullbacks p).pullbackFunctor
          (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
            (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj ⟨x, hx⟩).2
        hp hRS).functor.obj
      (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B) : Type max (u + 1) v w)

Sources

• Section 98.21, Tag 07Y6
• AxiomMath/Stacks at 5ed82d14

LeanDeformation.Artin.liftFunctorOfPullback · Deformation.Artin.liftFunctor_unique · Deformation.Artin.liftFunctor_comp · Deformation.Artin.liftOutFunctorOfPullback · Deformation.Artin.liftOutFunctor_unique · Deformation.Artin.liftFunctorOfHom_comp · Deformation.Artin.exists_infComparison · Deformation.Artin.exists_actionOnLifts

Section98.22 Obstruction theories#

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

Tag 07YG, a definition

Tag 07YG in the Stacks Project.

Deformation.Artin.ObstructionTheory, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/Theory.lean, line 232.

An obstruction theory for a category fibred in groupoids over the big fppf site of S: a linear functor of obstruction modules at every object over the spectrum of an S-algebra mapping into an affine open, functorial in the triple (x, A, M), together with an obstruction element for every deformation situation whose vanishing is equivalent to the existence of a lift.

public structure ObstructionTheory (hp : p.IsFiberedInGroupoids)

Tag 0CYF, a lemma

Tag 0CYF in the Stacks Project.

Deformation.Artin.isOpenVersality_of_obstructionTheory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Versality/OpennessObstruction.lean, line 90.

Let S be a locally Noetherian scheme and let 𝒳 be a category fibred in groupoids over the big fppf site of S. Assume

1. the diagonal Δ : 𝒳 ⟶ 𝒳 × 𝒳 is representable by algebraic spaces,
2. 𝒳 has (RS*),
3. 𝒳 is limit preserving,
4. there exists an obstruction theory O,
5. for an object x of 𝒳 over Spec A and A-modules Mₙ, n ≥ 1, (a) T_x(∏ Mₙ) = ∏ T_x(Mₙ), and (b) 𝒪_x(∏ Mₙ) ⟶ ∏ 𝒪_x(Mₙ) is injective.

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

theorem isOpenVersality_of_obstructionTheory [IsLocallyNoetherian S]
    (𝒳 : CatFiberedInGroupoids.{u, u, u + 1, u + 1} (AlgebraicGeometry.BigFppfOver B S hS))
    (h1 : AlgebraicGeometry.Stack.HasRepresentableDiagonal B S hS 𝒳)
    (h2 : SatisfiesRSStar B S hS 𝒳.val.p 𝒳.isFiberedInGroupoids)
    (h3 : IsLimitPreserving.{u, u, u, u + 1, u} B S hS 𝒳)
    (O : ObstructionTheory B S hS 𝒳.val.p 𝒳.isFiberedInGroupoids)
    (h5a : TangentPreservesCountableProducts B S hS 𝒳.val.p 𝒳.isFiberedInGroupoids h2)
    (h5b : O.InjectiveOnCountableProducts) :
    ∀ (U : Over S), LocallyOfFiniteType U.hom →
      ∀ (x : 𝒳.val.obj) (hx : (𝒳.val.p ⋙ Over.post B.inclusion).obj x = U) (u₀ : U.left),
        IsFiniteTypePoint u₀ →
        IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u₀ x hx →
        ∃ W : U.left.Opens, u₀ ∈ W.1 ∧
          ∀ u ∈ W.1, IsFiniteTypePoint u →
            IsVersalAt U (𝒳.val.p ⋙ Over.post B.inclusion) u x hx

Tag 07YH, an example

Tag 07YH in the Stacks Project.

Deformation.Artin.SectionsSheaf.exists_obstructionTheory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/SectionsObstructionTheory.lean, line 787.

Stacks 07YH. Let S = Spec Λ with Λ Noetherian, W → S a morphism of schemes and 𝓕 a quasi-coherent 𝒪_W-module flat over S. The category fibred in groupoids 𝒳 attached to F : T/S ↦ H⁰(W_T, 𝓕_T) has an obstruction theory (Stacks 07YG) whose obstruction modules at an object x over Spec A are 𝒪_x(M) = H¹(W_A, 𝓕_A ⊗_A M) (affineObstruction, i.e. obstructionFunctor, as a functor of M), and whose obstruction element at a deformation situation (x, A' → A) is the image of x under the boundary map H⁰(W_A, 𝓕_A) → H¹(W_A, 𝓕_A ⊗_A I) of 0 → 𝓕_A ⊗_A I → 𝓕_{A'} → 𝓕_A → 0.

theorem exists_obstructionTheory [IsNoetherianRing Λ]
    (hF : AlgebraicGeometry.IsFlatOver g.toLRSHom.toShHom F) :
    ∃ θ : ObstructionTheory B (Spec (.of Λ)) hS (sectionsFibredCategory g F B hS)
        (Functor.IsFiberedInSets.isFiberedInGroupoids _),
      ∃ e : ∀ P, (θ.obstruction P).functor ≅ (affineObstruction g F P).functor,
        ∀ P t, (e P).hom.app t.kernelObj (θ.obs P t) = sectionsObstructionClass B hS g F hF P t

Tag 07YI, an example

Tag 07YI in the Stacks Project.

Deformation.Artin.KeyExample.objEquivTuple, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 197. The attribute's comment: “x corresponds to a tuple (a_1, …, a_n) killing J”.

An object x of 𝒳 = (Sch/Spec R)_{fppf} over Spec A, that is a Λ-algebra map R → A with R = Λ[x_1, …, x_n]/J, is the same datum as a tuple (a_1, …, a_n) of elements of A with f(a_1, …, a_n) = 0 in A for every f ∈ J.

noncomputable def objEquivTuple :
    ((MvPolynomial (Fin n) Λ ⧸ J) →ₐ[Λ] A) ≃
      {a : Fin n → A // ∀ f ∈ J, MvPolynomial.aeval a f = 0}

Deformation.Artin.KeyExample.exists_isHomotopyEquiv_nl_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 228. The attribute's comment: “NL_{R/Λ} is canonically homotopy equivalent to J/J² → ⊕ R dx_i”. References: SGA 6 0 (4.3), “partial”; SGA 6 0 (4.4), “special case”.

The naive cotangent complex NL_{R/Λ} is canonically homotopy equivalent to the two-term complex J/J² → ⊕_{i = 1, …, n} R dx_i attached to the presentation Λ[x_1, …, x_n] → R: there is a morphism of presentations onto the canonical presentation, and the induced chain map is a homotopy equivalence. This is Stacks 00S1(4) read at the presentation of the key example; presentation_ker identifies the conormal module of presentation J with J/J².

theorem exists_isHomotopyEquiv_nl_canonical :
    ∃ φ : P.Hom (NaiveCotangent.canonicalGenerators Λ R),
      NaiveCotangent.IsHomotopyEquiv
        (NaiveCotangent.nlMap P (NaiveCotangent.canonicalGenerators Λ R) φ)

Deformation.Artin.KeyExample.exists_basis_nl_cotangentSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 241. The attribute's comment: “the degree-0 term is the free module ⊕_{i = 1, …, n} R dx_i”.

The degree-0 term of the two-term complex of the key example is the free R-module ⊕_{i = 1, …, n} R dx_i on the classes dx_i of the variables.

theorem exists_basis_nl_cotangentSpace :
    ∃ b : Module.Basis (Fin n) R (NaiveCotangent.NL P).X₀,
      ∀ i, b i = 1 ⊗ₜ[P.toExtension.Ring]
        (KaehlerDifferential.D Λ P.toExtension.Ring) (MvPolynomial.X i)

Deformation.Artin.KeyExample.Situation.Lift.obsHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 409. The attribute's comment: “the map J/J² → I, f ↦ f(a'_1, …, a'_n)”.

The obstruction map: the R-linear map J/J² → I sending the class of f ∈ J to f(a'_1, …, a'_n), where a'_i are the chosen lifts. It is the map induced on conormal modules by the morphism of extensions Lift.hom; its target is I/I², which is I because I² = 0 (see Situation.cotangentEquivKernel).

noncomputable def Lift.obsHom (l : t.Lift) :
    P.toExtension.Cotangent →ₗ[R] t.ext.Cotangent

Deformation.Artin.KeyExample.Situation.Lift.obsHom_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 416. The attribute's comment: “o_x(A') is represented by the map f ↦ f(a'_1, …, a'_n)”.

The obstruction map sends the class of f ∈ J to f(a'_1, …, a'_n) ∈ I, through the identification I/I² = I of Situation.cotangentEquivKernel.

theorem Lift.obsHom_mk (l : t.Lift) (f : P.ker) :
    l.obsHom (Algebra.Extension.Cotangent.mk f) =
      t.cotangentEquivKernel
        ⟨MvPolynomial.aeval l.val (f : MvPolynomial (Fin n) Λ), l.aeval_mem_kernel f⟩

Deformation.Artin.KeyExample.obstructionModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 473. The attribute's comment: “the obstruction module Hom_R(J/J², M)/Hom_R(R^{⊕n}, M)”.

The obstruction module, 𝒪_x(M) = Hom_R(J/J², M)/Hom_R(R^{⊕n}, M): the R-linear maps out of the conormal module J/J² of the presentation, modulo those that factor through the differential J/J² → ⊕_i R dx_i of the naive cotangent complex. The quotient is taken by the range of precomposition with that differential; since ⊕_i R dx_i is free on the dx_i, the submodule divided out is the image of Hom_R(R^{⊕n}, M).

abbrev obstructionModule (P : Algebra.Generators Λ R (Fin n)) (M : Type v) [AddCommGroup M]
    [Module R M]

Deformation.Artin.KeyExample.obstructionModuleAddEquivExtOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 490. The attribute's comment: “Hom_R(J/J², M)/Hom_R(R^{⊕n}, M) = Ext¹_R(NL_{R/Λ}, M)”.

The obstruction module Hom_R(J/J², M)/Hom_R(R^{⊕n}, M) is Ext¹_R(NL_{R/Λ}, M): the comparison of Stacks 0GPU, NaiveCotangent.extOne_naiveCotangentComplex_addEquiv_cokernel, read at the presentation of the key example.

noncomputable def obstructionModuleAddEquivExtOne
    (P : Algebra.Generators Λ R (Fin n)) (M : Type v) [AddCommGroup M] [Module R M]

Deformation.Artin.KeyExample.Situation.obsClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 501. The attribute's comment: “the obstruction element o_x(A')”.

The obstruction element o_x(A'): the class in the obstruction module of the map J/J² → I, f ↦ f(a'_1, …, a'_n).

noncomputable def obsClass (l : t.Lift) : obstructionModule P t.ext.Cotangent

Deformation.Artin.KeyExample.Situation.obsClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 509. The attribute's comment: “o_x(A') is independent of the choice of lifts”.

o_x(A') does not depend on the choice of the lifts a'_i. Two families of lifts induce morphisms of extensions whose maps on conormal modules differ by precomposition with the differential of the naive cotangent complex, so their classes in Hom_R(J/J², I)/Hom_R(R^{⊕n}, I) agree.

theorem obsClass_eq (l l' : t.Lift) : obsClass l = obsClass l'

Deformation.Artin.KeyExample.Situation.obsClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 605. The attribute's comment: “o_x(A') = 0 if and only if Lift(x, A') is nonempty”.

o_x(A') = 0 if and only if x lifts. This is condition (iii) of Stacks 07YG for the key example.

theorem obsClass_eq_zero_iff (l : t.Lift) : obsClass l = 0 ↔ HasLift t

Deformation.Artin.KeyExample.Situation.coe_cotangentEquivKernel_symm_obsHom_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExample.lean, line 629. The attribute's comment: “a morphism of deformation situations carries o_x(A') to o_y(B')”.

Functoriality of the obstruction element. For a morphism of deformation situations (x, A' → A) → (y, B' → B) the obstruction map of x is carried to the obstruction map of y by the map I → I₂ induced on kernels by A' → B', so o_x(A') maps to o_y(B').

theorem coe_cotangentEquivKernel_symm_obsHom_pushforward {t₂ : Situation P}
    (ι : t.thick →ₐ[Λ] t₂.thick) (κ : t.base →ₐ[Λ] t₂.base)
    (hcomm : t₂.proj.comp ι = κ.comp t.proj) (hobj : κ.comp t.obj = t₂.obj) (l : t.Lift)
    (f : P.ker) :
    ((t₂.cotangentEquivKernel.symm
          ((l.pushforward ι κ hcomm hobj).obsHom
            (Algebra.Extension.Cotangent.mk f))).1 : t₂.thick) =
      ι (((t.cotangentEquivKernel.symm
        (l.obsHom (Algebra.Extension.Cotangent.mk f))).1 : t.thick))

Deformation.Artin.KeyExample.baseChangedObstructionModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExampleBaseChange.lean, line 184. The attribute's comment: “the obstruction module computed from NL_{R/Λ} ⊗_R A”.

The obstruction module of Stacks 07YI computed after base change, the cokernel Hom_A(A ⊗_R J/J², M)/Hom_A(A ⊗_R R^{⊕n}, M) of the dual of the differential of NL_{R/Λ} ⊗_R A.

abbrev baseChangedObstructionModule

Deformation.Artin.KeyExample.obstructionModuleBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExampleBaseChange.lean, line 195. The attribute's comment: “Hom_R(J/J², M)/Hom_R(R^{⊕n}, M) = Hom_A(A ⊗ J/J², M)/Hom_A(A ⊗ R^{⊕n}, M)”.

Stacks 07YI. The obstruction module Hom_R(J/J², M)/Hom_R(R^{⊕n}, M) of the key example agrees with the obstruction module computed from NL_{R/Λ} ⊗_R A: the tensor-hom adjunction carries one cokernel presentation onto the other.

def obstructionModuleBaseChange :
    obstructionModule P M ≃+ baseChangedObstructionModule P A M

Deformation.Artin.KeyExample.extOneNaiveCotangentBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExampleBaseChange.lean, line 212. The attribute's comment: “Ext¹_R(NL_{R/Λ}, I) = Ext¹_A(NL_{R/Λ} ⊗_R A, I)”.

Stacks 07YI: Ext¹_R(NL_{R/Λ}, M) = Ext¹_A(NL_{R/Λ} ⊗_R A, M). The first extension group of the naive cotangent complex of R over Λ with coefficients in an A-module M is the first extension group over A of the base change NL_{R/Λ} ⊗_R A. Both complexes are realized as the mapping cone of their differential, so that the conormal module lies in degree -1.

def extOneNaiveCotangentBaseChange :
    DerivedCategory.Ext
        (DerivedCategory.Q.obj (HomologicalComplex.homotopyCofiber
          (NaiveCotangent.ExtCokernelLinear.singleMap
            (ModuleCat.ofHom P.toExtension.cotangentComplex))))
        ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R M)) 1 ≃+
      DerivedCategory.Ext
        (DerivedCategory.Q.obj (HomologicalComplex.homotopyCofiber
          (NaiveCotangent.ExtCokernelLinear.singleMap
            (ModuleCat.ofHom (P.toExtension.cotangentComplex.baseChange A)))))
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A M)) 1

Deformation.Artin.nlBaseChangeToNaive, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExampleCotangentClass.lean, line 651. The attribute's comment: “the map NL_{R/Λ} ⊗_R A → NL_{A/Λ}”.

The morphism NL_{R/Λ} ⊗_R A ⟶ NL_{A/Λ} in the derived category of A-modules: functoriality of the naive cotangent complex for the Λ-algebra map R → A, with the source written as the termwise base change of the two-term complex of the presentation Λ[x_1, …, x_n] → R.

def nlBaseChangeToNaive :
    DerivedCategory.Q.obj (double
        (ModuleCat.ofHom (P.toExtension.cotangentComplex.baseChange A))
        upIntRelNegOneZero) ⟶
      derivedNaiveCotangentComplex Λ A

Deformation.Artin.cotangentComposition_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExampleCotangentClass.lean, line 700. The attribute's comment: “the composite NL_{R/Λ} ⊗_R A → NL_{A/Λ} → NL_{A/A'} = I[1]”.

Stacks 07YI: the invariant description of the obstruction element. The composite NL_{R/Λ} ⊗_R A ⟶ NL_{A/Λ} ⟶ NL_{A/A'} = I[1] in the derived category of A-modules is the class of the conormal functional compositeObsFunctional.

theorem cotangentComposition_eq :
    letI := Stacks.Smooth.kerModule hq hsq
    nlBaseChangeToNaive Λ R A P ≫ cotangentExtensionClass Λ A' A hq hsq =
      DerivedCategory.Q.map (doubleToSingleNegOne
        (ModuleCat.ofHom (P.toExtension.cotangentComplex.baseChange A))
        (ModuleCat.ofHom (compositeObsFunctional Λ R A A' P hq hsq)))

Deformation.Artin.coe_compositeObsFunctional_one_tmul_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExampleCotangentClass.lean, line 801. The attribute's comment: “the composite is represented by the map f ↦ f(a'_1, …, a'_n)”.

The conormal functional of the composite, in coordinates: on 1 ⊗ (class of f) it is f(a'_1, …, a'_n), where a'_i are the lifts canonicalLift i. This is the map J/J² → I of Stacks 07YI.

theorem coe_compositeObsFunctional_one_tmul_mk (f : P.toExtension.ker) :
    letI := Stacks.Smooth.kerModule hq hsq
    ((compositeObsFunctional Λ R A A' P hq hsq
          (1 ⊗ₜ[R] Algebra.Extension.Cotangent.mk f)).1 : A') =
      (MvPolynomial.aeval (canonicalLift Λ R A A' P hq) :
        P.toExtension.Ring →ₐ[Λ] A') f.1

Deformation.Artin.doubleCokernelExtEquiv_cotangentComposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/KeyExampleCotangentClass.lean, line 820. The attribute's comment: “o_x(A') equals the composite NL_{R/Λ} → NL_{A/Λ} → NL_{A/A'} = I[1]”.

Stacks 07YI: the obstruction element is the composite of cotangent complexes. Under the identification of Hom_{D(A)}(NL_{R/Λ} ⊗_R A, I[1]) = Ext¹_A(NL_{R/Λ} ⊗_R A, I) with the cokernel Hom_A(A ⊗_R J/J², I)/Hom_A(A ⊗_R R^{⊕n}, I), the composite NL_{R/Λ} ⊗_R A ⟶ NL_{A/Λ} ⟶ NL_{A/A'} = I[1] is the class of the functional whose value on 1 ⊗ (class of f) is f(a'_1, …, a'_n), for the lifts a'_i = canonicalLift i of the coordinates of x. That class is the obstruction element o_x(A') of Deformation.Artin.KeyExample.Situation.obsClass, which by Deformation.Artin.KeyExample.Situation.obsClass_eq does not depend on the chosen lifts.

theorem doubleCokernelExtEquiv_cotangentComposition :
    letI := Stacks.Smooth.kerModule hq hsq
    doubleCokernelExtEquiv (P.toExtension.cotangentComplex.baseChange A)
        (RingHom.ker (algebraMap A' A))
        (nlBaseChangeToNaive Λ R A P ≫ cotangentExtensionClass Λ A' A hq hsq) =
      Submodule.Quotient.mk (compositeObsFunctional Λ R A A' P hq hsq)

Sources

• Section 98.22, Tag 07YF
• AxiomMath/Stacks at 5ed82d14

LeanDeformation.Artin.ObstructionTheory · Deformation.Artin.isOpenVersality_of_obstructionTheory · Deformation.Artin.SectionsSheaf.exists_obstructionTheory · Deformation.Artin.KeyExample.objEquivTuple · Deformation.Artin.KeyExample.exists_isHomotopyEquiv_nl_canonical · Deformation.Artin.KeyExample.exists_basis_nl_cotangentSpace · Deformation.Artin.KeyExample.Situation.Lift.obsHom · Deformation.Artin.KeyExample.Situation.Lift.obsHom_mk

Section98.23 Naive obstruction theories#

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

Tag 07YK, a lemma

Tag 07YK in the Stacks Project.

DerivedCategory.extIntoFieldEquivDualBaseChangeHomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/IntoField.lean, line 537. The attribute's comment: “equivalence”.

Ext into a field is the linear dual of the cohomology of canonical derived base change.

public noncomputable def extIntoFieldEquivDualBaseChangeHomology
    {A : Type uA} {k : Type uk} [CommRing A] [Field k] (f : A →+* k)
    (E : DerivedCategory.Minus (ModuleCat.{max v uA uk} A)) (i : ℤ) :
    DerivedCategory.Ext E.1
        ((DerivedCategory.singleFunctor (ModuleCat.{max v uA uk} A) 0).obj
          ((ModuleCat.restrictScalars f).obj (ModuleCat.of k (ULift.{max v uA} k)))) i ≃+
      ((DerivedCategory.homologyFunctor (ModuleCat.{max v uA uk} k) (-i)).obj
        ((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{uA, uk, v}
          f).functor.obj E.1) ⟶ ModuleCat.of k (ULift.{max v uA} k))

DerivedCategory.extIntoFieldEquivDualBaseChangeHomology_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/IntoField.lean, line 559. The attribute's comment: “k-linearity”.

The Ext/base-change duality equivalence respects the intrinsic scalar action of k.

public theorem extIntoFieldEquivDualBaseChangeHomology_smul
    {A : Type uA} {k : Type uk} [CommRing A] [Field k] (f : A →+* k)
    (E : DerivedCategory.Minus (ModuleCat.{max v uA uk} A)) (i : ℤ)
    (x : k) (α : DerivedCategory.Ext E.1
      ((DerivedCategory.singleFunctor (ModuleCat.{max v uA uk} A) 0).obj
        ((ModuleCat.restrictScalars f).obj (ModuleCat.of k (ULift.{max v uA} k)))) i) :
  extIntoFieldEquivDualBaseChangeHomology f E i (x • α) =
      x • extIntoFieldEquivDualBaseChangeHomology f E i α

DerivedCategory.extIntoFieldEquivDualBaseChangeHomology_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/IntoField.lean, line 586. The attribute's comment: “naturality in the derived object”.

The Ext/base-change duality equivalence is contravariantly natural in derived objects.

public theorem extIntoFieldEquivDualBaseChangeHomology_naturality
    {A : Type uA} {k : Type uk} [CommRing A] [Field k] (f : A →+* k)
    (E E' : DerivedCategory.Minus (ModuleCat.{max v uA uk} A)) (i : ℤ)
    (g : E'.1 ⟶ E.1)
    (α : DerivedCategory.Ext E.1
      ((DerivedCategory.singleFunctor (ModuleCat.{max v uA uk} A) 0).obj
        ((ModuleCat.restrictScalars f).obj (ModuleCat.of k (ULift.{max v uA} k)))) i) :
    extIntoFieldEquivDualBaseChangeHomology f E' i (g ≫ α) =
      (DerivedCategory.homologyFunctor (ModuleCat.{max v uA uk} k) (-i)).map
        ((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{uA, uk, v}
          f).functor.map g) ≫
        extIntoFieldEquivDualBaseChangeHomology f E i α

DerivedCategory.extIntoFieldEquivDualBaseChangeHomology_restrictScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Homology/DerivedCategory/Ext/IntoField.lean, line 605. The attribute's comment: “naturality under change of source ring”.

The duality intertwines pullback of Ext classes across A → B with the dual of the canonical map E ⊗ᴸ_A k ⟶ F ⊗ᴸ_B k.

public theorem extIntoFieldEquivDualBaseChangeHomology_restrictScalars
    {A : Type uA} {B : Type uB} {k : Type uk}
    [CommRing A] [CommRing B] [Field k] (f : A →+* B) (g : B →+* k)
    (E : DerivedCategory.Minus (ModuleCat.{max v uA uB uk} A))
    (F : DerivedCategory.Minus (ModuleCat.{max v uA uB uk} B))
    (h : E.1 ⟶ (ModuleCat.restrictScalars f).mapDerivedCategory.obj F.1) (i : ℤ)
    (α : DerivedCategory.Ext F.1
      ((DerivedCategory.singleFunctor (ModuleCat.{max v uA uB uk} B) 0).obj
        ((ModuleCat.restrictScalars g).obj (ModuleCat.of k (ULift.{max v uA uB} k)))) i) :
    extIntoFieldEquivDualBaseChangeHomology.{uA, uk, max v uB} (g.comp f) E i
        (extIntoFieldRestriction.{uA, uk, v, uB} f g E.1 F.1 h i α) =
        (DerivedCategory.homologyFunctor (ModuleCat.{max v uA uB uk} k) (-i)).map
        (derivedBaseChangeMap.{uA, uk, v, uB} f g E.1 F.1 h) ≫
        extIntoFieldEquivDualBaseChangeHomology.{uB, uk, max v uA} g F i α

Tag 07YL, a lemma

Tag 07YL in the Stacks Project.

Deformation.Artin.exists_squareZeroExtension_killing_cotangent_morphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/DerivedSquareZeroExtension.lean, line 1083.

Stacks Project, Tag 07YL. Let Λ → A → k = κ(𝔭) be finite type maps of Noetherian rings and let ξ : E ⟶ NL_{A/Λ} be a morphism in D⁻(A) such that H⁻¹(ξ ⊗ᴸ k) is not surjective. Then there is a surjection of Λ-algebras A' → A whose kernel I has square zero and is isomorphic to k as an A-module, which does not change differentials modulo 𝔭, and for which the composite of ξ with NL_{A/Λ} ⟶ NL_{A/A'} vanishes.

public theorem exists_squareZeroExtension_killing_cotangent_morphism
    (Λ A : Type u) [CommRing Λ] [CommRing A] [Algebra Λ A]
    [IsNoetherianRing Λ] [IsNoetherianRing A] [Algebra.FiniteType Λ A]
    (p : Ideal A) [p.IsPrime] [Algebra.FiniteType A p.ResidueField]
    (T : DerivedTensorProduct A)
    (E : DerivedCategory (ModuleCat.{u} A))
    (hE : (DerivedCategory.TStructure.t
      (C := ModuleCat.{u} A)).minus E)
    (ξ : E ⟶ derivedNaiveCotangentComplex Λ A)
    (hξ : ¬ Function.Surjective
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-1)).map
        ((T.tensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
            (ModuleCat.of A p.ResidueField))).map ξ))) :
    ∃ (A' : Type u) (_ : CommRing A') (_ : Algebra Λ A') (_ : Algebra A' A)
      (_ : IsScalarTower Λ A' A),
      Function.Surjective (algebraMap A' A) ∧
      let I := RingHom.ker (algebraMap A' A)
      I ^ 2 = ⊥ ∧
      ∃ (_ : Module A I),
        (∀ (a' : A') (x : I), (algebraMap A' A a') • x = a' • x) ∧
        Nonempty (I ≃ₗ[A] p.ResidueField) ∧
        Function.Bijective (differentialsBaseChangeMap Λ A' A p.ResidueField) ∧
        ξ ≫ naiveCotangentBaseMap Λ A' A = 0

Tag 07YM, a lemma

Tag 07YM in the Stacks Project.

AlgebraicGeometry.finiteType_residueField_of_isClosed_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteTypePoint.lean, line 151. The attribute's comment: “the use of closedness: the residue field at the point is of finite type”.

The residue field at a closed point of an affine scheme is of finite type over the ring.

This is the use that the converse direction of [Stacks, Tag 07YM] makes of closedness: it is the finiteness hypothesis under which [Stacks, Tag 07YL] builds its square-zero extension, and the source notes that the step "fails if u₀ is not closed".

public theorem finiteType_residueField_of_isClosed_singleton {A : Type u} [CommRing A]
    {u₀ : Spec (CommRingCat.of A)}
    (hu₀ : IsClosed ({u₀} : Set (Spec (CommRingCat.of A)))) :
    letI : u₀.asIdeal.IsPrime := u₀.isPrime
    Algebra.FiniteType A u₀.asIdeal.ResidueField

Deformation.Artin.surjective_derivedFibre_neg_one_iff_injective_extOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersality.lean, line 212. The attribute's comment: “condition (2) in degree -1 as injectivity of Ext¹(NL_{A/Λ}, k) → Ext¹(E, k)”.

Stacks 07YM, condition (2) in degree -1. For a morphism ξ : E ⟶ NL_{A/Λ} of D⁻(A) and a ring map A ⟶ k to a field, the map H^{-1}(E ⊗ᴸ_A k) ⟶ H^{-1}(NL_{A/Λ} ⊗ᴸ_A k) is surjective exactly when the induced map Ext¹_A(NL_{A/Λ}, k) ⟶ Ext¹_A(E, k), that is precomposition with ξ, is injective. This is the first of the two invocations of Stacks 07YK in the proof of Stacks 07YM: in the direction (1) ⇒ (2) a failure of the surjectivity produces a nonzero class of Ext¹_A(NL_{A/Λ}, k) killed by ξ, which is the input of Stacks 07YL, and in the direction (2) ⇒ (1) the injectivity is what forces the obstruction class to vanish.

public theorem surjective_derivedFibre_neg_one_iff_injective_extOne
    {Λ A k : Type u} [CommRing Λ] [CommRing A] [Field k] [Algebra Λ A] (f : A →+* k)
    (E : DerivedCategory (ModuleCat.{u} A))
    (hE : (DerivedCategory.TStructure.t (C := ModuleCat.{u} A)).minus E)
    (ξ : E ⟶ derivedNaiveCotangentComplex Λ A) :
    Function.Surjective
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} k) (-1)).map
          ((totalDerivedExtensionScalars.{u, u, u} f).functor.map ξ)) ↔
      Function.Injective
        (fun α : DerivedCategory.Ext (derivedNaiveCotangentComplex Λ A)
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              ((ModuleCat.restrictScalars f).obj (ModuleCat.of k (ULift.{u} k)))) 1 =>
          ξ ≫ α)

Deformation.Artin.injective_derivedFibre_zero_iff_surjective_extZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersality.lean, line 236. The attribute's comment: “condition (2) in degree 0 as surjectivity of Ext⁰(NL_{A/Λ}, k) → Ext⁰(E, k)”.

Stacks 07YM, condition (2) in degree 0. For a morphism ξ : E ⟶ NL_{A/Λ} of D⁻(A) and a ring map A ⟶ k to a field, the map H^0(E ⊗ᴸ_A k) ⟶ H^0(NL_{A/Λ} ⊗ᴸ_A k) is injective exactly when the induced map Ext⁰_A(NL_{A/Λ}, k) ⟶ Ext⁰_A(E, k), that is precomposition with ξ, is surjective. This is the second of the two invocations of Stacks 07YK in the proof of Stacks 07YM: condition (ii) identifies the right-hand map with the map Der_Λ(A, k) ⟶ T_x(k) from tangent vectors of U at u₀ to infinitesimal deformations of x₀, whose surjectivity is what versality provides.

public theorem injective_derivedFibre_zero_iff_surjective_extZero
    {Λ A k : Type u} [CommRing Λ] [CommRing A] [Field k] [Algebra Λ A] (f : A →+* k)
    (E : DerivedCategory (ModuleCat.{u} A))
    (hE : (DerivedCategory.TStructure.t (C := ModuleCat.{u} A)).minus E)
    (ξ : E ⟶ derivedNaiveCotangentComplex Λ A) :
    Function.Injective
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} k) 0).map
          ((totalDerivedExtensionScalars.{u, u, u} f).functor.map ξ)) ↔
      Function.Surjective
        (fun α : DerivedCategory.Ext (derivedNaiveCotangentComplex Λ A)
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              ((ModuleCat.restrictScalars f).obj (ModuleCat.of k (ULift.{u} k)))) 0 =>
          ξ ≫ α)

Deformation.Artin.exists_pow_inf_eq_bot_of_mul_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersality.lean, line 267. The attribute's comment: “the Artin–Rees step of (1) ⇒ (2): (p')^n ∩ I = 0 for some n > 1”.

Stacks 07YM, the Artin–Rees step of the implication (1) ⇒ (2). Let A' be a Noetherian ring and let p' and I be ideals with p' · I = 0. Then (p')^n ∩ I = 0 for some n > 1.

In the source A' ⟶ A is the square-zero extension supplied by Stacks 07YL, I is its kernel and p' = Ker(A' ⟶ k) is the prime over the closed point u₀; the kernel is a one-dimensional k-vector space, so it is annihilated by p', and the conclusion is what makes the kernel of A'/(p')^n ⟶ A/p^n equal to I and hence that map a small extension of local Artinian rings. The proof is the Artin–Rees lemma (Stacks 00IN) applied to the ideal p' of A' and the submodule I of A': beyond the Artin–Rees constant c the intersection (p')^n ∩ I is contained in (p')^{n - c} · I, which vanishes as soon as n > c.

public theorem exists_pow_inf_eq_bot_of_mul_eq_bot {A' : Type*} [CommRing A']
    [IsNoetherianRing A'] (p' I : Ideal A') (hpI : p' * I = ⊥) :
    ∃ n > 1, p' ^ n ⊓ I = ⊥

Deformation.Artin.surjective_derivedTensorFibre_neg_one_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDegreeNegOne.lean, line 124. The attribute's comment: “(1) implies (2), degree -1”.

Stacks 07YM, (1) ⇒ (2) in degree -1. Let x be a family over Spec A whose deformation theory is controlled by ξ : E ⟶ NL_{A/Λ} as in hypothesis (i) of the tag: x lifts across a deformation situation A' → A whenever ξ composed with NL_{A/Λ} ⟶ NL_{A/A'} vanishes. If x is versal at a closed point u₀ of Spec A, then the map H^{-1}(E ⊗ᴸ_A κ(u₀)) ⟶ H^{-1}(NL_{A/Λ} ⊗ᴸ_A κ(u₀)) on the derived fibre at u₀ is surjective.

Were it not, [Stacks, Tag 07YL] would supply a square-zero extension A' → A killing ξ and not changing differentials modulo κ(u₀), hypothesis (i) would lift x to Spec A', and the Artin–Rees step would turn the extension into a small extension A' ⧸ (𝔭') ^ n ⟶ A ⧸ 𝔭 ^ n of 𝒞_Λ which [Stacks, Tag 06H0] makes an essential surjection. Versality applied to the arrow joining the restrictions of x and of its lift to the two Artinian quotients then lifts A through that extension, hence splits it — contradicting essential surjectivity.

public theorem surjective_derivedTensorFibre_neg_one_of_isVersalAt
    (hclosed : IsClosed ({u₀} : Set (Spec (CommRingCat.of A))))
    (hLifts : ∀ (A' : Type u) [CommRing A'] [Algebra Λ A'] [Algebra A' A]
      [IsScalarTower Λ A' A] (D : SquareZeroThickening A B S hS toS hA A'),
      D.q = algebraMap A' A →
      Spec.map (CommRingCat.ofHom (algebraMap Λ A')) ≫ baseMap = B.inclusion.map D.toS' →
      ξ ≫ naiveCotangentBaseMap Λ A' A = 0 →
      Nonempty ((Under.post p).Fiber (Under.mk (eqToHom hx ≫ D.arrow))))
    (hversal : IsVersalAt (Over.mk toS) (p ⋙ Over.post B.inclusion) u₀ x
      (by change (Over.post B.inclusion).obj (p.obj x) = _; rw [hx]; rfl)) :
    Function.Surjective
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-1)).map
        ((T.tensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
            (ModuleCat.of A u₀.asIdeal.ResidueField))).map ξ))

Deformation.Artin.surjective_comp_of_liftsAtResiduePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDegreeZero.lean, line 191. The attribute's comment: “(1) implies (2), degree 0: precomposition with xi is surjective”.

Stacks 07YM, the surjectivity hypothesis (ii) turns versality into. If the lifting property defining versality holds at the point of Spec A determined by the A-algebra structure of a field k, then precomposition with ξ is surjective on morphisms NL_{A/Λ} ⟶ k[0] of D(A).

This is Deformation.Artin.surjective_canonicalTangentMap_of_liftsAtResiduePoint, the surjectivity of the map Der_Λ(A, k) ⟶ T_x(k) on tangent spaces, read through the functorial isomorphism of hypothesis (ii): by Deformation.Artin.tangentEquiv_canonicalTangentMap that isomorphism carries the image of a tangent vector θ to ξ followed by the augmentation followed by θ, so a surjection onto T_x(k) becomes a surjection onto the morphisms E ⟶ k[0] factoring through ξ. The two identifications of T_x(k) with classes of lifts are bijections, so the surjectivity of the composite in that statement is the surjectivity of the tangent map itself.

public theorem surjective_comp_of_liftsAtResiduePoint [Mono baseMap]
    (hlifts : LiftsAtResiduePoint (Λ := R) (k := k) iR (p ⋙ Over.post B.inclusion)
      (Over.mk toS) x hxS (Spec.map (CommRingCat.ofHom (algebraMap A k)))) :
    Function.Surjective (fun f : derivedNaiveCotangentComplex Λ A ⟶
        (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A k) =>
      ξ ≫ f)

Deformation.Artin.injective_derivedTensorFibre_zero_of_liftsAtResiduePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDegreeZero.lean, line 268. The attribute's comment: “(1) implies (2), degree 0, at a field in the site”.

Stacks 07YM, condition (2) in degree 0 from the lifting property. If the lifting property defining versality holds at the point of Spec A determined by the A-algebra structure of a field k no larger than max ℵ₀ #A, then the map H^0(E ⊗ᴸ_A k) ⟶ H^0(NL_{A/Λ} ⊗ᴸ_A k) is injective.

Deformation.Artin.injective_derivedTensorFibre_zero_iff_surjective_comp turns the conclusion into the surjectivity of precomposition with ξ on morphisms into ULift k, restricted along A ⟶ k; Deformation.Artin.uliftRestrictScalarsIso identifies that coefficient module with the A-module ULift k, at which Deformation.Artin.surjective_comp_of_liftsAtResiduePoint supplies the surjectivity. The lifting property is moved from k to ULift k by Deformation.Artin.liftsAtResiduePoint_changeResidueField, and the three memberships in the site that the lift chain asks of ULift k are derived from the cardinality bound.

public theorem injective_derivedTensorFibre_zero_of_liftsAtResiduePoint [Mono baseMap]
    (hmk : Cardinal.mk k ≤ max Cardinal.aleph0 (Cardinal.mk A))
    (hlifts : LiftsAtResiduePoint (Λ := R) (k := k) iR (p ⋙ Over.post B.inclusion)
      (Over.mk toS) x hxS (Spec.map (CommRingCat.ofHom (algebraMap A k)))) :
    Function.Injective
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map
        ((T.tensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
            (ModuleCat.of A k))).map ξ))

Deformation.Artin.injective_derivedTensorFibre_zero_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDegreeZero.lean, line 357. The attribute's comment: “(1) implies (2), degree 0”.

Stacks 07YM, (1) ⇒ (2) in degree 0. Let x be a family over Spec A whose tangent theory is represented by ξ : E ⟶ NL_{A/Λ} as in hypothesis (ii) of the tag. If x is versal at a point u₀ of Spec A, then the map H^0(E ⊗ᴸ_A κ(u₀)) ⟶ H^0(NL_{A/Λ} ⊗ᴸ_A κ(u₀)) on the derived fibre at u₀ is injective.

Versality is the lifting property at the residue-field point (Deformation.Artin.liftsAtResiduePoint_of_isVersalAt), the residue field at a prime of A is no larger than max ℵ₀ #A (Cardinal.mk_residueField_le_max), and Deformation.Artin.specMap_primeResidueFieldAlgebra_comp_fromSpecStalk is the compatibility of the residue-field point with the local ring of S at the image of u₀; with those, Deformation.Artin.injective_derivedTensorFibre_zero_of_liftsAtResiduePoint applies.

No closedness of the point is used: the source invokes closedness only for the H^{-1} half of condition (2).

public theorem injective_derivedTensorFibre_zero_of_isVersalAt [Mono baseMap]
    (hversal : IsVersalAt (Over.mk toS) (p ⋙ Over.post B.inclusion) u₀ x
      (by change (Over.post B.inclusion).obj (p.obj x) = _; rw [hx]; rfl)) :
    Function.Injective
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map
        ((T.tensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
            (ModuleCat.of A u₀.asIdeal.ResidueField))).map ξ))

Deformation.Artin.bijective_comp_naiveCotangentToDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDegreeZeroConverse.lean, line 343. The attribute's comment: “Ext^0_A(NL_{A/Lambda}, M) = Der_Lambda(A, M)”.

Ext⁰_A(NL_{A/Λ}, M) = Der_Λ(A, M). Composing the augmentation NL_{A/Λ} ⟶ Ω_{A/Λ}[0] with a module map Ω_{A/Λ} ⟶ M is a bijection onto the morphisms NL_{A/Λ} ⟶ M[0] of D(A).

This is the identification the proof of [Stacks, Tag 07YM] writes as Ext⁰_A(NL_{A/Λ}, k) = Der_Λ(A, k). The naive cotangent complex lies in degrees ≤ 0 and M[0] in degrees ≥ 0, so H⁰ computes the morphisms between them (DerivedCategory.bijective_homologyFunctor_map_of_isLE_of_isGE); the augmentation is an isomorphism on H⁰ (Deformation.Artin.isIso_homologyFunctor_map_naiveCotangentToDifferentials), and the single functor of D(A) is fully faithful, so a morphism Ω_{A/Λ}[0] ⟶ M[0] is a module map.

public theorem bijective_comp_naiveCotangentToDifferentials (M : ModuleCat.{u} A) :
    Function.Bijective (fun θ : differentialsModule Λ A ⟶ M =>
      naiveCotangentToDifferentials Λ A ≫
        (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).map θ)

Deformation.Artin.surjective_canonicalTangentMap_of_surjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDegreeZeroConverse.lean, line 419. The attribute's comment: “(2) implies (1), degree 0: the map on tangent spaces is surjective”.

Stacks 07YM, (2) ⇒ (1) in degree 0. If precomposition with ξ is surjective on morphisms NL_{A/Λ} ⟶ k[0] of D(A), then the map Der_Λ(A, k) ⟶ T_x(k) on tangent spaces is surjective.

The hypothesis is condition (2) of the tag in degree 0: by Deformation.Artin.injective_derivedTensorFibre_zero_iff_surjective_comp the injectivity of H^0(ξ ⊗ᴸ_A k) is exactly this surjectivity, and DerivedCategory.surjective_extZero_comp_iff_surjective_comp reads it on Ext⁰ if wanted. The conclusion is the first condition of the versality criterion of Stacks 06IU, read through the identification of T_x(k) with the infinitesimal deformations of x₀.

The source's sentence is that the map on tangent spaces is the dual of H^0(ξ ⊗ᴸ_A k) under Ext⁰_A(NL_{A/Λ}, k) = Der_Λ(A, k) and Ext⁰_A(E, k) = T_x(k). The second identification is hypothesis (ii), and Deformation.Artin.tangentEquiv_canonicalTangentMap is its value on the map on tangent spaces: a tangent vector θ goes to ξ followed by the augmentation followed by θ. The first identification is Deformation.Artin.bijective_comp_naiveCotangentToDifferentials, which is what turns the arbitrary morphism NL_{A/Λ} ⟶ k[0] produced by the hypothesis into such a θ.

public theorem surjective_canonicalTangentMap_of_surjective_comp
    (hsurj : Function.Surjective (fun f : derivedNaiveCotangentComplex Λ A ⟶
        (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A k) =>
      ξ ≫ f)) :
    Function.Surjective (canonicalTangentMap Λ A k B S hS toS hA p x hx hp hRS hΩ hk baseMap
      baseFactorization)

Deformation.Artin.exists_extends_of_surjective_canonicalTangentMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDegreeZeroConverse.lean, line 481. The attribute's comment: “(2) implies (1): an infinitesimal deformation over the dual numbers extends”.

Stacks 07YM, (2) ⇒ (1) at the dual numbers. If the map Der_Λ(A, k) ⟶ T_x(k) on tangent spaces is surjective, then every lift of x₀ along the square-zero immersion Spec k ⟶ Spec k[k] extends to x: its structure arrow composes with an arrow from its target to x to give the chosen restriction arrow.

This is the exact converse of Deformation.Artin.exists_extends_of_liftsAtResiduePoint, and is the dual-numbers content of the first condition of the versality criterion of Stacks 06IU.

The class of the lift is hit by a tangent vector θ, through the two bijections Deformation.Artin.canonicalFieldBaseChangeEquiv and the tangent functor's liftEquiv. By Deformation.Artin.canonicalFieldBaseChangeEquiv_canonicalTangentMap that class is also the class of the connecting arrow χ attached to any lift (y, φ) of x along Deformation.Artin.canonicalDualNumbersArrow θ, one of which exists because p is fibred in groupoids (Deformation.Artin.exists_canonicalDualNumbersLift). Two lifts in one class are isomorphic over k[k] compatibly with their arrows from x₀, so the isomorphism's component at the target carries the given lift's structure arrow to χ, and Deformation.Artin.canonicalDualNumbersConnectingArrow_fac says χ ≫ φ is the chosen restriction arrow.

Mono baseMap is not needed here, although the forward direction needs it: it enters the forward direction through Deformation.Artin.exists_unique_eq_canonicalDualNumbersArrow, which recovers a tangent vector from an arrow of the site, and this direction is handed the tangent vector instead.

public theorem exists_extends_of_surjective_canonicalTangentMap
    (hsurj : Function.Surjective (canonicalTangentMap Λ A k B S hS toS hA p x hx hp hRS hΩ hk
      baseMap baseFactorization)) :
    letI : p.IsFibered := hp.isFibered
    ∀ (w : (Under.post p).Fiber (Under.mk (eqToHom
          (((Functor.chosenPullbacks p).pullbackFunctor
            (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
              (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj ⟨x, hx⟩).2 ≫
        squareZeroArrow k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk
          (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B)))),
      ∃ b : w.1.right ⟶ x,
        w.1.hom ≫ b = (Functor.chosenPullbacks p).map
          (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
            (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl) ⟨x, hx⟩

Deformation.Artin.surjective_derivedTensorFibre_neg_one_iff_injective_extOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDerivedFibre.lean, line 84. The attribute's comment: “condition (2) in degree -1, through a chosen derived tensor product”.

Stacks 07YM, condition (2) in degree -1. For a morphism ξ : E ⟶ NL_{A/Λ} of D⁻(A) and a field k which is an A-algebra, the map H^{-1}(E ⊗ᴸ_A k) ⟶ H^{-1}(NL_{A/Λ} ⊗ᴸ_A k), formed through a chosen derived tensor product, is surjective exactly when precomposition with ξ is injective on Ext¹_A(−, k), that is when Ext¹_A(NL_{A/Λ}, k) ⟶ Ext¹_A(E, k) is injective.

This is Deformation.Artin.surjective_derivedFibre_neg_one_iff_injective_extOne, which proves the same statement for the total derived extension of scalars, composed with the comparison Deformation.Artin.surjective_derivedTensorFibre_iff_surjective_derivedExtensionScalars of the two presentations of the derived fibre.

public theorem surjective_derivedTensorFibre_neg_one_iff_injective_extOne
    (T : DerivedTensorProduct A) (E : DerivedCategory (ModuleCat.{u} A))
    (hE : (DerivedCategory.TStructure.t (C := ModuleCat.{u} A)).minus E)
    (ξ : E ⟶ derivedNaiveCotangentComplex Λ A) :
    Function.Surjective
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-1)).map
          ((T.tensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              (ModuleCat.of A k))).map ξ)) ↔
      Function.Injective
        (fun α : DerivedCategory.Ext (derivedNaiveCotangentComplex Λ A)
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              ((ModuleCat.restrictScalars (algebraMap A k)).obj
                (ModuleCat.of k (ULift.{u} k)))) 1 =>
          ξ ≫ α)

Deformation.Artin.injective_derivedTensorFibre_zero_iff_surjective_extZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDerivedFibre.lean, line 113. The attribute's comment: “condition (2) in degree 0, through a chosen derived tensor product”.

Stacks 07YM, condition (2) in degree 0. For a morphism ξ : E ⟶ NL_{A/Λ} of D⁻(A) and a field k which is an A-algebra, the map H^0(E ⊗ᴸ_A k) ⟶ H^0(NL_{A/Λ} ⊗ᴸ_A k), formed through a chosen derived tensor product, is injective exactly when precomposition with ξ is surjective on Ext⁰_A(−, k), that is when Ext⁰_A(NL_{A/Λ}, k) ⟶ Ext⁰_A(E, k) is surjective.

This is Deformation.Artin.injective_derivedFibre_zero_iff_surjective_extZero composed with the comparison Deformation.Artin.injective_derivedTensorFibre_iff_injective_derivedExtensionScalars of the two presentations of the derived fibre.

public theorem injective_derivedTensorFibre_zero_iff_surjective_extZero
    (T : DerivedTensorProduct A) (E : DerivedCategory (ModuleCat.{u} A))
    (hE : (DerivedCategory.TStructure.t (C := ModuleCat.{u} A)).minus E)
    (ξ : E ⟶ derivedNaiveCotangentComplex Λ A) :
    Function.Injective
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map
          ((T.tensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              (ModuleCat.of A k))).map ξ)) ↔
      Function.Surjective
        (fun α : DerivedCategory.Ext (derivedNaiveCotangentComplex Λ A)
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              ((ModuleCat.restrictScalars (algebraMap A k)).obj
                (ModuleCat.of k (ULift.{u} k)))) 0 =>
          ξ ≫ α)

Deformation.Artin.injective_derivedTensorFibre_zero_iff_surjective_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityDerivedFibre.lean, line 140. The attribute's comment: “condition (2) in degree 0, as a condition on morphisms”.

Stacks 07YM, condition (2) in degree 0, as a condition on morphisms. The injectivity of H^0(ξ ⊗ᴸ_A k) is the surjectivity of precomposition with ξ on morphisms NL_{A/Λ} ⟶ k[0] of D(A).

This is Deformation.Artin.injective_derivedTensorFibre_zero_iff_surjective_extZero followed by DerivedCategory.surjective_extZero_comp_iff_surjective_comp: in degree 0 an Ext class is a morphism. It is the form in which condition (2) meets the tangent-space description of versality, whose statements are about morphisms of the derived category.

public theorem injective_derivedTensorFibre_zero_iff_surjective_comp
    (T : DerivedTensorProduct A) (E : DerivedCategory (ModuleCat.{u} A))
    (hE : (DerivedCategory.TStructure.t (C := ModuleCat.{u} A)).minus E)
    (ξ : E ⟶ derivedNaiveCotangentComplex Λ A) :
    Function.Injective
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map
          ((T.tensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              (ModuleCat.of A k))).map ξ)) ↔
      Function.Surjective
        (fun f : derivedNaiveCotangentComplex Λ A ⟶
            (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
              ((ModuleCat.restrictScalars (algebraMap A k)).obj
                (ModuleCat.of k (ULift.{u} k))) =>
          ξ ≫ f)

Deformation.Artin.exists_unique_eq_canonicalDualNumbersArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityFieldArrowShape.lean, line 171. The attribute's comment: “the dual-numbers arrows over Spec A are the tangent vectors”.

Stacks 07YM. An arrow ν : Spec k[k] ⟶ Spec A of the site over S whose restriction along the square-zero immersion Spec k ⟶ Spec k[k] is the point of Spec A determined by the A-algebra structure of k is Deformation.Artin.canonicalDualNumbersArrow θ for a unique A-linear map θ : Ω[A⁄Λ] →ₗ[A] k.

The ring map r : A ⟶ k[k] underlying ν exists because the two objects are spectra and Spec is full; the compatibility of ν with the structure morphisms to S, combined with the factorization of Spec A ⟶ S through the monomorphism baseMap, makes r a Λ-algebra map, and the hypothesis on the augmentation says that composing it with the projection k[k] ⟶ k is the structure map A ⟶ k. By Deformation.Artin.exists_unique_kaehler_of_fstHom_comp_eq such an r is a ↦ (a mod 𝔭, θ (d a)) for a unique θ, which is the ring map of canonicalDualNumbersArrow θ by Deformation.Artin.canonicalDualNumbersMap_apply.

public theorem exists_unique_eq_canonicalDualNumbersArrow [Mono baseMap]
    (ν : squareZeroOver k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS)
          (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B) ⟶
        algebraOver A B S hS toS hA)
    (hν : squareZeroArrow k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk
          (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B) ≫ ν =
        algebraOverMapOfRingHom (algebraMap A k) B S hS toS
          (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl) :
    ∃! θ : Ω[A⁄Λ] →ₗ[A] k,
      ν = canonicalDualNumbersArrow Λ A k B S hS toS hA p x hx hp hRS hΩ hkk baseMap
        baseFactorization θ

Deformation.Artin.canonicalFieldBaseChangeEquiv_canonicalTangentMap_of_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityFieldClassEquationLift.lean, line 85. The attribute's comment: “the class equation at an arbitrary connecting arrow”.

Stacks 07YM, the class equation at an arbitrary connecting arrow. Let (y, φ) be a lift of x along Deformation.Artin.canonicalDualNumbersArrow θ, and let χ : x₀ ⟶ y be any arrow from the chosen pullback of x to Spec k, lying over the square-zero immersion Spec k ⟶ Spec k[k], which factors the chosen restriction arrow η : x₀ ⟶ x through φ. Then the class of χ as an infinitesimal deformation of x₀ over the dual numbers of k is the image of θ under the map on tangent spaces, moved across the identification Deformation.Artin.canonicalFieldBaseChangeEquiv of lift classes over A[k] with lift classes over k[k].

Such a χ is the chosen connecting arrow Deformation.Artin.canonicalDualNumbersConnectingArrow: both lie over the square-zero immersion and both factor η through φ, so both are the arrow produced by the universal property of the strongly Cartesian arrow φ. The statement then reduces to Deformation.Artin.canonicalFieldBaseChangeEquiv_canonicalTangentMap.

public theorem canonicalFieldBaseChangeEquiv_canonicalTangentMap_of_fac
    (θ : Ω[A⁄Λ] →ₗ[A] k) (y : X) (φ : y ⟶ x)
    (hφ : p.IsHomLift
      (canonicalDualNumbersArrow Λ A k B S hS toS hA p x hx hp hRS hΩ hkk baseMap
        baseFactorization θ) φ) :
    letI : p.IsFibered := hp.isFibered
    ∀ (χ : (((Functor.chosenPullbacks p).pullbackFunctor
          (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
            (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj
          ⟨x, hx⟩).1 ⟶ y),
      p.IsHomLift
          (squareZeroArrow k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk
            (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B)) χ →
        χ ≫ φ = (Functor.chosenPullbacks p).map
            (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
              (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl) ⟨x, hx⟩ →
          ∀ hmem : (Under.post p).obj (Under.mk χ) =
            Under.mk (eqToHom (((Functor.chosenPullbacks p).pullbackFunctor
                (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
                  (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj
                ⟨x, hx⟩).2 ≫
              squareZeroArrow k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk
                (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B)),
          canonicalFieldBaseChangeEquiv A k B S hS toS hA p x hx hp hRS hk hAk hkk
              ((tangentFunctor A B S hS toS hA p x hx hp hRS).liftEquiv
                (⟨ModuleCat.of A k, hk⟩ : SiteModule A B)
                (canonicalTangentMap Λ A k B S hS toS hA p x hx hp hRS hΩ hk baseMap
                  baseFactorization θ)) =
            Quotient.mk _ ⟨Under.mk χ, hmem⟩

Deformation.Artin.exists_canonicalTangentMap_eq_of_extends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityFieldTangentImage.lean, line 107. The attribute's comment: “an extendable infinitesimal deformation is in the image of the tangent map”.

Stacks 07YM. Let x₀ be the chosen pullback of x to Spec k and let w represent an infinitesimal deformation of x₀ over the dual numbers k[k], that is a lift of x₀ along the square-zero immersion Spec k ⟶ Spec k[k]. If the representative extends to x, that is if there is an arrow b from its target to x composing with it to the chosen restriction arrow η : x₀ ⟶ x, then the class of w is the image of a tangent vector θ : Ω[A⁄Λ] →ₗ[A] k under the map on tangent spaces, moved across the identification Deformation.Artin.canonicalFieldBaseChangeEquiv.

Versality of x at the point is exactly what supplies the extension b; no other property of it enters. The θ is the one attached to the arrow of the site that b lies over by Deformation.Artin.exists_unique_eq_canonicalDualNumbersArrow, which applies because the restriction of that arrow along the square-zero immersion is forced, by the factorization through η, to be the point of Spec A determined by the A-algebra structure of k; the class is then computed by Deformation.Artin.canonicalFieldBaseChangeEquiv_canonicalTangentMap_of_fac.

public theorem exists_canonicalTangentMap_eq_of_extends [Mono baseMap] :
    letI : p.IsFibered := hp.isFibered
    ∀ (w : (Under.post p).Fiber (Under.mk (eqToHom
          (((Functor.chosenPullbacks p).pullbackFunctor
            (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
              (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj ⟨x, hx⟩).2 ≫
        squareZeroArrow k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk
          (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B))))
      (b : w.1.right ⟶ x),
      w.1.hom ≫ b = (Functor.chosenPullbacks p).map
          (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
            (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl) ⟨x, hx⟩ →
        ∃ θ : Ω[A⁄Λ] →ₗ[A] k,
          canonicalFieldBaseChangeEquiv A k B S hS toS hA p x hx hp hRS hk hAk hkk
              ((tangentFunctor A B S hS toS hA p x hx hp hRS).liftEquiv
                (⟨ModuleCat.of A k, hk⟩ : SiteModule A B)
                (canonicalTangentMap Λ A k B S hS toS hA p x hx hp hRS hΩ hk baseMap
                  baseFactorization θ)) =
            Quotient.mk _ w

Deformation.Artin.exists_extends_of_liftsAtResiduePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityFieldVersalLift.lean, line 262. The attribute's comment: “versality tested at the dual numbers of a residue field”.

Stacks 07YM, the dual-numbers instance of versality. Let x₀ be the chosen pullback of x to Spec k and let w be a lift of x₀ along the square-zero immersion Spec k ⟶ Spec k[k]. If the lifting property defining versality holds at the point of Spec A determined by the A-algebra structure of k, then w's structure arrow extends to x: there is an arrow b from its target to x composing with it to the chosen restriction arrow.

This is the instantiation of Deformation.Artin.IsVersalAt at the surjection k[k] ⟶ k of 𝒞_R, which is Deformation.Artin.squareZeroArtinianProjection; the objects Deformation.Artin.squareZeroArtinianObj and Deformation.Artin.fieldArtinianObj are the site's own square-zero ring and the field, so the two descriptions of the base — the spectrum of an object of 𝒞_R over Spec R, and the site's square-zero object over Spec A — agree by Deformation.Artin.squareZeroOver_post_eq and Deformation.Artin.algebraOver_post_eq.

public theorem exists_extends_of_liftsAtResiduePoint
    (hkk : B.Contains (Spec (squareZeroRing k (ModuleCat.of k k))))
    (hlifts : LiftsAtResiduePoint (Λ := R) (k := k) iR (p ⋙ Over.post B.inclusion)
      (Over.mk toS) x hxS (Spec.map (CommRingCat.ofHom (algebraMap A k)))) :
    letI : p.IsFibered := hp.isFibered
    ∀ (w : (Under.post p).Fiber (Under.mk (eqToHom
          (((Functor.chosenPullbacks p).pullbackFunctor
            (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
              (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl)).obj ⟨x, hx⟩).2 ≫
        squareZeroArrow k B S hS (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hAk
          (⟨ModuleCat.of k k, hkk⟩ : SiteModule k B)))),
      ∃ b : w.1.right ⟶ x,
        w.1.hom ≫ b = (Functor.chosenPullbacks p).map
          (algebraOverMapOfRingHom (algebraMap A k) B S hS toS
            (Spec.map (CommRingCat.ofHom (algebraMap A k)) ≫ toS) hA hAk rfl) ⟨x, hx⟩

Deformation.Artin.surjective_canonicalTangentMap_of_liftsAtResiduePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityFieldVersalLift.lean, line 388. The attribute's comment: “(1) implies (2), degree 0: the map on tangent spaces is surjective”.

Stacks 07YM, the surjectivity of the map on tangent spaces. If the lifting property defining versality holds at the point of Spec A determined by the A-algebra structure of k, then every infinitesimal deformation of x₀ over the dual numbers of k is the image of a tangent vector θ : Ω[A⁄Λ] →ₗ[A] k under the map on tangent spaces, moved across Deformation.Artin.canonicalFieldBaseChangeEquiv.

This is Deformation.Artin.exists_extends_of_liftsAtResiduePoint, which produces from versality the extension of a lift's structure arrow to x, composed with Deformation.Artin.exists_canonicalTangentMap_eq_of_extends, which computes the class of an extendable lift as the image of a tangent vector. Dually — Stacks 07YK — this surjectivity is the injectivity of H^0(ξ ⊗ᴸ_A k), which is condition (2) of the tag in degree 0.

public theorem surjective_canonicalTangentMap_of_liftsAtResiduePoint [Mono baseMap]
    (hlifts : LiftsAtResiduePoint (Λ := R) (k := k) iR (p ⋙ Over.post B.inclusion)
      (Over.mk toS) x hxS (Spec.map (CommRingCat.ofHom (algebraMap A k)))) :
    letI : p.IsFibered := hp.isFibered
    Function.Surjective (fun θ : Ω[A⁄Λ] →ₗ[A] k =>
      canonicalFieldBaseChangeEquiv A k B S hS toS hA p x hx hp hRS hk hAk hkk
        ((tangentFunctor A B S hS toS hA p x hx hp hRS).liftEquiv
          (⟨ModuleCat.of A k, hk⟩ : SiteModule A B)
          (canonicalTangentMap Λ A k B S hS toS hA p x hx hp hRS hΩ hk baseMap
            baseFactorization θ)))

Deformation.Artin.liftsAtResiduePoint_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityFieldVersalLift.lean, line 493. The attribute's comment: “versality as the lifting property at the residue field of the prime”.

Stacks 07YM. Versality of x at u₀ is the lifting property at the point of Spec A determined by the algebra structure of the residue field Ideal.ResidueField u₀.asIdeal of the prime -- the field in which the whole 07YM lift chain is written.

Deformation.Artin.IsVersalAt is literally the lifting property at the canonical residue-field point Spec (U.left.residueField u₀) ⟶ U.left (Deformation.Artin.isVersalAt_iff_liftsAtResiduePoint), and the property transports along an isomorphism of residue fields over the local ring (Deformation.Artin.liftsAtResiduePoint_changeResidueField); the isomorphism is the one induced by AlgebraicGeometry.Scheme.Spec.residueFieldIso, and it carries the canonical point to the one written here.

public theorem liftsAtResiduePoint_of_isVersalAt
    (hversal : IsVersalAt (Over.mk toS) q u₀ x hx) :
    LiftsAtResiduePoint (Λ := S.presheaf.stalk (basePoint (Over.mk toS) u₀))
      (k := u₀.asIdeal.ResidueField) (alg := primeResidueFieldAlgebra toS u₀)
      (S.fromSpecStalk (basePoint (Over.mk toS) u₀)) q (Over.mk toS) x hx
      (Spec.map (CommRingCat.ofHom (algebraMap A u₀.asIdeal.ResidueField)))

Deformation.Artin.exists_algHom_section_of_surjective_derivedTensorFibre_neg_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityObstructionVanishing.lean, line 404. The attribute's comment: “(2) implies (1): condition (2) in degree -1 forces the obstruction class of a square-zero extension with one-dimensional kernel to vanish, so the extension splits”.

Stacks 07YM, the obstruction step of (2) ⇒ (1). Let A' → A be a square-zero surjection of Λ-algebras whose kernel I is one-dimensional over an A-algebra field k, and let ξ : E ⟶ NL_{A/Λ} be a morphism of D⁻(A) with H^{-1}(ξ ⊗ᴸ_A k) surjective. If ξ composed with NL_{A/Λ} ⟶ NL_{A/A'} vanishes, then A' → A admits a Λ-algebra section.

Condition (2) in degree -1 kills the extension class NL_{A/Λ} ⟶ I[1] of the thickening (Deformation.Artin.cotangentExtensionClass_eq_zero_of_surjective_derivedTensorFibre_neg_one). Computed through the canonical presentation of A over Λ (Deformation.Artin.derivedNaiveCotangentComplexIso_hom_comp_cotangentExtensionClass), that class is the map J/J² → I, f ↦ f(a'_1, …), read in the derived category, and its vanishing makes that map factor through the differential J/J² → ⊕_i A dx_i (Deformation.Artin.exists_comp_eq_of_Q_map_twoTermProjection_comp_eq_zero). Correcting the chosen lifts of the generators by the factorization produces lifts at which every element of J vanishes, hence the section (Deformation.Artin.exists_algHom_section_of_cotangentComplex_comp_eq).

public theorem exists_algHom_section_of_surjective_derivedTensorFibre_neg_one
    (hq : Function.Surjective (algebraMap A' A))
    (hsq : RingHom.ker (algebraMap A' A) ^ 2 = ⊥)
    (eI : letI := Stacks.Smooth.kerModule hq hsq
      RingHom.ker (algebraMap A' A) ≃ₗ[A] k)
    (T : DerivedTensorProduct A) (E : DerivedCategory (ModuleCat.{u} A))
    (hE : (DerivedCategory.TStructure.t (C := ModuleCat.{u} A)).minus E)
    (ξ : E ⟶ derivedNaiveCotangentComplex Λ A)
    (hsurj : Function.Surjective
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-1)).map
        ((T.tensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
            (ModuleCat.of A k))).map ξ)))
    (hkill : ξ ≫ naiveCotangentBaseMap Λ A' A = 0) :
    ∃ σ : A →ₐ[Λ] A', (algebraMap A' A).comp (σ : A →+* A') = RingHom.id A

Deformation.ArtinianLocalAlgCat.isEssentialSurjection_powQuotientMap_of_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityPowQuotientEssential.lean, line 68. The attribute's comment: “A'/(𝔭') ^ n ⟶ A/𝔭 ^ n is an essential surjection of 𝒞_Λ”.

The essential surjection of [Stacks, Tag 07YM]. Let Λ → A' → A → k be a tower with k a field and both maps onto k surjective, let 𝔭 and 𝔭' be the two augmentation ideals and let n ≥ 2. If A' → A does not change differentials modulo k, then the induced morphism A' ⧸ (𝔭') ^ n ⟶ A ⧸ 𝔭 ^ n of 𝒞_Λ is an essential surjection.

Deformation.Artin.differentialsBaseChangeMap_bijective_powQuotient transfers the bijectivity to the quotients and Deformation.ArtinianLocalAlgCat.isEssentialSurjection_iff_bijective_differentialsBaseChangeMap is [Stacks, Tag 06H0]; what this adds is the identification of the algebra structures rebuilt from ε, ε' and φ with the ambient ones, which Algebra.algebra_ext provides and which the proof then substitutes.

public theorem isEssentialSurjection_powQuotientMap_of_bijective
    {Λ A' A k : Type u} [CommRing Λ] [Field k] [Algebra Λ k] [CommRing A'] [CommRing A]
    [Algebra Λ A'] [Algebra Λ A] [IsNoetherianRing A'] [IsNoetherianRing A]
    [Algebra A' A] [Algebra A' k] [Algebra A k]
    [IsScalarTower Λ A' A] [IsScalarTower Λ A' k] [IsScalarTower Λ A k] [IsScalarTower A' A k]
    (ε : A →ₐ[Λ] k) (hεeq : ∀ a, ε a = algebraMap A k a) (hε : Function.Surjective ε)
    (ε' : A' →ₐ[Λ] k) (hε'eq : ∀ a', ε' a' = algebraMap A' k a')
    (hε' : Function.Surjective ε')
    (φ : A' →ₐ[Λ] A) (hφeq : ∀ a', φ a' = algebraMap A' A a') (hφ : ε.comp φ = ε')
    (n : ℕ) [NeZero n] (hn : 2 ≤ n)
    (hbij : Function.Bijective (Deformation.Artin.differentialsBaseChangeMap Λ A' A k)) :
    IsEssentialSurjection (powQuotientMap hφ hε' hε n)

Deformation.Artin.liftsAtResiduePoint_prime_base_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityPrimeBase.lean, line 135. The attribute's comment: “versality over any affine base at the residue field of the prime”.

Stacks 07YM, versality in the form the degree -1 endgame consumes. If x is versal at a point u₀ of Spec A, then the lifting property holds with any Spec Λ ⟶ S as deformation base, at the point of Spec A determined by the A-algebra structure of the residue field Ideal.ResidueField u₀.asIdeal of the prime.

Deformation.Artin.liftsAtResiduePoint_of_isVersalAt is versality read at that field over the local ring 𝒪_{S,s}, and Deformation.Artin.liftsAtResiduePoint_changeBase moves the base to Λ; the compatibility of the residue point with the local ring that the move asks for is Deformation.Artin.specMap_primeResidueFieldAlgebra_comp_fromSpecStalk, and the locality of the structure map is Deformation.Artin.isLocalHom_primeResidueFieldAlgebra.

Nothing is asked of Spec Λ ⟶ S: not that it be an open immersion, nor a monomorphism.

public theorem liftsAtResiduePoint_prime_base_of_isVersalAt
    (hversal : IsVersalAt (Over.mk toS) q u₀ x hx) :
    LiftsAtResiduePoint (Λ := Λ) (k := u₀.asIdeal.ResidueField) iΛ q (Over.mk toS) x hx
      (Spec.map (CommRingCat.ofHom (algebraMap A u₀.asIdeal.ResidueField)))

Deformation.Artin.differentialsBaseChangeMap_bijective_powQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityQuotientDifferentials.lean, line 156. The attribute's comment: “A'/(𝔭') ^ n ⟶ A/𝔭 ^ n does not change differentials either”.

The quotient transfer of [Stacks, Tag 07YL]'s bijectivity. Let A' → A be a map of Λ-algebras with compatible surjective augmentations onto a field k, let 𝔭 = Ker ε and 𝔭' = Ker ε', and let n ≥ 2. If A' → A does not change differentials modulo k, neither does the induced map A' ⧸ (𝔭') ^ n ⟶ A ⧸ 𝔭 ^ n.

This is Deformation.Artin.differentialsBaseChangeMap_bijective_of_square at the square whose vertical maps are the two quotient maps: each is surjective, and the kernel of A' → A' ⧸ (𝔭') ^ n is (𝔭') ^ n ≤ (𝔭') ^ 2, the augmentation ideal being the kernel of A' ⟶ k. Composed with Deformation.ArtinianLocalAlgCat.isEssentialSurjection_iff_bijective_differentialsBaseChangeMap it says that A' ⧸ (𝔭') ^ n ⟶ A ⧸ 𝔭 ^ n is an essential surjection of 𝒞_Λ, which is the contradiction the direction (1) ⇒ (2) of [Stacks, Tag 07YM] drives at.

public theorem differentialsBaseChangeMap_bijective_powQuotient
    {ε' : A' →ₐ[Λ] k} {ε : A →ₐ[Λ] k} {φ : A' →ₐ[Λ] A} (hφ : ε.comp φ = ε')
    (n : ℕ) [NeZero n] (hn : 2 ≤ n) :
    letI : Algebra A' A := φ.toRingHom.toAlgebra
    letI : Algebra A' k := ε'.toRingHom.toAlgebra
    letI : Algebra A k := ε.toRingHom.toAlgebra
    letI : IsScalarTower Λ A' A := .of_algebraMap_eq fun l => (φ.commutes l).symm
    letI : IsScalarTower Λ A' k := .of_algebraMap_eq fun l => (ε'.commutes l).symm
    letI : IsScalarTower Λ A k := .of_algebraMap_eq fun l => (ε.commutes l).symm
    letI : IsScalarTower A' A k :=
      .of_algebraMap_eq fun a => (DFunLike.congr_fun hφ a).symm
    letI : Algebra (A' ⧸ RingHom.ker ε'.toRingHom ^ n) (A ⧸ RingHom.ker ε.toRingHom ^ n) :=
      (powQuotientMapAlgHom hφ n).toRingHom.toAlgebra
    letI : Algebra (A' ⧸ RingHom.ker ε'.toRingHom ^ n) k :=
      (powQuotientAug ε' n).toRingHom.toAlgebra
    letI : Algebra (A ⧸ RingHom.ker ε.toRingHom ^ n) k :=
      (powQuotientAug ε n).toRingHom.toAlgebra
    letI : IsScalarTower Λ (A' ⧸ RingHom.ker ε'.toRingHom ^ n)
        (A ⧸ RingHom.ker ε.toRingHom ^ n) :=
      .of_algebraMap_eq fun l => ((powQuotientMapAlgHom hφ n).commutes l).symm
    letI : IsScalarTower Λ (A' ⧸ RingHom.ker ε'.toRingHom ^ n) k :=
      .of_algebraMap_eq fun l => ((powQuotientAug ε' n).commutes l).symm
    letI : IsScalarTower Λ (A ⧸ RingHom.ker ε.toRingHom ^ n) k :=
      .of_algebraMap_eq fun l => ((powQuotientAug ε n).commutes l).symm
    letI : IsScalarTower (A' ⧸ RingHom.ker ε'.toRingHom ^ n)
        (A ⧸ RingHom.ker ε.toRingHom ^ n) k :=
      .of_algebraMap_eq fun b => (powQuotientAug_powQuotientMapAlgHom hφ n b).symm
    Function.Bijective (differentialsBaseChangeMap Λ A' A k) →
      Function.Bijective (differentialsBaseChangeMap Λ
        (A' ⧸ RingHom.ker ε'.toRingHom ^ n) (A ⧸ RingHom.ker ε.toRingHom ^ n) k)

Deformation.Artin.schemeMap_restrictAlongArrow_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityRestriction.lean, line 179. The attribute's comment: “the restriction of x along a ring map, over Spec of that map”.

The bridge from a ring map to an arrow of the fibred category. For a ring map φ : A → C compatible with the structure morphisms, the restriction Deformation.Artin.restrictAlong is an object lying over Spec C whose structure arrow to x has underlying morphism of schemes exactly Spec φ.

This is the shape Deformation.Artin.LiftsAtResiduePoint consumes, with the two bases presented as objects of the slice over S.

public theorem schemeMap_restrictAlongArrow_mk
    (hw : (p ⋙ Over.post B.inclusion).obj x = Over.mk toS) :
    schemeMap (p ⋙ Over.post B.inclusion)
        (restrictAlong_objS φ B S hS toS toSC hA hC hφ p x hx) hw
        (restrictAlongArrow φ B S hS toS toSC hA hC hφ p x hx) =
      Spec.map (CommRingCat.ofHom φ)

Deformation.Artin.comp_ringHom_of_schemeMap_of_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalitySquareLift.lean, line 117. The attribute's comment: “i ≫ b = a read as an identity of ring maps”.

An equation of arrows of the fibred category, read as an identity of ring maps. Let i : y ⟶ z, b : z ⟶ x and a : y ⟶ x be arrows with i ≫ b = a, between objects presented over S by spectra of rings, and suppose the morphisms of schemes underlying i and a are the spectra of ring maps f and g. Then f composed with the ring map underlying b is g.

Both ends being affine, Deformation.Artin.schemeMap_comp turns the equation into an equation of morphisms of affine schemes, and the faithfulness of Scheme.Spec turns that into the identity of ring maps. This is what converts the conclusion i ≫ b = a of Deformation.Artin.LiftsAtResiduePoint into the hypothesis ∀ a, f (σ a) = Ideal.Quotient.mk (𝔭 ^ n) a of Deformation.ArtinianLocalAlgCat.not_isEssentialSurjection_of_lift_powQuotient.

public theorem comp_ringHom_of_schemeMap_of_comp_eq
    {A C C' : Type u} [CommRing A] [CommRing C] [CommRing C']
    {S : Scheme.{u}} {toS : Spec (CommRingCat.of A) ⟶ S}
    {toSC : Spec (CommRingCat.of C) ⟶ S} {toSC' : Spec (CommRingCat.of C') ⟶ S}
    {Y : Type v} [Category.{w} Y] (q : Y ⥤ Over S) {y z x : Y}
    (hy : q.obj y = Over.mk toSC) (hz : q.obj z = Over.mk toSC')
    (hx : q.obj x = Over.mk toS)
    {i : y ⟶ z} {b : z ⟶ x} {a : y ⟶ x} (hab : i ≫ b = a)
    {f : C' →+* C} (hi : schemeMap q hy hz i = Spec.map (CommRingCat.ofHom f))
    {g : A →+* C} (ha : schemeMap q hy hx a = Spec.map (CommRingCat.ofHom g)) :
    f.comp (ringHom_of_schemeMap (schemeMap q hz hx b)) = g

Deformation.Artin.exists_algHom_powQuotient_of_liftsAtResiduePoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalitySquareLift.lean, line 158. The attribute's comment: “versality lifts A through A'/(𝔭') ^ n”.

The section of [Stacks, Tag 07YM]. Let A' → A be a map of augmented Noetherian Λ-algebras over a field κ, with φ surjective, let x be a family over Spec A and x' a lift of it to Spec A', presented over S through the affine open Spec Λ ⟶ S. If the lifting property defining versality holds at the residue point of A determined by its augmentation, then the quotient map A → A ⧸ 𝔭 ^ n lifts through the small extension A' ⧸ (𝔭') ^ n ⟶ A ⧸ 𝔭 ^ n to a Λ-algebra map σ : A →ₐ[Λ] A' ⧸ (𝔭') ^ n.

The two restrictions are the chosen pullbacks Deformation.Artin.restrictAlong, the arrow between them is Deformation.Artin.exists_unique_schemeMap_eq_of_square applied to the commuting square of rings A' → A → A ⧸ 𝔭 ^ n and A' → A' ⧸ (𝔭') ^ n → A ⧸ 𝔭 ^ n, the residue condition that versality asks of the arrow to x is the compatibility of the induced augmentation with the quotient map, and the ring map is read off the resulting arrow by Deformation.Artin.algHom_of_schemeMap_over, whose output is the identity Deformation.Artin.comp_ringHom_of_schemeMap_of_comp_eq converts.

public theorem exists_algHom_powQuotient_of_liftsAtResiduePoint
    (ε : A →ₐ[Λ] κ) (hε : Function.Surjective ε)
    (ε' : A' →ₐ[Λ] κ) (hε' : Function.Surjective ε')
    (φ : A' →ₐ[Λ] A) (hφ : ε.comp φ = ε') (hsurjφ : Function.Surjective φ)
    (n : ℕ) [NeZero n]
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (toS : Spec (CommRingCat.of A) ⟶ S) (hA : B.Contains (Spec (CommRingCat.of A)))
    (hA' : B.Contains (Spec (CommRingCat.of A')))
    (baseMap : Spec (CommRingCat.of Λ) ⟶ S) [Mono baseMap]
    (hbase : Spec.map (CommRingCat.ofHom (algebraMap Λ A)) ≫ baseMap = toS)
    (hC : B.Contains (Spec (CommRingCat.of (A ⧸ RingHom.ker ε.toRingHom ^ n))))
    (hC' : B.Contains (Spec (CommRingCat.of (A' ⧸ RingHom.ker ε'.toRingHom ^ n))))
    (p : X ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) (x x' : X)
    (hx : p.obj x = algebraOver A B S hS toS hA)
    (hxS : (p ⋙ Over.post B.inclusion).obj x = Over.mk toS)
    (hx' : p.obj x' = algebraOver A' B S hS
      (Spec.map (CommRingCat.ofHom (algebraMap Λ A')) ≫ baseMap) hA')
    (hx'S : (p ⋙ Over.post B.inclusion).obj x' =
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap Λ A')) ≫ baseMap))
    (lift : x ⟶ x')
    (hlift : schemeMap (p ⋙ Over.post B.inclusion) hxS hx'S lift =
      Spec.map (CommRingCat.ofHom φ.toRingHom))
    (hlifts : LiftsAtResiduePoint (Λ := Λ) (k := κ) baseMap (p ⋙ Over.post B.inclusion)
      (Over.mk toS) x hxS (Spec.map (CommRingCat.ofHom ε.toRingHom))) :
    ∃ σ : A →ₐ[Λ] (powQuotientObj ε' hε' n : Type u),
      ∀ t : A, (powQuotientMap hφ hε' hε n).hom (σ t) =
        Ideal.Quotient.mk (RingHom.ker ε.toRingHom ^ n) t

Deformation.Artin.liftsAtResiduePoint_changeBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityStalkBase.lean, line 337. The attribute's comment: “the lifting property over the local ring of S transfers to the affine open”.

The change of deformation base. If the lifting property defining versality holds with the local ring of S at s as deformation base, it holds with any Λ whose spectrum maps to S compatibly with the chosen residue point.

Every Artinian local Λ-algebra occurring in a lifting problem has its residue point at the chosen point of S — for the target because the lifting property already imposes that of the arrow a, read through Deformation.Artin.schemeMap_over, and for the source because the surjection is Λ-linear and respects the residue identifications — so each is canonically an 𝒪_{S,s}-algebra (Deformation.Artin.stalkObj), the surjection between them is a morphism of 𝒞_{𝒪_{S,s}} with the same underlying ring map (Deformation.Artin.stalkHom), and the two presentations of each base over S agree (Deformation.Artin.specMap_stalkAlgebra_comp_fromSpecStalk).

Nothing is asked of iΛ: not that it be an open immersion, nor even a monomorphism. The factorization through the local ring is produced at the level of schemes, so 𝒪_{S,s} is never identified with a localization of Λ.

public theorem liftsAtResiduePoint_changeBase
    (hstalk : LiftsAtResiduePoint (Λ := S.presheaf.stalk s) (k := k) (alg := algStalk)
      (S.fromSpecStalk s) q U x hx κ) :
    LiftsAtResiduePoint (Λ := Λ) (k := k) iΛ q U x hx κ

Deformation.Artin.liftsAtResiduePoint_base_of_isVersalAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityStalkBase.lean, line 404. The attribute's comment: “versality gives the lifting property over any affine deformation base”.

Versality at a point, read with an arbitrary affine deformation base. If x is versal at u₀ then the lifting property holds with any Spec Λ ⟶ S as deformation base, at the canonical residue-field point of u₀.

Deformation.Artin.IsVersalAt is literally the lifting property with the local ring of S at the image of u₀ as base (Deformation.Artin.isVersalAt_iff_liftsAtResiduePoint), and Deformation.Artin.liftsAtResiduePoint_changeBase moves the base; the one compatibility it asks of the residue point is that it factor through that local ring, which is AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk.

This is the form the degree -1 half of the direction (1) ⇒ (2) of [Stacks, Tag 07YM] consumes: the small extension it tests versality against is built from Λ-algebras, Λ being the ring of the affine open the family maps into, and the objects of 𝒞_{𝒪_{S,s}} are not available to it. Nothing is asked of iΛ — in particular not that it be an open immersion.

public theorem liftsAtResiduePoint_base_of_isVersalAt
    (hversal : IsVersalAt U q u₀ x hx) :
    LiftsAtResiduePoint (Λ := Λ) (k := U.left.residueField u₀) iΛ q U x hx
      (U.left.fromSpecResidueField u₀)

Deformation.Artin.naiveVersalityCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityTag.lean, line 94.

Stacks 07YM. Let S be a locally Noetherian scheme, let 𝒳 be a category fibred in groupoids over the big fppf site of S satisfying (RS*), let U = Spec A be affine of finite type over S mapping into an affine open Spec Λ ⊆ S, let x be an object of 𝒳 over U, and let ξ : E ⟶ NL_{A/Λ} be a morphism of D⁻(A) such that

1. for every deformation situation (x, A' → A) the object x lifts to Spec A' exactly when E ⟶ NL_{A/Λ} ⟶ NL_{A/A'} is zero, and
2. there is an isomorphism of functors T_x(−) ⟶ Ext⁰_A(E, −) carrying the canonical element to E ⟶ NL_{A/Λ} ⟶ Ω_{A/Λ}.

Let u₀ ∈ U be a finite type point with residue field k. Then x is versal at u₀ as soon as ξ induces a surjection H^{-1}(E ⊗ᴸ_A k) ⟶ H^{-1}(NL_{A/Λ} ⊗ᴸ_A k) and an injection H^0(E ⊗ᴸ_A k) ⟶ H^0(NL_{A/Λ} ⊗ᴸ_A k); and conversely, if u₀ is a closed point at which x is versal, then ξ induces such a surjection and such an injection.

Both directions are stated at once, as the predicate Deformation.Artin.NaiveVersalityCriterion which [Stacks, Tag 07YN] and [Stacks, Tag 07YU] consume as a hypothesis.

public theorem naiveVersalityCriterion : NaiveVersalityCriterion hp hRS P hΩ E ξ

Deformation.Artin.tangentEquiv_canonicalTangentMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityTangentFactorization.lean, line 90. The attribute's comment: “the map on tangent spaces factors through the augmentation”.

Stacks 07YM, hypothesis (ii) in use. Under the functorial isomorphism T_x(-) ≅ Ext⁰_A(E, -) of hypothesis (ii), the map on tangent spaces of Stacks 07YC sends a tangent vector θ : Ω_{A/Λ} →ₗ[A] k to ξ followed by the augmentation Deformation.Artin.naiveCotangentToDifferentials followed by θ.

This is the naturality of the isomorphism at the morphism of site modules attached to θ, together with its prescribed value at the canonical element: Deformation.Artin.canonicalTangentMap is by definition the image of the canonical element under that morphism.

public theorem tangentEquiv_canonicalTangentMap (θ : Ω[A⁄Λ] →ₗ[A] k) :
    tangentEquiv (⟨ModuleCat.of A k, hk⟩ : SiteModule A B)
        (canonicalTangentMap Λ A k B S hS toS hA p x hx hp hRS hΩ hk baseMap
          baseFactorization θ) =
      ξ ≫ naiveCotangentToDifferentials Λ A ≫
        (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).map (ModuleCat.ofHom θ)

Deformation.Artin.length_ker_eq_one_of_linearEquiv_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityThickeningSite.lean, line 241. The attribute's comment: “the kernel I of A' → A has length one over A'”.

The length-one hypothesis of Deformation.ArtinianLocalAlgCat.isSmallExtension_powQuotientMap. The kernel of the thickening of [Stacks, Tag 07YL] has length one over A': it is a copy of the residue field at a maximal ideal of A, hence a simple A-module (Deformation.Artin.isSimpleModule_residueField), and the A'-submodules of it are its A-submodules because the two actions agree through the surjection A' → A (isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective).

public theorem length_ker_eq_one_of_linearEquiv_residueField
    (p : Ideal A) [p.IsMaximal]
    (e : RingHom.ker (algebraMap A' A) ≃ₗ[A] p.ResidueField) :
    Module.length A' (RingHom.ker (algebraMap A' A)) = 1

Deformation.Artin.mul_ker_eq_bot_of_linearEquiv_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityThickeningSite.lean, line 262. The attribute's comment: “𝔭' annihilates the kernel I of A' → A”.

The Artin–Rees input of [Stacks, Tag 07YM]. An ideal of A' carried by the surjection A' → A into the kernel of A ⟶ κ(𝔭) annihilates the kernel I of that surjection: the two actions on I agree, and I is a copy of κ(𝔭), on which 𝔭 acts by zero.

Applied with q = Ker(A' ⟶ κ(𝔭)) this is the hypothesis 𝔭' · I = 0 of Deformation.Artin.exists_pow_inf_eq_bot_of_mul_eq_bot, which produces the exponent n > 1 with (𝔭') ^ n ⊓ I = 0. Only primality of 𝔭 is used.

public theorem mul_ker_eq_bot_of_linearEquiv_residueField
    (p : Ideal A) [p.IsPrime]
    (e : RingHom.ker (algebraMap A' A) ≃ₗ[A] p.ResidueField)
    (q : Ideal A')
    (hq : ∀ a' ∈ q, algebraMap A' A a' ∈ RingHom.ker (algebraMap A p.ResidueField)) :
    q * RingHom.ker (algebraMap A' A) = ⊥

Deformation.ArtinianLocalAlgCat.powQuotientObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/AugmentedPowQuotient.lean, line 143. The attribute's comment: “the object A/𝔭 ^ n of 𝒞_Λ at a closed point”. References: EGA 0 (19.5.6.2), “special case”.

The object R ⧸ 𝔭 ^ n of 𝒞_Λ, for 𝔭 = Ker ε the augmentation ideal of a surjective augmentation of a Noetherian Λ-algebra and n ≠ 0. The algebra R itself is not asked to be local or Artinian.

public noncomputable def powQuotientObj [IsNoetherianRing R] (ε : R →ₐ[Λ] k)
    (hε : Function.Surjective ε) (n : ℕ) [NeZero n] : ArtinianLocalAlgCat.{u, v, w} Λ k

Deformation.ArtinianLocalAlgCat.maximalIdeal_pow_powQuotientObj_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/AugmentedPowQuotient.lean, line 169. The attribute's comment: “the maximal ideal of the object A'/(𝔭') ^ n of 𝒞_Λ has vanishing power”.

The n-th power of the maximal ideal of R ⧸ 𝔭 ^ n vanishes. This is the hypothesis 𝔪_{B'} ^ n = 0 of Deformation.ArtinianLocalAlgCat.not_isEssentialSurjection_of_lift_powQuotient, read at the object Deformation.ArtinianLocalAlgCat.powQuotientObj of 𝒞_Λ rather than at the bare quotient ring; it is IsLocalRing.maximalIdeal_quotient_pow_pow_eq_bot, the augmentation ideal being maximal.

public theorem maximalIdeal_pow_powQuotientObj_eq_bot [IsNoetherianRing R] (ε : R →ₐ[Λ] k)
    (hε : Function.Surjective ε) (n : ℕ) [NeZero n] :
    maximalIdeal (powQuotientObj ε hε n : Type v) ^ n = ⊥

Deformation.ArtinianLocalAlgCat.ker_powQuotientMapAlgHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/AugmentedPowQuotient.lean, line 235. The attribute's comment: “the kernel of A'/(𝔭') ^ n ⟶ A/𝔭 ^ n is the image of I = Ker(A' → A)”.

The kernel computation of [Stacks, Tag 07YM]. For φ : R' ↠ R surjective, the kernel of R' ⧸ (𝔭') ^ n ⟶ R ⧸ 𝔭 ^ n is the image of Ker φ.

The preimage of 𝔭 ^ n under φ is (𝔭') ^ n + Ker φ, because 𝔭 ^ n is the image of (𝔭') ^ n; passing to R' ⧸ (𝔭') ^ n kills the first summand.

public theorem ker_powQuotientMapAlgHom {ε' : R' →ₐ[Λ] k} {ε : R →ₐ[Λ] k} {φ : R' →ₐ[Λ] R}
    (hφ : ε.comp φ = ε') (n : ℕ) (hsurj : Function.Surjective φ) :
    RingHom.ker (powQuotientMapAlgHom hφ n).toRingHom =
      (RingHom.ker φ.toRingHom).map
        (Ideal.Quotient.mk (RingHom.ker ε'.toRingHom ^ n))

Deformation.ArtinianLocalAlgCat.powQuotientMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/AugmentedPowQuotient.lean, line 257. The attribute's comment: “the morphism A'/(𝔭') ^ n ⟶ A/𝔭 ^ n of 𝒞_Λ”.

The morphism R' ⧸ (𝔭') ^ n ⟶ R ⧸ 𝔭 ^ n of 𝒞_Λ induced by a map of augmented Noetherian algebras.

public noncomputable def powQuotientMap [IsNoetherianRing R'] [IsNoetherianRing R]
    {ε' : R' →ₐ[Λ] k} {ε : R →ₐ[Λ] k} {φ : R' →ₐ[Λ] R} (hφ : ε.comp φ = ε')
    (hε' : Function.Surjective ε') (hε : Function.Surjective ε) (n : ℕ) [NeZero n] :
    powQuotientObj ε' hε' n ⟶ powQuotientObj ε hε n

Deformation.ArtinianLocalAlgCat.isSmallExtension_powQuotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/AugmentedPowQuotient.lean, line 294. The attribute's comment: “A'/(𝔭') ^ n ⟶ A/𝔭 ^ n is a small extension”.

The small extension of [Stacks, Tag 07YM]. Let φ : R' ↠ R be a surjection of augmented Noetherian Λ-algebras whose kernel I has length one over R', and suppose (𝔭') ^ n ⊓ I = 0. Then R' ⧸ (𝔭') ^ n ⟶ R ⧸ 𝔭 ^ n is a small extension of Artinian local rings.

The kernel is the image of I by ker_powQuotientMapAlgHom, and (𝔭') ^ n ⊓ I = 0 makes that image a copy of I, hence again of length one. In the source I is a one-dimensional k-vector space and the hypothesis (𝔭') ^ n ⊓ I = 0 is the conclusion of the Artin–Rees step Deformation.Artin.exists_pow_inf_eq_bot_of_mul_eq_bot.

public theorem isSmallExtension_powQuotientMap [IsNoetherianRing R'] [IsNoetherianRing R]
    {ε' : R' →ₐ[Λ] k} {ε : R →ₐ[Λ] k} {φ : R' →ₐ[Λ] R} (hφ : ε.comp φ = ε')
    (hε' : Function.Surjective ε') (hε : Function.Surjective ε)
    (hsurj : Function.Surjective φ) (n : ℕ) [NeZero n]
    (hinf : RingHom.ker ε'.toRingHom ^ n ⊓ RingHom.ker φ.toRingHom = ⊥)
    (hlen : Module.length R' (RingHom.ker φ.toRingHom) = 1) :
    InfinitesimalLifting.IsSmallExtension
      (CommRingCat.ofHom (powQuotientMap hφ hε' hε n).hom.toRingHom)

Deformation.ArtinianLocalAlgCat.exists_section_of_lift_powQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/AugmentedPowQuotientSection.lean, line 95. The attribute's comment: “the lift factors through A/𝔭 ^ n, giving a section of the small extension”.

The section of [Stacks, Tag 07YM]. If the quotient map R → R ⧸ 𝔭 ^ n lifts through a morphism f : C ⟶ R ⧸ 𝔭 ^ n of 𝒞_Λ whose source has 𝔪_C ^ n = 0, then f has a section in 𝒞_Λ.

The lift factors through R ⧸ 𝔭 ^ n by IsLocalRing.exists_isLocalHom_comp_mk_pow, and the factorization is a morphism of 𝒞_Λ: it is a Λ-algebra map because σ is, it is local by that lemma, and it respects the identifications of the residue fields because f does.

public theorem exists_section_of_lift_powQuotient
    (hn : maximalIdeal (C : Type v) ^ n = ⊥) :
    ∃ s : powQuotientObj ε hε n ⟶ C, s ≫ f = 𝟙 (powQuotientObj ε hε n)

Deformation.ArtinianLocalAlgCat.not_isEssentialSurjection_of_lift_powQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/BaseCategory/AugmentedPowQuotientSection.lean, line 125. The attribute's comment: “a lift of A through A'/(𝔭') ^ n contradicts essential surjectivity”.

The contradiction of [Stacks, Tag 07YM]. A small extension f : C ⟶ R ⧸ 𝔭 ^ n of 𝒞_Λ whose source has 𝔪_C ^ n = 0 and through which the quotient map R → R ⧸ 𝔭 ^ n lifts is not an essential surjection: the lift produces a section (Deformation.ArtinianLocalAlgCat.exists_section_of_lift_powQuotient), and a small extension with a section is not essential (Deformation.not_isEssentialSurjection_iff_exists_section).

public theorem not_isEssentialSurjection_of_lift_powQuotient
    (hn : maximalIdeal (C : Type v) ^ n = ⊥)
    (hf : InfinitesimalLifting.IsSmallExtension (CommRingCat.ofHom f.hom.toRingHom)) :
    ¬ IsEssentialSurjection f

isLocalRing_quotient_pow_of_isMaximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RadicalMaximalQuotient.lean, line 109. The attribute's comment: “the local half of A/𝔭 ^ n, for 𝔭 the prime of a closed point”.

For a maximal ideal p of a ring that need not be local and n ≠ 0, the ring R ⧸ p ^ n is local.

public theorem isLocalRing_quotient_pow_of_isMaximal (p : Ideal R) [p.IsMaximal] {n : ℕ}
    (hn : n ≠ 0) : IsLocalRing (R ⧸ p ^ n)

isArtinianRing_quotient_pow_of_isMaximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RadicalMaximalQuotient.lean, line 116. The attribute's comment: “the Artinian half of A/𝔭 ^ n, for 𝔭 the prime of a closed point”.

For a maximal ideal p of a Noetherian ring that need not be local and n ≠ 0, the ring R ⧸ p ^ n is Artinian.

public theorem isArtinianRing_quotient_pow_of_isMaximal [IsNoetherianRing R] (p : Ideal R)
    [p.IsMaximal] {n : ℕ} (hn : n ≠ 0) : IsArtinianRing (R ⧸ p ^ n)

IsLocalRing.maximalIdeal_quotient_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RadicalMaximalQuotient.lean, line 143. The attribute's comment: “the maximal ideal of A/𝔭 ^ n, for 𝔭 the prime of a closed point”.

For a maximal ideal p and n ≠ 0, the maximal ideal of R ⧸ p ^ n is the image of p.

public theorem IsLocalRing.maximalIdeal_quotient_pow (p : Ideal R) [p.IsMaximal] (n : ℕ)
    [NeZero n] :
    IsLocalRing.maximalIdeal (R ⧸ p ^ n) = p.map (Ideal.Quotient.mk (p ^ n))

IsLocalRing.maximalIdeal_quotient_pow_pow_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RadicalMaximalQuotient.lean, line 159. The attribute's comment: “the maximal ideal of A'/(𝔭') ^ n has vanishing n-th power”.

For a maximal ideal p and n ≠ 0, the n-th power of the maximal ideal of R ⧸ p ^ n vanishes: that maximal ideal is the image of p, so its n-th power is the image of p ^ n, which is the ideal being quotiented out.

This is the hypothesis 𝔪_{B'} ^ n = 0 under which a lift of R through a morphism onto R ⧸ p ^ n factors (IsLocalRing.exists_isLocalHom_comp_mk_pow), and in [Stacks, Tag 07YM] it is the sentence "since the maximal ideal of B' has nth power equal to zero". The ring R is not asked to be local.

public theorem IsLocalRing.maximalIdeal_quotient_pow_pow_eq_bot (p : Ideal R) [p.IsMaximal]
    (n : ℕ) [NeZero n] : IsLocalRing.maximalIdeal (R ⧸ p ^ n) ^ n = ⊥

IsLocalRing.exists_isLocalHom_comp_mk_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RadicalMaximalQuotient.lean, line 205. The attribute's comment: “σ : A → B' with 𝔪_{B'} ^ n = 0 factors through A/𝔭 ^ n”.

The local factorization of [Stacks, Tag 07YM]. A ring map σ : R → S into a local ring whose maximal ideal satisfies 𝔪_S ^ n = 0 factors through R ⧸ p ^ n for every ideal p whose image under σ lies in 𝔪_S, and the factorization is a local homomorphism as soon as p is maximal and n ≠ 0.

The ring R is not asked to be local: in the source σ goes from the finite-type algebra A to an Artinian local ring B' and p is the prime of the closed point, so the hypothesis p.map σ ≤ 𝔪_S — rather than IsLocalHom σ — is what is available. Maximality of p and n ≠ 0 are used only to make R ⧸ p ^ n a local ring, hence only for the IsLocalHom half; the factorization itself is Ideal.Quotient.lift applied to Ideal.pow_le_ker_of_map_le and holds for an arbitrary ideal p and arbitrary n.

public theorem IsLocalRing.exists_isLocalHom_comp_mk_pow [IsLocalRing S] (f : R →+* S)
    (p : Ideal R) [p.IsMaximal] {n : ℕ} [NeZero n]
    (hp : p.map f ≤ IsLocalRing.maximalIdeal S)
    (hn : IsLocalRing.maximalIdeal S ^ n = ⊥) :
    ∃ F : R ⧸ p ^ n →+* S, IsLocalHom F ∧ F.comp (Ideal.Quotient.mk (p ^ n)) = f

Tag 07YN, a lemma

Tag 07YN in the Stacks Project.

Deformation.Artin.isOpenVersalityAt_of_naiveObstructionAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveVersalityTag.lean, line 124.

Stacks 07YN, with the versality criterion of Stacks 07YM discharged rather than assumed.

Deformation.Artin.exists_isOpen_isVersalAt_of_naiveObstructionAt takes that criterion as a hypothesis, and must: it lives in a module this one imports, while the criterion is proved here, so it cannot apply it without a cycle. This is the same statement with the hypothesis supplied by Deformation.Artin.naiveVersalityCriterion, so the tag sits on a declaration that grants nothing.

public theorem isOpenVersalityAt_of_naiveObstructionAt
    (data : NaiveObstructionAt hp hRS P hΩ E ξ)
    (hFinite : ∀ n : ℤ,
      Module.Finite P.ring ((DerivedCategory.homologyFunctor (ModuleCat.{u} P.ring) n).obj E))
    (u₀ : Spec (.of P.ring)) (hu₀ : IsClosed ({u₀} : Set (Spec (.of P.ring))))
    (hversal : IsVersalAt (Over.mk P.obj.alg.toScheme) (p ⋙ Over.post B.inclusion) u₀ P.point
      P.overScheme_eq) :
    ∃ V : Set (Spec (.of P.ring)), IsOpen V ∧ u₀ ∈ V ∧
      ∀ u ∈ V, IsFiniteTypePoint u →
        IsVersalAt (Over.mk P.obj.alg.toScheme) (p ⋙ Over.post B.inclusion) u P.point
          P.overScheme_eq

Tag 07YP, a definition

Tag 07YP in the Stacks Project.

Deformation.Artin.NaiveObstructionTheory, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveTheory.lean, line 474.

Stacks 07YP. A naive obstruction theory for a category fibred in groupoids 𝒳 over the big fppf site of S satisfying (RS*), relative to a fixed affine chart Spec Λ ⊆ S: a complex E_x ∈ D⁻(A) with a map ξ_x : E_x ⟶ NL_{A/Λ} for every object x of 𝒳 over Spec A, identifications of Inf_x and T_x with Ext^{-1}_A(E_x, −) and Ext^0_A(E_x, −), and a functoriality map E_x ⟶ E_y for every ring map A ⟶ B, subject to the five conditions of the source.

public structure NaiveObstructionTheory (hp : p.IsFiberedInGroupoids)
    (hRS : SatisfiesRSStar B S hS p hp) (c : AffineChart S)

Tag 07YT, a lemma

Tag 07YT in the Stacks Project.

Deformation.Artin.NaiveObstructionTheory.functoriality_homology_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveTheoryFunctoriality.lean, line 175.

Stacks 07YT. Let 𝒳 be fibred in groupoids over the big fppf site of S, satisfying (RS*) and endowed with a naive obstruction theory. Let A ⟶ B be a ring map in the site, let y = x|_{Spec B} be the restriction of an object x of 𝒳 over Spec A, and let k be a B-algebra which is a field whose two module structures occur in the site. Then the functoriality map E_x ⟶ E_y induces bijections H^i(E_x ⊗ᴸ_A k) ⟶ H^i(E_y ⊗ᴸ_B k) for i = 0 and i = 1.

Nothing about the comparison is assumed. The first step of the source proof is the (RS*) identification of the lifts of x over A[k] with the lifts of y over B[k], on isomorphism classes by Deformation.Artin.bijective_squareZeroLiftBaseChangeMap and on the automorphisms of the trivial lift by Deformation.Artin.bijective_of_isInfinitesimalAutomorphismBaseChange; through clauses (2) and (iii) of Stacks 07YP these give bijectivity on Ext^0 and on Ext^{-1}, and the duality of Stacks 07YK turns that into the conclusion in degrees 0 and 1.

theorem NaiveObstructionTheory.functoriality_homology_bijective
    {hp : p.IsFiberedInGroupoids} {hRS : SatisfiesRSStar B S hS p hp} {c : AffineChart S}
    (N : NaiveObstructionTheory B S hS p hp hRS c) (P Q : ChartedObject B S hS p c)
    (hom : AffineObject.Hom P.obj Q.obj) [Algebra P.ring Q.ring]
    [IsScalarTower c.ring P.ring Q.ring] (halg : algebraMap P.ring Q.ring = hom.alg.ringMap)
    {k : Type u} [Field k] (g : Q.ring →+* k)
    (hM : IsSiteModule P.ring B
      ((ModuleCat.restrictScalars (g.comp (algebraMap P.ring Q.ring))).obj
        (ModuleCat.of k (ULift.{u} k))))
    (hN : IsSiteModule Q.ring B
      ((ModuleCat.restrictScalars g).obj (ModuleCat.of k (ULift.{u} k)))) :
    Function.Bijective (((DerivedCategory.homologyFunctor (ModuleCat.{u} k) 0).map
        (naiveObstructionFieldBaseChangeMap N P Q hom halg g)).hom) ∧
      Function.Bijective (((DerivedCategory.homologyFunctor (ModuleCat.{u} k) 1).map
        (naiveObstructionFieldBaseChangeMap N P Q hom halg g)).hom)

Tag 07YU, a lemma

Tag 07YU in the Stacks Project.

Deformation.Artin.isOpenVersality_of_naiveObstructionTheory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/NaiveTheoryVersalityOpenness.lean, line 176.

Stacks 07YU. Let S be a locally Noetherian scheme and 𝒳 a category fibred in groupoids over the big fppf site of S. Assume that 𝒳 satisfies (RS*) and that 𝒳 has a naive obstruction theory, and assume the proviso of the source: the complexes E_x of Stacks 07YP have finitely generated cohomology groups for the pairs (A, x) with A of finite type over S. Then openness of versality holds for 𝒳: if U is a scheme locally of finite type over S, x an object of 𝒳 over U and u₀ a finite type point of U at which x is versal, then there is an open neighbourhood of u₀ at every finite type point of which x is versal.

The conclusion is the body of Deformation.Artin.IsOpenVersality, written out; see the implementation notes of this file for why the predicate itself cannot be used.

public theorem isOpenVersality_of_naiveObstructionTheory [IsLocallyNoetherian S]
    (N : ∀ c : AffineChart S, NaiveObstructionTheory B S hS p hp hRS c)
    (hFinite : ∀ (c : AffineChart S) (Q : ChartedObject B S hS p c),
      Algebra.FiniteType c.ring Q.ring → ∀ n : ℤ, Module.Finite Q.ring
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} Q.ring) n).obj ((N c).complex Q).obj))
    (U : Over S) (hUft : LocallyOfFiniteType U.hom) (x : X)
    (hx : (p ⋙ Over.post B.inclusion).obj x = U) (u₀ : U.left)
    (hu₀ : IsFiniteTypePoint u₀)
    (hversal : IsVersalAt U (p ⋙ Over.post B.inclusion) u₀ x hx) :
    ∃ V : U.left.Opens, u₀ ∈ V.1 ∧
      ∀ u ∈ V.1, IsFiniteTypePoint u →
        IsVersalAt U (p ⋙ Over.post B.inclusion) u x hx

Sources

• Section 98.23, Tag 07YJ
• AxiomMath/Stacks at 5ed82d14

LeanDerivedCategory.extIntoFieldEquivDualBaseChangeHomology · DerivedCategory.extIntoFieldEquivDualBaseChangeHomology_smul · DerivedCategory.extIntoFieldEquivDualBaseChangeHomology_naturality · DerivedCategory.extIntoFieldEquivDualBaseChangeHomology_restrictScalars · Deformation.Artin.exists_squareZeroExtension_killing_cotangent_morphism · AlgebraicGeometry.finiteType_residueField_of_isClosed_singleton · Deformation.Artin.surjective_derivedFibre_neg_one_iff_injective_extOne · Deformation.Artin.injective_derivedFibre_zero_iff_surjective_extZero

Section98.24 A dual notion#

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

Tag 07YW, an example

Tag 07YW in the Stacks Project.

Deformation.Artin.SectionsObstructionModel.exists_finiteProjectiveModel_obstructionSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/SectionsObstructionModel.lean, line 208. The attribute's comment: “the obstruction spaces of the example of Tag 07YH are 𝒪_x(M) = H¹(N ⊗_Λ M)”.

[Stacks, Tag 07YW], the obstruction spaces. Let Λ be Noetherian, let g : W ⟶ Spec Λ be proper and let 𝓕 be a coherent 𝒪_W-module flat over Λ. Then there is a finite complex N of finite projective Λ-modules such that, for every Λ-algebra A, every cartesian square exhibiting W_A as the base change of W, and every A-module M,

𝒪_x(M) = H¹(W_A, 𝓕_A ⊗_A M) ≅ H¹((N ⊗_Λ A) ⊗_A M),

the obstruction space of the obstruction theory of [Stacks, Tag 07YH] at M. In degree i the right-hand complex is M ⊗_Λ Nⁱ by Deformation.Artin.SectionsPerfectComplex.tensorComplexXLinearEquiv, so the right-hand side is the source's H¹(N ⊗_Λ M).

Composed with Deformation.Artin.SectionsPerfectComplex.nonempty_derivedCohomology_two_iso_homology_one this is the source's reformulation 𝒪_x(M) = H²(K ⊗^𝐋_A M) with K = (N ⊗_Λ A)[-1].

theorem exists_finiteProjectiveModel_obstructionSpace {Λ : Type u} [CommRing Λ]
    {W : Scheme.{u}} (g : W ⟶ Spec (CommRingCat.of Λ)) (F : W.Modules)
    [IsNoetherianRing Λ] [IsProper g] [F.IsCoherent]
    (hflat : IsFlatOver g.toLRSHom.toShHom F) :
    ∃ (N : CochainComplex (ModuleCat.{u} Λ) ℤ) (a b : ℤ),
      N.IsStrictlyGE a ∧ N.IsStrictlyLE b ∧
        (∀ i : ℤ, Module.Finite Λ (N.X i)) ∧ (∀ i : ℤ, Module.Projective Λ (N.X i)) ∧
        ∀ (A : Type u) [CommRing A] (φ : Λ →+* A) {W' : Scheme.{u}}
          {g' : W' ⟶ Spec (CommRingCat.of A)} {p : W' ⟶ W}
          (_hsq : IsPullback p g' g (Spec.map (CommRingCat.ofHom φ)))
          (M : ModuleCat.{u} A),
          Nonempty ((obstructionFunctor g' ((Scheme.Modules.pullback p).obj F)).obj M ≅
            ((tensorComplex M).obj (extendScalarsComplex φ N)).homology 1)

Deformation.Artin.SectionsObstructionModel.exists_finiteProjectiveModel_homology_iso_obstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/SectionsObstructionModel.lean, line 284. The attribute's comment: “there exists a finite complex N of finite projective Λ-modules which universally computes the cohomology of 𝓕”.

[Stacks, Tag 07YW], the complex N. Let Λ be Noetherian, let g : W ⟶ Spec Λ be proper and let 𝓕 be a coherent 𝒪_W-module flat over Λ. Then there is a finite complex N of finite projective Λ-modules which universally computes the cohomology of 𝓕 — for every base change φ : Λ → Λ', Hⁱ(W_{Λ'}, 𝓕_{Λ'}) ≅ Hⁱ(N ⊗_Λ Λ') — and, writing K = (N ⊗_Λ A)[-1] for a Λ-algebra A, the degree-one cohomology of N ⊗_Λ M is the degree-two cohomology of K ⊗^𝐋_A M for every A-module M.

This is Deformation.Artin.SectionsPerfectComplex.exists_finiteProjectiveModel_obstruction without its binder _haffineBase, the affine-base case of [Stacks, Tag 02O5], which that proof never uses: [Stacks, Tag 07VL] (Stacks.AlgebraicGeometry.ProperFlatGlobalSections.exists_finiteProjectiveModel_homology_iso) is unconditional.

theorem exists_finiteProjectiveModel_homology_iso_obstruction {Λ : Type u} [CommRing Λ]
    {W : Scheme.{u}} (g : W ⟶ Spec (CommRingCat.of Λ)) (F : W.Modules)
    [IsNoetherianRing Λ] [IsProper g] [F.IsCoherent]
    (hflat : IsFlatOver g.toLRSHom.toShHom F) :
    ∃ (N : CochainComplex (ModuleCat.{u} Λ) ℤ) (a b : ℤ),
      N.IsStrictlyGE a ∧ N.IsStrictlyLE b ∧
        (∀ i : ℤ, Module.Finite Λ (N.X i)) ∧ (∀ i : ℤ, Module.Projective Λ (N.X i)) ∧
        (∀ {Λ' : Type u} [CommRing Λ'] (φ : Λ →+* Λ') {W' : Scheme.{u}}
          {g' : W' ⟶ Spec (.of Λ')} {p : W' ⟶ W}
          (_hsq : IsPullback p g' g (Spec.map (CommRingCat.ofHom φ))) (i : ℤ),
          Nonempty ((DerivedCategory.homologyFunctor (ModuleCat.{u} Λ') i).obj
              (derivedGlobalSectionsOverBase g' ((Scheme.Modules.pullback p).obj F)) ≅
            (extendScalarsComplex φ N).homology i)) ∧
        ∀ (A : Type u) [CommRing A] (φ : Λ →+* A) (M : ModuleCat.{u} A),
          Nonempty ((Deformation.Artin.derivedCohomology A
                (DerivedCategory.Q.obj
                  (Deformation.Artin.SectionsPerfectComplex.shiftedBaseChange φ N)) 2).obj M ≅
            ((tensorComplex M).obj (extendScalarsComplex φ N)).homology 1)

Deformation.Artin.SectionsPerfectComplex.nonempty_derivedCohomology_two_iso_homology_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/SectionsPerfectComplex.lean, line 185. The attribute's comment: “the reformulation 𝒪(M) = H²(K ⊗^𝐋_A M) with K = (N ⊗_Λ A)[-1], from the description 𝒪(M) = H¹(N ⊗_Λ M)”.

[Stacks, Tag 07YW], the degree shift. With K = (N ⊗_Λ A)[-1] for a bounded above complex N of flat Λ-modules, the degree-one cohomology of N ⊗_Λ M — the obstruction module of [Stacks, Tag 07YH] in the form the source reaches through [Stacks, Tag 07VL] — is the degree-two cohomology of K ⊗^𝐋_A M:

H¹((N ⊗_Λ A) ⊗_A M) ≅ H²(K ⊗^𝐋_A M).

In degree i the left-hand complex is M ⊗_Λ Nⁱ by tensorComplexXLinearEquiv, so the left-hand side is the source's H¹(N ⊗_Λ M).

public theorem nonempty_derivedCohomology_two_iso_homology_one {Λ : Type u} [CommRing Λ]
    (φ : Λ →+* A) (N : CochainComplex (ModuleCat.{u} Λ) ℤ) (b : ℤ) [N.IsStrictlyLE b]
    (hN : ∀ i : ℤ, Module.Flat Λ (N.X i)) (M : ModuleCat.{u} A) :
    Nonempty ((Deformation.Artin.derivedCohomology A
          (DerivedCategory.Q.obj (shiftedBaseChange φ N)) 2).obj M ≅
      ((tensorComplex M).obj
        (Stacks.AlgebraicGeometry.ProperFlatGlobalSections.extendScalarsComplex φ N)).homology
          1)

Tag 07YX, a situation

Tag 07YX in the Stacks Project.

Deformation.Artin.DualDeformationSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/DualSituation.lean, line 167.

Stacks 07YX. A dual deformation situation: a complex K of A-modules whose first derived-tensor cohomology is the tangent functor of x, together with obstruction elements in its second derived-tensor cohomology which are functorial in the deformation situation and vanish exactly when x lifts.

public structure DualDeformationSituation (A Λ : Type u) [CommRing A] [CommRing Λ]
    [Algebra Λ A] (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [IsLocallyNoetherian S] (toS : Spec (.of A) ⟶ S) (hA : B.Contains (Spec (.of A)))
    (X : Type v) [Category.{w} X] (p : X ⥤ BigFppfOver B S hS)

Tag 07YY, a lemma

Tag 07YY in the Stacks Project.

Deformation.Artin.exists_obstructionEvaluation_eq_obstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/CotangentClass/ClauseOne.lean, line 550. The attribute's comment: “clause (1) alone, and WITHOUT the boundary condition (iv): a single class ξ on NL_{A/Λ} whose canonical evaluation obstructionEvaluation at every deformation situation is that situation's obstruction element. The whole tag — clause (1) together with clause (2), that ξ's image in H¹(K ⊗ᴸ Ω_{A/Λ}) is the canonical element of the tangent functor — is Deformation.Artin.exists_isCotangentObstructionClass, which assumes (iv) and whose conclusion is Deformation.Artin.IsCotangentObstructionClass, the full conjunction. This theorem is kept beside it because clause (1) needs no hypothesis: the class it produces is adjusted there by an element of H¹(K ⊗ᴸ Ω_{P/Λ} ⊗_P A) to achieve clause (2), an adjustment clause (1) cannot see because mor₁ ≫ mor₂ = 0.”.

There is a class ξ in H¹(K ⊗ᴸ NL_{A/Λ}) such that every square-zero thickening D : A' → A of the situation sit admits a ring map Λ → A' compatible with sit.affineOpen and with Λ → A, along which the evaluation obstructionEvaluation of ξ is the obstruction element sit.obstruction A' D.

public theorem exists_obstructionEvaluation_eq_obstruction :
    ∃ ξ : (derivedTensorCohomology A sit.K 1).obj (derivedNaiveCotangentComplex Λ A),
      ∀ (A' : Type u) [CommRing A'] (D : SquareZeroThickening A B S hS toS hA A'),
        ∃ f : Λ →+* A',
          Spec.map (CommRingCat.ofHom f) ≫ sit.affineOpen = B.inclusion.map D.toS' ∧
          ∃ hf : D.q.comp f = algebraMap Λ A,
          letI : Algebra Λ A' := f.toAlgebra
          letI : Algebra A' A := D.q.toAlgebra
          letI : IsScalarTower Λ A' A :=
            IsScalarTower.of_algebraMap_eq fun r =>
              (congrArg (fun g : Λ →+* A => g r) hf).symm
          obstructionEvaluation Λ A' A sit.K D.squareZeroSurjection.1
              D.squareZeroSurjection.2 ξ = sit.obstruction A' D

Deformation.Artin.exists_isCotangentObstructionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/CotangentClassCanonical/ObstructionClass.lean, line 692.

Stacks 07YY. A dual deformation situation satisfying the boundary condition (iv) has a cotangent obstruction class: a single class ξ on NL_{A/Λ} whose evaluation at every square-zero thickening is that thickening's obstruction element, and whose image in H¹(K ⊗ᴸ Ω_{A/Λ}) is the canonical element of the tangent functor.

The class of clause (1), built at a chosen presentation, need not satisfy clause (2); it is corrected by an element of H¹(K ⊗ᴸ Ω_{P/Λ} ⊗_P A) supplied by Deformation.Artin.exists_correction_of_boundaryCondition, and the correction is invisible to clause (1) because the inclusion of the degree-zero term of NL(α) followed by the projection onto the conormal module is zero.

public theorem exists_isCotangentObstructionClass
    (hiv : DualNotion.ObstructionBoundaryCondition Λ A B S hS toS hA X p sit) :
    ∃ ξ, IsCotangentObstructionClass Λ A B S hS toS hA X p sit ξ

Tag 07YZ, a lemma

Tag 07YZ in the Stacks Project.

Deformation.Artin.DualNotion.exists_isOpen_isVersalAt_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/Obstruction/DualNotionTag.lean, line 156.

Stacks 07YZ. In Situation 07YX assume that (iv) of Lemma 07YY holds and that K is a perfect object of D(A). In this case, if x is versal at a closed point u₀ ∈ U = Spec A then there exists an open neighbourhood u₀ ∈ U' ⊆ U such that x is versal at every finite type point of U'.

public theorem exists_isOpen_isVersalAt_of_isPerfect
    (hboundary : ObstructionBoundaryCondition Λ A B S hS toS hA X p sit)
    (hperfect : StacksDraft.Perfect.IsPerfect sit.K)
    (u₀ : Spec (.of A)) (hu₀ : IsClosed ({u₀} : Set (Spec (.of A))))
    (hversal : IsVersalAt (Over.mk toS) (p ⋙ Over.post B.inclusion) u₀ sit.x
      (versalityBase Λ A B S hS toS hA X p sit)) :
    ∃ V : Set (Spec (.of A)), IsOpen V ∧ u₀ ∈ V ∧
      ∀ u ∈ V, IsFiniteTypePoint u →
        IsVersalAt (Over.mk toS) (p ⋙ Over.post B.inclusion) u sit.x
          (versalityBase Λ A B S hS toS hA X p sit)

Sources

• Section 98.24, Tag 07YV
• AxiomMath/Stacks at 5ed82d14

LeanDeformation.Artin.SectionsObstructionModel.exists_finiteProjectiveModel_obstructionSpace · Deformation.Artin.SectionsObstructionModel.exists_finiteProjectiveModel_homology_iso_obstruction · Deformation.Artin.SectionsPerfectComplex.nonempty_derivedCohomology_two_iso_homology_one · Deformation.Artin.DualDeformationSituation · Deformation.Artin.exists_obstructionEvaluation_eq_obstruction · Deformation.Artin.exists_isCotangentObstructionClass · Deformation.Artin.DualNotion.exists_isOpen_isVersalAt_of_isPerfect

Section98.25 Limit preserving functors on Noetherian schemes#

Section 98.25 of the Stacks Project, Tag 0GE1. 5 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GE1, the section

Tag 0GE1 in the Stacks Project.

AlgebraicGeometry.isLocallyNoetherian_of_mem_precoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/LocallyNoetherianObjects.lean, line 84. The attribute's comment: “part (3): the members of a covering family of a locally Noetherian scheme”.

A member of a τ-covering family of a locally Noetherian scheme is locally Noetherian.

public theorem isLocallyNoetherian_of_mem_precoverage (τ : CoveringTopology) {X : Scheme.{u}}
    (hX : IsLocallyNoetherian X) {R : Presieve X}
    (hR : R ∈ Scheme.precoverage (coveringMorphismProperty.{u} τ) X)
    {Y : Scheme.{u}} {f : Y ⟶ X} (hf : R f) : IsLocallyNoetherian Y

AlgebraicGeometry.isLocallyNoetherian_of_isCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/LocallyNoetherianObjects.lean, line 93. The attribute's comment: “part (3): the sources of a covering of a locally Noetherian object”.

If a chosen covering family of a big site has locally Noetherian target, then each of its sources is locally Noetherian.

public theorem isLocallyNoetherian_of_isCovering (B : BigSite.{u} τ)
    {𝒰 : Covering (siteCategory B)} (h𝒰 : isCovering τ B 𝒰)
    (hX : IsLocallyNoetherian ((schemeBelowInclusion (cutoff τ B)).obj 𝒰.1)) (i : 𝒰.2.I₀) :
    IsLocallyNoetherian ((schemeBelowInclusion (cutoff τ B)).obj (𝒰.2.X i))

AlgebraicGeometry.isLocallyNoetherian_of_isCovering_bigFppfOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/LocallyNoetherianObjects.lean, line 103. The attribute's comment: “part (3) for the big fppf site over a base scheme”.

If a covering family of the big fppf category over S has locally Noetherian target, then each of its sources is locally Noetherian.

public theorem isLocallyNoetherian_of_isCovering_bigFppfOver (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {E : Covering (BigFppfOver B S hS)}
    (hE : BigFppfOver.IsCovering B S hS E)
    (hX : IsLocallyNoetherian ((BigFppfOver.toScheme B S hS).obj E.1)) (i : E.2.I₀) :
    IsLocallyNoetherian ((BigFppfOver.toScheme B S hS).obj (E.2.X i))

AlgebraicGeometry.isLocallyNoetherian_of_locallyOfFiniteType_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/LocallyNoetherianObjects.lean, line 115. The attribute's comment: “part (1): a morphism locally of finite type has locally Noetherian source”. References: EGA IV (1.3.3), “special case”.

If f : X ⟶ Y is a morphism of the big site over S whose underlying morphism of schemes is locally of finite type and whose target is locally Noetherian, then its source is locally Noetherian.

public theorem isLocallyNoetherian_of_locallyOfFiniteType_over (B : BigSite.{u} τ)
    (S : Scheme.{u}) (hS : S.size < cutoff τ B) {X Y : Over (base B S hS)} (f : X ⟶ Y)
    (hY : IsLocallyNoetherian ((schemeBelowInclusion (cutoff τ B)).obj Y.left))
    (hf : LocallyOfFiniteType ((schemeBelowInclusion (cutoff τ B)).map f.left)) :
    IsLocallyNoetherian ((schemeBelowInclusion (cutoff τ B)).obj X.left)

AlgebraicGeometry.isLocallyNoetherian_of_isPullback_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/LocallyNoetherianObjects.lean, line 141. The attribute's comment: “part (2): the fibre product along a morphism locally of finite type”.

Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of the big site over S with f locally of finite type on underlying schemes and Z locally Noetherian. Then the vertex of a fibre product square on f and g is locally Noetherian.

public theorem isLocallyNoetherian_of_isPullback_over (B : BigSite.{u} τ) (S : Scheme.{u})
    (hS : S.size < cutoff τ B) {W X Y Z : Over (base B S hS)}
    {p : W ⟶ X} {q : W ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ Y} (h : IsPullback p q f g)
    (hf : LocallyOfFiniteType ((schemeBelowInclusion (cutoff τ B)).map f.left))
    (hZ : IsLocallyNoetherian ((schemeBelowInclusion (cutoff τ B)).obj Z.left)) :
    IsLocallyNoetherian ((schemeBelowInclusion (cutoff τ B)).obj W.left)

Tag 0GE2, a remark

Tag 0GE2 in the Stacks Project.

AlgebraicGeometry.LocallyNoetherianOver.not_hasPullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Sites/NoetherianSiteNoFibreProducts.lean, line 475. The attribute's comment: “the first assertion, for tau = fppf and S the spectrum of a countable field”.

Stacks 0GE2, first assertion. The site (Noetherian/S)_τ does not have fibre products, here for τ = fppf and S = Spec k with k a countable field.

The diagram without a fibre product is Spec K ⟶ S ⟵ Spec K for K = k(u₀, u₁, u₂, …). A fibre product would be a locally Noetherian scheme receiving, compatibly, the square-zero extensions Spec (K ⊕ Kⁿ) with their two maps to Spec K; all of these meet it in one point, whose local ring would have to dominate maximal ideals of unbounded embedding dimension.

public theorem not_hasPullbacks (B : BigFppfSite.{u}) (baseField : Type u) [Field baseField]
    [Countable baseField] (hS : B.Contains (Spec (.of baseField))) :
    ¬ HasPullbacks (LocallyNoetherianOver B (Spec (.of baseField)) hS)

Declarations registered for the tag:

• AlgebraicGeometry.LocallyNoetherianOver.not_isMorphismOfSites_toBigFppfOver, declared in the repository, registered with add_to_stacks in StacksFrontier/Examples/Sites/NoetherianSiteNotMorphismOfSites.lean, line 486 (StacksFrontier): “the second assertion, for tau = fppf and S = Spec F_p: the example of Examples, Section 0GE8 that the remark defers to”.

Tag 0GE3, a lemma

Tag 0GE3 in the Stacks Project.

AlgebraicGeometry.ExtendingFunctors.isEquivalence_limitPreservingRestriction_noetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsRestrictionFullness.lean, line 182.

Stacks 0GE3. Let S be a locally Noetherian scheme and let τ be one of the five topologies — Zariski, étale, smooth, syntomic and fppf. Restriction along the inclusion of the full subcategory of locally Noetherian objects of Sch/S is an equivalence from the category of limit preserving sheaves on (Sch/S)_τ to the category of limit preserving sheaves on the site (Noetherian/S)_τ.

Faithfulness is the sharp uniqueness statement of Stacks 0EUW, essential surjectivity is the existence statement of Stacks 0EUW together with the sheaf property of the extension supplied by Stacks 0GDW, and fullness is the functoriality of that extension.

theorem isEquivalence_limitPreservingRestriction_noetherian (τ : CoveringTopology)
    {S : Scheme.{u}} [IsLocallyNoetherian S] :
    (limitPreservingRestriction (P := IsLocallyNoetherianOver (S := S)) τ
      (hasCoveringPullbacks_isLocallyNoetherianOver τ)).IsEquivalence

Tag 0GE4, a lemma

Tag 0GE4 in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_of_limitPreserving_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/Flattening/LimitPreservingNoetherian.lean, line 119. References: SGA 3 XI (3.2), “partial”.

A limit-preserving representable functor on the locally Noetherian site represents a scheme locally of finite presentation over the base.

theorem locallyOfFinitePresentation_of_limitPreserving_yoneda
    (B : BigFppfSite.{u}) (S : Scheme.{u})
    [IsLocallyNoetherian S] (hS : B.Contains S)
    (X : LocallyNoetherianOver B S hS)
    (hX : LimitPreserving.{u, u, u, u, u + 1, u}
      (LocallyNoetherianOver.toScheme B S hS) (yoneda.obj X)) :
    LocallyOfFinitePresentation (B.inclusion.map X.1.hom)

Tag 0GE5, a lemma

Tag 0GE5 in the Stacks Project.

AlgebraicGeometry.ExtendingFunctors.relativelyRepresentable_restriction_of_limitPreservingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsNoetherianRepresentable.lean, line 398. The attribute's comment: “implication (1) ⇒ (2)”.

Stacks 0GE5, implication (1) ⇒ (2). Let S be a locally Noetherian scheme, let τ be one of the five topologies — Zariski, étale, smooth, syntomic and fppf — and let F', G' be limit preserving sheaves on (Sch/S)_τ. If a transformation a' : F' ⟶ G' is representable, in the sense of Categories Definition 001X, then so is its restriction a to the full subcategory of locally Noetherian objects: for every locally Noetherian object V over S and every map V ⟶ G the fibre product F ×_G V is represented by a locally Noetherian object over S.

Only limit preservation of F' and G' enters the proof; the sheaf condition and the topology are carried because the source states them, and the sharper statement is AlgebraicGeometry.ExtendingFunctors.relativelyRepresentable_restriction.

theorem relativelyRepresentable_restriction_of_limitPreservingSheaf
    (τ : CoveringTopology) [IsLocallyNoetherian S]
    {F' G' : (Over S)ᵒᵖ ⥤ Type (max w (u + 1))} (a' : F' ⟶ G')
    (hF' : IsLimitPreservingSheaf τ F') (hG' : IsLimitPreservingSheaf τ G')
    (h1 : (uliftYoneda.{max w (u + 1)}).relativelyRepresentable a') :
    (uliftYoneda.{max w (u + 1)}).relativelyRepresentable
      (Functor.whiskerLeft (IsLocallyNoetherianOver (S := S)).ι.op a')

AlgebraicGeometry.ExtendingFunctors.isRepresentableOnAffineFiniteType_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsNoetherianRepresentable.lean, line 412. The attribute's comment: “implication (2) ⇒ (3)”.

Stacks 0GE5, implication (2) ⇒ (3). If the restriction of a' to the locally Noetherian objects over S is representable, then it is representable at every test object which is affine of finite type over S and maps into an affine open of S: criterion (3) is criterion (2) with its test object restricted.

theorem isRepresentableOnAffineFiniteType_of_relativelyRepresentable
    {P : ObjectProperty (Over S)}
    {F G : P.FullSubcategoryᵒᵖ ⥤ Type (max w (u + 1))} {a : F ⟶ G}
    (h : (uliftYoneda.{max w (u + 1)}).relativelyRepresentable a) :
    IsRepresentableOnAffineFiniteType.{w} a

AlgebraicGeometry.ExtendingFunctors.relativelyRepresentable_of_isRepresentableOnAffineFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsNoetherianRepresentableConverse.lean, line 951. The attribute's comment: “implication (3) ⇒ (1)”. References: SGA 3 XI (3.4), “special case”.

Stacks 0GE5, implication (3) ⇒ (1). Let S be a locally Noetherian scheme, let τ be one of the five topologies — Zariski, étale, smooth, syntomic and fppf — and let F', G' be limit preserving sheaves on (Sch/S)_τ. If the restriction a of a transformation a' : F' ⟶ G' to the locally Noetherian objects over S is representable at every test object which is affine of finite type over S and maps into an affine open of S, then a' itself is representable, in the sense of Categories Definition 001X.

For an arbitrary object T of Sch/S and a section of G' over it, the fibre product is represented over every member of the basis of opens of T which are affine and lie over an affine open of S; those representing objects glue by Stacks 01LH, the local sections of F' glue because F' is a Zariski sheaf, and the glued object has the universal property of the fibre product at every object of Sch/S, both the existence and the uniqueness being local on that object.

theorem relativelyRepresentable_of_isRepresentableOnAffineFiniteType
    (τ : CoveringTopology) [IsLocallyNoetherian S]
    {F' G' : (Over S)ᵒᵖ ⥤ Type (max w (u + 1))} (a' : F' ⟶ G')
    (hF' : IsLimitPreservingSheaf τ F') (hG' : IsLimitPreservingSheaf τ G')
    (h3 : IsRepresentableOnAffineFiniteType.{w}
      (Functor.whiskerLeft (IsLocallyNoetherianOver (S := S)).ι.op a')) :
    (uliftYoneda.{max w (u + 1)}).relativelyRepresentable a'

AlgebraicGeometry.ExtendingFunctors.relativelyRepresentable_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ExtendingFunctorsNoetherianRepresentableConverse.lean, line 975.

Stacks 0GE5. Let S be a locally Noetherian scheme, let τ be one of the five topologies — Zariski, étale, smooth, syntomic and fppf — and let F', G' be limit preserving sheaves on (Sch/S)_τ. For a transformation a' : F' ⟶ G' with restriction a to the full subcategory of locally Noetherian objects over S, the following are equivalent:

1. a' is representable;
2. a is representable;
3. a is representable at every test object which is affine of finite type over S and maps into an affine open of S.

theorem relativelyRepresentable_tfae (τ : CoveringTopology) [IsLocallyNoetherian S]
    {F' G' : (Over S)ᵒᵖ ⥤ Type (max w (u + 1))} (a' : F' ⟶ G')
    (hF' : IsLimitPreservingSheaf τ F') (hG' : IsLimitPreservingSheaf τ G') :
    List.TFAE
      [(uliftYoneda.{max w (u + 1)}).relativelyRepresentable a',
       (uliftYoneda.{max w (u + 1)}).relativelyRepresentable
         (Functor.whiskerLeft (IsLocallyNoetherianOver (S := S)).ι.op a'),
       IsRepresentableOnAffineFiniteType.{w}
         (Functor.whiskerLeft (IsLocallyNoetherianOver (S := S)).ι.op a')]

Sources

• Section 98.25, Tag 0GE1
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isLocallyNoetherian_of_mem_precoverage · AlgebraicGeometry.isLocallyNoetherian_of_isCovering · AlgebraicGeometry.isLocallyNoetherian_of_isCovering_bigFppfOver · AlgebraicGeometry.isLocallyNoetherian_of_locallyOfFiniteType_over · AlgebraicGeometry.isLocallyNoetherian_of_isPullback_over · AlgebraicGeometry.LocallyNoetherianOver.not_hasPullbacks · AlgebraicGeometry.LocallyNoetherianOver.not_isMorphismOfSites_toBigFppfOver · AlgebraicGeometry.ExtendingFunctors.isEquivalence_limitPreservingRestriction_noetherian

Section98.26 Algebraic spaces in the Noetherian setting#

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

Tag 0GE7, a proposition

Tag 0GE7 in the Stacks Project.

AlgebraicGeometry.LocallyNoetherianOver.existsUnique_isAlgebraicSpace_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/Artin/LocallyNoetherianAlgebraicSpaceCriterion.lean, line 1039.

Stacks 0GE7. Let S be a locally Noetherian scheme and let F be a set-valued functor on the locally Noetherian étale site (Noetherian/S)_étale. If the diagonal Δ : F ⟶ F × F is representable (Categories 001X), F satisfies Artin's axioms [-1], [0], [1], [2], [3], [4], [5] in the form of Section 0GE6, and the local rings of S at its finite type points are G-rings, then there is a limit preserving algebraic space F' on the big fppf site (Sch/S)_fppf whose restriction to (Noetherian/S)_étale is F, and it is unique: two such are identified by a unique isomorphism compatible with the identifications of their restrictions with F.

The extension is the one of Stacks 0GE3, its diagonal is representable by Stacks 0GE5, the axioms [-1], [2], [3], [4], [5] pass to it because they only involve locally Noetherian test objects, and Stacks 07Y1 shows it is an algebraic space.

theorem existsUnique_isAlgebraicSpace_restriction_iso [IsLocallyNoetherian S]
    (F : (LocallyNoetherianOver B S hS)ᵒᵖ ⥤ Type u)
    (hdiag : (yoneda (C := LocallyNoetherianOver B S hS)).relativelyRepresentable (diag F))
    (hax : SatisfiesArtinAxioms B S hS F)
    (hG : ∀ s : S, IsFiniteTypePoint s → IsGRing (S.presheaf.stalk s)) :
    (∃ F' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u, IsAlgebraicSpace B S hS F' ∧
        LimitPreserving.{u, u, u, u, u + 1, u} (BigFppfOver.toScheme B S hS) F' ∧
        Nonempty ((LocallyNoetherianOver.toBigFppfOver B S hS).op ⋙ F' ≅ F)) ∧
      ∀ (F₁ F₂ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u),
        IsAlgebraicSpace B S hS F₁ → IsAlgebraicSpace B S hS F₂ →
        LimitPreserving.{u, u, u, u, u + 1, u} (BigFppfOver.toScheme B S hS) F₁ →
        LimitPreserving.{u, u, u, u, u + 1, u} (BigFppfOver.toScheme B S hS) F₂ →
        ∀ (e₁ : (LocallyNoetherianOver.toBigFppfOver B S hS).op ⋙ F₁ ≅ F)
          (e₂ : (LocallyNoetherianOver.toBigFppfOver B S hS).op ⋙ F₂ ≅ F),
        ∃! e : F₁ ≅ F₂,
          Functor.isoWhiskerLeft (LocallyNoetherianOver.toBigFppfOver B S hS).op e ≪≫ e₂ = e₁

Sources

• Section 98.26, Tag 0GE6
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.LocallyNoetherianOver.existsUnique_isAlgebraicSpace_restriction_iso

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.