91.10 Modules on first order… to 91.16 Deformations of complexes…

Section91.10 Modules on first order thickenings of ringed topoi #

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

Tag 08MB, an equation

Tag 08MB in the Stacks Project.

Deformation.ToposThickening.extensionActionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Basic.lean, line 1391. The attribute's comment: “canonical action map”.

The canonical map I ⊗[O] F → K, characterized by multiplication by an ideal section after lifting a section of F to the middle module.

public noncomputable def extensionActionMap
    [X.J.HasSheafCompose (forget RingCat.{w})]
    [Y.J.HasSheafCompose (forget RingCat.{w'})]
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [Y.J.HasSheafCompose (forget₂ CommRingCat.{w'} RingCat.{w'})]
    {i : RingedToposHom X Y}
    [Y.J.WEqualsLocallyBijective AddCommGrpCat.{w'}]
    [HasSheafify Y.J AddCommGrpCat.{w'}]
    [HasWeakSheafify Y.J AddCommGrpCat.{w'}]
    (hi : FirstOrderThickening i)
    {F K : SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O))}
    (E : Abelian.YonedaExtension
      ((SheafOfModules.restrictScalars
        (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
            Stacks.SheafOfModules.Tensor.ringSheaf
              ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
          (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj F)
      ((SheafOfModules.restrictScalars
        (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
            Stacks.SheafOfModules.Tensor.ringSheaf
              ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
          (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj K) 0) :
    { c : ((Stacks.SheafOfModules.Tensor.sheafTensor
        ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F ⟶ K //
      ∀ (U : Y.Cᵒᵖ) (a : hi.I.val.obj U) (x : E.Z.left.val.obj U),
        E.f.val.app U
            (c.val.app U
              (((PresheafOfModules.sheafificationAdjunction
                (R := Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor
                  i.toToposHom).obj X.O))
                (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor
                  i.toToposHom).obj X.O)).obj)).unit.app
                (PresheafOfModules.tensorObj hi.I.val F.val)).app U
                (a ⊗ₜ[((pushforwardCommRingFunctor i.toToposHom).obj X.O).obj.obj U]
                  E.g.val.app U x))) =
          (show (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj.obj U from
            hi.incl.val.app U a) • x }

Declarations registered for the tag:

CategoryTheory.Abelian.YonedaExtension, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/ToposThickening/Basic.lean, line 1386 (StacksFrontier).

Tag 08MC, a lemma

Tag 08MC in the Stacks Project.

Deformation.ToposThickening.compatibleMap_add_quotientKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CompatibleLifts.lean, line 89. The attribute's comment: “compatible_lifts_torsor”.

Adding a map which factors through the first quotient and the second kernel preserves compatibility.

theorem compatibleMap_add_quotientKernel
    (D : TwoExtensions i) (c : CompatibleMap D) (α : D.F ⟶ D.L) :
    ∃ d : CompatibleMap D,
      d.hom = c.hom +
        (D.firstExtension.g ≫
          (SheafOfModules.restrictScalars
            ((sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).map α ≫
          D.secondExtension.f)

Deformation.ToposThickening.compatibleMap_unique_quotientKernel_difference, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CompatibleLifts.lean, line 111. The attribute's comment: “compatible_lifts_torsor”.

Any two compatible maps differ by a unique map from the first quotient to the second kernel. Together with closure under those translations, this is the torsor assertion.

theorem compatibleMap_unique_quotientKernel_difference
    (D : TwoExtensions i) (c d : CompatibleMap D) :
    ∃! α : D.F ⟶ D.L,
      d.hom = c.hom +
        (D.firstExtension.g ≫
      (SheafOfModules.restrictScalars
        ((sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).map α ≫
          D.secondExtension.f)

Declarations registered for the tag:

idealActionMap_naturality registered with add_to_stacks in StacksFrontier/Deformation/ToposThickening/CompatibleLifts.lean, line 162 (StacksFrontier): “ideal_action_compatible”.

Tag 08MD, a lemma

Tag 08MD in the Stacks Project.

Deformation.ToposThickening.obstructionClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionObstruction.lean, line 270. The attribute's comment: “obstruction class”.

The obstruction class in the first Ext group over the quotient structure sheaf. Its vanishing characterizes lifts of the prescribed end maps.

noncomputable def obstructionClass
    [HasExt.{e} (SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    (D : TwoExtensions i) (h : CompatibleActions D) :
    Abelian.Ext D.F D.L 1

Deformation.ToposThickening.obstructionClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionObstruction.lean, line 280. The attribute's comment: “vanishing criterion”.

The obstruction vanishes exactly when the end maps extend to a map of the two extensions.

theorem obstructionClass_eq_zero_iff
    [HasExt.{e} (SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    (D : TwoExtensions i) (h : CompatibleActions D) :
    obstructionClass D h = 0 ↔
      ∃ φ' : D.firstExtension.Z.left ⟶ D.secondExtension.Z.left,
        IsExtensionLift D φ'

Tag 08ME, a lemma

Tag 08ME in the Stacks Project.

Deformation.ToposThickening.fixedActionExtensionClass_torsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModulesOnThickening/FixedAction/Torsor.lean, line 685.

Stacks 08ME. If some extension over a first order thickening of ringed topoi induces the prescribed action c of the square-zero ideal, then the isomorphism classes of extensions inducing c form a principal homogeneous space under the first Ext group over the quotient structure sheaf.

theorem fixedActionExtensionClass_torsor
    [HasExt.{e} (SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))]
    (hi : FirstOrderThickening i)
    (F K : SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    (c : ((Stacks.SheafOfModules.Tensor.sheafTensor
      ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F ⟶ K)
    (h : Nonempty (FixedActionExtensionClass.{_, _, _, _, _, _, e} hi F K c)) :
    Nonempty (AddTorsor (Abelian.Ext F K 1)
      (FixedActionExtensionClass.{_, _, _, _, _, _, e} hi F K c))

Deformation.ToposThickening.exists_addTorsor_fixedActionExtensionIsoClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModulesOnThickening/FixedActionIsoClasses.lean, line 170.

Stacks 08ME. Let i be a first order thickening of ringed topoi, F, K modules over the quotient structure sheaf and c : I ⊗ F ⟶ K linear. If there is an extension 0 → K → F' → F → 0 of O'-modules with c_{F'} = c, then the set of isomorphism classes of these extensions is a principal homogeneous space under Ext¹_O(F, K): there is a torsor structure in which a sends the class of F'₁ to the class of F'₂ exactly when the Ext¹_{O'} class of F'₂ is the Baer sum of that of F'₁ with the image of a.

theorem exists_addTorsor_fixedActionExtensionIsoClass
    [HasExt.{e} (SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))]
    (hi : FirstOrderThickening i)
    (F K : SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    (c : ((Stacks.SheafOfModules.Tensor.sheafTensor
      ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F ⟶ K)
    (h : Nonempty (FixedActionExtension hi F K c)) :
    ∃ T : AddTorsor (Abelian.Ext.{e} F K 1) (FixedActionExtensionIsoClass hi F K c),
      ∀ (a : Abelian.Ext.{e} F K 1) (E E' : FixedActionExtension hi F K c),
        (T.vadd a ⟦E⟧ = ⟦E'⟧) ↔
          extensionClass F K E'.1 =
            (SheafOfModules.restrictScalars (structureRingMap i)).mapExtAddHom F K 1 a +
              extensionClass F K E.1

Tag 08MF, a lemma

Tag 08MF in the Stacks Project.

Deformation.ToposThickening.existenceObstructionClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModulesOnThickening/FixedAction/ExistenceObstruction.lean, line 618. The attribute's comment: “obstruction class”.

Stacks 08MF. The obstruction to the existence of an extension over a first order thickening of ringed topoi inducing a prescribed action c of the square-zero ideal: a class in the second Ext group over the quotient structure sheaf.

noncomputable def existenceObstructionClass
    [HasExt.{e} (SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))]
    (hi : FirstOrderThickening i)
    (F K : SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    (c : ((Stacks.SheafOfModules.Tensor.sheafTensor
      ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F ⟶ K) :
    Abelian.Ext F K 2

Deformation.ToposThickening.existenceObstructionClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModulesOnThickening/FixedAction/ExistenceObstruction.lean, line 636. The attribute's comment: “vanishing criterion”.

Stacks 08MF. The obstruction class vanishes exactly when there is an extension of F by K over the first order thickening whose canonical action of the square-zero ideal is c.

theorem existenceObstructionClass_eq_zero_iff
    [HasExt.{e} (SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))]
    (hi : FirstOrderThickening i)
    (F K : SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    (c : ((Stacks.SheafOfModules.Tensor.sheafTensor
      ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F ⟶ K) :
    existenceObstructionClass hi F K c = 0 ↔
      ∃ E : Abelian.YonedaExtension
        ((SheafOfModules.restrictScalars
          (structureRingMap i)).obj F)
        ((SheafOfModules.restrictScalars
          (structureRingMap i)).obj K) 0,
        (extensionActionMap hi E).1 = c

Tag 08MG, a remark

Tag 08MG in the Stacks Project.

Deformation.ToposThickening.Trivialization, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/Basic.lean, line 68. The attribute's comment: “trivial_first_order_thickening_and_trivialization”.

A retraction of a morphism of ringed topoi: a morphism in the reverse direction whose composite direct-image functor is identified with the identity, compatibly with the structure-sheaf map.

structure Trivialization (i : RingedToposHom X Y)

Deformation.ToposThickening.IsTrivial, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/Basic.lean, line 87. The attribute's comment: “trivial_first_order_thickening_and_trivialization”.

A morphism of ringed topoi is trivial if it admits a trivialization.

abbrev IsTrivial (i : RingedToposHom X Y) : Prop

Deformation.ToposThickening.TrivializedThickening.moduleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/ModuleEquivalence.lean, line 532. The attribute's comment: “trivialized first order thickenings are the O-modules; morphisms of thickenings run in the algebraic direction (A_T ⟶ A_S of sheaves of rings, the opposite of the source's ringed-topos morphisms of Stacks 08MK), so the module side carries no ᵒᵖ; stated at a single universe (site C : Type u with Category.{u} C, sheaves valued in Type u), which is the source's own setting since the Stacks Project fixes one universe throughout”.

Stacks 08MG. The category of trivialized first order thickenings of a ringed topos (Sh(C), O) is equivalent to the category of O-modules: a module goes to the square-zero extension O ⊕ M, and a trivialized thickening goes to its ideal.

There is no ᵒᵖ on the module side because the Hom of Deformation.ToposThickening.TrivializedThickening O runs in the algebraic direction, a morphism T ⟶ S being a morphism A_T ⟶ A_S of sheaves of rings, so that this category is the opposite of the source's category of trivialized thickenings (whose morphisms are morphisms of ringed topoi, Stacks 08MK) and M ↦ O ⊕ M is covariant. The ringed space form of this remark, AlgebraicGeometry.RingedSpaceThickening.trivializedThickeningEquivalence (Stacks 08L9), keeps the geometric Hom and so does carry an ᵒᵖ; the two statements agree. See the "## Variance" section of this module.

noncomputable def moduleEquivalence :
    SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O) ≌ TrivializedThickening O

Deformation.ToposThickening.trivializationOfSplitting, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/OfSplitting.lean, line 59. The attribute's comment: “splitting_determines_trivialization”.

A splitting of the structure sheaf of a first order thickening determines a trivialization whose structure map is the given section.

noncomputable def trivializationOfSplitting (i : RingedToposHom X Y)
    (_hi : FirstOrderThickening i)
    (split : X.O ⟶ (inverseImageCommRingFunctor i.toToposHom).obj Y.O)
    (split_comp : split ≫ i.fSharpInverseImage = 𝟙 X.O) :
    { π : Trivialization i //
      ∃ α : pushforwardCommRingFunctor π.retraction.toToposHom ≅
          inverseImageCommRingFunctor i.toToposHom,
        π.retraction.fSharp ≫ α.hom.app Y.O = split }

Deformation.ToposThickening.splittingFromTrivialization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/SplittingOf.lean, line 55. The attribute's comment: “splitting_from_trivialization”.

A trivialization splits the structure map of a first order thickening. The natural equivalence identifies the ring sheaf with the square-zero extension of its quotient by its kernel.

noncomputable def splittingFromTrivialization (i : RingedToposHom X Y)
    (hi : FirstOrderThickening i) (π : Trivialization i) :
    Σ' split : ((pushforwardCommRingFunctor i.toToposHom).obj X.O).obj ⟶ Y.O.obj,
      Σ' hs : SplitMono split,
        { _e : PresheafTrivialSquareZeroEquiv Y.O.obj
            ((pushforwardCommRingFunctor i.toToposHom).obj X.O).obj
            i.fSharp.hom split // hs.retraction = i.fSharp.hom }

Deformation.ToposThickening.TrivializedThickening, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/TrivializedCategory.lean, line 98. The attribute's comment: “the category of trivialized first order thickenings: objects”.

A trivialized first order thickening of the ringed topos (Sh(C), O), presented on the site C: a sheaf of commutative rings A with a surjection onto O whose kernel has square zero, together with a chosen splitting of that surjection.

structure TrivializedThickening (O : Sheaf J CommRingCat.{u})

Deformation.ToposThickening.TrivializedThickening.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/TrivializedCategory.lean, line 131. The attribute's comment: “the category of trivialized first order thickenings: morphisms, in the algebraic direction A_T ⟶ A_S (the opposite of the source's ringed-topos morphisms of Stacks 08MK)”.

A morphism of trivialized first order thickenings: a morphism of the structure sheaves compatible with both the surjections and the trivializations.

This runs in the algebraic direction, that of h^♯. The source's morphism of trivialized thickenings is a morphism of ringed topoi h : (Sh(D₁), O'₁) ⟶ (Sh(D₂), O'₂) over (Sh(C), O) (Stacks 08MK), so a Hom T S here is such an h with T the target of h and S its source, and this category is the opposite of the source's. See the "## Variance" section of this module.

structure Hom (T S : TrivializedThickening O)

Deformation.ToposThickening.trivializedThickeningOfTrivialization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/TrivializedComparison.lean, line 153. The attribute's comment: “a trivialized thickening is an object of the category; the target ringed topos is at a single universe, forced by Deformation.ToposThickening.TrivializedThickening, whose category is declared over a site C : Type u with Category.{u} C and sheaves valued in Type u — the source's own setting, since the Stacks Project fixes one universe throughout”.

A trivialization of a first order thickening of ringed topoi exhibits the thickening as an object of the category of trivialized first order thickenings of (Sh(D), i_*O), which is the ringed topos (Sh(C), O) read through the equivalence of underlying topoi.

noncomputable def trivializedThickeningOfTrivialization (i : RingedToposHom X Y)
    (hi : FirstOrderThickening i) (π : Trivialization i) :
    TrivializedThickening ((pushforwardCommRingFunctor i.toToposHom).obj X.O)

Deformation.ToposThickening.TrivializedThickening.exists_thickening_trivialization_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/Trivialization/TrivializedComparison.lean, line 638. The attribute's comment: “clause (4) for the source's objects: every object of the category of trivialized first order thickenings of (Sh(C), O) is the trivialized thickening of a first order thickening of ringed topoi (Sh(C), O) ⟶ (Sh(C), A) with a trivialization of it, up to the isomorphism of objects supplied here and the equivalence of categories Deformation.ToposThickening.TrivializedThickening.baseIsoEquivalence that reads the base through the comparison of the direct image along the identity morphism of topoi with the identity functor; together with Deformation.ToposThickening.trivializedThickeningOfTrivialization in the other direction this identifies the objects of the two presentations, which is what makes Deformation.ToposThickening.TrivializedThickening.moduleEquivalence the source's sentence about the source's objects; the thickening is presented on the site of the base, which loses nothing because the direct image of a first order thickening is an equivalence of topoi, and at a single universe, the Stacks Project's own convention”.

Stacks 08MG, clause (4), for the source's objects. Every object of the category of trivialized first order thickenings of (Sh(C), O) is, up to isomorphism, the trivialized thickening of a first order thickening of ringed topoi (Sh(C), O) ⟶ (Sh(C), A) together with a trivialization of it. With Deformation.ToposThickening.trivializedThickeningOfTrivialization in the other direction this identifies the objects of the two presentations, so that Deformation.ToposThickening.TrivializedThickening.moduleEquivalence reads as the source's sentence about the source's objects: the category of trivialized first order thickenings of (Sh(C), O) is equivalent to the category of O-modules.

theorem exists_thickening_trivialization_iso :
    ∃ (hi : FirstOrderThickening T.toRingedToposHom) (π : Trivialization T.toRingedToposHom),
      Nonempty (trivializedThickeningOfTrivialization T.toRingedToposHom hi π ≅
        (baseIsoFunctor (pushforwardIdIso O).symm).obj T)

Tag 08MI, a remark

Tag 08MI in the Stacks Project.

Deformation.ToposThickening.trivialExtension_bijective_underlyingExtensionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/TrivialExtension.lean, line 887.

Stacks 08MI. Let i : (Sh(C), O) ⟶ (Sh(D), O') be a first order thickening of ringed topoi with square-zero ideal I, and π a trivialization of it. Let F, K be O-modules and c : I ⊗_O F ⟶ K a map.

The trivial extension F'_{c,triv} = F ⊕ K (trivialExtensionModule, trivialExtension) carries the O'-module structure r · (m, k) = (q r · m, q r · k + c(d r ⊗ m)) built from the splitting O' = O ⊕ I of π and from c, and it is an extension 0 ⟶ K ⟶ F'_{c,triv} ⟶ F ⟶ 0 as in Stacks 08MB with c_{F'_{c,triv}} = c.

The class ξ_{F'} ∈ Ext¹_O(F, K) of an extension F', obtained by reading F' as an O-module through π^♯ (underlyingExtensionClass), only depends on the class of F' (through splitRestrictionExtHom), and F' ↦ ξ_{F'} is a bijection from the isomorphism classes of extensions with c_{F'} = c onto Ext¹_O(F, K). The isomorphism classes are represented by their classes in Ext¹_{O'}(F, K) (FixedActionExtensionClass); the bijection is also stated on extensions: every class is ξ_{F'} of an extension with c_{F'} = c, and two such extensions with the same ξ are isomorphic as extensions.

The trivial extension maps to the zero class.

theorem trivialExtension_bijective_underlyingExtensionClass
    (c : ((Stacks.SheafOfModules.Tensor.sheafTensor
      ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F ⟶ K) :
    (∀ (U : Y.Cᵒᵖ) (r : (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj.obj U)
        (z : (trivialExtensionModule hi π F K c).val.obj U),
        r • z = (structureApp i U r • z.1, structureApp i U r • z.2 +
          extensionPairing hi F K c U (trivializationDerivation hi π U r) z.1)) ∧
      (extensionActionMap hi (trivialExtension hi π F K c)).1 = c ∧
      (∀ E : Abelian.YonedaExtension
          ((SheafOfModules.restrictScalars
            (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
      Stacks.SheafOfModules.Tensor.ringSheaf
        ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
    (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj F)
          ((SheafOfModules.restrictScalars
            (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
      Stacks.SheafOfModules.Tensor.ringSheaf
        ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
    (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj K) 0,
        underlyingExtensionClass i hi π F K E =
          splitRestrictionExtHom hi π F K (extensionClass F K E)) ∧
      Function.Bijective (fun ξ : FixedActionExtensionClass.{_, _, _, _, _, _, e} hi F K c =>
        splitRestrictionExtHom hi π F K ξ.1) ∧
      (∀ η : Abelian.Ext F K 1, ∃ E : Abelian.YonedaExtension
          ((SheafOfModules.restrictScalars
            (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
      Stacks.SheafOfModules.Tensor.ringSheaf
        ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
    (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj F)
          ((SheafOfModules.restrictScalars
            (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
      Stacks.SheafOfModules.Tensor.ringSheaf
        ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
    (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj K) 0,
        (extensionActionMap hi E).1 = c ∧ underlyingExtensionClass i hi π F K E = η) ∧
      (∀ E E' : Abelian.YonedaExtension
          ((SheafOfModules.restrictScalars
            (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
      Stacks.SheafOfModules.Tensor.ringSheaf
        ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
    (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj F)
          ((SheafOfModules.restrictScalars
            (show Stacks.SheafOfModules.Tensor.ringSheaf Y.O ⟶
      Stacks.SheafOfModules.Tensor.ringSheaf
        ((pushforwardCommRingFunctor i.toToposHom).obj X.O) from
    (sheafCompose Y.J (forget₂ CommRingCat RingCat)).map i.fSharp)).obj K) 0,
        (extensionActionMap hi E).1 = c → (extensionActionMap hi E').1 = c →
        underlyingExtensionClass i hi π F K E = underlyingExtensionClass i hi π F K E' →
        ∃ φ : E.Z.left ≅ E'.Z.left, E.f ≫ φ.hom = E'.f ∧ φ.hom ≫ E'.g = E.g) ∧
      underlyingExtensionClass i hi π F K (trivialExtension hi π F K c) = 0

Tag 08MJ, a remark

Tag 08MJ in the Stacks Project.

Deformation.ToposThickening.MorphismOfFirstOrderThickenings.PushoutExtensionData.extensionOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPushout/TwistedDescent.lean, line 425. The attribute's comment: “the canonical map on extensions, by pushout along the map of kernel modules”.

Stacks Project, Tag 08MJ. The extension over the first thickening produced from an extension over the second: the pushout F'₂ ⊔_{K₂} K₁ carries an O'₁-module structure, built by descending the action of T = O'₂ ⋉ I₁ twisted by c₁ along the locally surjective q : T ⟶ O'₁, and sits in a short exact sequence 0 → K₁ → F'₂ ⊔_{K₂} K₁ → F → 0 of O'₁-modules. Its middle term restricted along q is identified with the pushout by middleIso, compatibly with the two maps by restrictScalars_extInclOne and restrictScalars_extQuotOne.

noncomputable def extensionOne :
    Abelian.YonedaExtension
      ((SheafOfModules.restrictScalars (structureRingMap i)).obj dat.F)
      ((SheafOfModules.restrictScalars (structureRingMap i)).obj dat.K₁) 0

Deformation.ToposThickening.MorphismOfFirstOrderThickenings.PushoutExtensionData.extensionOne_actionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPushout/TwistedDescent.lean, line 506. The attribute's comment: “the action map of the pushed-out extension is c₁”.

Stacks Project, Tag 08MJ. The canonical action map of the extension produced over the first thickening is the prescribed c₁.

theorem extensionOne_actionMap :
    (extensionActionMap D.first (dat.extensionOne E₂ hE₂)).1 = dat.c₁

Tag 08MK, a remark

Tag 08MK in the Stacks Project.

Deformation.ToposThickening.underlyingExtensionClass_eq_comp_mk₀, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/TrivializedThickeningComparison.lean, line 266. The attribute's comment: “the commutative square: the extension class of the image extension is the image of the extension class under functoriality of Ext in the map of kernel modules”.

If h is a morphism of trivialized first order thickenings of (Sh(C), O) and an extension F'₂ of F by K₂ over the second thickening maps to an extension F'₁ of F by K₁ over the first, inducing κ : K₂ ⟶ K₁ on the kernels and the identity on F, then the class ξ_{F'₁} is the image of ξ_{F'₂} under the map Ext¹_O(F, K₂) ⟶ Ext¹_O(F, K₁) given by functoriality of Ext in κ.

theorem underlyingExtensionClass_eq_comp_mk₀
    [HasExt.{e} (SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor ι).obj X.O)))]
    (h : O₂ ⟶ O₁) (hh : h ≫ s₁ = s₂)
    (hπ : splittingRingHom (homOn ι s₁) hi₁ π₁ =
      splittingRingHom (homOn ι s₂) hi₂ π₂ ≫ morphismRingHom h)
    (F K₁ K₂ : SheafOfModules.{w'}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor ι).obj X.O)))
    (κ : K₂ ⟶ K₁)
    (E₂ : Abelian.YonedaExtension
      ((SheafOfModules.restrictScalars (structureRingHom s₂)).obj F)
      ((SheafOfModules.restrictScalars (structureRingHom s₂)).obj K₂) 0)
    (E₁ : Abelian.YonedaExtension
      ((SheafOfModules.restrictScalars (structureRingHom s₁)).obj F)
      ((SheafOfModules.restrictScalars (structureRingHom s₁)).obj K₁) 0)
    (φ : E₂.Z.left ⟶
      (SheafOfModules.restrictScalars (morphismRingHom h)).obj E₁.Z.left)
    (hφf : E₂.f ≫ φ = (SheafOfModules.restrictScalars (structureRingHom s₂)).map κ ≫
      (presentationCompIso s₁ s₂ h hh K₁).hom ≫
        (SheafOfModules.restrictScalars (morphismRingHom h)).map E₁.f)
    (hφg : φ ≫ (SheafOfModules.restrictScalars (morphismRingHom h)).map E₁.g =
      E₂.g ≫ (presentationCompIso s₁ s₂ h hh F).hom) :
    underlyingExtensionClass (homOn ι s₁) hi₁ π₁ F K₁ E₁ =
      (underlyingExtensionClass (homOn ι s₂) hi₂ π₂ F K₂ E₂).comp
        (Abelian.Ext.mk₀ κ) (add_zero 1)

Tag 0CYC, a remark

Tag 0CYC in the Stacks Project.

Deformation.ToposThickening.MorphismOfFirstOrderThickenings.existenceObstructionClass_first, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ObstructionCompatibility.lean, line 405.

The obstruction classes of the two thickenings are compatible: the map Ext²_O(F, K₂) ⟶ Ext²_O(F, K₁) induced by κ carries o(F, K₂, c₂) to o(F, K₁, c₁).

theorem existenceObstructionClass_first
    [HasExt.{e} (SheafOfModules.{w₂} (Stacks.SheafOfModules.Tensor.ringSheaf D.O₂))]
    (F K₁ K₂ : SheafOfModules.{w₂} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRing i)))
    (c₁ : ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj D.first.I).obj F ⟶ K₁)
    (c₂ : ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj D.second.I).obj F ⟶ K₂)
    (κ : K₂ ⟶ K₁)
    (hκ : c₂ ≫ κ =
      ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).map D.idealMap).app F ≫ c₁) :
    existenceObstructionClass D.first F K₁ c₁ =
      (existenceObstructionClass D.second F K₂ c₂).comp (Abelian.Ext.mk₀ κ) (add_zero 2)

Tag 08ML, a remark

Tag 08ML in the Stacks Project.

Deformation.ToposThickening.FirstOrderThickeningSequence, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FirstOrderThickeningSequence.lean, line 109. The attribute's comment: “the sequence of morphisms of first order thickenings being classified”.

Stacks 08ML. A sequence of morphisms of first order thickenings of a ringed topos X: three first order thickenings i₁, i₂, i₃ of X, with their defining ideals, and two composable morphisms f₁₂, f₂₃ between them lying over the identity of X.

structure FirstOrderThickeningSequence

Deformation.ToposThickening.FirstOrderThickeningSequence.IsComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FirstOrderThickeningSequence.lean, line 205. The attribute's comment: “paragraph (1), the definition: the complex condition on the ideal maps”.

Stacks 08ML. A sequence of morphisms of first order thickenings of a ringed topos is a complex when the induced maps of its defining ideals compose to zero, so that I₃ ⟶ I₂ ⟶ I₁ is a complex of modules.

def IsComplex : Prop

Deformation.ToposThickening.FirstOrderThickeningSequence.IsShortExactSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FirstOrderThickeningSequence.lean, line 225. The attribute's comment: “paragraph (2): the short exact sequence condition on the ideal maps”.

Stacks 08ML. A sequence of morphisms of first order thickenings of a ringed topos is a short exact sequence when its induced maps of defining ideals form a short exact sequence 0 ⟶ I₃ ⟶ I₂ ⟶ I₁ ⟶ 0 of modules: the sequence is a complex, the map I₃ ⟶ I₂ is a monomorphism, the map I₂ ⟶ I₁ is an epimorphism, and the complex is exact in the middle.

def IsShortExactSequence : Prop

Deformation.ToposThickening.FirstOrderThickeningComplex.fSharp₃_comp_splitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningComplexTrivialization.lean, line 175. The attribute's comment: “the composition D₁ ⟶ D₃ factors through the base”.

Stacks 08ML. For a complex of first order thickenings, the composition (Sh(D₁), O'₁) ⟶ (Sh(D₃), O'₃) factors through (Sh(C), O) ⟶ (Sh(D₃), O'₃): on structure sheaves, the composite O'₃ ⟶ O'₁ is O'₃ ⟶ O ⟶ O'₁.

theorem fSharp₃_comp_splitting : S.fSharp₃ ≫ S.splitting hS = S.whole.hSharp

Deformation.ToposThickening.FirstOrderThickeningComplex.trivialization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningComplexTrivialization.lean, line 207. The attribute's comment: “the canonical trivialization of the smallest thickening”.

Stacks 08ML. The canonical trivialization π : (Sh(D₁), O'₁) ⟶ (Sh(C), O) of the smallest thickening of a complex of first order thickenings.

noncomputable def trivialization : Trivialization i

Deformation.ToposThickening.FirstOrderThickeningComplex.isTrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningComplexTrivialization.lean, line 213. The attribute's comment: “the smallest thickening of a complex is trivial”.

Stacks 08ML. The smallest thickening of a complex of first order thickenings is a trivial first order thickening of the base.

theorem isTrivial (S : FirstOrderThickeningComplex i) (hS : S.IsComplex) : IsTrivial i

Deformation.ToposThickening.FirstOrderThickeningSequence.i₃_fSharp_comp_splitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningSequenceTrivialization.lean, line 465. The attribute's comment: “the composition D₁ ⟶ D₃ factors through the base”.

Stacks 08ML. For a complex of first order thickenings, the composition (Sh(D₁), O'₁) ⟶ (Sh(D₃), O'₃) factors through (Sh(C), O) ⟶ (Sh(D₃), O'₃): on structure sheaves, the composite O'₃ ⟶ O'₁ is O'₃ ⟶ O ⟶ O'₁, the second map being the canonical map carried to the topos of the third thickening.

theorem i₃_fSharp_comp_splitting (hS : S.IsComplex) :
    S.i₃.fSharp ≫ S.baseIso.inv ≫ (pushforwardCommRingFunctor S.f₂₃.toToposHom).map
        ((pushforwardCommRingFunctor S.f₁₂.toToposHom).map (S.splitting hS)) =
      S.wholeSharp

Deformation.ToposThickening.FirstOrderThickeningSequence.trivialization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningSequenceTrivialization.lean, line 509. The attribute's comment: “the canonical trivialization of the smallest thickening”.

Stacks 08ML. The canonical trivialization π : (Sh(D₁), O'₁) ⟶ (Sh(C), O) of the smallest thickening of a complex of first order thickenings.

noncomputable def trivialization (hS : S.IsComplex) : Trivialization S.i₁

Deformation.ToposThickening.FirstOrderThickeningSequence.isTrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningSequenceTrivialization.lean, line 516. The attribute's comment: “the smallest thickening of a complex is trivial”.

Stacks 08ML. The smallest thickening of a complex of first order thickenings is a trivial first order thickening of the base.

theorem isTrivial (hS : S.IsComplex) : IsTrivial S.i₁

Tag 08MM, a remark

Tag 08MM in the Stacks Project.

Deformation.ToposThickening.FirstOrderThickeningComplex.boundary_underlyingExtensionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningComplexBoundary.lean, line 199. The attribute's comment: “the claim: the boundary of the extension class is the obstruction class”.

Let (Sh(C), O) be a ringed topos, F an O-module, and let O'₃ ⟶ O'₂ ⟶ O'₁ be a complex of first order thickenings of (Sh(C), O) presented on one site, with π a trivialization of O'₁. Let (Kₖ, cₖ) be pairs with cₖ : Iₖ ⊗_O F ⟶ Kₖ and let 0 ⟶ K₃ ⟶ K₂ ⟶ K₁ ⟶ 0 be a short exact sequence of O-modules making the two squares _hc₂₁ and hc₃₂ of the remark commute. Let F'₂ be an extension as in Stacks 08MB over O'₂ with c_{F'₂} = c₂ and let F'₁ be the extension over O'₁ that Stacks 08MJ produces from it.

Then the boundary map ∂ : Ext¹_O(F, K₁) ⟶ Ext²_O(F, K₃) of 0 ⟶ K₃ ⟶ K₂ ⟶ K₁ ⟶ 0 — Yoneda composition with the class of that sequence — carries the class ξ_{F'₁} of Stacks 08MI to the obstruction class o(F, K₃, c₃) of Stacks 08MF, for comparison data Q₃, E₃, presentation, w, hw and χ at the third thickening.

theorem boundary_underlyingExtensionClass (_hS : S.IsComplex) (π : Trivialization i)
    (F K₁ K₂ K₃ : SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRing i)))
    (c₁ : ((Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w', w', w'}
      (baseRing i)).obj S.lower.first.I).obj F ⟶ K₁)
    (c₂ : ((Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w', w', w'}
      (baseRing i)).obj S.lower.second.I).obj F ⟶ K₂)
    (c₃ : ((Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w', w', w'}
      (baseRing i)).obj S.third.I).obj F ⟶ K₃)
    (k₃₂ : K₃ ⟶ K₂) (k₂₁ : K₂ ⟶ K₁) (hk : k₃₂ ≫ k₂₁ = 0)
    (hK : (ShortComplex.mk k₃₂ k₂₁ hk).ShortExact)
    (_hc₂₁ : c₂ ≫ k₂₁ = ((Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w', w', w'}
      (baseRing i)).map S.idealMap₂₁).app F ≫ c₁)
    (hc₃₂ : c₃ ≫ k₃₂ = ((Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w', w', w'}
      (baseRing i)).map S.idealMap₃₂).app F ≫ c₂)
    (E₂ : Abelian.YonedaExtension ((structureRestrict (reshapeHom i S.lower.O₂
        S.lower.fSharp₂)).obj F)
      ((structureRestrict (reshapeHom i S.lower.O₂ S.lower.fSharp₂)).obj K₂) 0)
    (_hE₂ : (extensionActionMap S.lower.second E₂).1 = c₂)
    (E₁ : Abelian.YonedaExtension ((structureRestrict i).obj F)
      ((structureRestrict i).obj K₁) 0)
    (_hE₁ : (extensionActionMap S.lower.first E₁).1 = c₁)
    {Q₃ : SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRing i))}
    {E₃ : Abelian.YonedaExtension ((structureRestrict S.thirdHom).obj F)
      ((structureRestrict S.thirdHom).obj Q₃) 0}
    (presentation : MonoActionPresentation S.third E₃) (w : Q₃ ⟶ K₂)
    (hw : (extensionActionMap S.third E₃).1 ≫ w =
      ((Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w', w', w'}
        (baseRing i)).map S.idealMap₃₂).app F ≫ c₂)
    (χ : E₃.Z.left ⟶
      (structureRestrict S.thirdHom).obj ((splitRestriction i S.lower.first π).obj E₁.Z.left))
    (hχf : E₃.f ≫ χ = (structureRestrict S.thirdHom).map (w ≫ k₂₁) ≫
      (structureRestrict S.thirdHom).map (splitExtension i S.lower.first π F K₁ E₁).f)
    (hχg : χ ≫ (structureRestrict S.thirdHom).map
      (splitExtension i S.lower.first π F K₁ E₁).g = E₃.g) :
    (underlyingExtensionClass i S.lower.first π F K₁ E₁).comp hK.extClass (by decide) =
      existenceObstructionClass S.third F K₃ c₃

Deformation.ToposThickening.FirstOrderThickeningComplex.boundary_underlyingExtensionClass_eq_obstructionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningComplexBoundaryCanonical.lean, line 247.

Stacks Project, Tag 08MM. Let (Sh(C), O) be a ringed topos, F an O-module and O'₃ ⟶ O'₂ ⟶ O'₁ a complex of first order thickenings of (Sh(C), O) (Stacks 08ML), presented on one site. Let cₖ : Iₖ ⊗_O F ⟶ Kₖ be maps and 0 ⟶ K₃ ⟶ K₂ ⟶ K₁ ⟶ 0 a short exact sequence of O-modules for which the second square hc₃₂ of the remark commutes. Let F'₂ be an extension 0 ⟶ K₂ ⟶ F'₂ ⟶ F ⟶ 0 over O'₂ as in Stacks 08MB with c_{F'₂} = c₂, and let F'₁ be the extension over O'₁ that the functoriality of Stacks 08MJ produces from it. That functoriality carries F'₂ to an extension of F by K₁ over O'₁ together with a map of extensions u from F'₂, which is K₂ ⟶ K₁ on kernel modules and the identity on F; the statement is made for every extension F'₁ receiving such a map, so in particular for the one of Stacks 08MJ (boundary_underlyingExtensionClass_extensionOne_eq_obstructionClass).

Then the boundary map ∂ : Ext¹_O(F, K₁) ⟶ Ext²_O(F, K₃) of 0 ⟶ K₃ ⟶ K₂ ⟶ K₁ ⟶ 0 — Yoneda composition with the class of that sequence — sends the class ξ_{F'₁} of Stacks 08MI, formed with the canonical splitting π = S.trivialization hS of Stacks 08ML, to the obstruction class o(F, K₃, c₃) of Stacks 08MF.

The map c₁ and the first compatibility square of the remark are what make Stacks 08MJ applicable; once F'₁ and u are given they are not needed for the identity of classes, so they are not hypotheses here. They are hypotheses of the version for the extension that Stacks 08MJ constructs.

theorem boundary_underlyingExtensionClass_eq_obstructionClass
    (F K₁ K₂ K₃ : SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRing i)))
    (k₃₂ : K₃ ⟶ K₂) (k₂₁ : K₂ ⟶ K₁) (hk : k₃₂ ≫ k₂₁ = 0)
    (hK : (ShortComplex.mk k₃₂ k₂₁ hk).ShortExact)
    (c₂ : ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj S.lower.second.I).obj F ⟶
      K₂)
    (c₃ : ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj S.third.I).obj F ⟶ K₃)
    (hc₃₂ : c₃ ≫ k₃₂ =
      ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).map S.idealMap₃₂).app F ≫ c₂)
    (E₂ : Abelian.YonedaExtension
      ((structureRestrict (reshapeHom i S.lower.O₂ S.lower.fSharp₂)).obj F)
      ((structureRestrict (reshapeHom i S.lower.O₂ S.lower.fSharp₂)).obj K₂) 0)
    (hE₂ : (extensionActionMap S.lower.second E₂).1 = c₂)
    (E₁ : Abelian.YonedaExtension ((structureRestrict i).obj F)
      ((structureRestrict i).obj K₁) 0)
    (u : E₂.Z.left ⟶ (S.lower.restrictedExtension E₁).Z.left)
    (hu : E₂.f ≫ u =
      (structureRestrict (reshapeHom i S.lower.O₂ S.lower.fSharp₂)).map k₂₁ ≫
        (S.lower.restrictedExtension E₁).f)
    (hug : u ≫ (S.lower.restrictedExtension E₁).g = E₂.g) :
    (underlyingExtensionClass i S.lower.first (S.trivialization hS) F K₁ E₁).comp hK.extClass
        (by decide) =
      existenceObstructionClass S.third F K₃ c₃

Deformation.ToposThickening.FirstOrderThickeningComplex.boundary_underlyingExtensionClass_extensionOne_eq_obstructionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ThickeningComplexBoundaryCanonical.lean, line 337.

Stacks Project, Tag 08MM, for the extension F'₁ that Stacks 08MJ constructs. Let (Sh(C), O) be a ringed topos, F an O-module and O'₃ ⟶ O'₂ ⟶ O'₁ a complex of first order thickenings of (Sh(C), O) (Stacks 08ML), presented on one site. Let (Kₖ, cₖ), k = 1, 2, 3, be pairs of an O-module Kₖ and a map cₖ : Iₖ ⊗_O F ⟶ Kₖ, and let 0 ⟶ K₃ ⟶ K₂ ⟶ K₁ ⟶ 0 be a short exact sequence of O-modules making the two squares hc₂₁ and hc₃₂ of the remark commute. Let F'₂ be an extension 0 ⟶ K₂ ⟶ F'₂ ⟶ F ⟶ 0 of O'₂-modules as in Stacks 08MB with c_{F'₂} = c₂, and let F'₁ be the extension of O'₁-modules that the functoriality of Stacks 08MJ produces from it (MorphismOfFirstOrderThickenings.PushoutExtensionData.extensionOne, built on the data (F, K₁, K₂, c₁, c₂, K₂ ⟶ K₁) and the first square).

Then the boundary map ∂ : Ext¹_O(F, K₁) ⟶ Ext²_O(F, K₃) of 0 ⟶ K₃ ⟶ K₂ ⟶ K₁ ⟶ 0 sends the class ξ_{F'₁} of Stacks 08MI, formed with the canonical splitting π = S.trivialization hS of Stacks 08ML, to the obstruction class o(F, K₃, c₃) of Stacks 08MF.

theorem boundary_underlyingExtensionClass_extensionOne_eq_obstructionClass
    (F K₁ K₂ K₃ :
      SheafOfModules.{max v₂ u₂} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRing i)))
    (c₁ : ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj S.lower.first.I).obj F ⟶
      K₁)
    (c₂ : ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj S.lower.second.I).obj F ⟶
      K₂)
    (c₃ : ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj S.third.I).obj F ⟶ K₃)
    (k₃₂ : K₃ ⟶ K₂) (k₂₁ : K₂ ⟶ K₁) (hk : k₃₂ ≫ k₂₁ = 0)
    (hK : (ShortComplex.mk k₃₂ k₂₁ hk).ShortExact)
    (hc₂₁ : c₂ ≫ k₂₁ =
      ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).map S.idealMap₂₁).app F ≫ c₁)
    (hc₃₂ : c₃ ≫ k₃₂ =
      ((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).map S.idealMap₃₂).app F ≫ c₂)
    (E₂ : Abelian.YonedaExtension
      ((structureRestrict (reshapeHom i S.lower.O₂ S.lower.fSharp₂)).obj F)
      ((structureRestrict (reshapeHom i S.lower.O₂ S.lower.fSharp₂)).obj K₂) 0)
    (hE₂ : (extensionActionMap S.lower.second E₂).1 = c₂) :
    (underlyingExtensionClass i S.lower.first (S.trivialization hS) F K₁
        ((S.lower.pushoutDataOfPushout c₂ c₁ k₂₁ hc₂₁).extensionOne E₂ hE₂)).comp
        hK.extClass (by decide) =
      existenceObstructionClass S.third F K₃ c₃

Sources

LeanDeformation.ToposThickening.extensionActionMap · CategoryTheory.Abelian.YonedaExtension · Deformation.ToposThickening.compatibleMap_add_quotientKernel · Deformation.ToposThickening.compatibleMap_unique_quotientKernel_difference · idealActionMap_naturality · Deformation.ToposThickening.obstructionClass · Deformation.ToposThickening.obstructionClass_eq_zero_iff · Deformation.ToposThickening.fixedActionExtensionClass_torsor

Section91.11 Infinitesimal deformations of modules on ringed topoi #

Section 91.11 of the Stacks Project, Tag 08MN. 8 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08MP, a lemma

Tag 08MP in the Stacks Project.

Deformation.ToposThickening.moduleMapLift_torsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/PushforwardComparison/ModuleMapLifts.lean, line 382.

Stacks 08MP. If a map of pullbacks across a first order thickening has a lift, then its lifts form a principal homogeneous space under the maps from the pullback of F' to the descent of the ideal product I·G', with translation given by adding the corresponding map into I·G' followed by its inclusion into G'.

theorem moduleMapLift_torsor (hi : FirstOrderThickening i)
    (F' G' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    (φ : (i.toRingedToposModulesHom.pullbackModules).obj F' ⟶
      (i.toRingedToposModulesHom.pullbackModules).obj G')
    (h : Nonempty (ModuleMapLift F' G' φ)) :
    ∃ t : AddTorsor
        ((i.toRingedToposModulesHom.pullbackModules).obj F' ⟶
          (idealProductModule hi G').val)
        (ModuleMapLift F' G' φ),
      ∀ (α : (i.toRingedToposModulesHom.pullbackModules).obj F' ⟶ (idealProductModule hi G').val)
        (c : ModuleMapLift F' G' φ),
        (t.vadd α c).val = c.val +
          idealProductHomEquiv hi F' G' α ≫ (idealProductSubmodule hi G').ι

Tag 08MQ, a lemma

Tag 08MQ in the Stacks Project.

Deformation.ToposThickening.isFlat_iff_isIso_canonicalMap_of_isStrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatLiftFlatness.lean, line 113.

Stacks 08MQ. Let (f, f') be a morphism of first order thickenings of ringed topoi as in Situation 08M7, let ℱ' be an O'-module and set ℱ = i^*ℱ'. Assume that ℱ is flat over O_ℬ and that (f, f') is a strict morphism of thickenings (Definition 08M9). Then the following are equivalent:

ℱ' is flat over O_{ℬ'}, and

the canonical map f^*𝒥 ⊗_O ℱ ⟶ I·ℱ' is an isomorphism.

Moreover, in this case the maps f^*𝒥 ⊗_O ℱ ⟶ I ⊗_O ℱ ⟶ I·ℱ' are isomorphisms.

How the source's objects are read:

the square is Deformation.ToposThickening.MorphismOfThickenings.ofFirstOrderThickenings, built from the first order thickenings hi and ht and the commutativity comm;

O-modules live on the thickened topos as i_*O-modules, as throughout this tree, and ℱ = i^*ℱ' is presented by the short exact sequence 0 ⟶ I·ℱ' ⟶ ℱ' ⟶ ℱ ⟶ 0 given by q, hq and hqex (the form Deformation.ToposThickening.HasFlatLift uses); the statement holds for every such presentation;

"ℱ flat over O_ℬ" is Deformation.ToposThickening.IsFlatOverBase, and "ℱ' flat over O_{ℬ'}" is flatness of Deformation.ToposThickening.baseModule, that is, over f⁻¹O_{ℬ'}, which is the definition the source's proof opens with;

strictness is Deformation.ToposThickening.MorphismOfThickenings.IsStrict, Definition 08M9;

the canonical map is Deformation.ToposThickening.canonicalMap, the composite of Deformation.ToposThickening.canonicalFirstFactor (f^*𝒥 ⊗_O ℱ ⟶ I ⊗_O ℱ) and Deformation.ToposThickening.canonicalSecondFactor (I ⊗_O ℱ ⟶ I·ℱ'). Its source is written f⁻¹𝒥 ⊗_{f⁻¹O_ℬ} ℱ, which the source's proof identifies with f^*𝒥 ⊗_O ℱ ("observe that f^*𝒥 ⊗_O ℱ = f⁻¹𝒥 ⊗_{f⁻¹O_ℬ} ℱ"; in this tree Stacks.FlatChangeOfRings.cancelExtendScalarsTensorSheafIso'), and the composite is read over f⁻¹O_{ℬ'}, the ring over which both factors are linear; being an isomorphism does not depend on that reading.

The proof is the source's: strictness gives ℱ = ℱ'/(f⁻¹𝒥)ℱ', and the equivalence is the flatness criterion of Stacks 08M4 for the square-zero extension f⁻¹O_{ℬ'} ⟶ f⁻¹O_ℬ; see Deformation.ToposThickening.isFlat_iff_isIso_canonicalMap.

theorem isFlat_iff_isIso_canonicalMap_of_isStrict
    (i : RingedToposHom X X') (t : RingedToposHom S S') (f : RingedToposHom X S)
    (f' : RingedToposHom X' S') (hi : FirstOrderThickening i) (ht : FirstOrderThickening t)
    (comm : f'.comp i = t.comp f)
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    (F' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))
    (q : F' ⟶ (SheafOfModules.restrictScalars (ringMap i.fSharp)).obj F)
    (hq : (idealProductSubmodule hi F').ι ≫ q = 0)
    (hqex : (ShortComplex.mk (idealProductSubmodule hi F').ι q hq).ShortExact)
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hF : IsFlatOverBase i f F) :
    (AlgebraicGeometry.SheafOfModules.IsFlat (baseModule f' F') ↔
        IsIso (canonicalMap i t f f' hi ht comm F F' q hq hqex)) ∧
      (IsIso (canonicalMap i t f f' hi ht comm F F' q hq hqex) →
        IsIso (canonicalFirstFactor i t f f' hi ht comm F) ∧
          IsIso (canonicalSecondFactor i hi F F' q hq hqex))

Tag 08VU, a lemma

Tag 08VU in the Stacks Project.

Deformation.ToposThickening.isFinitePresentation_iff_pullbackModules_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FinitePresentationFlatLift.lean, line 809.

Stacks 08VU. Let (f, f') be a morphism of first order thickenings of ringed topoi as in Situation 08M7, let ℱ' be an O'-module and set ℱ = i^*ℱ'. Assume that ℱ' is flat over O_{ℬ'} and that (f, f') is a strict morphism of thickenings. Then ℱ' is an O'-module of finite presentation if and only if ℱ is an O-module of finite presentation.

Flatness of ℱ' over O_{ℬ'} is flatness of ℱ' read as an (f')^{-1}O_{ℬ'}-module, as in Deformation.ToposThickening.HasFlatLift, and ℱ = i^*ℱ' is the pullback of Stacks 03D6.

The direction (1) ⇒ (2) is Stacks 03DO and uses none of the hypotheses. For (2) ⇒ (1), Stacks 03DM moves ℱ to the site of the thickening, where each local presentation of it lifts to one of ℱ'; flatness and strictness enter only through the injectivity of the action of I on ℱ' (Deformation.ToposThickening.isIdealActionMono). See the module docstring.

theorem isFinitePresentation_iff_pullbackModules_of_isFlat
    (i : RingedToposHom X X') (t : RingedToposHom S S') (f : RingedToposHom X S)
    (f' : RingedToposHom X' S') (hi : FirstOrderThickening i) (ht : FirstOrderThickening t)
    (comm : f'.comp i = t.comp f) (F' : SheafOfModules.{w} (ringSheaf X'.O))
    (hflat : AlgebraicGeometry.SheafOfModules.IsFlat
      ((SheafOfModules.restrictScalars
        ((sheafCompose X'.J (forget₂ CommRingCat.{w} RingCat.{w})).map
          f'.fSharpInverseImage)).obj F'))
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict) :
    F'.IsFinitePresentation ↔
      (i.toRingedToposModulesHom.pullbackModules.obj F').IsFinitePresentation

Tag 08MR, a lemma

Tag 08MR in the Stacks Project.

Deformation.ToposThickening.moduleMapLift_torsor_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatLiftTorsors.lean, line 398. The attribute's comment: “granting Stacks 08MQ, carried as the hypothesis IsIdealProductTensorIso”.

Stacks 08MR. Let (f, f') be a strict morphism of first order thickenings of ringed topoi as in Situation 08M7, let ℱ' and 𝒢' be O'-modules with 𝒢' flat over O_{ℬ'}, and let φ : i^*ℱ' ⟶ i^*𝒢' be a map of O-modules. If φ has at least one lift to an O'-linear map ℱ' ⟶ 𝒢', then its lifts form a principal homogeneous set under Hom_O(i^*ℱ', f^*J ⊗_O i^*𝒢').

The source's proof is "combine Lemmas 08MP and 08MQ": Stacks 08MP makes the lifts a principal homogeneous set under Hom_O(i^*ℱ', I·𝒢'), and Stacks 08MQ identifies I·𝒢' with f^*J ⊗_O i^*𝒢'. Here the second step is the hypothesis hMQ.

theorem moduleMapLift_torsor_of_isFlat (i : RingedToposHom X X') (t : RingedToposHom S S')
    (f : RingedToposHom X S) (f' : RingedToposHom X' S') (hi : FirstOrderThickening i)
    (ht : FirstOrderThickening t) (comm : f'.comp i = t.comp f)
    (F' G' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hG : AlgebraicGeometry.SheafOfModules.IsFlat
      ((SheafOfModules.restrictScalars
        ((sheafCompose X'.J (forget₂ CommRingCat.{w} RingCat.{w})).map
          f'.fSharpInverseImage)).obj G'))
    (hMQ : IsIdealProductTensorIso i t f f' hi ht comm G')
    (φ : (i.toRingedToposModulesHom.pullbackModules).obj F' ⟶
      (i.toRingedToposModulesHom.pullbackModules).obj G')
    (hne : Nonempty (ModuleMapLift F' G' φ)) :
    Nonempty (AddTorsor
      ((pullbackModules i.toRingedToposModulesHom).obj F' ⟶
        ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} X.O).obj
            (basePullbackIdeal t f ht)).obj
          ((pullbackModules i.toRingedToposModulesHom).obj G'))
      (ModuleMapLift F' G' φ))

Deformation.ToposThickening.exists_addTorsor_moduleMapLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealProductTensorIso.lean, line 310.

Stacks 08MR. Let (f, f') be a strict morphism of first order thickenings of ringed topoi as in Situation 08M7, let ℱ' and 𝒢' be O'-modules with 𝒢' flat over O_{ℬ'}, set ℱ = i^*ℱ' and 𝒢 = i^*𝒢', and let φ : ℱ ⟶ 𝒢 be a map of O-modules. If φ has at least one lift to an O'-linear map φ' : ℱ' ⟶ 𝒢', then its lifts form a principal homogeneous set under Hom_O(ℱ, 𝒢 ⊗_O f^*J).

The action is the one of the source's proof, "combine Lemmas 08MP and 08MQ": an element α : ℱ ⟶ 𝒢 ⊗_O f^*J sends a lift φ' to φ' + ι ∘ α, where ι ∘ α : ℱ' ⟶ 𝒢' is the O'-linear map corresponding to α followed by the symmetry 𝒢 ⊗_O f^*J ≅ f^*J ⊗_O 𝒢, the canonical identification f^*J ⊗_O 𝒢 ≅ I·𝒢' of Stacks 08MQ (Deformation.ToposThickening.idealProductTensorIso) and the inclusion I·𝒢' ⊂ 𝒢'. Concretely, α composed with those identifications is a map into the descent of I·𝒢', which Deformation.ToposThickening.idealProductHomEquiv (the adjunction i^* ⊣ i_*) reads as a map ℱ' ⟶ I·𝒢'.

theorem exists_addTorsor_moduleMapLift
    (F' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hG : AlgebraicGeometry.SheafOfModules.IsFlat
      ((SheafOfModules.restrictScalars (ringMap f'.fSharpInverseImage)).obj G'))
    (φ : (pullbackModules i.toRingedToposModulesHom).obj F' ⟶
      (pullbackModules i.toRingedToposModulesHom).obj G')
    (hne : Nonempty (ModuleMapLift F' G' φ)) :
    ∃ T : AddTorsor
        ((pullbackModules i.toRingedToposModulesHom).obj F' ⟶
          ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} X.O).flip.obj
              (basePullbackIdeal t f ht)).obj
            ((pullbackModules i.toRingedToposModulesHom).obj G'))
        (ModuleMapLift F' G' φ),
      ∀ (α : (pullbackModules i.toRingedToposModulesHom).obj F' ⟶
          ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} X.O).flip.obj
              (basePullbackIdeal t f ht)).obj
            ((pullbackModules i.toRingedToposModulesHom).obj G'))
        (φ' : ModuleMapLift F' G' φ),
        (T.vadd α φ').val = φ'.val +
          idealProductHomEquiv hi F' G'
              (α ≫ ((Stacks.SheafOfModules.FlatSquareZero.tensorLeftIsoTensorRight X.O
                  (basePullbackIdeal t f ht)).app
                  ((pullbackModules i.toRingedToposModulesHom).obj G')).inv ≫
                (idealProductTensorIso i t f f' hi ht comm G' hstrict hG).hom) ≫
            (idealProductSubmodule hi G').ι

Tag 08MS, a lemma

Tag 08MS in the Stacks Project.

Deformation.ToposThickening.moduleMapObstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModuleMapObstruction.lean, line 240.

Stacks 08MS. There is a class o(φ) in Ext¹_O(Li^*F', I·G') whose vanishing is necessary and sufficient for the O-linear map φ : i^*F' ⟶ i^*G' to be the pullback of an O'-linear map F' ⟶ G'.

The class is the connecting class of the sequence 0 ⟶ I·G' ⟶ G' ⟶ i_*i^*G' ⟶ 0 on the adjoint transpose of φ, read across Li^* ⊣ Ri_*.

noncomputable def moduleMapObstruction :
    { o : DerivedCategory.Ext
        (d.functor.obj ((DerivedCategory.singleFunctor
          (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj F'))
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := X.J)) X.O)) 0).obj
            (idealProductModule hi G').val) 1 //
      o = 0 ↔ Nonempty (ModuleMapLift F' G' φ) }

Deformation.ToposThickening.moduleMapObstructionClass, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModuleMapObstruction.lean, line 273.

Stacks 08MS. The obstruction class o(φ) ∈ Ext¹_O(Li^*F', I·G') itself.

noncomputable abbrev moduleMapObstructionClass :
    DerivedCategory.Ext
      (d.functor.obj ((DerivedCategory.singleFunctor
        (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) 0).obj F'))
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := X.J)) X.O)) 0).obj
          (idealProductModule hi G').val) 1

Deformation.ToposThickening.moduleMapObstructionClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModuleMapObstruction.lean, line 284.

Stacks 08MS. The obstruction class vanishes exactly when φ lifts.

theorem moduleMapObstructionClass_eq_zero_iff :
    moduleMapObstructionClass hi d F' G' φ = 0 ↔ Nonempty (ModuleMapLift F' G' φ)

Deformation.ToposThickening.moduleMapLiftObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ModuleMapObstructionDerivedPullback.lean, line 113.

Stacks 08MS. Let i : (Sh(C), O) ⟶ (Sh(D), O') be a first order thickening of ringed topoi, let F', G' be O'-modules and let φ : i^*F' ⟶ i^*G' be O-linear. The element o(φ) ∈ Ext¹_O(Li^*F', I·G') vanishes if and only if φ lifts to an O'-linear map φ' : F' ⟶ G', i.e. one with i^*φ' = φ.

theorem moduleMapLiftObstruction_eq_zero_iff (hi : FirstOrderThickening i)
    (F' G' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    (φ : (i.toRingedToposModulesHom.pullbackModules).obj F' ⟶
      (i.toRingedToposModulesHom.pullbackModules).obj G') :
    moduleMapLiftObstruction hi F' G' φ = 0 ↔ Nonempty (ModuleMapLift F' G' φ)

Tag 08MT, a lemma

Tag 08MT in the Stacks Project.

Deformation.ToposThickening.relativeModuleMapObstructionClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealActionMono.lean, line 254.

Stacks 08MT. Let (f, f') be a strict morphism of first order thickenings of ringed topoi as in Situation 08M7, let ℱ' and 𝒢' be O'-modules flat over O_{ℬ'}, set ℱ = i^*ℱ' and 𝒢 = i^*𝒢', and let φ : ℱ ⟶ 𝒢 be an O-linear map. The element o(φ) ∈ Ext¹_O(ℱ, 𝒢 ⊗_O f^*𝒥) of Deformation.ToposThickening.relativeModuleMapObstructionClass vanishes if and only if φ lifts to an O'-linear map φ' : ℱ' ⟶ 𝒢'.

The class vanishes exactly when the pulled-back sequence it is the class of splits after i^*; a splitting descends to one before i^*, the unit of the adjunction being invertible on a direct image, and a splitting of the pulled-back sequence is a factorization of the transpose of φ through 𝒢' ⟶ i_*𝒢, which is a lift of φ.

theorem relativeModuleMapObstructionClass_eq_zero_iff
    (F' G' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hF : AlgebraicGeometry.SheafOfModules.IsFlat
      ((SheafOfModules.restrictScalars
        ((sheafCompose X'.J (forget₂ CommRingCat.{w} RingCat.{w})).map
          f'.fSharpInverseImage)).obj F'))
    (hG : AlgebraicGeometry.SheafOfModules.IsFlat
      ((SheafOfModules.restrictScalars
        ((sheafCompose X'.J (forget₂ CommRingCat.{w} RingCat.{w})).map
          f'.fSharpInverseImage)).obj G'))
    (φ : (pullbackModules i.toRingedToposModulesHom).obj F' ⟶
      (pullbackModules i.toRingedToposModulesHom).obj G') :
    relativeModuleMapObstructionClass.{_, _, _, _, _, _, _, _, _, _, _, e} i t f f' hi ht comm F' G'
        hstrict hF hG φ = 0 ↔
      Nonempty (ModuleMapLift F' G' φ)

Tag 08MU, a lemma

Tag 08MU in the Stacks Project.

Deformation.ToposThickening.exists_addTorsor_flatLiftClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatLiftClassTorsor.lean, line 96.

Stacks 08MU. Let (f, f') be a strict morphism of first order thickenings of ringed topoi as in Situation 08M7 and let ℱ be an O-module flat over O_ℬ. If there is a pair (ℱ', α) consisting of an O'-module ℱ' flat over O_{ℬ'} and an isomorphism α : i^*ℱ' ≅ ℱ, then the isomorphism classes of such pairs form a principal homogeneous set under Ext¹_O(ℱ, I ⊗_O ℱ).

The action is the one of the source's proof. A pair (ℱ', α) gives the extension 0 ⟶ I ⊗_O ℱ ⟶ ℱ' ⟶ ℱ ⟶ 0 of O'-modules whose first map is the canonical map I ⊗_O ℱ ≅ I·ℱ' ⊂ ℱ' (Deformation.ToposThickening.FlatLift.fixedActionExtension; the canonical map is an isomorphism onto I·ℱ' by Stacks 08MQ), and a ∈ Ext¹_O(ℱ, I ⊗_O ℱ) sends the class of (ℱ', α) to the class of (𝒢', β) exactly when the Ext¹_{O'} class of the extension of 𝒢' is that of ℱ' plus the image of a, which is the action of Stacks 08ME.

theorem exists_addTorsor_flatLiftClass (i : RingedToposHom X X') (t : RingedToposHom S S')
    (f : RingedToposHom X S) (f' : RingedToposHom X' S') (hi : FirstOrderThickening i)
    (ht : FirstOrderThickening t) (comm : f'.comp i = t.comp f)
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    [HasExt.{e} (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hflat : IsFlatOverBase i f F) (hne : Nonempty (FlatLift i f' hi F)) :
    ∃ T : AddTorsor
        (Abelian.Ext.{e} F
          (((Stacks.SheafOfModules.Tensor.sheafTensor
            ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I) 1)
        (FlatLiftClass i f' hi F),
      ∀ (a : Abelian.Ext.{e} F
          (((Stacks.SheafOfModules.Tensor.sheafTensor
            ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I) 1)
        (A B : FlatLift i f' hi F),
        T.vadd a (Quotient.mk (flatLiftSetoid i f' hi F) A) =
            Quotient.mk (flatLiftSetoid i f' hi F) B ↔
          extensionClass F
              (((Stacks.SheafOfModules.Tensor.sheafTensor
                ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I)
              (B.fixedActionExtension i t f f' hi ht comm F
                ((isStrictPullbackIdealMap_iff_isStrict i t f f' hi ht comm).mpr hstrict)
                (isFlat_reducedBaseModule_of_isFlatOverBase i t f f' hi ht comm F hflat)) =
            (SheafOfModules.restrictScalars (structureRingMap i)).mapExtAddHom F
                (((Stacks.SheafOfModules.Tensor.sheafTensor
                  ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I) 1 a +
              extensionClass F
                (((Stacks.SheafOfModules.Tensor.sheafTensor
                  ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I)
                (A.fixedActionExtension i t f f' hi ht comm F
                  ((isStrictPullbackIdealMap_iff_isStrict i t f f' hi ht comm).mpr hstrict)
                  (isFlat_reducedBaseModule_of_isFlatOverBase i t f f' hi ht comm F hflat))

Deformation.ToposThickening.flatLiftClass_torsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatLiftTorsors.lean, line 322. The attribute's comment: “granting Stacks 08MQ, carried as the hypothesis IsFlatLiftClassCorrespondence”.

Stacks 08MU. Let (f, f') be a strict morphism of first order thickenings of ringed topoi as in Situation 08M7 and let ℱ be an O-module flat over O_ℬ. If ℱ has at least one lift to an O'-module flat over O_{ℬ'}, then the isomorphism classes of such lifts form a principal homogeneous set under Ext¹_O(ℱ, I ⊗_O ℱ).

The source proves this by applying Stacks 08MQ to see that the canonical map f^*J ⊗ ℱ ⟶ I ⊗ ℱ is an isomorphism, which identifies the lifts with the extensions of ℱ by I ⊗_O ℱ whose action map is the identity, and then quoting Stacks 08ME for those. Here the first step is the hypothesis hMQ and the second is Deformation.ToposThickening.fixedActionExtensionClass_torsor.

theorem flatLiftClass_torsor (i : RingedToposHom X X') (t : RingedToposHom S S')
    (f : RingedToposHom X S) (f' : RingedToposHom X' S') (hi : FirstOrderThickening i)
    (ht : FirstOrderThickening t) (comm : f'.comp i = t.comp f)
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    [HasExt.{e} (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hflat : IsFlatOverBase i f F)
    (hMQ : IsFlatLiftClassCorrespondence.{_, _, _, _, _, _, _, _, _, _, _, e}
      i t f f' hi ht comm F)
    (hne : Nonempty (FlatLift i f' hi F)) :
    Nonempty (AddTorsor
      (Abelian.Ext.{e} F
        (((Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w, w, w}
          ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F) 1)
      (FlatLiftClass i f' hi F))

Tag 08MV, a lemma

Tag 08MV in the Stacks Project.

Deformation.ToposThickening.hasFlatLift_iff_isIso_and_obstruction_eq_zero', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatLiftCorrespondence.lean, line 232.

Stacks 08MV, unconditionally. Let (f, f') be a morphism of first order thickenings of ringed topoi as in Situation 08M7, strict, and let ℱ be an O-module flat over O_ℬ. Then ℱ has a lift to an O'-module flat over O_{ℬ'} if and only if the canonical map f^*J ⊗ ℱ ⟶ I ⊗ ℱ is an isomorphism and the obstruction class o(ℱ, I ⊗_O ℱ, 1) of Stacks 08MF vanishes.

This is Deformation.ToposThickening.hasFlatLift_iff_isIso_and_obstruction_eq_zero with its Deformation.ToposThickening.IsFlatLiftCorrespondence hypothesis supplied by Deformation.ToposThickening.isFlatLiftCorrespondence.

theorem hasFlatLift_iff_isIso_and_obstruction_eq_zero'
    [HasExt.{e} (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hflat : IsFlatOverBase i f F) :
    HasFlatLift i f' hi F ↔
      IsIso (idealTensorComparison i t f f' hi ht comm F) ∧
        existenceObstructionClass hi F
            (((Stacks.SheafOfModules.Tensor.sheafTensor ((pushforwardCommRingFunctor
                i.toToposHom).obj X.O)).flip.obj F).obj hi.I)
            (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor ((pushforwardCommRingFunctor
                i.toToposHom).obj X.O)).flip.obj F).obj
              hi.I)) = 0

Deformation.ToposThickening.hasFlatLift_iff_isIso_and_obstruction_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatLiftObstruction.lean, line 310. The attribute's comment: “granting Stacks 08MQ, carried as the hypothesis IsFlatLiftCorrespondence”.

Stacks 08MV. Let (f, f') be a morphism of first order thickenings of ringed topoi as in Situation 08M7, strict, and let ℱ be an O-module flat over O_ℬ. Then ℱ has a lift to an O'-module flat over O_{ℬ'} if and only if the canonical map f^*J ⊗ ℱ ⟶ I ⊗ ℱ is an isomorphism and the obstruction class o(ℱ, I ⊗_O ℱ, 1) of Stacks 08MF vanishes.

theorem hasFlatLift_iff_isIso_and_obstruction_eq_zero
    (i : RingedToposHom X X') (t : RingedToposHom S S') (f : RingedToposHom X S)
    (f' : RingedToposHom X' S') (hi : FirstOrderThickening i) (ht : FirstOrderThickening t)
    (comm : f'.comp i = t.comp f)
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    [HasExt.{e} (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hflat : IsFlatOverBase i f F)
    (hMQ : IsFlatLiftCorrespondence i t f f' hi ht comm F) :
    HasFlatLift i f' hi F ↔
      IsIso (idealTensorComparison i t f f' hi ht comm F) ∧
        existenceObstructionClass hi F
            (((sheafTensor.{u', v', w, w, w}
              ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F)
            (𝟙 (((sheafTensor.{u', v', w, w, w}
              ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F)) = 0

Sources

Section91.12 Application to flat modules on flat thickenings of ringed topoi #

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

Tag 08VW, a lemma

Tag 08VW in the Stacks Project.

Deformation.ToposThickening.hasFlatLift_iff_obstruction_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatLiftObstruction.lean, line 343. The attribute's comment: “part (1) only; (2) and (3) are not proved; granting 08MQ as hypotheses”.

Stacks 08VW, part (1). In the situation of Stacks 08VV — a strict morphism (f, f') of first order thickenings of ringed topoi with f' flat, and an O-module ℱ flat over O_ℬ — the module ℱ has a lift to an O'-module flat over O_{ℬ'} if and only if the obstruction class o(ℱ, f^*J ⊗_O ℱ, 1) of Stacks 08MF vanishes. The class is written here for I ⊗_O ℱ, the two agreeing because I = f^*J under these hypotheses.

theorem hasFlatLift_iff_obstruction_eq_zero
    (i : RingedToposHom X X') (t : RingedToposHom S S') (f : RingedToposHom X S)
    (f' : RingedToposHom X' S') (hi : FirstOrderThickening i) (ht : FirstOrderThickening t)
    (comm : f'.comp i = t.comp f)
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    [HasExt.{e} (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hf' : f'.IsFlat) (hflat : IsFlatOverBase i f F)
    (hMQ : IsFlatLiftCorrespondence i t f f' hi ht comm F)
    (hMQ' : IsIdealComparisonIsoOfFlat i t f f' hi ht comm F) :
    HasFlatLift i f' hi F ↔
      existenceObstructionClass hi F
          (((sheafTensor.{u', v', w, w, w}
            ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F)
          (𝟙 (((sheafTensor.{u', v', w, w, w}
            ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).obj hi.I).obj F)) = 0

Deformation.ToposThickening.hasFlatLift_iff_basePullbackIdeal_obstruction_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatThickeningFlatLifts.lean, line 236.

Stacks 08VW, part (1). In Situation 08VV — (f, f') a strict morphism of first order thickenings of ringed topoi with f' flat, and ℱ an O-module flat over O_ℬ — there is an O'-module ℱ' flat over O_{ℬ'} with i^*ℱ' ≅ ℱ if and only if the class o(ℱ, f^*J ⊗_O ℱ, 1) ∈ Ext²_O(ℱ, f^*J ⊗_O ℱ) of Stacks 08MF vanishes.

Here 1 is the action I ⊗_O ℱ ⟶ f^*J ⊗_O ℱ which is the identity under the identification I = f^*J of Situation 08VV, i.e. the inverse of Deformation.ToposThickening.basePullbackIdealTensorIso.

theorem hasFlatLift_iff_basePullbackIdeal_obstruction_eq_zero
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    [HasExt.{e} (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hf' : f'.IsFlat) (hflat : IsFlatOverBase i f F) :
    HasFlatLift i f' hi F ↔
      existenceObstructionClass hi F
        (((Stacks.SheafOfModules.Tensor.sheafTensor
          ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj
          (basePullbackIdealOverThickened i t f ht))
        (basePullbackIdealTensorIso i t f f' hi ht comm hf' hstrict F).inv = 0

Deformation.ToposThickening.exists_addTorsor_flatLiftClass_basePullbackIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatThickeningFlatLifts.lean, line 268.

Stacks 08VW, part (2). In Situation 08VV, if ℱ has a lift to an O'-module flat over O_{ℬ'}, then the isomorphism classes of such lifts form a principal homogeneous set under Ext¹_O(ℱ, f^*J ⊗_O ℱ).

The action is the one of Stacks 08MU, read through the identification f^*J ⊗_O ℱ ≅ I ⊗_O ℱ (Deformation.ToposThickening.basePullbackIdealTensorIso): a lift ℱ' gives the extension 0 ⟶ I ⊗_O ℱ ⟶ ℱ' ⟶ ℱ ⟶ 0 of O'-modules (Deformation.ToposThickening.FlatLift.fixedActionExtension), and a sends the class of ℱ' to the class of 𝒢' exactly when the Ext¹_{O'} class of the extension of 𝒢' is that of ℱ' plus the image of a in Ext¹_{O'}(ℱ, I ⊗_O ℱ).

theorem exists_addTorsor_flatLiftClass_basePullbackIdeal
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    [HasExt.{e} (SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X'.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (hf' : f'.IsFlat) (hflat : IsFlatOverBase i f F) (hne : Nonempty (FlatLift i f' hi F)) :
    ∃ T : AddTorsor
        (Abelian.Ext.{e} F
          (((Stacks.SheafOfModules.Tensor.sheafTensor
            ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj
            (basePullbackIdealOverThickened i t f ht)) 1)
        (FlatLiftClass i f' hi F),
      ∀ (a : Abelian.Ext.{e} F
          (((Stacks.SheafOfModules.Tensor.sheafTensor
            ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj
            (basePullbackIdealOverThickened i t f ht)) 1)
        (A B : FlatLift i f' hi F),
        T.vadd a (Quotient.mk (flatLiftSetoid i f' hi F) A) =
            Quotient.mk (flatLiftSetoid i f' hi F) B ↔
          extensionClass F
              (((Stacks.SheafOfModules.Tensor.sheafTensor
                ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I)
              (B.fixedActionExtension i t f f' hi ht comm F
                ((isStrictPullbackIdealMap_iff_isStrict i t f f' hi ht comm).mpr hstrict)
                (isFlat_reducedBaseModule_of_isFlatOverBase i t f f' hi ht comm F hflat)) =
            (SheafOfModules.restrictScalars (structureRingMap i)).mapExtAddHom F
                (((Stacks.SheafOfModules.Tensor.sheafTensor
                  ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I) 1
                (a.comp (Abelian.Ext.mk₀
                  (basePullbackIdealTensorIso i t f f' hi ht comm hf' hstrict F).hom)
                  (add_zero 1)) +
              extensionClass F
                (((Stacks.SheafOfModules.Tensor.sheafTensor
                  ((pushforwardCommRingFunctor i.toToposHom).obj X.O)).flip.obj F).obj hi.I)
                (A.fixedActionExtension i t f f' hi ht comm F
                  ((isStrictPullbackIdealMap_iff_isStrict i t f f' hi ht comm).mpr hstrict)
                  (isFlat_reducedBaseModule_of_isFlatOverBase i t f f' hi ht comm F hflat))

Deformation.ToposThickening.autOverIdentityExtZeroEquiv_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatThickeningFlatLifts.lean, line 345.

Stacks 08VW, part (3). In Situation 08VV, given a lift ℱ' of ℱ to an O'-module flat over O_{ℬ'}, the set of automorphisms of ℱ' which pull back to the identity of ℱ is canonically isomorphic to Ext⁰_O(ℱ, f^*J ⊗_O ℱ) (with ℱ written as i^*ℱ'): the bijection Deformation.ToposThickening.autOverIdentityExtZeroEquiv sends α to 1 + α, and it carries addition to composition, so it is an isomorphism of groups.

theorem autOverIdentityExtZeroEquiv_spec
    (F : SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((pushforwardCommRingFunctor i.toToposHom).obj X.O)))
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))]
    (hstrict : (MorphismOfThickenings.ofFirstOrderThickenings i t f f' hi ht comm).IsStrict)
    (L : FlatLift i f' hi F) :
    (∀ α, (autOverIdentityExtZeroEquiv.{_, _, _, _, _, _, _, _, _, _, _, e} i t f f' hi ht comm F
        hstrict L α).val.hom =
      𝟙 L.module' + idealProductHomEquiv hi L.module' L.module'
          (Abelian.Ext.addEquiv₀ α ≫
            (idealProductTensorIso i t f f' hi ht comm L.module' hstrict L.isFlat).hom) ≫
        (idealProductSubmodule hi L.module').ι) ∧
    ∀ α β, autOverIdentityExtZeroEquiv i t f f' hi ht comm F hstrict L (α + β) =
      autOverIdentityExtZeroEquiv i t f f' hi ht comm F hstrict L α *
        autOverIdentityExtZeroEquiv i t f f' hi ht comm F hstrict L β

Tag 0CYD, a situation

Tag 0CYD in the Stacks Project.

Deformation.ToposThickening.FlatThickeningMorphismSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfFlatThickenings.lean, line 107. The attribute's comment: “the situation”.

Stacks 0CYD. Two strict flat morphisms of first order thickenings of one morphism of ringed topoi f : (Sh(C), O) ⟶ (Sh(B), O_B), related by a morphism of the thickenings they deform f by, together with an O-module flat over O_B.

structure FlatThickeningMorphismSituation
    (D₁ : MorphismOfThickenings X X₁ S S₁) (D₂ : MorphismOfThickenings X X₂ S S₂)

Tag 0CYE, a lemma

Tag 0CYE in the Stacks Project.

Deformation.ToposThickening.MorphismOfFirstOrderThickenings.existenceObstructionClass_first_tensorIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatObstructionCompatibility.lean, line 142. The attribute's comment: “coefficients and Ext map written through the ideals Iₖ, which are f^*Jₖ by 08MQ”.

Stacks 0CYE. In the situation of Stacks 0CYD the canonical map Ext²_O(ℱ, f^*J₂ ⊗_O ℱ) ⟶ Ext²_O(ℱ, f^*J₁ ⊗_O ℱ) carries the obstruction class o(ℱ, f^*J₂ ⊗_O ℱ, 1) of the second column to the obstruction class o(ℱ, f^*J₁ ⊗_O ℱ, 1) of the first.

The coefficient module of the k-th column is written Iₖ ⊗_O ℱ and the map on Ext² is the one induced by the map I₂ ⟶ I₁ of square-zero ideals of the upper row; under the hypotheses of Stacks 0CYD the comparison f^*Jₖ ⟶ Iₖ is an isomorphism, which is the reading under which Deformation.ToposThickening.hasFlatLift_iff_obstruction_eq_zero states Stacks 08VW. See the implementation notes.

This is Stacks 0CYC at Kₖ = Iₖ ⊗_O ℱ and cₖ = 1.

theorem existenceObstructionClass_first_tensorIdeal :
    existenceObstructionClass D.first F
        (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj D.first.I).obj F)
        (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj D.first.I).obj F)) =
      (existenceObstructionClass D.second F
          (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj D.second.I).obj F)
          (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).obj D.second.I).obj F))).comp
        (Abelian.Ext.mk₀
          (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).map D.idealMap).app F))
        (add_zero 2)

Tag 08VX, a situation

Tag 08VX in the Stacks Project.

Deformation.ToposThickening.ShortExactFlatThickeningSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ShortExactFlatThickenings.lean, line 176. The attribute's comment: “the situation”.

Stacks 08VX. A short exact sequence of first order thickenings of a ringed topos (Sh(C), O) mapping to a short exact sequence of first order thickenings of a ringed topos (Sh(B), O_B), by three strict flat deformations of one morphism f : (Sh(C), O) ⟶ (Sh(B), O\_B), together with an O'₂-module flat over O\_\{B'₂} and the canonical splitting of the upper row.

structure ShortExactFlatThickeningSituation
    (upper : FirstOrderThickeningSequence X X₁ X₂ X₃)
    (lower : FirstOrderThickeningSequence S S₁ S₂ S₃)

Deformation.ToposThickening.ShortExactFlatThickeningSituation.F, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ShortExactFlatThickenings.lean, line 243. The attribute's comment: “the module ℱ = ℱ'₂ ⊗ O”.

Stacks 08VX. The O-module ℱ = ℱ'₂ ⊗ O: the pullback of ℱ'₂ along the middle thickening of the upper row.

noncomputable def F (D : ShortExactFlatThickeningSituation upper lower) :
    SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)

Tag 08VY, a lemma

Tag 08VY in the Stacks Project.

Deformation.ToposThickening.FirstOrderThickeningComplex.boundary_underlyingExtensionClass_eq_obstruction_pushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatThickeningBoundaryPushout.lean, line 221. The attribute's comment: “the tag's own statement, at the two lifts the source names: the trivial extension of 08MI for π^ℱ and the 08MJ pushout of ℱ'₂ for h^ℱ'₂. UNCONDITIONAL on Stacks 08MQ: this declaration assumes none of 08MQ's consequences. All of them that it needs are proved and supplied -- IsIdealTensorShortExact by FirstOrderThickeningComplex.isIdealTensorShortExact, IsFlatOfFixedActionIdentity by isFlatOfFixedActionIdentity, IsFlatLiftCorrespondence by isFlatLiftCorrespondence, and IsIdealComparisonIsoOfFlat by isIdealComparisonIsoOfFlat. IsIdealTensorShortExact was FALSE as first stated -- refuted -- and is repaired with Situation 08VX's two horizontal squares, which its proof consumes twice each. The general form boundary_underlyingExtensionClass_eq_obstruction in FlatThickeningBoundary.lean still carries the binders, because the producer's module imports that file and discharging there would cycle; coefficients are written through the ideals Iₖ, which are f^*𝒥ₖ by 08MQ.”.

Stacks Project, Tag 08VY. In Situation 08VX the modules π^*ℱ and h^*ℱ'₂ are O'₁-modules flat over O_{ℬ'₁} restricting to ℱ on (Sh(C), O). Their difference (Stacks 08VW) is an element θ of Ext¹_O(ℱ, f^*𝒥₁ ⊗_O ℱ) whose boundary in Ext²_O(ℱ, f^*𝒥₃ ⊗_O ℱ) equals the obstruction (Stacks 08VW) to lifting ℱ to an O'₃-module flat over O_{ℬ'₃}.

This is Deformation.ToposThickening.FirstOrderThickeningComplex .boundary_underlyingExtensionClass_eq_obstruction' at the two lifts of the source: π^*ℱ is the trivial extension of Stacks 08MI attached to the canonical splitting π, and h^*ℱ'₂ is the extension S.coefficientExtensionOne that Stacks 08MJ produces from ℱ'₂, which receives from ℱ'₂ the canonical map S.coefficientComparisonMap satisfying the pushout identities. The seven clauses of the conclusion are, in order: the canonical action map of h^*ℱ'₂ and of π^*ℱ is the identity, so the kernel of each of h^*ℱ'₂ ⟶ ℱ and π^*ℱ ⟶ ℱ is I₁ ⊗_O ℱ = f^*𝒥₁ ⊗_O ℱ and each restricts to ℱ; each of π^*ℱ and h^*ℱ'₂ is flat over O_{ℬ'₁}; the class θ = ξ_{h^*ℱ'₂} is the difference of the two lifts under the bijection ℱ' ↦ ξ_{ℱ'} of Stacks 08MI; the obstruction class is, by Stacks 08VW for the third column, the obstruction to lifting ℱ to an O'₃-module flat over O_{ℬ'₃}; and the boundary of θ for the coefficient sequence equals that obstruction class.

See the implementation notes for the two readings inherited from the general form: the coefficient modules are written through the ideals Iₖ, which are f^*𝒥ₖ by Stacks 08MQ, and every consequence of Stacks 08MQ that the proof consumes is now supplied rather than assumed: this statement carries no stand-in hypothesis.

theorem boundary_underlyingExtensionClass_eq_obstruction_pushout
    [HasExt.{e} (SheafOfModules.{max v₂ u₂} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRing i)))]
    [HasExt.{e} (SheafOfModules.{max v₂ u₂} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))]
    [HasExt.{e} (SheafOfModules.{max v₂ u₂} (Stacks.SheafOfModules.Tensor.ringSheaf S.O₃))]
    (hS : S.IsComplex) (hT : T.IsComplex)
    (hTSE : (ShortComplex.mk T.idealMap₃₂ T.idealMap₂₁ hT).ShortExact)
    (π : Trivialization i)
    (hπ : S.upper.ringMapH ≫ S.lower.ringMapH =
      S.whole.ringMap₂ ≫ splittingRingHom i S.lower.first π)
    (hstrict₁ : (MorphismOfThickenings.ofFirstOrderThickenings i t f f₁
      S.lower.first T.lower.first commf₁).IsStrict)
    (hstrict₂ : (MorphismOfThickenings.ofFirstOrderThickenings
      (reshapeHom i S.lower.O₂ S.lower.fSharp₂) (reshapeHom t T.lower.O₂ T.lower.fSharp₂) f f₂
      S.lower.second T.lower.second commf₂).IsStrict)
    (hstrict₃ : (MorphismOfThickenings.ofFirstOrderThickenings S.thirdHom T.thirdHom f f₃
      S.third T.third commf₃).IsStrict)
    (hf₁ : f₁.IsFlat) (hf₂ : f₂.IsFlat) (hf₃ : f₃.IsFlat)
    (commh : f₂.comp S.lowerHorizontalHom = T.lowerHorizontalHom.comp f₁)
    (commh₃₂ : f₃.comp S.upperHorizontalHom = T.upperHorizontalHom.comp f₂)
    (hF : IsFlatOverBase i f F) :
    (extensionActionMap S.lower.first (S.coefficientExtensionOne F E₂ hE₂)).1 =
        𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
            S.lower.first.I) ∧
      (extensionActionMap S.lower.first (trivialExtension S.lower.first π F
          (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj S.lower.first.I)
          (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
              S.lower.first.I)))).1 =
        𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
            S.lower.first.I) ∧
      AlgebraicGeometry.SheafOfModules.IsFlat
          ((SheafOfModules.restrictScalars
            ((sheafCompose Y.J (forget₂ CommRingCat.{max v₂ u₂} RingCat.{max v₂ u₂})).map
              f₁.fSharpInverseImage)).obj
            (trivialExtension S.lower.first π F
              (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                  S.lower.first.I)
              (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                  S.lower.first.I))).Z.left) ∧
      AlgebraicGeometry.SheafOfModules.IsFlat
          ((SheafOfModules.restrictScalars
            ((sheafCompose Y.J (forget₂ CommRingCat.{max v₂ u₂} RingCat.{max v₂ u₂})).map
              f₁.fSharpInverseImage)).obj (S.coefficientExtensionOne F E₂ hE₂).Z.left) ∧
      underlyingExtensionClass.{e} i S.lower.first π F
            (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                S.lower.first.I)
            (S.coefficientExtensionOne F E₂ hE₂) =
          splitRestrictionExtHom.{e} S.lower.first π F
              (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                  S.lower.first.I)
              (extensionClass.{_, _, _, _, _, _, e} F
                (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                    S.lower.first.I)
                (S.coefficientExtensionOne F E₂ hE₂)) -
            splitRestrictionExtHom.{e} S.lower.first π F
              (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                  S.lower.first.I)
              (extensionClass.{_, _, _, _, _, _, e} F
                (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                    S.lower.first.I)
                (trivialExtension S.lower.first π F
                  (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                      S.lower.first.I)
                  (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                      S.lower.first.I)))) ∧
      (HasFlatLift S.thirdHom f₃ S.third F ↔
          existenceObstructionClass S.third F
              (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj S.third.I)
              (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                  S.third.I)) = 0) ∧
      (underlyingExtensionClass.{e} i S.lower.first π F
            (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
                S.lower.first.I)
            (S.coefficientExtensionOne F E₂ hE₂)).comp
          (S.isIdealTensorShortExact T hS f f₁ f₂ f₃ commf₁ commf₂ commf₃ F
            hT hTSE hF hstrict₁ hstrict₂ hstrict₃ hf₁ hf₂ hf₃ commh commh₃₂).extClass
          (by decide) =
        existenceObstructionClass S.third F
          (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj S.third.I)
          (𝟙 (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj F).obj
            S.third.I))

Deformation.ToposThickening.FlatThickeningComplexSituation.boundary_difference_trivialLift_pulledLift_eq_obstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatThickeningComplexBoundaryObstruction.lean, line 227.

Stacks Project, Tag 08VY. In Situation Stacks 08VX — a short exact sequence of first order thickenings O'₃ ⟶ O'₂ ⟶ O'₁ of (Sh(C), O) over a short exact sequence of first order thickenings of (Sh(B), O_ℬ), every (f, f'ₖ) strict and every f'ₖ flat, and an O'₂-module ℱ'₂ flat over O_{ℬ'₂}, with ℱ = ℱ'₂ ⊗ O — let π : (Sh(C'₁), O'₁) ⟶ (Sh(C), O) be the canonical splitting of Remark Stacks 08ML.

π^*ℱ and h^*ℱ'₂ are O'₁-modules flat over O_{ℬ'₁} (the first two conjuncts) restricting to ℱ on (Sh(C), O): they are the flat lifts trivialLift and pulledLift of ℱ across the first column (the third and fourth conjuncts record their modules), whose maps to i₁_*ℱ are the canonical identifications (the fifth and sixth conjuncts): for π^*ℱ = k^*ι_*ℱ, with π = ι^{-1} ∘ k the canonical splitting, the transpose under k^* ⊣ s^* of ι_*ℱ = s^*q^*ι_*ℱ; for h^*ℱ'₂, the transpose under h^* ⊣ h_* of the unit ℱ'₂ ⟶ i₂_*i₂^*ℱ'₂ = h_*i₁_*ℱ.

The maps f^*𝒥₃ ⟶ f^*𝒥₂ ⟶ f^*𝒥₁ of the coefficient sequence below, defined as the maps I₃ ⟶ I₂ ⟶ I₁ of the upper row read through the identifications f^*𝒥ₖ = Iₖ, are the maps induced by the maps 𝒥₃ ⟶ 𝒥₂ ⟶ 𝒥₁ of the lower row (the seventh and eighth conjuncts), as in Stacks 08VT.

The isomorphism classes of flat lifts of ℱ across the first column form a principal homogeneous set under Ext¹_O(ℱ, f^*𝒥₁ ⊗_O ℱ) with the action of Stacks 08VW (2) (Deformation.ToposThickening.exists_addTorsor_flatLiftClass_basePullbackIdeal), and the difference θ = [h^*ℱ'₂] - [π^*ℱ] has for boundary along 0 ⟶ f^*𝒥₃ ⊗_O ℱ ⟶ f^*𝒥₂ ⊗_O ℱ ⟶ f^*𝒥₁ ⊗_O ℱ ⟶ 0 (short exact by baseIdealTensor_shortExact) the class o(ℱ, f^*𝒥₃ ⊗_O ℱ, 1) of Stacks 08VW (1) for the third column, which vanishes exactly when ℱ lifts to an O'₃-module flat over O_{ℬ'₃} (the last conjunct).

theorem boundary_difference_trivialLift_pulledLift_eq_obstruction
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf (baseRing i)))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))]
    [HasExt.{e} (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf D.upper.O₃))] :
    AlgebraicGeometry.SheafOfModules.IsFlat
        ((SheafOfModules.restrictScalars
          ((sheafCompose Y.J (forget₂ CommRingCat.{w} RingCat.{w})).map
            D.f₁.fSharpInverseImage)).obj D.trivialModule) ∧
      AlgebraicGeometry.SheafOfModules.IsFlat
        ((SheafOfModules.restrictScalars
          ((sheafCompose Y.J (forget₂ CommRingCat.{w} RingCat.{w})).map
            D.f₁.fSharpInverseImage)).obj D.pulledModule) ∧
      D.trivialLift.module' = D.trivialModule ∧ D.pulledLift.module' = D.pulledModule ∧
      D.trivialLift.π = D.trivialModuleIsoPullback.hom ≫
        (D.splittingChangeAdjunction.homEquiv _ _).symm
          (splitRestrictionRestrictScalarsIso i D.upper.lower.first D.π D.F).inv ∧
      D.pulledLift.π = (D.adjH.homEquiv _ _).symm
        (D.i₂.pullbackAdjPushforwardModulesViaComparison.unit.app D.F' ≫
          (D.upper.lower.restrictHIso D.F).inv) ∧
      D.baseIdealMap₃₂ = D.inducedBaseIdealMap₃₂ ∧ D.baseIdealMap₂₁ = D.inducedBaseIdealMap₂₁ ∧
      ∃ T : AddTorsor
          (Abelian.Ext.{e} D.F
            (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj D.F).obj
              (basePullbackIdealOverThickened i t D.f D.lower.lower.first)) 1)
          (FlatLiftClass i D.f₁ D.upper.lower.first D.F),
        (∀ (a : Abelian.Ext.{e} D.F
            (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj D.F).obj
              (basePullbackIdealOverThickened i t D.f D.lower.lower.first)) 1)
          (A B : FlatLift i D.f₁ D.upper.lower.first D.F),
          T.vadd a (Quotient.mk (flatLiftSetoid i D.f₁ D.upper.lower.first D.F) A) =
              Quotient.mk (flatLiftSetoid i D.f₁ D.upper.lower.first D.F) B ↔
            extensionClass D.F
                (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj D.F).obj
                  D.upper.lower.first.I)
                (B.fixedActionExtension i t D.f D.f₁ D.upper.lower.first D.lower.lower.first
                  D.restrict₁ D.F D.isStrictPullbackIdealMap₁ D.isFlat_reducedBaseModule₁) =
              (SheafOfModules.restrictScalars (structureRingMap i)).mapExtAddHom D.F
                  (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj D.F).obj
                    D.upper.lower.first.I) 1
                  (a.comp (Abelian.Ext.mk₀
                    (basePullbackIdealTensorIso i t D.f D.f₁ D.upper.lower.first D.lower.lower.first
                      D.restrict₁ D.flat₁ D.strict₁ D.F).hom) (add_zero 1)) +
                extensionClass D.F
                  (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj D.F).obj
                    D.upper.lower.first.I)
                  (A.fixedActionExtension i t D.f D.f₁ D.upper.lower.first D.lower.lower.first
                    D.restrict₁ D.F D.isStrictPullbackIdealMap₁ D.isFlat_reducedBaseModule₁)) ∧
        (@VSub.vsub _ _ T.toVSub
            (Quotient.mk (flatLiftSetoid i D.f₁ D.upper.lower.first D.F) D.pulledLift)
            (Quotient.mk (flatLiftSetoid i D.f₁ D.upper.lower.first D.F) D.trivialLift)).comp
            D.baseIdealTensor_shortExact.extClass (by decide) =
          existenceObstructionClass D.upper.third D.F
            (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj D.F).obj
              (basePullbackIdealOverThickened D.upper.thirdHom D.lower.thirdHom D.f D.lower.third))
            (basePullbackIdealTensorIso D.upper.thirdHom D.lower.thirdHom D.f D.f₃ D.upper.third
              D.lower.third D.restrict₃ D.flat₃ D.strict₃ D.F).inv ∧
        (HasFlatLift D.upper.thirdHom D.f₃ D.upper.third D.F ↔
          existenceObstructionClass D.upper.third D.F
            (((Stacks.SheafOfModules.Tensor.sheafTensor (baseRing i)).flip.obj D.F).obj
              (basePullbackIdealOverThickened D.upper.thirdHom D.lower.thirdHom D.f D.lower.third))
            (basePullbackIdealTensorIso D.upper.thirdHom D.lower.thirdHom D.f D.f₃ D.upper.third
              D.lower.third D.restrict₃ D.flat₃ D.strict₃ D.F).inv = 0)

Sources

Section91.13 Deformations of ringed topoi and the naive cotangent complex #

Section 91.13 of the Stacks Project, Tag 08UE. 11 tags here are carried by 54 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08UF, an equation

Tag 08UF in the Stacks Project.

Deformation.ToposThickening.ArbitrarySiteExtensionProblem.CompatibleFirstOrderThickening, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/UniversalFirstOrder/ArbitrarySite.lean, line 167. The attribute's comment: “arbitrary equivalent sites”.

Stacks 08UF on arbitrary equivalent sites. A solution of the extension problem on a given thickened source ringed topos X'. The displayed diagram of sheaves is pulled back along the equivalence underlying i, and the invertible 2-morphism records the morphism of thickenings.

public structure CompatibleFirstOrderThickening
    (S : ArbitrarySiteExtensionProblem X B B')
    (X' : RingedTopos.{v''', u''', w'''})
    [X'.J.HasSheafCompose (forget RingCat.{w'''})]
    [X'.J.HasSheafCompose (forget₂ CommRingCat.{w'''} RingCat.{w'''})]

Declarations registered for the tag:

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/ToposThickening/UniversalFirstOrder/ArbitrarySite.lean, line 88 (StacksFrontier).

Tag 08UG, a lemma

Tag 08UG in the Stacks Project.

Deformation.ToposThickening.LiftDiagram.translate_existsUnique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingBetweenThickenings.lean, line 649. The attribute's comment: “clause (2): the lifts are a principal homogeneous space under Derivation”.

Stacks Project, Tag 08UG, clause (2). The morphisms (Sh(C'₂), O'₂) ⟶ (Sh(C'₁), O'₁) fitting into the source's diagram compatibly with ν form a principal homogeneous space: any one of them is carried to any other by exactly one derivation of the diagram. Together with translate_zero and translate_add this is the free and transitive action of the source's clause (2), with the acting group written as the group of section-wise derivations out of O'₁ rather than as Hom_{O₁}(Ω_{O₁/O_{B₁}}, g_*G₂).

public theorem translate_existsUnique (p q : Lift D) :
    ∃! δ : Derivation D.toSituation, translate p δ = q

Deformation.ToposThickening.FirstOrderLiftDiagram.derivationEquivDifferentialsHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingDerivationGroup.lean, line 510. The attribute's comment: “clause (2): the identification of the acting group of FirstOrderLiftDiagram.existsUnique_translateHom with the first group of the source's display, Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_* G_2). Nothing assumed”.

The derivations of the diagram, under which the lifts form a principal homogeneous space by Deformation.ToposThickening.FirstOrderLiftDiagram.existsUnique_translateHom, are the homomorphisms Hom_{𝒪₁}(Ω_{𝒪₁/𝒪_{ℬ₁}}, g_*𝒢₂).

public noncomputable def derivationEquivDifferentialsHom :
    Derivation D.toSituation ≃+ (frontDifferentials D ⟶ pushedIdeal D)

Deformation.ToposThickening.FirstOrderLiftDiagram.translateHom_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingDerivationGroup.lean, line 530. The attribute's comment: “clause (2): triviality of the action of 0 in the principal homogeneous space structure under Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_* G_2)”.

The zero homomorphism acts trivially on the lifts of the diagram.

public theorem translateHom_zero (p : D.Lift) : translateHom D p 0 = p

Deformation.ToposThickening.FirstOrderLiftDiagram.translateHom_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingDerivationGroup.lean, line 536. The attribute's comment: “clause (2): additivity of the action in the principal homogeneous space structure under Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_* G_2)”.

Translation of the lifts of the diagram is additive in the translating homomorphism.

public theorem translateHom_add (p : D.Lift) (a b : frontDifferentials D ⟶ pushedIdeal D) :
    translateHom D (translateHom D p a) b = translateHom D p (a + b)

Deformation.ToposThickening.FirstOrderLiftDiagram.existsUnique_translateHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingDerivationGroup.lean, line 547. The attribute's comment: “clause (2) in full, with nothing assumed: the morphisms fitting into the source's diagram compatibly with nu are a principal homogeneous space under the source's own acting group Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_* G_2), the underlying topoi identified as in the source's own reduction”.

The morphisms (Sh(𝒞'₂), 𝒪'₂) ⟶ (Sh(𝒞'₁), 𝒪'₁) fitting into the diagram compatibly with ν form a principal homogeneous space under Hom_{𝒪₁}(Ω_{𝒪₁/𝒪_{ℬ₁}}, g_*𝒢₂): any one of them is carried to any other by exactly one homomorphism.

public theorem existsUnique_translateHom (p q : D.Lift) :
    ∃! a : frontDifferentials D ⟶ pushedIdeal D, translateHom D p a = q

Deformation.ToposThickening.RingedToposLiftDiagram.obstructionClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/RingedToposLiftDiagramObstruction.lean, line 114. The attribute's comment: “clause (1) for genuine morphisms of ringed topoi between four arbitrary ringed topoi: the canonical class in Ext^1_{O_2}(Lg^NL_{O_1/O_{B_1}}, G_2), Lg^ the derived pullback of 06YY, is zero exactly when a morphism (Sh(C'_2), O'_2) -> (Sh(C'_1), O'_1) fitting into (08UH) compatibly with nu exists”.

Stacks Project, Tag 08UG, clause (1). For the diagram (08UH) of ringed topoi, whose horizontal arrows are first order thickenings, and a g⁻¹𝒪₁-linear map ν : g⁻¹𝒢₁ ⟶ 𝒢₂ making (08UI) commute with front and back rows solutions of (08UF), the canonical element obstructionClass D of Ext¹_{𝒪₂}(Lg^*NL_{𝒪₁/𝒪_{ℬ₁}}, 𝒢₂) vanishes if and only if there is a morphism of ringed topoi (Sh(𝒞'₂), 𝒪'₂) ⟶ (Sh(𝒞'₁), 𝒪'₁) fitting into (08UH) compatibly with ν.

theorem obstructionClass_eq_zero_iff :
    obstructionClass D = 0 ↔ Nonempty (CompatibleLift D)

Deformation.ToposThickening.RingedToposLiftDiagram.pullbackDifferentialsHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/RingedToposLiftDiagramTorsor.lean, line 120. The attribute's comment: “clause (2), the first equality of the display: Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_ G_2) = Hom_{O_2}(g^ Omega_{O_1/O_{B_1}}, G_2), as an additive equivalence, for genuine morphisms of ringed topoi”.

The first equality of the display of Stacks 08UG, clause (2): Hom_{𝒪₁}(Ω_{𝒪₁/𝒪_{ℬ₁}}, g_*𝒢₂) = Hom_{𝒪₂}(g^*Ω_{𝒪₁/𝒪_{ℬ₁}}, 𝒢₂), the adjunction g^* ⊣ g_* of sheaves of modules of Stacks 03D7.

def pullbackDifferentialsHomEquiv :
    (D.g.toRingedToposModulesHom.pullbackModules.obj (differentials₁ D) ⟶
      (show SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X₂.O) from D.S₂.G)) ≃+
      (differentials₁ D ⟶ pushedIdeal₁ D)

Deformation.ToposThickening.RingedToposLiftDiagram.extZeroEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/RingedToposLiftDiagramTorsor.lean, line 140. The attribute's comment: “clause (2), the second equality of the display: Ext^0_{O_2}(Lg^ NL_{O_1/O_{B_1}}, G_2) = Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_ G_2), as an additive equivalence, for genuine morphisms of ringed topoi”.

The second equality of the display of Stacks 08UG, clause (2): Hom_{𝒪₁}(Ω_{𝒪₁/𝒪_{ℬ₁}}, g_*𝒢₂) = Ext⁰_{𝒪₂}(Lg^*NL_{𝒪₁/𝒪_{ℬ₁}}, 𝒢₂), as an additive equivalence: Stacks 0GQ8 in degree 0, Ext⁰(NL, 𝒢) = Hom(Ω, 𝒢) on 𝒞₂, and the identification actingGroupEquiv. Lg^* is the derived pullback of Tag 06YY, at the model HasDerivedCategory.standard at which it is constructed.

def extZeroEquiv :
    @DerivedCategory.Ext _ _ _ (HasDerivedCategory.standard _)
      ((Stacks.Cohomology.DerivedPullbackOfToposHom.derivedPullback D.g).obj
        ((@DerivedCategory.Q _ _ _ (HasDerivedCategory.standard _)).obj
          (Stacks.SheafOfModules.naiveCotangentComplex.{u, u, u, u} X₁.J
            ((inverseImageCommRingFunctor D.S₁.f.toToposHom).obj B₁.O) X₁.O
            D.S₁.f.fSharpInverseImage)))
      ((@DerivedCategory.singleFunctor _ _ _ (HasDerivedCategory.standard _) 0).obj D.S₂.G) 0 ≃+
      (differentials₁ D ⟶ pushedIdeal₁ D)

Deformation.ToposThickening.RingedToposLiftDiagram.translate_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/RingedToposLiftDiagramTorsor.lean, line 163. The attribute's comment: “clause (2), for genuine morphisms of ringed topoi: triviality of the action of 0 in the principal homogeneous space structure under Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_* G_2)”.

Stacks Project, Tag 08UG, clause (2): the zero homomorphism acts trivially.

theorem translate_zero (p : CompatibleLift D) : translate D p 0 = p

Deformation.ToposThickening.RingedToposLiftDiagram.translate_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/RingedToposLiftDiagramTorsor.lean, line 170. The attribute's comment: “clause (2), for genuine morphisms of ringed topoi: additivity of the action in the principal homogeneous space structure under Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_* G_2)”.

Stacks Project, Tag 08UG, clause (2): the action is additive.

theorem translate_add (p : CompatibleLift D) (a b : differentials₁ D ⟶ pushedIdeal₁ D) :
    translate D (translate D p a) b = translate D p (a + b)

Deformation.ToposThickening.RingedToposLiftDiagram.existsUnique_translate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/RingedToposLiftDiagramTorsor.lean, line 182. The attribute's comment: “clause (2) for genuine morphisms of ringed topoi between four arbitrary ringed topoi: the morphisms fitting into (08UH) compatibly with nu are a principal homogeneous space under Hom_{O_1}(Omega_{O_1/O_{B_1}}, g_* G_2), with the action translate_zero, translate_add”.

Stacks Project, Tag 08UG, clause (2). If there is a morphism of ringed topoi (Sh(𝒞'₂), 𝒪'₂) ⟶ (Sh(𝒞'₁), 𝒪'₁) fitting into (08UH) compatibly with ν, the set of all such morphisms is a principal homogeneous space under Hom_{𝒪₁}(Ω_{𝒪₁/𝒪_{ℬ₁}}, g_*𝒢₂): any one of them is carried to any other by exactly one homomorphism.

theorem existsUnique_translate (p q : CompatibleLift D) :
    ∃! a : differentials₁ D ⟶ pushedIdeal₁ D, translate D p a = q

Tag 08UH, an equation

Tag 08UH in the Stacks Project.

Deformation.ToposThickening.LiftDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingBetweenThickenings.lean, line 269. The attribute's comment: “the displayed commutative diagram of morphisms of ringed topoi, with the underlying topoi identified as in the source's convention and its own reduction”.

Stacks Project, Tag 08UH and Tag 08UI. The displayed commutative diagram of morphisms of ringed topoi of [Stacks Project, Tag 08UG] together with its diagram of exact ideal rows: two layers, the comparison morphisms g, gB, gB' running from the index 1 layer to the index 2 layer (the direction of g^{-1} in the source, the underlying topoi being identified), and the comparison ν of the two ideal modules. The comparison of the two thickened sources is absent: producing it is the lifting problem of Tag 08UG.

public structure LiftDiagram

Deformation.ToposThickening.RingedToposLiftDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/RingedToposLiftDiagram.lean, line 260. The attribute's comment: “the commutative diagram of morphisms of ringed topoi, for genuine morphisms f₁, f₂, g, h between four arbitrary ringed topoi, each thickening presented on the site of its reduction as in the source's convention”.

The diagram of first order thickenings of ringed topoi and the diagram (08UI) of their ideals, for genuine morphisms of ringed topoi.

S₁, Q₁ are the front layer: the morphism f₁ : (Sh(𝒞₁), 𝒪₁) ⟶ (Sh(ℬ₁), 𝒪_{ℬ₁}), the first order thickening t₁ of the base, with f₁⁻¹𝒥₁, the ideal 𝒢₁ of i₁, and the front row of (08UI), which is a solution of (08UF) — the thickening 𝒪'₁ ⟶ 𝒪₁ with its ideal 𝒢₁ and the structure map f₁⁻¹𝒪_{ℬ'₁} ⟶ 𝒪'₁ of f'₁.

S₂, Q₂ are the back layer, the same data with index 2.

g : (Sh(𝒞₂), 𝒪₂) ⟶ (Sh(𝒞₁), 𝒪₁) and h : (Sh(ℬ₂), 𝒪_{ℬ₂}) ⟶ (Sh(ℬ₁), 𝒪_{ℬ₁}) are the two oblique arrows of the reduced part, with f₁ ∘ g = h ∘ f₂.

hB' is the oblique arrow h' : (Sh(ℬ'₂), 𝒪_{ℬ'₂}) ⟶ (Sh(ℬ'₁), 𝒪_{ℬ'₁}) of the thickened bases; the underlying topoi being identified it induces h on the topoi, and it is recorded by its comorphism h⁻¹𝒪_{ℬ'₁} ⟶ 𝒪_{ℬ'₂}. hB'_reduction is t₁ ∘ h = h' ∘ t₂.

nu is ν : g⁻¹𝒢₁ ⟶ 𝒢₂, linear over g⁻¹𝒪₁, and nu_base the commutativity of the left square of (08UI); see the module docstring.

The faces f'ⱼ ∘ iⱼ = tⱼ ∘ fⱼ of (08UH) are part of the solutions Qⱼ.

structure RingedToposLiftDiagram

Tag 08UI, an equation

Tag 08UI in the Stacks Project.

Deformation.ToposThickening.LiftDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingBetweenThickenings.lean, line 269. The attribute's comment: “the displayed diagram of exact ideal rows: the two exact rows of each layer are the ideal sequences of its two first order thickenings, and the comparison ν of the two upper ideals is nu, compatible by nu_base with the two maps from the base ideals”.

Stacks Project, Tag 08UH and Tag 08UI. The displayed commutative diagram of morphisms of ringed topoi of [Stacks Project, Tag 08UG] together with its diagram of exact ideal rows: two layers, the comparison morphisms g, gB, gB' running from the index 1 layer to the index 2 layer (the direction of g^{-1} in the source, the underlying topoi being identified), and the comparison ν of the two ideal modules. The comparison of the two thickened sources is absent: producing it is the lifting problem of Tag 08UG.

public structure LiftDiagram

Tag 08UJ, a lemma

Tag 08UJ in the Stacks Project.

Stacks.SheafOfModules.exists_presentation_conormalExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangentExtClass.lean, line 899.

Let A ⟶ B be a homomorphism of sheaves of rings on a site, let G be a B-module and let ξ be a first Ext class of the naive cotangent complex NL_{B/A} with values in G. Then there is a map of sheaves of sets α : E ⟶ B presenting B over A for which ξ, viewed in Ext¹_B(NL(α), G) along the canonical comparison map, is the class of a homomorphism I/I² ⟶ G out of the conormal sheaf of the presentation.

theorem exists_presentation_conormalExtClass
    (ξ : DerivedCategory.Ext (DerivedCategory.Q.obj
        (naiveCotangentComplex.{v, u, max w u v, w} J A B a))
      ((DerivedCategory.singleFunctor _ 0).obj G) 1) :
    ∃ (E : Sheaf J (Type (max w u v))) (α : E.obj ⟶ underlyingPresheaf J B)
      (hsurj : Presheaf.IsLocallySurjective J (presentation J A B a E.obj α).hom),
      letI : Presheaf.IsLocallySurjective J (presentation J A B a E.obj α).hom := hsurj
      ∃ f : (presentationConormalSequence.{v, u, max w u v, w} J A B a E.obj α).X₁ ⟶ G,
        DerivedCategory.Q.map
            (naiveCotangentComplexComparison.{v, u, max w u v, w} J A B a E.obj α) ≫ ξ =
          presentationConormalExtClass.{v, u, w, t} J A B a E.obj α G f

Tag 08UK, a lemma

Tag 08UK in the Stacks Project.

Deformation.ToposThickening.RingedToposExtensionProblem.exists_addTorsor_isomorphismClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionClassesNaiveExtTorsor.lean, line 91.

Stacks Project, Tag 08UK. For the square-zero extension problem of [Stacks 08UF] — a first order thickening of (Sh(ℬ), 𝒪_ℬ) with ideal 𝒥, a morphism of ringed topoi f : (Sh(𝒞), 𝒪) ⟶ (Sh(ℬ), 𝒪_ℬ), an 𝒪-module 𝒢 and c : f⁻¹𝒥 ⟶ 𝒢 — if a solution exists, then the set of isomorphism classes of solutions is principal homogeneous under Ext¹_𝒪(NL_{𝒪/𝒪_ℬ}, 𝒢).

The structure is the source's: ξ carries the class of a solution 𝒪' to the class of the pushout solution 𝒪'_ξ of the proof, and it carries the class of 𝒪'₁ to the class of 𝒪'₂ exactly when the obstruction class o(𝒪'₁, 𝒪'₂) of [Stacks 08UG] is ξ.

theorem exists_addTorsor_isomorphismClasses (S : RingedToposExtensionProblem X B)
    (hne : Nonempty S.CompatibleFirstOrderThickening) :
    ∃ T : AddTorsor
        (Stacks.SheafOfModules.naiveCotangentExt.{u, u, u, u, t} X.J
          ((inverseImageCommRingFunctor S.f.toToposHom).obj B.O) X.O S.f.fSharpInverseImage S.G 1)
        (IsomorphismClasses S),
      (∀ (ξ : Stacks.SheafOfModules.naiveCotangentExt.{u, u, u, u, t} X.J
          ((inverseImageCommRingFunctor S.f.toToposHom).obj B.O) X.O S.f.fSharpInverseImage S.G 1)
          (P Q : S.CompatibleFirstOrderThickening),
        T.vadd ξ (Quotient.mk (isomorphicSetoid S) P) = Quotient.mk (isomorphicSetoid S) Q ↔
          pairObstruction P Q = ξ) ∧
      ∀ (ξ : Stacks.SheafOfModules.naiveCotangentExt.{u, u, u, u, t} X.J
          ((inverseImageCommRingFunctor S.f.toToposHom).obj B.O) X.O S.f.fSharpInverseImage S.G 1)
          (P : S.CompatibleFirstOrderThickening),
        T.vadd ξ (Quotient.mk (isomorphicSetoid S) P) =
          Quotient.mk (isomorphicSetoid S) (P.twist ξ)

Deformation.ToposThickening.RingedToposExtensionProblem.isomorphic_iff_nonempty_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionIsomorphism.lean, line 336. The attribute's comment: “the half asserting that the obstruction class of Stacks 08UG separates the isomorphism classes of solutions, namely that a morphism of solutions of the extension problem of Stacks 08UF is automatically an isomorphism; not the torsor half, which needs the pair-dependent presentation of the source's last paragraph and its omitted calculation”.

Stacks Project, Tag 08UK, the half asserting that the obstruction class separates the isomorphism classes of solutions. Two solutions of the square-zero extension problem of [Stacks Project, Tag 08UF] are isomorphic exactly when there is a morphism of solutions between them: by CompatibleFirstOrderThickening.Hom.isIso every morphism of solutions is already invertible.

This is the source's "clearly, this element is the obstruction to the existence of an isomorphism, hence separates the isomorphism classes" — the obstruction class of [Stacks Project, Tag 08UG], which obstructs a morphism O'₁ ⟶ O'₂ fitting into the diagram (Deformation.ToposThickening.LiftDiagram.liftingObstruction_eq_zero_iff), thereby obstructs an isomorphism of solutions.

The other half of the tag — that the isomorphism classes form a principal homogeneous space under Ext¹_O(NL_{O/O_B}, G) — is not claimed here; see the implementation notes of this file.

public theorem isomorphic_iff_nonempty_hom (P Q : S.CompatibleFirstOrderThickening) :
    CompatibleFirstOrderThickening.Isomorphic P Q ↔
      Nonempty (CompatibleFirstOrderThickening.Hom P Q)

Deformation.ToposThickening.RingedToposExtensionProblem.isomorphismClasses_mk_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionIsomorphism.lean, line 354. The attribute's comment: “the half asserting that the obstruction class of Stacks 08UG separates the isomorphism classes, stated for the quotient IsomorphismClasses itself: two solutions have the same isomorphism class exactly when a morphism of solutions joins them; not the torsor half”.

Stacks Project, Tag 08UK, the half asserting that the obstruction class separates the isomorphism classes, stated for the set of isomorphism classes itself. Two solutions of the square-zero extension problem of [Stacks Project, Tag 08UF] have the same class in CompatibleFirstOrderThickening.IsomorphismClasses S exactly when there is a morphism of solutions between them, so the obstruction class of [Stacks Project, Tag 08UG] — which obstructs such a morphism — is a complete invariant of the isomorphism class.

That these classes are moreover principal homogeneous under Ext¹_O(NL_{O/O_B}, G) is not claimed; see the implementation notes of this file.

public theorem isomorphismClasses_mk_eq_iff (P Q : S.CompatibleFirstOrderThickening) :
    (Quotient.mk (CompatibleFirstOrderThickening.isomorphicSetoid S) P :
        CompatibleFirstOrderThickening.IsomorphismClasses S) =
      Quotient.mk (CompatibleFirstOrderThickening.isomorphicSetoid S) Q ↔
      Nonempty (CompatibleFirstOrderThickening.Hom P Q)

Deformation.ToposThickening.LiftDiagram.liftingObstruction_eq_zero_iff_exists_isIso_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionIsomorphism.lean, line 463. The attribute's comment: “the half asserting that the obstruction class of Stacks 08UG separates the isomorphism classes, stated in the vocabulary of the diagram of that tag: when the two comparison maps of the diagram are bijective on sections the class vanishes exactly when an isomorphism fits into the diagram; the hypotheses carried are those of Stacks 08UG itself, and the torsor half of 08UK is not claimed”.

Stacks Project, Tag 08UK, the half asserting that the obstruction class separates the isomorphism classes, in the vocabulary of the diagram of [Stacks Project, Tag 08UG]. When the two comparison maps of the diagram are bijective on sections — as they are for two solutions of one square-zero extension problem, where both are identities — the class of Step 1 of the proof of Tag 08UG vanishes if and only if there is an isomorphism O'₁ ≅ O'₂ fitting into the diagram, and not merely a morphism.

This is the source's "clearly, this element is the obstruction to the existence of an isomorphism, hence separates the isomorphism classes", combined with the vanishing criterion Deformation.ToposThickening.LiftDiagram.liftingObstruction_eq_zero_iff of Tag 08UG, whose hypotheses P and ξ are inherited verbatim. That criterion is stated for the factorizations of ξ through the degree 0 term and assumes nothing; the bijection e of Steps 1 to 3 of the source's proof, which identifies those factorizations with the lifts of the diagram, is carried here.

public theorem liftingObstruction_eq_zero_iff_exists_isIso_lift (D : LiftDiagram J)
    {single : M ⥤ T} [single.Full] [single.Faithful] [single.Additive]
    (hg : ∀ U : Cᵒᵖ, Function.Bijective (D.g.hom.app U))
    (hgs : Presheaf.IsLocallySurjective J D.g.hom)
    (hnu : ∀ U : Cᵒᵖ, Function.Bijective (D.nuSection (U := U)))
    (P : NaiveCotangentTwoTerm single) (G : M) (ξ : P.conormal ⟶ G)
    (e : D.Lift ≃ {θ : P.base ⟶ G // P.d ≫ θ = ξ}) :
    liftingObstruction P G ξ = 0 ↔ ∃ p : D.Lift, IsIso p.hom

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.naiveIsomorphismClassesAddTorsor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionIsomorphismClassesExt.lean, line 86. The attribute's comment: “the half asserting that, if a solution exists, the set of isomorphism classes of solutions is principal homogeneous under Ext¹(NL_f, G); the element separating two classes is their obstruction class”.

Stacks 08UK, the torsor half: if the square-zero extension problem has a solution, the isomorphism classes of solutions are a principal homogeneous space under Ext¹_O(NL_f, G).

noncomputable def naiveIsomorphismClassesAddTorsor [Nonempty S.CompatibleFirstOrderThickening] :
    AddTorsor (S.f.naiveCotangentExt (targetG S) 1) (IsomorphismClasses S)

Tag 0GQ5, a lemma

Tag 0GQ5 in the Stacks Project.

Deformation.ToposThickening.RingedToposExtensionProblem.classesEquivExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroExtensionClasses.lean, line 152. The attribute's comment: “the bijection between isomorphism classes of square-zero extensions of 𝒪 by 𝒢 as f⁻¹𝒪_ℬ-algebras and Ext¹ of a FIXED presentation α, carrying the four inputs of SolutionObstruction (xi, hxi, rep, pushout) and the lift bijection e of 08UG; identifying Ext¹(NL(α), 𝒢) with Ext¹(NL_{𝒪/𝒪_ℬ}, 𝒢) is 08TY and 08TL, absent on a general site”.

The isomorphism classes of square-zero extensions 0 ⟶ 𝒢 ⟶ 𝒪' ⟶ 𝒪 ⟶ 0 of f⁻¹𝒪_ℬ-algebras — equivalently, of first order thickenings over the base with an 𝒪-module isomorphism 𝒢 ≅ Ker(i^♯), i.e. of solutions of the problem of [Stacks 08UF] whose base reduction is invertible — are in bijection with Ext¹(NL(α), 𝒢).

The bijection is the torsor of [Stacks 08UK] evaluated at the base point supplied by the trivial extension 𝒪 ⋉ 𝒢: a class q goes to the obstruction class separating it from the class of 𝒪 ⋉ 𝒢, and a class ξ of Ext¹ goes to the class of the solution obtained from 𝒪 ⋉ 𝒢 by twisting with ξ. The five inputs — the four of AlgebraicGeometry.RingedSpaceThickening.SolutionObstruction and the lift bijection e of [Stacks 08UG] — remain hypotheses; see the implementation notes of this file.

def classesEquivExt (h : IsIso S.baseReduction) (P : NaiveCotangentTwoTerm single)
    (xi : S.CompatibleFirstOrderThickening → S.CompatibleFirstOrderThickening →
      (P.conormal ⟶ S.G))
    (hxi : ∀ Q₁ Q₂ Q₃ : S.CompatibleFirstOrderThickening,
      xi Q₁ Q₂ + xi Q₂ Q₃ = xi Q₁ Q₃)
    (rep : ∀ ξ : P.obj ⟶ (single.obj S.G)⟦(1 : ℤ)⟧,
      { δ : P.conormal ⟶ S.G // liftingObstruction P S.G δ = ξ })
    (pushout : ∀ (Q : S.CompatibleFirstOrderThickening) (δ : P.conormal ⟶ S.G),
      { Q' : S.CompatibleFirstOrderThickening // xi Q Q' = δ })
    (e : ∀ Q₁ Q₂ : S.CompatibleFirstOrderThickening,
      CompatibleFirstOrderThickening.Hom Q₁ Q₂ ≃
        { θ : P.base ⟶ S.G // P.d ≫ θ = xi Q₁ Q₂ }) :
    CompatibleFirstOrderThickening.IsomorphismClasses S ≃
      (P.obj ⟶ (single.obj S.G)⟦(1 : ℤ)⟧)

Deformation.ToposThickening.RingedToposExtensionProblem.classesEquivExt_trivialSolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroExtensionClasses.lean, line 175. The attribute's comment: “that the bijection is canonical: the class of the trivial extension 𝒪 ⋉ 𝒢 goes to 0; the hypotheses carried are those of the bijection itself”.

The bijection classesEquivExt is the canonical one. It carries the isomorphism class of the trivial square-zero extension 𝒪 ⋉ 𝒢 to 0.

theorem classesEquivExt_trivialSolution (h : IsIso S.baseReduction)
    (P : NaiveCotangentTwoTerm single)
    (xi : S.CompatibleFirstOrderThickening → S.CompatibleFirstOrderThickening →
      (P.conormal ⟶ S.G))
    (hxi : ∀ Q₁ Q₂ Q₃ : S.CompatibleFirstOrderThickening,
      xi Q₁ Q₂ + xi Q₂ Q₃ = xi Q₁ Q₃)
    (rep : ∀ ξ : P.obj ⟶ (single.obj S.G)⟦(1 : ℤ)⟧,
      { δ : P.conormal ⟶ S.G // liftingObstruction P S.G δ = ξ })
    (pushout : ∀ (Q : S.CompatibleFirstOrderThickening) (δ : P.conormal ⟶ S.G),
      { Q' : S.CompatibleFirstOrderThickening // xi Q Q' = δ })
    (e : ∀ Q₁ Q₂ : S.CompatibleFirstOrderThickening,
      CompatibleFirstOrderThickening.Hom Q₁ Q₂ ≃
        { θ : P.base ⟶ S.G // P.d ≫ θ = xi Q₁ Q₂ }) :
    S.classesEquivExt h P xi hxi rep pushout e
        (Quotient.mk (CompatibleFirstOrderThickening.isomorphicSetoid S)
          (S.trivialSolution h)) = 0

Deformation.ToposThickening.RingedToposExtensionProblem.squareZeroExtensionClassesEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroExtensionNaiveExt.lean, line 230.

Stacks Project, Tag 0GQ5. Let f : (Sh(𝒞), 𝒪) ⟶ (Sh(ℬ), 𝒪_ℬ) be a morphism of ringed topoi and 𝒢 an 𝒪-module. The set of isomorphism classes of extensions of f⁻¹𝒪_ℬ-algebras 0 ⟶ 𝒢 ⟶ 𝒪' ⟶ 𝒪 ⟶ 0 with 𝒢 an ideal of square zero — the solutions of the problem ofTrivialBase f 𝒢 — is canonically bijective to Ext¹_𝒪(NL_{𝒪/𝒪_ℬ}, 𝒢).

The bijection is the one of the source's proof: the torsor of [Stacks 08UK] under Ext¹_𝒪(NL_{𝒪/𝒪_ℬ}, 𝒢) with base point the trivial extension 𝒪 ⊕ 𝒢. The class of 𝒪' goes to the obstruction class o(𝒪 ⊕ 𝒢, 𝒪') (squareZeroExtensionClassesEquiv_mk), and ξ goes to the class of the pushout extension (𝒪 ⊕ 𝒢)_ξ (squareZeroExtensionClassesEquiv_symm_apply).

def squareZeroExtensionClassesEquiv :
    CompatibleFirstOrderThickening.IsomorphismClasses (ofTrivialBase f G) ≃
      Stacks.SheafOfModules.naiveCotangentExt.{u, u, u, u, t} X.J
        ((inverseImageCommRingFunctor f.toToposHom).obj B.O) X.O f.fSharpInverseImage G 1

Deformation.ToposThickening.RingedToposExtensionProblem.squareZeroExtensionClassesEquiv_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroExtensionNaiveExt.lean, line 241.

The bijection of [Stacks 0GQ5] is the canonical one: it sends the isomorphism class of an extension 𝒪' to the obstruction class o(𝒪 ⊕ 𝒢, 𝒪') of [Stacks 08UG] separating it from the trivial extension, that is the element of Ext¹_𝒪(NL_{𝒪/𝒪_ℬ}, 𝒢) carrying the class of 𝒪 ⊕ 𝒢 to that of 𝒪' in the torsor of [Stacks 08UK].

theorem squareZeroExtensionClassesEquiv_mk
    (Q : (ofTrivialBase f G).CompatibleFirstOrderThickening) :
    squareZeroExtensionClassesEquiv f G
        (Quotient.mk (CompatibleFirstOrderThickening.isomorphicSetoid _) Q) =
      CompatibleFirstOrderThickening.pairObstruction
        ((ofTrivialBase f G).trivialSolution (IsIso.id B.O)) Q

Deformation.ToposThickening.RingedToposExtensionProblem.trivialSolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/TrivialSquareZeroSolution.lean, line 259. The attribute's comment: “the existence of a solution: the trivial extension 𝒪 ⋉ 𝒢; not the bijection with Ext¹, which needs the torsor statement of 08UK”. References: EGA 0 (18.2.3), “partial”.

The trivial square-zero extension is a solution of the square-zero extension problem of [Stacks 08UF] whose base reduction is invertible: 𝒪' = 𝒪 ⋉ 𝒢, with the projection as reduction, the inclusion m ↦ (0, m) as the identification of 𝒢 with the kernel, and the zero section composed with the structure map of f as the map from the inverse image of the thickened base.

This is the existence of a solution in the proof of [Stacks 0GQ5] — the source's "a solution exists, take 𝒢 ⊕ 𝒪". It is not the bijection with Ext¹, which needs the torsor statement of [Stacks 08UK]; see StacksFrontier/Deformation/ToposThickening/SquareZeroExtensionClasses.lean.

def trivialSolution (h : IsIso S.baseReduction) : S.CompatibleFirstOrderThickening

Deformation.ToposThickening.RingedToposExtensionProblem.nonempty_compatibleFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/TrivialSquareZeroSolution.lean, line 285. The attribute's comment: “the existence of a solution, as the base point the torsor of 08UK needs; not the bijection with Ext¹”.

A square-zero extension problem of ringed topoi whose bottom row is 0 ⟶ 0 ⟶ f⁻¹𝒪_B ⟶ f⁻¹𝒪_B ⟶ 0 has a solution, namely the trivial extension 𝒪 ⋉ 𝒢. This is the base point the torsor statement of [Stacks 08UK] needs in order to turn into the bijection of [Stacks 0GQ5].

theorem nonempty_compatibleFirstOrderThickening (h : IsIso S.baseReduction) :
    Nonempty S.CompatibleFirstOrderThickening

Tag 0GQ6, a remark

Tag 0GQ6 in the Stacks Project.

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.lift_comp_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentation.lean, line 253. The attribute's comment: “the commutative diagram over 𝒪' ⟶ 𝒪 for ℰ underlying 𝒪' with α' the identity”.

Stacks Project, Tag 0GQ6, the commutative diagram: α' followed by the reduction 𝒪' ⟶ 𝒪 is the presentation attached to α.

theorem lift_comp_reduction (base : inverseImageBaseRing S ⟶ P.extension)
    (hbase : base ≫ P.reduction = S.f.fSharpInverseImage) :
    P.lift base ≫ P.reduction = P.presentation

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.presentation_isLocallySurjective, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentation.lean, line 278. The attribute's comment: “surjectivity of f⁻¹𝒪_ℬ[ℰ] ⟶ 𝒪, which is what makes NL(α) defined”.

Stacks Project, Tag 0GQ6, surjectivity of f⁻¹𝒪_ℬ[ℰ] ⟶ 𝒪: the variables of the free algebra are all the local sections of 𝒪', and they already cover 𝒪 because the reduction does.

instance presentation_isLocallySurjective :
    Presheaf.IsLocallySurjective X.J P.presentation.hom

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.exists_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentation.lean, line 294. The attribute's comment: “the choice of ℰ with α' : ℰ ⟶ 𝒪' and α : ℰ ⟶ 𝒪 making f⁻¹𝒪_ℬ[ℰ] ⟶ 𝒪 surjective”.

Stacks Project, Tag 0GQ6, the choice the source makes is possible: there are a sheaf of sets ℰ and maps α' : ℰ ⟶ 𝒪', α : ℰ ⟶ 𝒪 forming a commutative triangle over the reduction 𝒪' ⟶ 𝒪 for which f⁻¹𝒪_ℬ[ℰ] ⟶ 𝒪 is surjective. The witness is the source's own: ℰ is the sheaf of sets underlying 𝒪' and α' is the identity.

theorem exists_generators :
    ∃ (E : Functor X.Cᵒᵖ (Type u)) (α' : E ⟶ underlyingPresheaf X.J P.extension)
      (α : E ⟶ underlyingPresheaf X.J X.O),
      α' ≫ Functor.whiskerRight P.reduction.hom (forget CommRingCat.{u}) = α ∧
        Presheaf.IsLocallySurjective X.J
          (Stacks.SheafOfModules.presentation X.J (inverseImageBaseRing S) X.O
            S.f.fSharpInverseImage E α).hom

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.conormalToIdeal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentation.lean, line 360. The attribute's comment: “the map 𝒥/𝒥² ⟶ 𝒢 determined by α'”.

Stacks Project, Tag 0GQ6, the map 𝒥/𝒥² ⟶ 𝒢 determined by α'.

abbrev conormalToIdeal (base : inverseImageBaseRing S ⟶ P.extension)
    (hbase : base ≫ P.reduction = S.f.fSharpInverseImage) :
    conormalSheaf.{u, u, u, u} X.J
        (freeAlgebraSheaf X.J (inverseImageBaseRing S) P.generators) X.O P.presentation ⟶
      S.G

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.extClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentation.lean, line 403. The attribute's comment: “the class in Ext¹_𝒪(NL(α), 𝒢) that α' determines through the map 𝒥/𝒥² ⟶ 𝒢”.

Stacks Project, Tag 0GQ6, the class in Ext¹_𝒪(NL(α), 𝒢) that α' determines: the first Ext class of the map 𝒥/𝒥² ⟶ 𝒢.

def extClass (base : inverseImageBaseRing S ⟶ P.extension)
    (hbase : base ≫ P.reduction = S.f.fSharpInverseImage) :
    DerivedCategory.Ext (DerivedCategory.Q.obj P.naiveCotangentComplex)
      ((DerivedCategory.singleFunctor _ 0).obj S.G) 1

Deformation.ToposThickening.RingedToposExtensionProblem.isLocallySurjective_presentation_of_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentationRemark.lean, line 287.

For any sheaf of sets ℰ with a surjection α' : ℰ ⟶ 𝒪', the presentation f⁻¹𝒪_ℬ[ℰ] ⟶ 𝒪 of α = α' followed by the reduction is surjective.

theorem isLocallySurjective_presentation_of_isLocallySurjective
    (Q : (ofTrivialBase f G).CompatibleFirstOrderThickening) (E : Functor X.Cᵒᵖ (Type u))
    (α' : E ⟶ underlyingPresheaf X.J Q.extension) [Presheaf.IsLocallySurjective X.J α'] :
    Presheaf.IsLocallySurjective X.J (Stacks.SheafOfModules.presentation X.J
      ((inverseImageCommRingFunctor f.toToposHom).obj B.O) X.O f.fSharpInverseImage E
        (α' ≫ Functor.whiskerRight Q.reduction.hom (forget CommRingCat.{u}))).hom

Deformation.ToposThickening.RingedToposExtensionProblem.exists_generators_ofTrivialBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentationRemark.lean, line 308.

For every extension 0 ⟶ 𝒢 ⟶ 𝒪' ⟶ 𝒪 ⟶ 0 of f⁻¹𝒪_ℬ-algebras there are a sheaf of sets ℰ and maps α' : ℰ ⟶ 𝒪', α : ℰ ⟶ 𝒪 forming a commutative triangle over 𝒪' ⟶ 𝒪 for which f⁻¹𝒪_ℬ[ℰ] ⟶ 𝒪 is surjective; for instance ℰ the sheaf of sets underlying 𝒪' and α' the identity.

theorem exists_generators_ofTrivialBase
    (Q : (ofTrivialBase f G).CompatibleFirstOrderThickening) :
    ∃ (E : Functor X.Cᵒᵖ (Type u)) (α' : E ⟶ underlyingPresheaf X.J Q.extension)
      (α : E ⟶ underlyingPresheaf X.J X.O),
      α' ≫ Functor.whiskerRight Q.reduction.hom (forget CommRingCat.{u}) = α ∧
        Presheaf.IsLocallySurjective X.J (Stacks.SheafOfModules.presentation X.J
          ((inverseImageCommRingFunctor f.toToposHom).obj B.O) X.O f.fSharpInverseImage E α).hom

Deformation.ToposThickening.RingedToposExtensionProblem.squareZeroExtensionClassesEquiv_mk_eq_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ExtensionPresentationRemark.lean, line 378.

Let f : (Sh(𝒞), 𝒪) ⟶ (Sh(ℬ), 𝒪_ℬ) be a morphism of ringed topoi, 𝒢 an 𝒪-module and 0 ⟶ 𝒢 ⟶ 𝒪' ⟶ 𝒪 ⟶ 0 an extension of f⁻¹𝒪_ℬ-algebras with 𝒢 an ideal of square zero. Let ℰ be a sheaf of sets with a commutative diagram α' : ℰ ⟶ 𝒪', α : ℰ ⟶ 𝒪 over 𝒪' ⟶ 𝒪 such that f⁻¹𝒪_ℬ[ℰ] ⟶ 𝒪 is surjective with kernel 𝒥. The map 𝒥/𝒥² ⟶ 𝒢 determined by α' has a class in Ext¹_𝒪(NL(α), 𝒢); transported along the isomorphism NL(α) ≅ NL_{𝒪/𝒪_ℬ} of [Stacks 08TY], it is the element of Ext¹_𝒪(NL_{𝒪/𝒪_ℬ}, 𝒢) corresponding to 𝒪' under the bijection of [Stacks 0GQ5].

theorem squareZeroExtensionClassesEquiv_mk_eq_generators
    [HasDerivedCategory.{t} (Sheaf.targetModules.{u, u, u} X.J X.O)] :
    inv (DerivedCategory.Q.map
        (Stacks.SheafOfModules.naiveCotangentComplexComparison.{u, u, u, u} X.J
          ((inverseImageCommRingFunctor f.toToposHom).obj B.O) X.O f.fSharpInverseImage E α)) ≫
      Stacks.SheafOfModules.presentationConormalExtClass.{u, u, u, t} X.J
        ((inverseImageCommRingFunctor f.toToposHom).obj B.O) X.O f.fSharpInverseImage E α G
        (Q.generatorsConormalToIdeal (A := (inverseImageCommRingFunctor f.toToposHom).obj B.O)
          (a := f.fSharpInverseImage) (base := Q.baseMap) hα
        (baseMap_comp_reduction_ofTrivialBase Q)) =
      squareZeroExtensionClassesEquiv f G
        (Quotient.mk (CompatibleFirstOrderThickening.isomorphicSetoid _) Q)

Tag 0GQ7, a lemma

Tag 0GQ7 in the Stacks Project.

Deformation.ToposThickening.LiftingMorphismDerived.nonempty_compatibleMorphism_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingMorphismDerivedCriterion.lean, line 738.

Let f : (Sh(𝒞), 𝒪_𝒞) ⟶ (Sh(ℬ), 𝒪_ℬ) and g : (Sh(𝒟), 𝒪_𝒟) ⟶ (Sh(𝒞), 𝒪_𝒞) be morphisms of ringed topoi, ℱ an 𝒪_𝒞-module, 𝒢 an 𝒪_𝒟-module and c : g^*ℱ ⟶ 𝒢 an 𝒪_𝒟-linear map. Let 0 ⟶ ℱ ⟶ 𝒪_{𝒞'} ⟶ 𝒪_𝒞 ⟶ 0 be an extension of f⁻¹𝒪_ℬ-algebras (a solution QC of the problem of Stacks 0GQ5 for f and ℱ) corresponding to ξ ∈ Ext¹_{𝒪_𝒞}(NL_{𝒪_𝒞/𝒪_ℬ}, ℱ), and 0 ⟶ 𝒢 ⟶ 𝒪_{𝒟'} ⟶ 𝒪_𝒟 ⟶ 0 an extension of g⁻¹f⁻¹𝒪_ℬ-algebras (a solution QD of the problem for f ∘ g and 𝒢) corresponding to ζ ∈ Ext¹_{𝒪_𝒟}(NL_{𝒪_𝒟/𝒪_ℬ}, 𝒢), the classes being those of Stacks 0GQ5. Then there is a morphism g' : (Sh(𝒟), 𝒪_{𝒟'}) ⟶ (Sh(𝒞), 𝒪_{𝒞'}) of ringed topoi over (Sh(ℬ), 𝒪_ℬ) compatible with g and c if and only if ξ and ζ map to the same element of Ext¹_{𝒪_𝒟}(Lg^*NL_{𝒪_𝒞/𝒪_ℬ}, 𝒢): ξ through Lg^* and Lg^*ℱ ⟶ g^*ℱ ⟶ 𝒢 (pullbackExtClass), ζ through the canonical map Lg^*NL_{𝒪_𝒞/𝒪_ℬ} ⟶ NL_{𝒪_𝒟/𝒪_ℬ} (restrictExtClass).

theorem nonempty_compatibleMorphism_iff :
    Nonempty (CompatibleMorphism g QC QD c) ↔
      pullbackExtClass g c
          (RingedToposExtensionProblem.squareZeroExtensionClassesEquiv f F
            (Quotient.mk
              (RingedToposExtensionProblem.CompatibleFirstOrderThickening.isomorphicSetoid _)
              QC)) =
        restrictExtClass f g
          (RingedToposExtensionProblem.squareZeroExtensionClassesEquiv (f.comp g) G
            (Quotient.mk
              (RingedToposExtensionProblem.CompatibleFirstOrderThickening.isomorphicSetoid _)
              QD))

Deformation.ToposThickening.LiftDiagram.pulledNaiveCotangentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingMorphismExtensionClasses.lean, line 138. The attribute's comment: “the canonical comparison g^*NL_{O_C/O_B} ⟶ NL_{O_D/O_B} along which ζ is read, for the DEGREEWISE pullback, built from the base-change and relative maps of Tag 0E1Y with the topoi identified as in 08UG's own reduction. The derived pullback Lg^*NL_{O_C/O_B} of the source's statement is NOT used: the LEFT-DERIVED extension of scalars along O_C ⟶ O_D is absent from the library, degreewise extension of scalars being only right exact. Tag 08TZ is NOT the missing input and is NOT absent from the library: it is carried as Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso, and it is about the inverse image along a morphism of TOPOI, whereas both layers here live on the one site J”.

The canonical comparison g^*NL_{𝒪_𝒞/𝒪_ℬ} ⟶ NL_{𝒪_𝒟/𝒪_ℬ}: the base-change map for f⁻¹𝒪_ℬ ⟶ 𝒪_𝒞 ⟶ 𝒪_𝒟 followed by the relative map for f⁻¹𝒪_ℬ ⟶ g⁻¹f⁻¹𝒪_ℬ ⟶ 𝒪_𝒟.

def pulledNaiveCotangentComparison :
    D.pulledNaiveCotangentComplex ⟶ D.relativeNaiveCotangentComplex

Deformation.ToposThickening.LiftDiagram.restrictExtClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingMorphismExtensionClasses.lean, line 172. The attribute's comment: “the map Ext¹(NL_{O_D/O_B}, G) ⟶ Ext¹(g^*NL_{O_C/O_B}, G) in which ζ is read, the second of the two maps the source's proof constructs. The first, through the derived pullback of Tag 06YY and Lg^*F ⟶ g^*F ⟶ G, is NOT constructed here”.

The map Ext¹_{𝒪_𝒟}(NL_{𝒪_𝒟/𝒪_ℬ}, 𝒢) ⟶ Ext¹_{𝒪_𝒟}(g^*NL_{𝒪_𝒞/𝒪_ℬ}, 𝒢): precomposition with the canonical comparison of the two naive cotangent complexes.

def restrictExtClass (ζ : D.relativeExtGroup) : D.pulledExtGroup

Deformation.ToposThickening.LiftDiagram.restrictExtClassHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingMorphismExtensionClasses.lean, line 178. The attribute's comment: “the same map as an additive homomorphism; the first of the source's two maps is not constructed here”.

The map in which ζ is read, as a homomorphism of the two Ext groups.

def restrictExtClassHom : D.relativeExtGroup →+ D.pulledExtGroup

Deformation.ToposThickening.LiftDiagram.nonempty_lift_iff_eq_restrictExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingMorphismExtensionClasses.lean, line 213. The attribute's comment: “the equivalence, from clause (1) of Tag 08UG: a morphism of ringed topoi over the base compatible with g and c exists exactly when the two Ext¹ classes agree. THIS IS THE DEGREEWISE ANALOGUE, NOT THE SOURCE'S STATEMENT: the comparison group is Ext¹(g^*NL, G) rather than Ext¹(Lg^*NL, G), the LEFT-DERIVED extension of scalars being absent from the library (NOT Tag 08TZ, which is carried as Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso and is about inverse images along a morphism of topoi, not about Lg^* on one site), and ξ is taken as its image there rather than mapped in. Carried: the two-term structure P with its identification hP, the bijection e (Steps 1 to 3 of the proof of 08UG), the Step 1 homomorphism δ, and hcompat -- the compatibility between the constructions in the proofs of Tags 0GQ5 and 08UG whose statement and proof THE SOURCE ITSELF OMITS, deferring to Tag 0GQ8. The same concession is made by the ringed-space twin Tag 0GQ1”.

Stacks Project, Tag 0GQ7. A morphism g' : (Sh(𝒟), 𝒪_{𝒟'}) ⟶ (Sh(𝒞), 𝒪_{𝒞'}) of ringed topoi over (Sh(ℬ), 𝒪_ℬ) compatible with g and the prescribed map c on the square-zero ideals exists if and only if the classes of the two extensions have the same image in Ext¹_{𝒪_𝒟}(g^*NL_{𝒪_𝒞/𝒪_ℬ}, 𝒢).

Those morphisms are the concrete type LiftDiagram.Lift of the diagram, identified by e with the factorizations of the difference homomorphism δ of Step 1 of the proof of Stacks 08UG through the degree 0 term of g^*NL_{𝒪_𝒞/𝒪_ℬ}; the hypothesis hcompat is the compatibility between the constructions in the proofs of Stacks 0GQ5 and Stacks 08UG, which the source omits and defers to Stacks 0GQ8: the difference of the two classes is the obstruction class of Stacks 08UG.

theorem nonempty_lift_iff_eq_restrictExtClass
    (P : NaiveCotangentTwoTerm (DerivedCategory.singleFunctor
      (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf D.back.O)) 0))
    (hP : P.obj = DerivedCategory.Q.obj D.pulledNaiveCotangentComplex)
    (δ : P.conormal ⟶ D.back.G)
    (e : D.Lift ≃ {θ : P.base ⟶ D.back.G // P.d ≫ θ = δ})
    (ξ : D.pulledExtGroup) (ζ : D.relativeExtGroup)
    (hcompat : eqToHom hP ≫ (ξ - D.restrictExtClass ζ) = P.conormalExtClass D.back.G δ) :
    Nonempty D.Lift ↔ ξ = D.restrictExtClass ζ

Deformation.ToposThickening.RingedToposExtensionProblem.nonempty_lift_iff_eq_pullbackExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionClassesDerivedExtFibre.lean, line 288. The attribute's comment: “the criterion for the DERIVED pullback Lf^*NL_{O_B/O_B'} of the source's statement, with the image of ξ the constructed map pullbackExtClass. Carried, exactly as in the degreewise form of this tag: the two-term structure P with hP, the bijection e of Steps 1 to 3 of 08UG, and hcompat, the 0GQ5/08UG compatibility whose statement and proof the source itself omits, deferring to Tag 0GQ8”.

Stacks Project, Tag 0GQ7 for the derived pullback of Stacks 06YY. A lift compatible with f and the prescribed map c exists if and only if the class of the extension 𝒪', restricted along a comparison q : Lf^*NL_{𝒪_ℬ/𝒪_{ℬ'}} ⟶ NL_{𝒪/𝒪_{ℬ'}}, agrees with the image of ξ ∈ Ext¹_{𝒪_ℬ}(NL_{𝒪_ℬ/𝒪_{ℬ'}}, 𝒥) in Ext¹_𝒪(Lf^*NL_{𝒪_ℬ/𝒪_{ℬ'}}, 𝒢).

Unlike the degreewise form Deformation.ToposThickening.LiftDiagram.nonempty_lift_iff_eq_restrictExtClass, the comparison group here is the Ext¹ of the derived pullback and the image of ξ is the constructed map pullbackExtClass, not a hypothesis. The compatible lifts are identified by e with the factorizations of the difference homomorphism δ through the degree 0 term — Steps 1 to 3 of the proof of Stacks 08UG — and hcompat is the compatibility between the constructions in the proofs of Stacks 0GQ5 and Stacks 08UG which the source omits, deferring to Stacks 0GQ8: the difference of the two classes is the obstruction class.

theorem nonempty_lift_iff_eq_pullbackExtClass
    {J : SheafOfModules.{max v' u' w'} (Stacks.SheafOfModules.Tensor.ringSheaf B.O)}
    (c : S.f.toModulesHom.pullbackModules.obj J ⟶ S.G)
    (q : S.derivedPullbackNaiveCotangent ⟶ S.relativeNaiveCotangentObj)
    (P : NaiveCotangentTwoTerm (DerivedCategory.singleFunctor
      (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0))
    (hP : P.obj = S.derivedPullbackNaiveCotangent)
    (δ : P.conormal ⟶ S.G) {Lift : Type*}
    (e : Lift ≃ {θ : P.base ⟶ S.G // P.d ≫ θ = δ})
    (xi : DerivedCategory.Ext S.baseNaiveCotangentObj
      ((DerivedCategory.singleFunctor _ 0).obj J) 1)
    (ζ : S.extOneRelativeNaiveCotangent)
    (hcompat : eqToHom hP ≫ (S.pullbackExtClass c xi - S.restrictDerivedExtClass q ζ) =
      P.conormalExtClass S.G δ) :
    Nonempty Lift ↔ S.pullbackExtClass c xi = S.restrictDerivedExtClass q ζ

Deformation.ToposThickening.RingedToposExtensionProblem.isCompatibleWithIdealClass_iff_eq_pullbackExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionClassesDerivedExtFibre.lean, line 357. The attribute's comment: “the criterion for the DERIVED pullback, read on isomorphism classes of extensions: this is the cutting-out condition of 0GQ9, proved rather than assumed. Carried are the two-term structure P with hP, the per-class bijections e of Steps 1 to 3 of 08UG, the per-class 0GQ5/08UG compatibilities that the source defers to 0GQ8, and the 0GQ5 bijection E”.

Stacks Project, Tag 0GQ7, read on isomorphism classes: a class of square-zero extensions of f⁻¹𝒪_{ℬ'}-algebras induces the prescribed map c on the base ideal — equivalently, is a class of solutions of Stacks 08UF — exactly when its image under E restricts, along a comparison q : Lf^*NL_{𝒪_ℬ/𝒪_{ℬ'}} ⟶ NL_{𝒪/𝒪_{ℬ'}}, to the image of ξ.

This is the cutting-out condition of Stacks 0GQ9, proved rather than assumed. E is the bijection of Stacks 0GQ5, and P, hP, δ, e and hcompat are the inputs of the criterion for the derived pullback.

theorem isCompatibleWithIdealClass_iff_eq_pullbackExtClass
    {J : SheafOfModules.{max v' u' w'} (Stacks.SheafOfModules.Tensor.ringSheaf B.O)}
    (c : S.f.toModulesHom.pullbackModules.obj J ⟶ S.G)
    (E : CompatibleFirstOrderThickening.IsomorphismClasses S.squareZeroProblem ≃
      S.extOneRelativeNaiveCotangent)
    (q : S.derivedPullbackNaiveCotangent ⟶ S.relativeNaiveCotangentObj)
    (xi : DerivedCategory.Ext S.baseNaiveCotangentObj
      ((DerivedCategory.singleFunctor _ 0).obj J) 1)
    (P : NaiveCotangentTwoTerm (DerivedCategory.singleFunctor
      (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0))
    (hP : P.obj = S.derivedPullbackNaiveCotangent)
    (δ : CompatibleFirstOrderThickening.IsomorphismClasses S.squareZeroProblem →
      (P.conormal ⟶ S.G))
    (e : ∀ p : CompatibleFirstOrderThickening.IsomorphismClasses S.squareZeroProblem,
      S.CompatibleSolutionInClass p ≃ {θ : P.base ⟶ S.G // P.d ≫ θ = δ p})
    (hcompat : ∀ p : CompatibleFirstOrderThickening.IsomorphismClasses S.squareZeroProblem,
      eqToHom hP ≫ (S.pullbackExtClass c xi - S.restrictDerivedExtClass q (E p)) =
        P.conormalExtClass S.G (δ p))
    (p : CompatibleFirstOrderThickening.IsomorphismClasses S.squareZeroProblem) :
    S.IsCompatibleWithIdealClass p ↔
      S.restrictDerivedExtClass q (E p) = S.pullbackExtClass c xi

Tag 0GQ8, a remark

Tag 0GQ8 in the Stacks Project.

Deformation.ToposThickening.InverseImageExtension.Data.pullbackExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/InverseImageExtensionComparison.lean, line 324. The attribute's comment: “the pullback extension 𝒪'₂ = 𝒪_{𝒟'} ×_{𝒪_𝒟} g⁻¹𝒪_𝒞 along g^♯, with the second displayed diagram its projections. Carried: that 𝒢 is the square-zero ideal of 𝒪_{𝒟'} with its 𝒪_𝒟-action (Data.ι, Data.inr_mul_inr, Data.smul_inr). NOT carried: that g⁻¹𝒪_{𝒞'} is an extension of g⁻¹𝒪_𝒞 by g⁻¹ℱ -- the ideal is the kernel ideal of g⁻¹(reduction) and local surjectivity is isLocallySurjective_invImage_map”.

Stacks 0GQ8, the second construction. Pulling the extension 0 ⟶ 𝒢 ⟶ 𝒪_{𝒟'} ⟶ 𝒪_𝒟 ⟶ 0 back along g^♯ : g⁻¹𝒪_𝒞 ⟶ 𝒪_𝒟 gives an extension 0 ⟶ 𝒢 ⟶ 𝒪'₂ ⟶ g⁻¹𝒪_𝒞 ⟶ 0 of g⁻¹f⁻¹𝒪_ℬ-algebras, with 𝒪'₂ = 𝒪_{𝒟'} ×_{𝒪_𝒟} g⁻¹𝒪_𝒞 the fibre product of sheaves of rings and the remark's second displayed diagram its two projections.

def pullbackExtension :
    AlgebraExtension ((invImage g).obj (baseRing f)) ((invImage g).obj X.O) d.invBase
      d.G.val.presheaf

Deformation.ToposThickening.InverseImageExtension.Data.pushoutExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/InverseImageExtensionComparison.lean, line 340. The attribute's comment: “the pushout extension 𝒪'₁ of g⁻¹𝒪_{𝒞'} along c : g⁻¹ℱ ⟶ 𝒢, with the first displayed diagram its comparison with g⁻¹𝒪_{𝒞'}. Carried: that 𝒢 is the square-zero ideal of 𝒪_{𝒟'}. NOT carried: that g⁻¹𝒪_{𝒞'} is an extension of g⁻¹𝒪_𝒞 by g⁻¹ℱ -- the ideal is the kernel ideal of g⁻¹(reduction), whose identification with g⁻¹ℱ is the left exactness of g⁻¹, and local surjectivity is isLocallySurjective_invImage_map”.

Stacks 0GQ8, the first construction. Pushing the extension 0 ⟶ g⁻¹ℱ ⟶ g⁻¹𝒪_{𝒞'} ⟶ g⁻¹𝒪_𝒞 ⟶ 0 out along c : g⁻¹ℱ ⟶ 𝒢 gives an extension 0 ⟶ 𝒢 ⟶ 𝒪'₁ ⟶ g⁻¹𝒪_𝒞 ⟶ 0 of g⁻¹f⁻¹𝒪_ℬ-algebras, with the remark's first displayed diagram its comparison with g⁻¹𝒪_{𝒞'}.

def pushoutExtension [HasWeakSheafify Y.J CommRingCat.{u}]
    [Y.J.WEqualsLocallyBijective CommRingCat.{u}] :
    AlgebraExtension ((invImage g).obj (baseRing f)) ((invImage g).obj X.O) d.invBase
      d.G.val.presheaf

Deformation.ToposThickening.InverseImageExtension.Data.nonempty_compatibleHom_iff_isomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/InverseImageExtensionComparison.lean, line 402. The attribute's comment: “the diagram chase: a morphism g' : (Sh(D), O_{D'}) ⟶ (Sh(C), O_{C'}) of ringed topoi over (Sh(B), O_B) compatible with g and c exists iff 𝒪'₁ ≅ 𝒪'₂ as g⁻¹f⁻¹O_B-algebra extensions of g⁻¹O_C by 𝒢; g' is in comorphism form, a morphism of ringed topoi inducing g by Data.ringedToposHomEquiv and Data.compatibleRingedToposHom. Carried: 𝒢 is the square-zero ideal of O_{D'}. NOT included: the remark's second half, identifying 𝒪'₁ with ξ and 𝒪'₂ with ζ”.

Stacks Project, Tag 0GQ8, the criterion. A morphism g' : (Sh(𝒟), 𝒪_{𝒟'}) ⟶ (Sh(𝒞), 𝒪_{𝒞'}) of ringed topoi over (Sh(ℬ), 𝒪_ℬ) compatible with g and c exists if and only if the pushout 𝒪'₁ and the pullback 𝒪'₂ are isomorphic as g⁻¹f⁻¹𝒪_ℬ-algebra extensions of g⁻¹𝒪_𝒞 by 𝒢.

The morphisms g' are the comorphisms of Data.CompatibleHom, which really are morphisms of ringed topoi between the two thickenings by Data.compatibleRingedToposHom, with the three compatibilities of the source read off in Data.compatibleRingedToposHom_base, Data.compatibleRingedToposHom_comp_p and Data.compatibleRingedToposHom_kernel.

theorem nonempty_compatibleHom_iff_isomorphic [HasWeakSheafify Y.J CommRingCat.{u}]
    [Y.J.WEqualsLocallyBijective CommRingCat.{u}] :
    Nonempty d.CompatibleHom ↔
      AlgebraExtension.Isomorphic d.pushoutExtension d.pullbackExtension

Deformation.ToposThickening.InverseImageExtension.pushoutSolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/InverseImageExtensionSolutions.lean, line 597. The attribute's comment: “the first construction: the pushout O'_1 of g⁻¹O_{C'} along c : g⁻¹F ⟶ G, an extension of g⁻¹O_C by G as g⁻¹f⁻¹O_B-algebras”.

Stacks 0GQ8, the pushout 𝒪'₁, as a square-zero extension of g⁻¹𝒪_𝒞 by 𝒢: a solution of inverseImageProblem f g 𝒢.

noncomputable def pushoutSolution : (inverseImageProblem f g G).CompatibleFirstOrderThickening

Deformation.ToposThickening.InverseImageExtension.pullbackSolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/InverseImageExtensionSolutions.lean, line 606. The attribute's comment: “the second construction: the pullback O'_2 of O_{D'} along g^♯ : g⁻¹O_C ⟶ O_D, an extension of g⁻¹O_C by G as g⁻¹f⁻¹O_B-algebras”. References: EGA 0 (18.2.5), “more general”.

Stacks 0GQ8, the pullback 𝒪'₂ = 𝒪_{𝒟'} ×_{𝒪_𝒟} g⁻¹𝒪_𝒞, as a square-zero extension of g⁻¹𝒪_𝒞 by 𝒢: a solution of inverseImageProblem f g 𝒢.

noncomputable def pullbackSolution : (inverseImageProblem f g G).CompatibleFirstOrderThickening

Deformation.ToposThickening.InverseImageExtension.nonempty_compatibleMorphism_iff_isomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/InverseImageExtensionSolutions.lean, line 750. The attribute's comment: “the diagram chase: a morphism g' over (Sh(B), O_B) compatible with g and c exists iff O'_1 and O'_2 are isomorphic as g⁻¹f⁻¹O_B-algebra extensions of g⁻¹O_C by G”.

Stacks Project, Tag 0GQ8, the diagram chase. A morphism g' : (Sh(𝒟), 𝒪_{𝒟'}) ⟶ (Sh(𝒞), 𝒪_{𝒞'}) of ringed topoi over (Sh(ℬ), 𝒪_ℬ) compatible with g and c exists if and only if the pushout 𝒪'₁ and the pullback 𝒪'₂ are isomorphic as g⁻¹f⁻¹𝒪_ℬ-algebra extensions of g⁻¹𝒪_𝒞 by 𝒢.

theorem nonempty_compatibleMorphism_iff_isomorphic :
    Nonempty (CompatibleMorphism g QC QD c) ↔
      RingedToposExtensionProblem.CompatibleFirstOrderThickening.Isomorphic
        (pushoutSolution g QC QD c) (pullbackSolution g QC QD c)

Deformation.ToposThickening.LiftingMorphismDerived.rhoEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingMorphismDerivedRhoEquiv.lean, line 598.

The identification of Ext groups Ext¹_{𝒪_𝒟}(Lg^*NL_{𝒪_𝒞/𝒪_ℬ}, 𝒢) = Ext¹_{g⁻¹𝒪_𝒞}(NL_{g⁻¹𝒪_𝒞/g⁻¹f⁻¹𝒪_ℬ}, 𝒢), the base of the right-hand side read as (f ∘ g)⁻¹𝒪_ℬ ≅ g⁻¹f⁻¹𝒪_ℬ: the bijection rhoClass, which sends e : Lg^*NL_{𝒪_𝒞/𝒪_ℬ} ⟶ 𝒢[1] to the composite of the identification NL_{g⁻¹𝒪_𝒞/g⁻¹f⁻¹𝒪_ℬ} ≅ g⁻¹NL_{𝒪_𝒞/𝒪_ℬ} of Stacks 08TZ, the derived unit g⁻¹NL_{𝒪_𝒞/𝒪_ℬ} ⟶ Lg^*NL_{𝒪_𝒞/𝒪_ℬ} read over g⁻¹𝒪_𝒞 (the tensor-hom adjunction along g^♯) and e read over g⁻¹𝒪_𝒞.

def rhoEquiv :
    DerivedCategory.Ext ((derivedPullback g).obj (DerivedCategory.Q.obj
        (Stacks.SheafOfModules.naiveCotangentComplex.{u, u, u, u} X.J
          ((inverseImageCommRingFunctor f.toToposHom).obj B.O) X.O f.fSharpInverseImage)))
      ((DerivedCategory.singleFunctor _ 0).obj G) 1 ≃
    DerivedCategory.Ext (DerivedCategory.Q.obj
        (Stacks.SheafOfModules.naiveCotangentComplex.{u, u, u, u} Y.J
        ((inverseImageCommRingFunctor (f.comp (toInverseImage g)).toToposHom).obj B.O)
        ((invImage g).obj X.O) (f.comp (toInverseImage g)).fSharpInverseImage))
      ((DerivedCategory.singleFunctor (SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf ((invImage g).obj X.O))) 0).obj
          (restrictedIdeal g G)) 1

Deformation.ToposThickening.LiftingMorphismDerived.rhoEquiv_extClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/LiftingMorphismDerivedRhoEquiv.lean, line 634.

The classes of 𝒪'₁ and 𝒪'₂. Under the identification rhoEquiv of Ext¹_{𝒪_𝒟}(Lg^*NL_{𝒪_𝒞/𝒪_ℬ}, 𝒢) with Ext¹_{g⁻¹𝒪_𝒞}(NL_{g⁻¹𝒪_𝒞/g⁻¹f⁻¹𝒪_ℬ}, 𝒢), the image of ξ (the class of QC, through Lg^* and Lg^*ℱ ⟶ g^*ℱ ⟶ 𝒢) is the class (Stacks 0GQ5) of the pushout 𝒪'₁ of g⁻¹𝒪_{𝒞'} along c, and the image of ζ (the class of QD, through Lg^*NL_{𝒪_𝒞/𝒪_ℬ} ⟶ NL_{𝒪_𝒟/𝒪_ℬ}) is the class of the pullback 𝒪'₂ of 𝒪_{𝒟'} along g^♯.

theorem rhoEquiv_extClass_eq :
    rhoEquiv g (pullbackExtClass g c
        (RingedToposExtensionProblem.squareZeroExtensionClassesEquiv f F
          (Quotient.mk
            (RingedToposExtensionProblem.CompatibleFirstOrderThickening.isomorphicSetoid _)
            QC))) =
      RingedToposExtensionProblem.squareZeroExtensionClassesEquiv (f.comp (toInverseImage g))
        (restrictedIdeal g G)
        (Quotient.mk (RingedToposExtensionProblem.CompatibleFirstOrderThickening.isomorphicSetoid _)
          (pushoutSolution g QC QD c)) ∧
    rhoEquiv g (restrictExtClass f g
        (RingedToposExtensionProblem.squareZeroExtensionClassesEquiv (f.comp g) G
          (Quotient.mk
            (RingedToposExtensionProblem.CompatibleFirstOrderThickening.isomorphicSetoid _)
            QD))) =
      RingedToposExtensionProblem.squareZeroExtensionClassesEquiv (f.comp (toInverseImage g))
        (restrictedIdeal g G)
        (Quotient.mk (RingedToposExtensionProblem.CompatibleFirstOrderThickening.isomorphicSetoid _)
          (pullbackSolution g QC QD c))

Tag 0GQ9, a lemma

Tag 0GQ9 in the Stacks Project.

Deformation.ToposThickening.RingedToposExtensionProblem.solutionEquivSquareZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionClassesFibre.lean, line 236. The attribute's comment: “the step the source states as -- of course this is the same thing as saying that O' is a solution of 08UF: a solution of the problem of Tag 08UF is exactly a square-zero extension of f⁻¹O_B'-algebras whose map from the thickened base induces the prescribed c on the base ideal. Fixed-site presentation of 08UF, as in Tag 0GQ5”.

The solutions of [Stacks 08UF] are exactly the square-zero extensions of f⁻¹𝒪_{ℬ'}-algebras that induce c. The two solution types carry the same thickened structure sheaf, reduction, map from the thickened base and kernel identification.

def solutionEquivSquareZero :
    S.CompatibleFirstOrderThickening ≃
      { Q : S.squareZeroProblem.CompatibleFirstOrderThickening // S.IsCompatibleWithIdeal Q }

Deformation.ToposThickening.RingedToposExtensionProblem.classesEquivFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionClassesFibre.lean, line 522. The attribute's comment: “the canonical bijection between the isomorphism classes of solutions of the problem of 08UF and the fibre over 0 of compatibilityObstruction on Ext¹ of a FIXED presentation. Carried: ONLY the five inputs of Tag 0GQ5 at the trivial-ideal problem. The cutting-out condition is PROVED, not assumed: the obstruction is the sectionwise difference between the map a square-zero extension of f⁻¹O_B'-algebras induces on f⁻¹J and the prescribed c, read in G, and it is shown to depend only on the Ext class. It is NOT the source's comparison map, whose target Ext¹(Lf^NL_{O_B/O_B'}, G) needs the derived pullback Lf^, absent from the library”.

Stacks Project, Tag 0GQ9. The isomorphism classes of solutions of the square-zero extension problem of [Stacks 08UF] are canonically bijective to the fibre over 0 of the compatibility obstruction on the first Ext group of the presentation.

The bijection is classesEquivCompatible, which identifies the solutions with the square-zero extensions of f⁻¹𝒪_{ℬ'}-algebras inducing c, followed by the bijection classesEquivExt of [Stacks 0GQ5] for the problem squareZeroProblem over the thickened base. That such an extension induces c exactly when its obstruction vanishes is isCompatibleWithIdeal_iff_idealObstruction_eq_zero, and the obstruction descends to Ext¹ through idealObstruction_of_iso. The hypotheses are exactly those of classesEquivExt; see the implementation notes of this file.

def classesEquivFibre
    (P : NaiveCotangentTwoTerm single)
    (xi : S.squareZeroProblem.CompatibleFirstOrderThickening →
      S.squareZeroProblem.CompatibleFirstOrderThickening → (P.conormal ⟶ S.G))
    (hxi : ∀ Q₁ Q₂ Q₃ : S.squareZeroProblem.CompatibleFirstOrderThickening,
      xi Q₁ Q₂ + xi Q₂ Q₃ = xi Q₁ Q₃)
    (rep : ∀ ζ : P.obj ⟶ (single.obj S.G)⟦(1 : ℤ)⟧,
      { δ : P.conormal ⟶ S.G // liftingObstruction P S.G δ = ζ })
    (pushout : ∀ (Q : S.squareZeroProblem.CompatibleFirstOrderThickening)
        (δ : P.conormal ⟶ S.G),
      { Q' : S.squareZeroProblem.CompatibleFirstOrderThickening // xi Q Q' = δ })
    (ee : ∀ Q₁ Q₂ : S.squareZeroProblem.CompatibleFirstOrderThickening,
      CompatibleFirstOrderThickening.Hom Q₁ Q₂ ≃
        { θ : P.base ⟶ S.G // P.d ≫ θ = xi Q₁ Q₂ }) :
    CompatibleFirstOrderThickening.IsomorphismClasses S ≃
      { ζ : P.obj ⟶ (single.obj S.G)⟦(1 : ℤ)⟧ //
        S.compatibilityObstruction P xi hxi rep pushout ee ζ = 0 }

Deformation.ToposThickening.RingedToposExtensionProblem.solutionClassesEquivDerivedExtFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionClassesNaiveExtFibre.lean, line 485.

Stacks Project, Tag 0GQ9. Let t : (Sh(ℬ), 𝒪_ℬ) ⟶ (Sh(ℬ'), 𝒪_{ℬ'}), 𝒥 = Ker(t^♯), f : (Sh(𝒞), 𝒪) ⟶ (Sh(ℬ), 𝒪_ℬ), 𝒢 and c : f⁻¹𝒥 ⟶ 𝒢 be as in (08UF) — the problem S — and let ξ ∈ Ext¹_{𝒪_ℬ}(NL_{𝒪_ℬ/𝒪_{ℬ'}}, 𝒥) be the element corresponding to the extension 𝒪_{ℬ'} of 𝒪_ℬ by 𝒥 via Stacks 0GQ5 (baseThickeningClass). The set of isomorphism classes of solutions is canonically bijective to the fibre of Ext¹_𝒪(NL_{𝒪/𝒪_{ℬ'}}, 𝒢) ⟶ Ext¹_𝒪(Lf^*NL_{𝒪_ℬ/𝒪_{ℬ'}}, 𝒢) over the image of ξ (derivedExtFibre), Lf^* being the derived pullback of Stacks 06YY.

The bijection is the one of the source's proof: the class of a solution 𝒪' goes to the element of Ext¹_𝒪(NL_{𝒪/𝒪_{ℬ'}}, 𝒢) which Stacks 0GQ5 for t ∘ f attaches to 𝒪' as an extension of (t ∘ f)⁻¹𝒪_{ℬ'}-algebras (solutionClassesEquivDerivedExtFibre_mk); that the classes so obtained are exactly the fibre is Stacks 0GQ7.

def solutionClassesEquivDerivedExtFibre :
    CompatibleFirstOrderThickening.IsomorphismClasses S ≃ S.derivedExtFibre

Deformation.ToposThickening.RingedToposExtensionProblem.solutionClassesEquivDerivedExtFibre_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionClassesNaiveExtFibre.lean, line 496.

The bijection of Stacks 0GQ9 is the canonical one: the class of a solution 𝒪' goes to the element of Ext¹_𝒪(NL_{𝒪/𝒪_{ℬ'}}, 𝒢) that Stacks 0GQ5 for t ∘ f attaches to 𝒪', read as a square-zero extension of (t ∘ f)⁻¹𝒪_{ℬ'}-algebras.

theorem solutionClassesEquivDerivedExtFibre_mk (P : S.CompatibleFirstOrderThickening) :
    (S.solutionClassesEquivDerivedExtFibre (Quotient.mk _ P)).1 =
      squareZeroExtensionClassesEquiv S.compBase S.G
        (Quotient.mk (CompatibleFirstOrderThickening.isomorphicSetoid _) (S.toCompSolution P))

Sources

LeanDeformation.ToposThickening.ArbitrarySiteExtensionProblem.CompatibleFirstOrderThickening · Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening · Deformation.ToposThickening.LiftDiagram.translate_existsUnique · Deformation.ToposThickening.FirstOrderLiftDiagram.derivationEquivDifferentialsHom · Deformation.ToposThickening.FirstOrderLiftDiagram.translateHom_zero · Deformation.ToposThickening.FirstOrderLiftDiagram.translateHom_add · Deformation.ToposThickening.FirstOrderLiftDiagram.existsUnique_translateHom · Deformation.ToposThickening.RingedToposLiftDiagram.obstructionClass_eq_zero_iff

Section91.14 Deformations of algebraic spaces #

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

Tag 0D16, a lemma

Tag 0D16 in the Stacks Project.

AlgebraicGeometry.Space.isThickeningHom_iff_isThickening_smallEtaleRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SmallEtaleRingedToposThickeningIff.lean, line 143.

Stacks 0D16. Let S be a scheme and i : Z ⟶ Z' a morphism of algebraic spaces over S. Then i is a thickening of algebraic spaces (Stacks 05ZJ, Definition 05ZK: a closed immersion identifying Z with a closed subspace of Z' having the same points, here in the morphism form AlgebraicGeometry.Space.IsThickeningHom) if and only if the associated morphism i_small : (Sh(Z_étale), 𝒪_Z) ⟶ (Sh(Z'_étale), 𝒪_{Z'}) of ringed topoi (Stacks 03G8, AlgebraicGeometry.Space.smallEtaleRingedToposHom) is a thickening in the sense of Stacks 08M6 (Deformation.ToposThickening.IsThickening).

theorem isThickeningHom_iff_isThickening_smallEtaleRingedToposHom
    {Z Z' : AlgebraicSpaces B S hS} (i : Z ⟶ Z') :
    IsThickeningHom B S hS i ↔
      Deformation.ToposThickening.IsThickening.{u, u + 1, u, u, u + 1, u}
        (smallEtaleRingedToposHom B S hS i)

Tag 0D17, a lemma

Tag 0D17 in the Stacks Project.

AlgebraicGeometry.Space.FlatThickeningDeformation.classes_addTorsor_and_autMulEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatThickeningDeformation/Classification.lean, line 91. References: SGA 7 VI (4.16), “special case”.

[Stacks Project, Tag 0D17]. Let S be a scheme, Y ⊂ Y' a first order thickening of algebraic spaces over S (hZ) and f : X ⟶ Y a flat morphism of algebraic spaces over S (hf). If there exists a flat f' : X' ⟶ Y' with an isomorphism a : X ≅ X' ×_{Y'} Y over Y (hD; a Deformation f is exactly such a pair, see Deformation.ofPair, Deformation.pairIso), then 1. the set Classes f of isomorphism classes of pairs (f', a) is principal homogeneous under Ext¹_{𝒪_X}(NL_{X/Y}, f^*𝒞_{Y/Y'}), and 2. for every such pair D, the group Aut D of automorphisms φ : X' ⟶ X' over Y' reducing to the identity on X' ×_{Y'} Y is Ext⁰_{𝒪_X}(NL_{X/Y}, f^*𝒞_{Y/Y'}).

NL_{X/Y} is the canonical naive cotangent complex naiveCotangentComplex B S hS f; the module f^*𝒞_{Y/Y'} is liftedPulledBackConormal hZ f (its sections lifted to the universe of those of NL_{X/Y}); the Ext groups are those of any model of the derived category of 𝒪_X-modules. The isomorphisms themselves are classes_addTorsor and Deformation.autMulEquivNaiveCotangentExtZero (an isomorphism of groups, which in particular identifies the underlying sets).

theorem classes_addTorsor_and_autMulEquiv (hf : IsFlat B S hS f.hom)
    (hD : Nonempty (Deformation f)) :
    Nonempty (AddTorsor
        (DerivedCategory.Ext (DerivedCategory.Q.obj (naiveCotangentComplex B S hS f))
          ((DerivedCategory.singleFunctor _ 0).obj (liftedPulledBackConormal hZ f)) 1)
        (Classes f)) ∧
      ∀ D : Deformation f, Nonempty (Aut D ≃* Multiplicative (DerivedCategory.Ext
        (DerivedCategory.Q.obj (naiveCotangentComplex B S hS f))
        ((DerivedCategory.singleFunctor _ 0).obj (liftedPulledBackConormal hZ f)) 0))

Tag 0D3P, a lemma

Tag 0D3P in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_of_isPushoutFunctor_of_isIso_coherator_map_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AlgebraExtensionPushoutQcqs.lean, line 296.

[Stacks Project, Tag 0D3P]. Let f : X ⟶ Y be a morphism of algebraic spaces with X quasi-compact and quasi-separated, let φ : ℱ ⟶ 𝒢 be a morphism of 𝒪_X-modules such that DQ_X(ℱ) ⟶ DQ_X(𝒢) is an isomorphism, where DQ_X is the right adjoint of D_QCoh(𝒪_X) ⥤ D(𝒪_X) of [Stacks Project, Tag 0CR4], and let F be pushout along φ, from extensions 0 ⟶ ℱ ⟶ 𝒪' ⟶ 𝒪_X ⟶ 0 of f⁻¹𝒪_Y-algebras on X_étale to extensions by 𝒢 (characterised by the universal property of the pushout). Then F is an equivalence of categories.

The quasi-coherence of NL_{X/Y} which the source's proof uses is AlgebraicGeometry.Space.qcohDerivedProp_modelNaiveCotangentComplex, from [Stacks Project, Tag 0D0Y].

theorem isEquivalence_of_isPushoutFunctor_of_isIso_coherator_map_of_qcqs
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hXc : IsQuasiCompactSpace B S hS X.1) (hXs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    {M N : SheafOfModules.{u} ((sheafCompose (SmallEtale.topology B S hS X.1)
      (forget₂ CommRingCat.{u} RingCat.{u})).obj (structureSheaf B S hS X.1 X.2))}
    (φ : M ⟶ N)
    {F : AlgebraExtension (J := SmallEtale.topology B S hS X.1) (inverseImageBaseMap B S hS f) M ⥤
      AlgebraExtension (J := SmallEtale.topology B S hS X.1) (inverseImageBaseMap B S hS f) N}
    (hF : IsPushoutFunctor.{u, u + 1, u} (a := inverseImageBaseMap B S hS f) φ F)
    (hDQ : letI := quasicoherentDerivedInclusion_isLeftAdjoint_of_qcqs B S hS hZ X.1 X.2 hXc hXs
      IsIso ((qcohDerivedProp B S hS X).ι.rightAdjoint.map
        ((DerivedCategory.singleFunctor (Modules.{u, u} B S hS X.1 X.2) 0).map φ))) :
    F.IsEquivalence

Tag 0D3Q, a lemma

Tag 0D3Q in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_of_isKernelPushoutFunctor_of_isIso_coherator_map_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ThickenedBasePushoutEquivalence.lean, line 66.

[Stacks Project, Tag 0D3Q]. Let f : X ⟶ D be a morphism of algebraic spaces with X quasi-compact and quasi-separated, and i : D ⟶ D' a closed immersion (for instance a first order thickening). Let P be a square-zero extension problem (91.13.0.1) of the small étale ringed topoi over f whose thickened base is i⁻¹𝒪_{D'}, its reduction being i♯, with prescribed ideal module ℱ. Let φ : ℱ ⟶ 𝒢 be a morphism of 𝒪_X-modules with DQ_X(ℱ) ⟶ DQ_X(𝒢) an isomorphism, DQ_X the right adjoint of D_QCoh(𝒪_X) ⥤ D(𝒪_X) of [Stacks Project, Tag 0CR4], and let FT be pushout along φ from the solutions of P to those of the problem with ideal module 𝒢 (characterised by the universal property of the pushout). Then FT is an equivalence of categories.

The source asks D ⊂ D' to be a first order thickening; the argument only uses that i is a closed immersion, the square-zero condition being part of the problem P.

theorem isEquivalence_of_isKernelPushoutFunctor_of_isIso_coherator_map_of_qcqs
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (hXc : IsQuasiCompactSpace B S hS X.1) (hXs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (f : X ⟶ D) (i : D ⟶ D') (hi : IsClosedImmersion B S hS i.hom)
    (P : RingedToposExtensionProblem (smallEtaleRingedTopos B S hS X)
      (smallEtaleRingedTopos B S hS D))
    (hPf : P.f = smallEtaleRingedToposHom B S hS f)
    (eBase : P.baseExtension ≅
      (smallEtaleInverseImageRing B S hS i).obj (smallEtaleRingedTopos B S hS D').O)
    (heBase : eBase.hom ≫ (smallEtaleRingedToposHom B S hS i).fSharpInverseImage =
      P.baseReduction)
    {N : SheafOfModules.{u} ((sheafCompose (SmallEtale.topology B S hS X.1)
      (forget₂ CommRingCat.{u} RingCat.{u})).obj (structureSheaf B S hS X.1 X.2))}
    (φ : P.G ⟶ N)
    {FT : P.CompatibleFirstOrderThickening ⥤
      (RingedToposExtensionProblem.changeKernel P φ).CompatibleFirstOrderThickening}
    (hFT : RingedToposExtensionProblem.IsKernelPushoutFunctor.{u, u + 1, u, u, u + 1, u}
      (S := P) φ FT)
    (hDQ : letI := quasicoherentDerivedInclusion_isLeftAdjoint_of_qcqs B S hS hZ X.1 X.2 hXc hXs
      IsIso ((qcohDerivedProp B S hS X).ι.rightAdjoint.map
        ((DerivedCategory.singleFunctor (Modules.{u, u} B S hS X.1 X.2) 0).map φ))) :
    FT.IsEquivalence

Sources

LeanAlgebraicGeometry.Space.isThickeningHom_iff_isThickening_smallEtaleRingedToposHom · AlgebraicGeometry.Space.FlatThickeningDeformation.classes_addTorsor_and_autMulEquiv · AlgebraicGeometry.Space.isEquivalence_of_isPushoutFunctor_of_isIso_coherator_map_of_qcqs · AlgebraicGeometry.Space.isEquivalence_of_isKernelPushoutFunctor_of_isIso_coherator_map_of_qcqs

Section91.15 Deformations of complexes #

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

Tag 0DYR, a lemma

Tag 0DYR in the Stacks Project.

Deformation.Obstruction.canonicalObstructionMap_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CanonicalObstructionBaseChange.lean, line 345. The attribute's comment: “part (3)”.

The canonical obstruction morphism is compatible with base change. Derived base change along b carries the canonical obstruction morphism of a bounded-above K for the square-zero surjection fR to the canonical obstruction morphism of its base change for fS, read through the comparison of the two targets attached to a bounded-above free K-flat representative P of K and a K-flat resolution q of I/I².

theorem canonicalObstructionMap_baseChange
    (hI : RingHom.ker fR ^ 2 = ⊥)
    (hJ : RingHom.ker fS = Ideal.map a (RingHom.ker fR))
    (K : DerivedCategory (ModuleCat.{u} R))
    (hK : (DerivedCategory.TStructure.t (C := ModuleCat.{u} R)).minus K)
    (P : CochainComplex (ModuleCat.{u} R) ℤ) (m : ℤ) (hPLE : P.IsStrictlyLE m)
    (hfree : ∀ n, Module.Free R (P.X n)) (hP : P.KFlat)
    (e : DerivedCategory.Q.obj P ≅ K)
    (T : CochainComplex (ModuleCat.{u} R) ℤ) (k : ℤ) (hTLE : T.IsStrictlyLE k)
    (hTproj : ∀ i, Projective (T.X i)) (hT : T.KFlat)
    (q : T ⟶ kernelComplex fR hfR) (hq : QuasiIso q)
    (hQq : IsIso (DerivedCategory.Q.map q)) :
    (derivedExtensionScalarsGeneral.{u, u, u} b).functor.map
        (canonicalObstructionMap fR hfR hI K hK).1 ≫
      ((derivedExtensionScalarsGeneral.{u, u, u} b).functor.commShiftIso (2 : ℤ)).hom.app
          (((canonicalDerivedTensorProductFunctor R).obj K).obj
            (squareZeroKernelObject fR hfR)) ≫
        (shiftFunctor (DerivedCategory (ModuleCat.{u} S)) (2 : ℤ)).map
          (obstructionTargetBaseChangeMap fR hfR fS hfS a b hcomm P hP e T hT q hQq) =
      (canonicalObstructionMap fS hfS (ker_sq_eq_bot_baseChange fR fS a hJ hI)
        ((derivedExtensionScalarsGeneral.{u, u, u} b).functor.obj K)
        ((derivedExtensionScalarsGeneral.{u, u, u} b).maps_boundedAbove ⟨K, hK⟩)).1

Deformation.Obstruction.existsUnique_isCanonicalObstructionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CanonicalObstructionMap/DerivedMorphism.lean, line 296. The attribute's comment: “canonical_obstruction_map”.

There is a unique morphism represented by the squares of lifted differentials on every bounded-above free representative, independently of the lifts and all comparison data.

theorem existsUnique_isCanonicalObstructionMap
    (f : R' →+* R) (hf : Function.Surjective f) (hzero : (RingHom.ker f) ^ 2 = ⊥)
    (K : DerivedCategory (ModuleCat.{u} R))
    (hK : (DerivedCategory.TStructure.t (C := ModuleCat.{u} R)).minus K) :
    ∃! ω : K ⟶ (((canonicalDerivedTensorProductFunctor R).obj K).obj
      (squareZeroKernelObject f hf))⟦(2 : ℤ)⟧, IsCanonicalObstructionMap f hf K ω

Deformation.Obstruction.canonicalObstructionMap_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CanonicalObstructionNaturality.lean, line 337. The attribute's comment: “naturality”.

The canonical obstruction morphism commutes with every morphism of bounded-above derived complexes.

theorem canonicalObstructionMap_natural
    {R' R : Type u} [CommRing R'] [CommRing R]
    (f : R' →+* R) (hf : Function.Surjective f)
    (hzero : (RingHom.ker f) ^ 2 = ⊥)
    {K L : DerivedCategory (ModuleCat.{u} R)}
    (hK : (DerivedCategory.TStructure.t (C := ModuleCat.{u} R)).minus K)
    (hL : (DerivedCategory.TStructure.t (C := ModuleCat.{u} R)).minus L)
    (g : K ⟶ L) :
    g ≫ (Deformation.Obstruction.canonicalObstructionMap
      f hf hzero L hL).val =
      (Deformation.Obstruction.canonicalObstructionMap
        f hf hzero K hK).val ≫
        (shiftFunctor (DerivedCategory (ModuleCat.{u} R)) (2 : ℤ)).map
          (((canonicalDerivedTensorProductFunctor R).map g).app
            (Deformation.Obstruction.squareZeroKernelObject f hf))

Deformation.Obstruction.canonicalObstructionMap_eq_zero_iff_exists_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CanonicalObstructionVanishing.lean, line 714. The attribute's comment: “vanishing_criterion”.

A bounded-above derived complex over R lifts across a square-zero surjection R' → R exactly when its canonical obstruction morphism is zero.

theorem canonicalObstructionMap_eq_zero_iff_exists_lift
    {R' R : Type u} [CommRing R'] [CommRing R]
    (f : R' →+* R) (hf : Function.Surjective f)
    (hzero : (RingHom.ker f) ^ 2 = ⊥)
    (K : DerivedCategory (ModuleCat.{u} R))
    (hK : (DerivedCategory.TStructure.t (C := ModuleCat.{u} R)).minus K) :
      (Deformation.Obstruction.canonicalObstructionMap f hf hzero K hK).val = 0 ↔
      ∃ K' : DerivedCategory (ModuleCat.{u} R'),
        Nonempty ((derivedExtensionScalarsGeneral.{u, u, u} f).functor.obj K' ≅ K)

Sources

LeanDeformation.Obstruction.canonicalObstructionMap_baseChange · Deformation.Obstruction.existsUnique_isCanonicalObstructionMap · Deformation.Obstruction.canonicalObstructionMap_natural · Deformation.Obstruction.canonicalObstructionMap_eq_zero_iff_exists_lift

Section91.16 Deformations of complexes on ringed topoi #

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

Tag 0DIT, a lemma

Tag 0DIT in the Stacks Project.

Stacks.SheafOfModules.ComplexLifting.exists_liftedComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatResolution/ComplexLifting.lean, line 582.

Stacks 0DIT. A bounded-above flat lifting exists for a bounded-above complex and a bounded-above graded flat family whose given maps form a map of complexes after extension of scalars. The ambient module universe contains the site and the ring sheaves.

theorem exists_liftedComplex [J.WEqualsLocallyBijective AddCommGrpCat.{max u v w z}]
    [HasSheafify J AddCommGrpCat.{max u v w z}] {O O₀ : Sheaf J CommRingCat.{w}} (f : O ⟶ O₀)
    (hf : Sheaf.IsLocallySurjective f)
    (G : GradedDifferential
      (_root_.SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (K₀ : CochainComplex
      (_root_.SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf O₀)) ℤ)
    (g : ∀ n, G.X n ⟶
      (_root_.SheafOfModules.restrictScalars (ringSheafMap f)).obj (K₀.X n))
    (hGflat : ∀ n, AlgebraicGeometry.SheafOfModules.IsFlat (G.X n))
    (hGbounded : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (G.X n))
    (hKbounded : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    (hG₀ : BaseChangeTo f G K₀ g) :
    Nonempty (LiftedComplex f G K₀ g)

Tag 0DIU, a lemma

Tag 0DIU in the Stacks Project.

Deformation.ComplexLift.unit_comp_curvature, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClass.lean, line 289. The attribute's comment: “variant: the curvature d ∘ d of the lifted differential, the complex-level map; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

The curvature computes the square of the lifted differential: pulled back to the lift and followed by the ideal inclusion it is d ∘ d. This is the identification of ω with the curvature class, read on the complex representing it.

theorem unit_comp_curvature (n : ℤ) :
    L.baseChange.unit n ≫ (restrict f).map (curvature T n) ≫ T.emb (n + 1 + 1) =
      L.F.d n ≫ L.F.d (n + 1)

Deformation.ComplexLift.obstructionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClass.lean, line 443. The attribute's comment: “variant: at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus, the map K₀ ⟶ (K₀ ⊗^L I)[2]”.

Stacks 0DIU. The canonical map ω(K₀) : K₀ ⟶ (K₀ ⊗^L_{O₀} I)[2] attached to a square-zero extension of sheaves of rings with ideal sheaf I. It is the curvature of the lifted differential of a bounded above flat lift of K₀, transported along the quasi-isomorphism identifying the reduction of that lift with K₀.

def obstructionMap {L : FlatLift f K₀} (T : IdealKernel S L) :
    DerivedCategory.Q.obj K₀ ⟶ (D.functor.obj (DerivedCategory.Q.obj K₀))⟦(2 : ℤ)⟧

Deformation.ComplexLift.obstructionMap_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClass.lean, line 478. The attribute's comment: “variant: naturality of ω along a morphism of flat lifts at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus_natural”.

Stacks 0DIU. Naturality of ω: for a map φ : K₀ ⟶ L₀ of bounded above complexes covered by a morphism of flat lifts, the square formed by ω(K₀), ω(L₀) and the maps induced by φ commutes.

theorem obstructionMap_natural :
    DerivedCategory.Q.map φ ≫ obstructionMap D TM =
      obstructionMap D TL ≫
        (CategoryTheory.shiftFunctor (DerivedCategory (SheafMod O₀)) (2 : ℤ)).map
          (D.functor.map (DerivedCategory.Q.map φ))

Deformation.ComplexLift.obstructionMap_eq_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClass.lean, line 511. The attribute's comment: “variant: independence of the flat lift at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU. Two flat lifts of the same complex joined by a morphism of lifts over the identity give the same map ω(K₀). Together with the existence of a lift receiving maps from any two, this is the independence of ω of the lift, hence its canonicality.

theorem obstructionMap_eq_of_hom {L M : FlatLift f K₀} (h : FlatLiftHom L M (𝟙 K₀))
    (TL : IdealKernel S L) (TM : IdealKernel S M)
    (hemb : ∀ n : ℤ, (restrict f).map (((idealTensorFunctor O₀ I).map h.red).f n) ≫
      TM.emb n = TL.emb n ≫ h.hom n) :
    obstructionMap D TL = obstructionMap D TM

Deformation.ComplexLift.tensorOmega, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClassDerivedTensor.lean, line 267. The attribute's comment: “the canonical map ω(K₀) : K₀ ⟶ (K₀ ⊗^L I)[2], on a bounded above complex”.

The map ω(K₀) : K₀ ⟶ (K₀ ⊗^L_{O₀} I)[2] of a bounded above complex. It is the curvature class of a bounded above flat lift of K₀ (Tag 0DIT), read through the canonical identification of the ideal part of the lift with the kernel of its reduction; by Deformation.ComplexLift.tensorObstruction_eq_of_lift it does not depend on the lift.

def tensorOmega (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (K₀ : CochainComplex (SheafMod O₀) ℤ)
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n)) :
    DerivedCategory.Q.obj K₀ ⟶
      ((derivedTensorRight.{d} I).obj (DerivedCategory.Q.obj K₀))⟦(2 : ℤ)⟧

Deformation.ComplexLift.tensorOmega_natural_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClassDerivedTensor.lean, line 302. The attribute's comment: “naturality of ω, on bounded above complexes”.

Naturality of ω along an arbitrary morphism of D(O₀) between bounded above complexes: such a morphism is a roof K₀ ⟶ M ⟵ L₀ of maps of complexes with the second leg a quasi-isomorphism, and ω is natural along both legs.

theorem tensorOmega_natural_derived (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    {K₀ L₀ : CochainComplex (SheafMod O₀) ℤ}
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    (hL : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (L₀.homology n))
    (ψ : DerivedCategory.Q.obj K₀ ⟶ DerivedCategory.Q.obj L₀) :
    ψ ≫ tensorOmega.{v, u, w, d} hf S L₀ hL =
      tensorOmega.{v, u, w, d} hf S K₀ hK ≫
        (CategoryTheory.shiftFunctor (DerivedCategory (SheafMod O₀)) (2 : ℤ)).map
          ((derivedTensorRight.{d} I).map ψ)

Deformation.ComplexLift.tensorOmegaObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClassDerivedTensor.lean, line 348. The attribute's comment: “the canonical map ω(K₀) : K₀ ⟶ (K₀ ⊗^L I)[2], on an object with bounded above cohomology”.

Stacks 0DIU. Let f : O ⟶ O₀ be a surjection of sheaves of commutative rings on a site whose kernel is an ideal sheaf I of square zero (S). For every object K₀ of D⁻(O₀) -- an object of D(O₀) whose cohomology vanishes in all sufficiently large degrees -- this is the canonical map

ω(K₀) : K₀ ⟶ (K₀ ⊗^L_{O₀} I)[2]

in D(O₀): it is Deformation.ComplexLift.tensorOmega on a complex representing K₀, the curvature of the lifted differential of a bounded above flat lift.

def tensorOmegaObj (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (X : DerivedCategory (SheafMod O₀))
    (hX : ∃ N : ℤ, ∀ n : ℤ, N ≤ n →
      IsZero ((DerivedCategory.homologyFunctor (SheafMod O₀) n).obj X)) :
    X ⟶ ((derivedTensorRight.{d} I).obj X)⟦(2 : ℤ)⟧

Deformation.ComplexLift.tensorOmegaObj_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClassDerivedTensor.lean, line 364. The attribute's comment: “naturality of ω, on objects with bounded above cohomology”.

Stacks 0DIU, naturality of ω. For every map ψ : K₀ ⟶ L₀ in D⁻(O₀) the square

ω(L₀) ∘ ψ = (ψ ⊗^L I)[2] ∘ ω(K₀)

commutes.

theorem tensorOmegaObj_natural (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    {X Y : DerivedCategory (SheafMod O₀)}
    (hX : ∃ N : ℤ, ∀ n : ℤ, N ≤ n →
      IsZero ((DerivedCategory.homologyFunctor (SheafMod O₀) n).obj X))
    (hY : ∃ N : ℤ, ∀ n : ℤ, N ≤ n →
      IsZero ((DerivedCategory.homologyFunctor (SheafMod O₀) n).obj Y))
    (ψ : X ⟶ Y) :
    ψ ≫ tensorOmegaObj.{v, u, w, d} hf S Y hY =
      tensorOmegaObj.{v, u, w, d} hf S X hX ≫
        (CategoryTheory.shiftFunctor (DerivedCategory (SheafMod O₀)) (2 : ℤ)).map
          ((derivedTensorRight.{d} I).map ψ)

Deformation.ComplexLift.tensorOmegaMinus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClassDerivedTensor.lean, line 406. The attribute's comment: “the canonical map ω(K₀) : K₀ ⟶ (K₀ ⊗^L I)[2] for every K₀ in D⁻(O₀)”.

Stacks 0DIU. Let f : O ⟶ O₀ be a surjection of sheaves of commutative rings on a site whose kernel is an ideal sheaf I of square zero (S). For every object K₀ of D⁻(O₀) there is a canonical map

ω(K₀) : K₀ ⟶ (K₀ ⊗^L_{O₀} I)[2]

in D(O₀), where - ⊗^L_{O₀} I is Deformation.ComplexLift.derivedTensorRight I. On a complex representing K₀ it is the curvature d ∘ d of the lifted differential of a bounded above flat lift; its naturality is Deformation.ComplexLift.tensorOmegaMinus_natural.

def tensorOmegaMinus (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (K₀ : DerivedCategory.Minus (SheafMod O₀)) :
    K₀.obj ⟶ ((derivedTensorRight.{d} I).obj K₀.obj)⟦(2 : ℤ)⟧

Deformation.ComplexLift.tensorOmegaMinus_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureClassDerivedTensor.lean, line 417. The attribute's comment: “naturality of ω along every map K₀ ⟶ L₀ in D⁻(O₀)”.

Stacks 0DIU, naturality of ω. For every map ψ : K₀ ⟶ L₀ in D⁻(O₀) the square

ω(L₀) ∘ ψ = (ψ ⊗^L I)[2] ∘ ω(K₀)

in D(O₀) commutes.

theorem tensorOmegaMinus_natural (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    {K₀ L₀ : DerivedCategory.Minus (SheafMod O₀)} (ψ : K₀.obj ⟶ L₀.obj) :
    ψ ≫ tensorOmegaMinus.{v, u, w, d} hf S L₀ =
      tensorOmegaMinus.{v, u, w, d} hf S K₀ ≫
        (CategoryTheory.shiftFunctor (DerivedCategory (SheafMod O₀)) (2 : ℤ)).map
          ((derivedTensorRight.{d} I).map ψ)

Deformation.ComplexLift.emb_coherence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureKernelCoherence.lean, line 187. The attribute's comment: “variant: a morphism of flat lifts carries the kernel identification to the kernel identification, a step of the proof; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, coherence of the kernel identifications. A morphism of flat lifts carries the identification of the ideal part of the source to that of the target. This is the hypothesis hemb of Deformation.ComplexLift.obstructionMap_natural and of Deformation.ComplexLift.obstructionMap_eq_of_hom, and it holds for every pair of identifications, because both are normalized by the same pure-tensor formula Deformation.ComplexLift.IdealKernel.emb_tmul.

theorem emb_coherence (hf : Sheaf.IsLocallySurjective f)
    {L : FlatLift f K₀} {M : FlatLift f L₀} {φ : K₀ ⟶ L₀} (h : FlatLiftHom L M φ)
    (TL : IdealKernel S L) (TM : IdealKernel S M) (n : ℤ) :
    (restrict f).map (((idealTensorFunctor O₀ I).map h.red).f n) ≫ TM.emb n =
      TL.emb n ≫ h.hom n

Deformation.ComplexLift.obstructionMap_eq_of_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureKernelCoherence.lean, line 264. The attribute's comment: “variant: ω depends on the complex alone at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, ω(K₀) does not depend on the flat lift. Given a kernel identification on every bounded above flat lift of K₀ -- no compatibility between them assumed, since Deformation.ComplexLift.emb_coherence supplies it -- the map ω(K₀) computed from any two flat lifts is the same. The comparison that forces the agreement is Deformation.ComplexLift.exists_flatLiftHom_pair, Stacks 0DIT applied to the direct sum of the two lifted families.

theorem obstructionMap_eq_of_lift (hf : Sheaf.IsLocallySurjective f)
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    (kern : ∀ M : FlatLift f K₀, IdealKernel S M) (L L' : FlatLift f K₀) :
    obstructionMap D (kern L) = obstructionMap D (kern L')

Deformation.ComplexLift.exists_flatLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureLiftExistence.lean, line 139. The attribute's comment: “variant: existence of a flat lift of a bounded above complex, a step of the proof; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, existence of a flat lift. A complex of O₀-modules whose cohomology vanishes in sufficiently high degrees admits a bounded above flat lift across a locally surjective f : O ⟶ O₀.

theorem exists_flatLift (hf : Sheaf.IsLocallySurjective f)
    (K₀ : CochainComplex (SheafMod O₀) ℤ)
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n)) :
    Nonempty (FlatLift f K₀)

Deformation.ComplexLift.exists_flatLiftHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureLiftExistence.lean, line 225. The attribute's comment: “variant: lifting a map of complexes to the flat lifts, a step of the proof; the tag is Deformation.ComplexLift.tensorOmegaMinus_natural”.

Stacks 0DIU, lifting a map of complexes. A map φ : K₀ ⟶ L₀ of complexes of O₀-modules, with the cohomology of L₀ vanishing in sufficiently high degrees, is covered by a morphism of flat lifts out of any given bounded above flat lift of K₀.

theorem exists_flatLiftHom (hf : Sheaf.IsLocallySurjective f)
    (L : FlatLift f K₀) (φ : K₀ ⟶ L₀)
    (hL₀ : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (L₀.homology n)) :
    ∃ M : FlatLift f L₀, Nonempty (FlatLiftHom L M φ)

Deformation.ComplexLift.exists_flatLiftHom_pair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureLiftExistence.lean, line 440. The attribute's comment: “variant: two flat lifts of a complex map to a common flat lift, a step of the proof; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, a common enlargement of two flat lifts. Two bounded above flat lifts of the same complex both map to a third one, over the identity. This is the comparison that the well-definedness of the canonical class rests on; it is Stacks 0DIT applied to the direct sum of the two lifted families.

theorem exists_flatLiftHom_pair (hf : Sheaf.IsLocallySurjective f)
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n)) :
    ∃ M : FlatLift f K₀,
      Nonempty (FlatLiftHom L M (𝟙 K₀)) ∧ Nonempty (FlatLiftHom L' M (𝟙 K₀))

Deformation.ComplexLift.exists_flatLift_of_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureLiftExistence.lean, line 488. The attribute's comment: “variant: a flat lift of a derived object with bounded above cohomology, a step of the proof; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, a flat lift for an object of the derived category. An object of D(O₀) with no cohomology above b is represented by a complex of O₀-modules carrying a bounded above flat lift across a locally surjective f : O ⟶ O₀.

theorem exists_flatLift_of_isLE (hf : Sheaf.IsLocallySurjective f) (b : ℤ)
    (E : DerivedCategory (SheafMod O₀)) [E.IsLE b] :
    ∃ K₀ : CochainComplex (SheafMod O₀) ℤ,
      Nonempty (DerivedCategory.Q.obj K₀ ≅ E) ∧ Nonempty (FlatLift f K₀)

Deformation.ComplexLift.exists_flatLift_of_minus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureLiftExistence.lean, line 500. The attribute's comment: “variant: a flat lift of a bounded above derived object, a step of the proof; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, a flat lift for a bounded above object. Every object of D⁻(O₀) is represented by a complex carrying a bounded above flat lift.

theorem exists_flatLift_of_minus (hf : Sheaf.IsLocallySurjective f)
    (E : DerivedCategory.Minus (SheafMod O₀)) :
    ∃ K₀ : CochainComplex (SheafMod O₀) ℤ,
      Nonempty (DerivedCategory.Q.obj K₀ ≅ E.obj) ∧ Nonempty (FlatLift f K₀)

Deformation.ComplexLift.obstructionMap_eq_of_common_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureLiftExistence.lean, line 521. The attribute's comment: “variant: independence of ω of the flat lift through a common enlargement at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, independence of the flat lift. Two flat lifts of the same complex that both map to a third one, compatibly with the kernel identifications, give the same canonical map ω(K₀).

theorem obstructionMap_eq_of_common_lift {L L' M : FlatLift f K₀}
    (h : FlatLiftHom L M (𝟙 K₀)) (h' : FlatLiftHom L' M (𝟙 K₀))
    (TL : IdealKernel S L) (TL' : IdealKernel S L') (TM : IdealKernel S M)
    (hemb : ∀ n : ℤ, (restrict f).map (((idealTensorFunctor O₀ I).map h.red).f n) ≫ TM.emb n =
      TL.emb n ≫ h.hom n)
    (hemb' : ∀ n : ℤ, (restrict f).map (((idealTensorFunctor O₀ I).map h'.red).f n) ≫ TM.emb n =
      TL'.emb n ≫ h'.hom n) :
    obstructionMap D TL = obstructionMap D TL'

Deformation.ComplexLift.obstructionMap_eq_of_coherentKernels, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CurvatureLiftExistence.lean, line 542. The attribute's comment: “variant: ω depends only on the complex at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, the canonical map does not depend on the flat lift. Suppose every bounded above flat lift of K₀ carries a kernel identification, and that these are carried to one another by every morphism of flat lifts over the identity -- which is the assertion that the identifications are the canonical ones, normalized by the pure-tensor formula of Deformation.ComplexLift.IdealKernel.emb_tmul. Then the map ω(K₀) computed from any two flat lifts of K₀ is the same, so ω(K₀) depends on K₀ alone.

The common enlargement that forces the agreement is exists_flatLiftHom_pair, Stacks 0DIT applied to the direct sum of the two lifted families.

theorem obstructionMap_eq_of_coherentKernels (hf : Sheaf.IsLocallySurjective f)
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    (kern : ∀ M : FlatLift f K₀, IdealKernel S M)
    (hcoh : ∀ {A B : FlatLift f K₀} (h : FlatLiftHom A B (𝟙 K₀)) (n : ℤ),
      (restrict f).map (((idealTensorFunctor O₀ I).map h.red).f n) ≫ (kern B).emb n =
        (kern A).emb n ≫ h.hom n)
    (L L' : FlatLift f K₀) :
    obstructionMap D (kern L) = obstructionMap D (kern L')

Deformation.ComplexLift.nonempty_idealKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealKernelExistence.lean, line 379. The attribute's comment: “variant: the ideal part of a flat lift is the kernel of its reduction, a step of the proof; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU. Every bounded above flat lift carries an identification of its ideal part with the kernel of its reduction, normalized by the pure-tensor formula x̄ ⊗ a ↦ a · x.

The identification is Deformation.ComplexLift.idealKernel; this is its existence statement, which is what the independence argument consumes.

theorem nonempty_idealKernel (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (L : FlatLift f K₀) : Nonempty (IdealKernel S L)

Deformation.ComplexLift.obstructionMap_eq_of_lift', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealKernelExistence.lean, line 448. The attribute's comment: “variant: independence of the flat lift at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU, ω(K₀) depends on the complex alone. Any two bounded above flat lifts of K₀, with any kernel identifications on them, compute the same map.

theorem obstructionMap_eq_of_lift' (hf : Sheaf.IsLocallySurjective f)
    (S : SquareZeroIdeal f I) (D : DerivedIdealTensor I)
    {K₀ : CochainComplex (SheafMod O₀) ℤ}
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    {L L' : FlatLift f K₀} (T : IdealKernel S L) (T' : IdealKernel S L') :
    obstructionMap D T = obstructionMap D T'

Deformation.ComplexLift.omega, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealKernelExistence.lean, line 473. The attribute's comment: “variant: the map ω(K₀) of a bounded above complex at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU. The canonical map ω(K₀) : K₀ ⟶ (K₀ ⊗^L_{O₀} I)[2] attached to a square-zero extension f : O ⟶ O₀ of sheaves of rings with ideal sheaf I, as a function of the bounded above complex K₀ alone: it is the curvature of the lifted differential of any bounded above flat lift of K₀, read through the canonical identification of the ideal part of that lift with the kernel of its reduction.

The kernel identification is not chosen: it is Deformation.ComplexLift.idealKernel, built from the lift. The lift itself is chosen -- Deformation.ComplexLift.exists_flatLift -- and that is irreducible here, because the bound the lifting construction is indexed by is available only inside the propositional hypothesis hK. That the choice does not matter is Deformation.ComplexLift.obstructionMap_eq_of_lift', and Deformation.ComplexLift.omega_eq computes ω(K₀) from any lift and any kernel identification, so nothing about ω(K₀) is hidden by it.

def omega (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (D : DerivedIdealTensor I) (K₀ : CochainComplex (SheafMod O₀) ℤ)
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n)) :
    DerivedCategory.Q.obj K₀ ⟶ (D.functor.obj (DerivedCategory.Q.obj K₀))⟦(2 : ℤ)⟧

Deformation.ComplexLift.omega_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealKernelExistence.lean, line 483. The attribute's comment: “variant: ω is computed by any flat lift at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU. The canonical map is computed by any bounded above flat lift and any kernel identification on it.

theorem omega_eq (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (D : DerivedIdealTensor I) {K₀ : CochainComplex (SheafMod O₀) ℤ}
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    {L : FlatLift f K₀} (T : IdealKernel S L) :
    omega hf S D K₀ hK = obstructionMap D T

Deformation.ComplexLift.omega_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealKernelExistence.lean, line 497. The attribute's comment: “variant: naturality of ω along a map of complexes at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus_natural”.

Stacks 0DIU, naturality of ω. For a map φ : K₀ ⟶ L₀ of bounded above complexes of O₀-modules the square formed by ω(K₀), ω(L₀) and the maps induced by φ commutes. No compatibility of lifts is assumed: the lift of φ is Deformation.ComplexLift.exists_flatLiftHom and the lift-independence is Deformation.ComplexLift.omega_eq.

theorem omega_natural (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (D : DerivedIdealTensor I) {K₀ L₀ : CochainComplex (SheafMod O₀) ℤ} (φ : K₀ ⟶ L₀)
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    (hL : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (L₀.homology n)) :
    DerivedCategory.Q.map φ ≫ omega hf S D L₀ hL =
      omega hf S D K₀ hK ≫
        (CategoryTheory.shiftFunctor (DerivedCategory (SheafMod O₀)) (2 : ℤ)).map
          (D.functor.map (DerivedCategory.Q.map φ))

Deformation.ComplexLift.omega_natural_derived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealKernelExistence.lean, line 521. The attribute's comment: “variant: naturality of ω along a derived map at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus_natural”.

Stacks 0DIU, naturality of ω for an arbitrary morphism of the derived category. For any ψ : K₀ ⟶ L₀ in D(O₀) between bounded above complexes -- not merely one coming from a map of complexes -- the square formed by ω(K₀), ω(L₀) and the maps induced by ψ commutes.

Every such ψ is a roof K₀ ⟶ M ⟵ L₀ of maps of complexes with the second leg a quasi-isomorphism (Deformation.ComplexLift.exists_roof_of_derived_hom), so this follows from naturality along maps of complexes applied to the two legs.

theorem omega_natural_derived (hf : Sheaf.IsLocallySurjective f) (S : SquareZeroIdeal f I)
    (D : DerivedIdealTensor I) {K₀ L₀ : CochainComplex (SheafMod O₀) ℤ}
    (hK : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (K₀.homology n))
    (hL : ∃ N : ℤ, ∀ n : ℤ, N ≤ n → IsZero (L₀.homology n))
    (ψ : DerivedCategory.Q.obj K₀ ⟶ DerivedCategory.Q.obj L₀) :
    ψ ≫ omega hf S D L₀ hL =
      omega hf S D K₀ hK ≫
        (CategoryTheory.shiftFunctor (DerivedCategory (SheafMod O₀)) (2 : ℤ)).map
          (D.functor.map ψ)

Deformation.ComplexLift.obstructionMap_eq_of_hom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/IdealKernelNaturality.lean, line 187. The attribute's comment: “variant: independence of the flat lift at a supplied derived ideal tensor datum D; the tag is Deformation.ComplexLift.tensorOmegaMinus”.

Stacks 0DIU. Two flat lifts of the same complex joined by a morphism of flat lifts over the identity give the same canonical class ω(K₀). No compatibility of the ideal parts is assumed: it is automatic.

theorem obstructionMap_eq_of_hom' [HasDerivedCategory.{d} (SheafMod O₀)]
    (D : DerivedIdealTensor I) (hf : Sheaf.IsLocallySurjective f) {L M : FlatLift f K₀}
    (h : FlatLiftHom L M (𝟙 K₀)) (TL : IdealKernel S L) (TM : IdealKernel S M) :
    obstructionMap D TL = obstructionMap D TM

Tag 0DIV, a lemma

Tag 0DIV in the Stacks Project.

Stacks.DerivedTensor.RingedSite.isIso_homologyMap_derivedTensorSingle_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/CohomologyAboveADegree.lean, line 132. The attribute's comment: “tensoring keeps the isomorphisms above the degree”.

Stacks 0DIV (2), the isomorphisms. If H^i(α) is an isomorphism in every degree > n and a surjection in degree n, then H^i(α ⊗_O^{L} 1_F) is an isomorphism in every degree > n.

theorem isIso_homologyMap_derivedTensorSingle_of_epi
    {K L : DerivedModules R} (α : K ⟶ L) (F : Modules R) (n : ℤ)
    (hiso : ∀ i : ℤ, n < i → IsIso ((DerivedCategory.homologyFunctor (Modules R) i).map α))
    (hepi : Epi ((DerivedCategory.homologyFunctor (Modules R) n).map α))
    (i : ℤ) (hi : n < i) :
    IsIso ((DerivedCategory.homologyFunctor (Modules R) i).map
      ((derivedTensorSingle R F).map α))

Stacks.DerivedTensor.RingedSite.epi_homologyMap_derivedTensorSingle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/CohomologyAboveADegree.lean, line 144. The attribute's comment: “tensoring keeps the surjection in the degree”.

Stacks 0DIV (2), the surjection. If H^i(α) is an isomorphism in every degree > n and a surjection in degree n, then H^n(α ⊗_O^{L} 1_F) is a surjection.

theorem epi_homologyMap_derivedTensorSingle
    {K L : DerivedModules R} (α : K ⟶ L) (F : Modules R) (n : ℤ)
    (hiso : ∀ i : ℤ, n < i → IsIso ((DerivedCategory.homologyFunctor (Modules R) i).map α))
    (hepi : Epi ((DerivedCategory.homologyFunctor (Modules R) n).map α)) :
    Epi ((DerivedCategory.homologyFunctor (Modules R) n).map
      ((derivedTensorSingle R F).map α))

Stacks.DerivedTensor.RingedSite.isIso_homologyMap_derivedTensorSingle_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/CohomologyAboveADegree.lean, line 163. The attribute's comment: “tensoring keeps the isomorphisms in all degrees at least the bound”.

Stacks 0DIV (1). If H^i(α) is an isomorphism in every degree ≥ n, then so is H^i(α ⊗_O^{L} 1_F).

Above n this is part (2). In degree n surjectivity is again part (2), and injectivity comes from the vanishing of the connecting map H^{n-1}(C ⊗^{L} F) ⟶ H^n(K ⊗^{L} F) of the tensored triangle, equivalently from surjectivity of H^{n-1}(L ⊗^{L} F) ⟶ H^{n-1}(C ⊗^{L} F). That is part (2) applied in degree n - 1 to τ^{<n} L ⟶ L ⟶ C: this composite is surjective on H^{n-1} — the truncation map is an isomorphism there and H^{n-1}(L) ⟶ H^{n-1}(C) is surjective because H^n(α) is injective — and it is an isomorphism on cohomology above n - 1 for the trivial reason that both its source and its target vanish there.

theorem isIso_homologyMap_derivedTensorSingle_of_isIso
    {K L : DerivedModules R} (α : K ⟶ L) (F : Modules R) (n : ℤ)
    (hα : ∀ i : ℤ, n ≤ i → IsIso ((DerivedCategory.homologyFunctor (Modules R) i).map α))
    (i : ℤ) (hi : n ≤ i) :
    IsIso ((DerivedCategory.homologyFunctor (Modules R) i).map
      ((derivedTensorSingle R F).map α))

Tag 0DIW, a lemma

Tag 0DIW in the Stacks Project.

Deformation.ComplexLift.obstructionMap_eq_zero_of_dd_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/FlatRepresentative.lean, line 188. The attribute's comment: “(2) implies (1), at a flat lift whose lifted differential squares to zero”.

Stacks 0DIW, the implication (2) ⇒ (1), at a flat lift whose differential squares to zero. If the lifted differential of a flat lift of K₀ already squares to zero — that is, if K₀ is the reduction of a bounded above complex of flat O-modules — then the class computed by that lift vanishes.

The curvature of such a lift is the zero map, because zero satisfies the characterization of the curvature; and ω(K₀) is the curvature transported along isomorphisms. The implication for an arbitrary K ∈ D⁻(O) with K ⊗^L_O O₀ ≅ K₀ is Deformation.ComplexLift.omega_eq_zero_of_nonempty_derivedLift, and the full equivalence of Tag 0DIW is Deformation.ComplexLift.omega_eq_zero_iff_nonempty_derivedLift.

theorem obstructionMap_eq_zero_of_dd_eq_zero (D : DerivedIdealTensor I) :
    obstructionMap D T = 0

Deformation.ComplexLift.omega_eq_zero_iff_nonempty_derivedLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ObstructionLiftCriterion.lean, line 356.

Stacks 0DIW. Let C be a site and f : O ⟶ O₀ a surjection of sheaves of commutative rings whose kernel is an ideal sheaf I of square zero. For every object K₀ of D⁻(O₀), represented by a complex K₀' of O₀-modules, the following are equivalent:

the canonical class ω(K₀) : K₀ ⟶ (K₀ ⊗^L_{O₀} I)[2] of Tag 0DIU, computed on K₀', is zero;

there exists K ∈ D⁻(O) with K ⊗^L_O O₀ ≅ K₀ in D(O₀).

Here T is any derived base change - ⊗^L_O O₀ (all are canonically isomorphic) and D the derived tensor product with I against which the base states ω. The bound on the cohomology of K₀' that ω is stated with is the one K₀ ∈ D⁻(O₀) provides, Deformation.ComplexLift.homology_boundedAbove_of_iso.

theorem omega_eq_zero_iff_nonempty_derivedLift (hf : Sheaf.IsLocallySurjective f)
    (S : SquareZeroIdeal f I) (D : DerivedIdealTensor I) (T : DerivedExtensionOfScalars f)
    (E : DerivedCategory.Minus (SheafMod O₀)) (K₀ : CochainComplex (SheafMod O₀) ℤ)
    (e : DerivedCategory.Q.obj K₀ ≅ E.obj) :
    omega hf S D K₀ (homology_boundedAbove_of_iso E e) = 0 ↔ Nonempty (DerivedLift T E)

Tag 0DIX, a lemma

Tag 0DIX in the Stacks Project.

Deformation.ComplexLift.exists_quasiIso_with_extensionOfScalars_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/ComplexMapLift.lean, line 316.

A quasi-isomorphism to the extension of scalars of F can be lifted, after replacing F by a quasi-isomorphic complex, to a factorization in the homotopy category.

theorem exists_quasiIso_with_extensionOfScalars_factorization
    [HasSheafify J AddCommGrpCat.{u}]
    [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [Epi f]
    (F : CochainComplex (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O)))) ℤ)
    (K₀ : CochainComplex (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O₀)))) ℤ)
    (q : K₀ ⟶ (extensionOfScalarsCochainComplex J f).obj F)
    (hq : QuasiIso q) :
    ∃ (G : CochainComplex (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O)))) ℤ)
      (g : G ⟶ F),
      QuasiIso g ∧
    (∃ h :
          (HomotopyCategory.quotient
              (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O₀))))
              (ComplexShape.up ℤ)).obj
                ((extensionOfScalarsCochainComplex J f).obj G) ⟶
            (HomotopyCategory.quotient
                (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O₀))))
              (ComplexShape.up ℤ)).obj K₀,
          (HomotopyCategory.quotient
              (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O₀))))
                (ComplexShape.up ℤ)).map
              ((extensionOfScalarsCochainComplex J f).map g) =
            h ≫
              (HomotopyCategory.quotient
                  (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O₀))))
                (ComplexShape.up ℤ)).map q)

Tag 0DIY, a lemma

Tag 0DIY in the Stacks Project.

Deformation.ComplexLift.DerivedReduction.liftObstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedLiftObstruction.lean, line 142. The attribute's comment: “the obstruction class of a morphism of reductions”.

Stacks 0DIY. The obstruction to lifting a morphism α₀ : K₁ ⊗^L O₀ ⟶ K₂ ⊗^L O₀ of reductions to a morphism K₁ ⟶ K₂: the composite of the unit of the adjunction with α₀ and the connecting morphism of the reduction triangle of K₂, a morphism K₁ ⟶ (K₂ ⊗^L I)⟦1⟧.

noncomputable def liftObstruction
    (K₁ K₂ : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O)))))
    (α₀ : T.baseChange.obj K₁ ⟶ T.baseChange.obj K₂) :
    K₁ ⟶ (R.restriction.obj (idealTensor.obj (T.baseChange.obj K₂)))⟦(1 : ℤ)⟧

Deformation.ComplexLift.DerivedReduction.liftObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedLiftObstruction.lean, line 155. The attribute's comment: “the vanishing criterion”.

Stacks 0DIY. The obstruction class of α₀ vanishes exactly when α₀ is the derived base change of a morphism K₁ ⟶ K₂. The forward implication is exactness of Hom(K₁, -) at the third vertex of the reduction triangle of K₂, followed by the universal property of the unit; the converse is the vanishing of the composite of the last two morphisms of that triangle.

theorem liftObstruction_eq_zero_iff
    (K₁ K₂ : DerivedCategory (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O)))))
    (α₀ : T.baseChange.obj K₁ ⟶ T.baseChange.obj K₂) :
    R.liftObstruction K₁ K₂ α₀ = 0 ↔ ∃ a : K₁ ⟶ K₂, T.baseChange.map a = α₀

Deformation.ComplexLift.DerivedReduction.extLiftObstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedLiftObstruction.lean, line 212. The attribute's comment: “the obstruction class in Ext¹”.

Stacks 0DIY. The obstruction class o(α₀) of a morphism α₀ : K₀ ⟶ L₀ of reductions as an element of Ext¹_{O₀}(K₀, L₀ ⊗^L_{O₀} I), the group the tag states it in: Deformation.ComplexLift.DerivedReduction.liftObstruction read through the adjunction.

noncomputable def extLiftObstruction
    (K₁ K₂ : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (α₀ : T.baseChange.obj K₁ ⟶ T.baseChange.obj K₂) :
    T.baseChange.obj K₁ ⟶ (idealTensor.obj (T.baseChange.obj K₂))⟦(1 : ℤ)⟧

Deformation.ComplexLift.DerivedReduction.extLiftObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedLiftObstruction.lean, line 234. The attribute's comment: “the vanishing criterion in Ext¹”.

Stacks 0DIY. The obstruction class in Ext¹_{O₀}(K₀, L₀ ⊗^L_{O₀} I) vanishes exactly when α₀ is the derived base change of a morphism K₁ ⟶ K₂: the identification of that group with the group of morphisms K₁ ⟶ ((L₀ ⊗^L_{O₀} I)|_O)⟦1⟧ is an isomorphism, so it reflects vanishing from Deformation.ComplexLift.DerivedReduction.liftObstruction_eq_zero_iff.

theorem extLiftObstruction_eq_zero_iff
    (K₁ K₂ : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (α₀ : T.baseChange.obj K₁ ⟶ T.baseChange.obj K₂) :
    R.extLiftObstruction K₁ K₂ α₀ = 0 ↔ ∃ a : K₁ ⟶ K₂, T.baseChange.map a = α₀

Deformation.ComplexLift.squareZeroObstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroDerivedObstruction.lean, line 278. The attribute's comment: “the obstruction class o(α₀) in Ext¹_{O₀}(K₀, L₀ ⊗^L_{O₀} I)”.

Stacks 0DIY, the obstruction class. Let f : O ⟶ O₀ be a surjection of sheaves of commutative rings whose kernel I has square zero, let K, L ∈ D⁻(O), and write K₀ = K ⊗^L_O O₀, L₀ = L ⊗^L_O O₀ for their derived base changes. For a morphism α₀ : K₀ ⟶ L₀ in D(O₀) this is the class o(α₀) ∈ Ext¹_{O₀}(K₀, L₀ ⊗^L_{O₀} I) = Hom_{D(O₀)}(K₀, (L₀ ⊗^L_{O₀} I)⟦1⟧): the composite K ⟶ K₀ ⟶ L₀ ⟶ (L ⊗^L_O I)⟦1⟧ of the unit, α₀ and the connecting morphism of the reduction triangle of L, read through the adjunction.

def squareZeroObstruction
    (K L : DerivedCategory.Minus (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (α₀ : (derivedExtensionOfScalars.{d, d₀} f).obj K.obj ⟶
      (derivedExtensionOfScalars.{d, d₀} f).obj L.obj) :
    (derivedExtensionOfScalars.{d, d₀} f).obj K.obj ⟶
      ((derivedTensorRight.{d₀, u, u, u'} (squareZeroIdeal.{u, u, u'} f hf hsq)).obj
        ((derivedExtensionOfScalars.{d, d₀} f).obj L.obj))⟦(1 : ℤ)⟧

Deformation.ComplexLift.squareZeroObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroDerivedObstruction.lean, line 290. The attribute's comment: “o(α₀) = 0 iff α₀ = α ⊗^L_O id for some α : K → L in D(O)”.

Stacks 0DIY. The obstruction class o(α₀) vanishes if and only if α₀ is the derived base change α ⊗^L_O id of a morphism α : K ⟶ L in D(O).

theorem squareZeroObstruction_eq_zero_iff
    (K L : DerivedCategory.Minus (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (α₀ : (derivedExtensionOfScalars.{d, d₀} f).obj K.obj ⟶
      (derivedExtensionOfScalars.{d, d₀} f).obj L.obj) :
    squareZeroObstruction f hf hsq K L α₀ = 0 ↔
      ∃ α : K.obj ⟶ L.obj, (derivedExtensionOfScalars.{d, d₀} f).map α = α₀

Deformation.ComplexLift.squareZeroObstructionMinus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroDerivedObstruction.lean, line 305. The attribute's comment: “the obstruction class o(α₀) in Ext¹_{O₀}(K₀, L₀ ⊗^L_{O₀} I), with K₀ and L₀ in D⁻(O₀)”.

Stacks 0DIY, the obstruction class, with K₀ and L₀ in D⁻(O₀). For K, L ∈ D⁻(O) the derived base changes K₀ = K ⊗^L_O O₀ and L₀ = L ⊗^L_O O₀ are bounded above (Deformation.ComplexLift.DerivedExtensionOfScalars.baseChangeMinus), and a morphism α₀ : K₀ ⟶ L₀ of D⁻(O₀) has the class o(α₀) ∈ Ext¹_{O₀}(K₀, L₀ ⊗^L_{O₀} I) of Deformation.ComplexLift.squareZeroObstruction.

def squareZeroObstructionMinus
    (K L : DerivedCategory.Minus (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (α₀ : (derivedExtensionOfScalarsData.{d, d₀} f).baseChangeMinus.obj K ⟶
      (derivedExtensionOfScalarsData.{d, d₀} f).baseChangeMinus.obj L) :
    ((derivedExtensionOfScalarsData.{d, d₀} f).baseChangeMinus.obj K).obj ⟶
      ((derivedTensorRight.{d₀, u, u, u'} (squareZeroIdeal.{u, u, u'} f hf hsq)).obj
        ((derivedExtensionOfScalarsData.{d, d₀} f).baseChangeMinus.obj L).obj)⟦(1 : ℤ)⟧

Deformation.ComplexLift.squareZeroObstructionMinus_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroDerivedObstruction.lean, line 319. The attribute's comment: “o(α₀) = 0 iff α₀ = α ⊗^L_O id for some α : K → L, with K₀, L₀ in D⁻(O₀)”.

Stacks 0DIY, with K₀ and L₀ in D⁻(O₀). The obstruction class of a morphism α₀ : K₀ ⟶ L₀ of D⁻(O₀) vanishes if and only if α₀ = α ⊗^L_O id for a morphism α : K ⟶ L of D⁻(O), the functor - ⊗^L_O O₀ : D⁻(O) ⥤ D⁻(O₀) being Deformation.ComplexLift.DerivedExtensionOfScalars.baseChangeMinus.

theorem squareZeroObstructionMinus_eq_zero_iff
    (K L : DerivedCategory.Minus (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (α₀ : (derivedExtensionOfScalarsData.{d, d₀} f).baseChangeMinus.obj K ⟶
      (derivedExtensionOfScalarsData.{d, d₀} f).baseChangeMinus.obj L) :
    squareZeroObstructionMinus f hf hsq K L α₀ = 0 ↔
      ∃ α : K ⟶ L, (derivedExtensionOfScalarsData.{d, d₀} f).baseChangeMinus.map α = α₀

Tag 0DIZ, a lemma

Tag 0DIZ in the Stacks Project.

Deformation.ComplexLift.DerivedLift, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedComplexLift.lean, line 115. The attribute's comment: “a lift of a bounded above derived complex”.

Stacks 0DIZ. A lift of a bounded above object K₀ of the derived category of O₀-modules across the derived base change T along f : O ⟶ O₀: a bounded above object K of the derived category of O-modules together with an isomorphism K ⊗_O^L O₀ ≅ K₀ in the derived category of O₀-modules.

structure DerivedLift (T : DerivedExtensionOfScalars f)
    (K₀ : DerivedCategory.Minus
      (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O₀)))))

Deformation.ComplexLift.automorphismsOfLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedLiftAutomorphisms.lean, line 137. The attribute's comment: “the automorphism group of a lift”.

Stacks 0DIZ. The automorphisms of a lift (K, α) of K₀: the automorphisms of K whose derived base change is the identity. Since α is an isomorphism these are exactly the automorphisms of the pair, and the subgroup does not depend on α.

noncomputable def automorphismsOfLift (T : DerivedExtensionOfScalars f)
    {K₀ :
      DerivedCategory.Minus (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (O₀))))}
    (L : DerivedLift T K₀) : Subgroup (Aut L.K.obj)

Deformation.ComplexLift.boundary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedLiftAutomorphisms.lean, line 319. The attribute's comment: “part (1): the map whose cokernel the automorphism group is”.

Stacks 0DIZ. The canonical map Ext⁻¹(K₀, K₀) ⟶ Hom(K₀, K₀ ⊗^L I): the connecting map of the reduction triangle of K, read in the two groups of the source through the adjunction and the identification α.

noncomputable def boundary :
    (K₀.obj ⟶ K₀.obj⟦(-1 : ℤ)⟧) →+ (K₀.obj ⟶ idealTensor.obj K₀.obj)

Deformation.ComplexLift.automorphismsOfLiftMulEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/DerivedLiftAutomorphisms.lean, line 382. The attribute's comment: “part (1): the automorphisms of a lift are a cokernel”.

Stacks 0DIZ (1). The automorphisms of a lift (K, α) of K₀ form the cokernel of the canonical map Ext⁻¹(K₀, K₀) ⟶ Hom(K₀, K₀ ⊗^L I).

noncomputable def automorphismsOfLiftMulEquiv :
    Multiplicative (K₀.obj ⟶ idealTensor.obj K₀.obj) ⧸
        AddSubgroup.toSubgroup (boundary R L).range ≃* automorphismsOfLift T L

Deformation.ComplexLift.squareZeroFlatLiftBoundary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroLiftTorsor.lean, line 79. The attribute's comment: “(1), the map Ext⁻¹(K₀, K₀) → Hom(K₀, K₀ ⊗^L I)”.

Stacks 0DIZ (1), the map. For a lift (K, α) of K₀ ∈ D⁻(O₀) across the square-zero surjection f, the canonical map

Ext⁻¹_{O₀}(K₀, K₀) ⟶ Hom_{O₀}(K₀, K₀ ⊗^L_{O₀} I)

whose cokernel the automorphism group of (K, α) is: the connecting map of the reduction triangle K ⊗^L_O I ⟶ K ⟶ K ⊗^L_O O₀ ⟶ (K ⊗^L_O I)⟦1⟧ of f (computed by a flat resolution), read through the adjunction between derived base change and restriction of scalars and through α.

def squareZeroFlatLiftBoundary (L : DerivedLift (derivedExtensionOfScalarsData.{d, d₀} f) K₀) :
    (K₀.obj ⟶ K₀.obj⟦(-1 : ℤ)⟧) →+
      (K₀.obj ⟶ (derivedTensorRight.{d₀} (squareZeroIdeal f hf hsq)).obj K₀.obj)

Deformation.ComplexLift.squareZeroFlatLiftAutEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroLiftTorsor.lean, line 91. The attribute's comment: “(1)”.

Stacks 0DIZ (1). Let f : O ⟶ O₀ be a surjection of sheaves of commutative rings on a site whose kernel I is an ideal of square zero, let K₀ ∈ D⁻(O₀) and let (K, α) be a lift of K₀, i.e. K ∈ D⁻(O) with α : K ⊗^L_O O₀ ≅ K₀ in D(O₀). Then the group of automorphisms of the pair (K, α) is canonically the cokernel of the map Ext⁻¹_{O₀}(K₀, K₀) ⟶ Hom_{O₀}(K₀, K₀ ⊗^L_{O₀} I) of Deformation.ComplexLift.squareZeroFlatLiftBoundary.

def squareZeroFlatLiftAutEquiv (L : DerivedLift (derivedExtensionOfScalarsData.{d, d₀} f) K₀) :
    Multiplicative (K₀.obj ⟶
        (derivedTensorRight.{d₀} (squareZeroIdeal f hf hsq)).obj K₀.obj) ⧸
        AddSubgroup.toSubgroup (squareZeroFlatLiftBoundary.{d, d₀} f hf hsq L).range ≃*
      automorphismsOfLift (derivedExtensionOfScalarsData.{d, d₀} f) L

Deformation.ComplexLift.exists_addTorsor_squareZeroLifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SquareZeroLiftTorsor.lean, line 106. The attribute's comment: “(2)”.

Stacks 0DIZ (2). Let f : O ⟶ O₀ be a surjection of sheaves of commutative rings on a site whose kernel I is an ideal of square zero, and let K₀ ∈ D⁻(O₀). If K₀ has a lift (K, α), K ∈ D⁻(O), α : K ⊗^L_O O₀ ≅ K₀, then the set of isomorphism classes of lifts of K₀ is principal homogeneous under Ext¹_{O₀}(K₀, K₀ ⊗^L_{O₀} I): there is a free and transitive action of that group on it under which ξ carries the class of (K', α') to the class of (K'', α'') exactly when ξ is the obstruction class of Stacks 0DIY of the comparison α'' ∘ α'⁻¹ of the two lifts.

theorem exists_addTorsor_squareZeroLifts
    [Nonempty (DerivedLift (derivedExtensionOfScalarsData.{d, d₀} f) K₀)] :
    ∃ τ : AddTorsor (K₀.obj ⟶
        ((derivedTensorRight.{d₀} (squareZeroIdeal f hf hsq)).obj K₀.obj)⟦(1 : ℤ)⟧)
        (Quotient (DerivedLift.setoid (T := derivedExtensionOfScalarsData.{d, d₀} f) (K₀ := K₀))),
      ∀ (ξ : K₀.obj ⟶ ((derivedTensorRight.{d₀} (squareZeroIdeal f hf hsq)).obj K₀.obj)⟦(1 : ℤ)⟧)
        (L' L'' : DerivedLift (derivedExtensionOfScalarsData.{d, d₀} f) K₀),
        τ.vadd ξ ⟦L'⟧ = ⟦L''⟧ ↔
          liftDifference (squareZeroFlatReduction.{d, d₀} f hf hsq) L'' L' = ξ

Sources

LeanStacks.SheafOfModules.ComplexLifting.exists_liftedComplex · Deformation.ComplexLift.unit_comp_curvature · Deformation.ComplexLift.obstructionMap · Deformation.ComplexLift.obstructionMap_natural · Deformation.ComplexLift.obstructionMap_eq_of_hom · Deformation.ComplexLift.tensorOmega · Deformation.ComplexLift.tensorOmega_natural_derived · Deformation.ComplexLift.tensorOmegaObj

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

91.10 Modules on first order… to 91.16 Deformations of complexes…

Section91.10 Modules on first order thickenings of ringed topoi#

Tag 08MB, an equation

Tag 08MC, a lemma

Tag 08MD, a lemma

Tag 08ME, a lemma

Tag 08MF, a lemma

Tag 08MG, a remark

Tag 08MI, a remark

Tag 08MJ, a remark

Tag 08MK, a remark

Tag 0CYC, a remark

Tag 08ML, a remark

Tag 08MM, a remark

Sources

Section91.11 Infinitesimal deformations of modules on ringed topoi#

Tag 08MP, a lemma

Tag 08MQ, a lemma

Tag 08VU, a lemma

Tag 08MR, a lemma

Tag 08MS, a lemma

Tag 08MT, a lemma

Tag 08MU, a lemma

Tag 08MV, a lemma

Sources

Section91.12 Application to flat modules on flat thickenings of ringed topoi#

Tag 08VW, a lemma

Tag 0CYD, a situation

Tag 0CYE, a lemma

Tag 08VX, a situation

Tag 08VY, a lemma

Sources

Section91.13 Deformations of ringed topoi and the naive cotangent complex#

Tag 08UF, an equation

Tag 08UG, a lemma

Tag 08UH, an equation

Tag 08UI, an equation

Tag 08UJ, a lemma

Tag 08UK, a lemma

Tag 0GQ5, a lemma

Tag 0GQ6, a remark

Tag 0GQ7, a lemma

Tag 0GQ8, a remark

Tag 0GQ9, a lemma

Sources

Section91.14 Deformations of algebraic spaces#

Tag 0D16, a lemma

Tag 0D17, a lemma

Tag 0D3P, a lemma

Tag 0D3Q, a lemma

Sources

Section91.15 Deformations of complexes#

Tag 0DYR, a lemma

Sources

Section91.16 Deformations of complexes on ringed topoi#

Tag 0DIT, a lemma

Tag 0DIU, a lemma

Tag 0DIV, a lemma

Tag 0DIW, a lemma

Tag 0DIX, a lemma

Tag 0DIY, a lemma

Tag 0DIZ, a lemma

Sources

Section91.10 Modules on first order thickenings of ringed topoi #

Section91.11 Infinitesimal deformations of modules on ringed topoi #

Section91.12 Application to flat modules on flat thickenings of ringed topoi #

Section91.13 Deformations of ringed topoi and the naive cotangent complex #

Section91.14 Deformations of algebraic spaces #

Section91.15 Deformations of complexes #

Section91.16 Deformations of complexes on ringed topoi #