91.2 Deformations of rings and… to 91.9 Thickenings of ringed topoi

Section91.2 Deformations of rings and the naive cotangent complex #

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

Tag 08S4, an equation

Tag 08S4 in the Stacks Project.

Stacks.Deformation.SquareZeroExtensionProblem.CompatibleExtension, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/Problem.lean, line 107.

A solution of a square-zero extension problem.

The map toB and its kernel give the exact upper row 0 → N → B' → B → 0; kernelEquiv supplies the displayed identification with N, and map_I says that the left square is the prescribed map c.

public structure CompatibleExtension (S : SquareZeroExtensionProblem)

Tag 08S5, a lemma

Tag 08S5 in the Stacks Project.

Deformation.RingThickening.fittingMap_addTorsor_kaehlerDifferentialHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/FittingMapTorsor.lean, line 432. The attribute's comment: “torsor”. References: EGA IV (16.5.17), “special case”; SGA 1 III (5.3), “special case”; SGA 3 III (0.1.8), “(a), special case”.

If a map filling a compatible square-zero deformation diagram exists, all such maps form a principal homogeneous space under Hom_{B₁}(Ω_{B₁/A₁}, N₂). Subtracting two fitting maps gives the unique differential map whose value on d b is the difference of their values on any lift of b.

theorem fittingMap_addTorsor_kaehlerDifferentialHom
    (D : CompatibleSquareZeroDeformationDiagram.{u₁, u₂, u₃, u₄,
      v₁, v₂, v₃, v₄, w₁, w₂})
    (h : Nonempty D.FittingMap) :
    Nonempty
      {t : AddTorsor
          (KaehlerDifferential D.S₁.A D.S₁.B →ₗ[D.S₁.B] D.S₂.N)
          D.FittingMap //
        letI : AddTorsor
            (KaehlerDifferential D.S₁.A D.S₁.B →ₗ[D.S₁.B] D.S₂.N)
            D.FittingMap := t
        ∀ (φ ψ : D.FittingMap) (b' : D.X₁.B'),
          ((D.X₂.kernelEquiv
            ((φ -ᵥ ψ) (KaehlerDifferential.D D.S₁.A D.S₁.B (D.X₁.toB b'))) :
              RingHom.ker D.X₂.toB.toRingHom) : D.X₂.B') =
            φ.toRingHom b' - ψ.toRingHom b'}

Stacks.Deformation.obstructionClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/Obstruction/ObstructionClass.lean, line 518. The attribute's comment: “obstruction”.

The canonical obstruction to filling a compatible square-zero deformation diagram.

Its value lies in Ext¹_{B₁}(NL_{B₁/A₁}, N₂). The subtype records the characteristic property of the obstruction: it is zero precisely when a fitting map B'₁ → B'₂ exists.

public def obstructionClass
    (D : CompatibleSquareZeroDeformationDiagram.{u₁, u₂, u₃, u₄,
      v₁, v₂, v₃, v₄, w₁, w₂}) :
    let K := ((ModuleCat.uliftFunctor.{v₄} D.S₁.B).mapHomologicalComplex
      (ComplexShape.down ℕ)).obj (Algebra.naiveCotangentComplex D.S₁.A D.S₁.B)
    {o : DerivedCategory.Ext
        (DerivedCategory.Q.obj
          (HomologicalComplex.double (K.d 1 0)
            (show (ComplexShape.up ℤ).Rel (-1) 0 from rfl)))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₂ u₃ v₄} D.S₁.B) 0).obj
          ((ModuleCat.uliftFunctor.{max u₂ u₃} D.S₁.B).obj
            (ModuleCat.of D.S₁.B D.S₂.N))) 1 //
      o = 0 ↔ Nonempty D.FittingMap}

Tag 08S7, a lemma

Tag 08S7 in the Stacks Project.

Stacks.Deformation.isomorphismClassesTorsor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/Torsor/IsomorphismClasses.lean, line 440. References: SGA 7 VI (4.16), “(b), affine case”.

If a square-zero extension problem has a solution, this is the canonical principal homogeneous-space structure on its isomorphism classes under Ext¹_B(NL_{B/A}, N).

public noncomputable def isomorphismClassesTorsor
    (S : SquareZeroExtensionProblem.{u₁, u₂, u₃, u₄})
    (h : Nonempty (SquareZeroExtensionProblem.CompatibleExtension.{v} S)) :
    AddTorsor (naiveCotangentExtOne S.A S.B S.N)
      (SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{u₁, u₂, u₃, u₄, v}
        S)

Stacks.Deformation.isomorphismClasses_vsub_eq_obstructionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/Torsor/IsomorphismClasses.lean, line 455. The attribute's comment: “canonical difference”.

In the canonical torsor of solutions, the difference [Y] -ᵥ [X] is the obstruction class o(X, Y) to a map from X to Y.

public theorem isomorphismClasses_vsub_eq_obstructionClass
    (S : SquareZeroExtensionProblem.{u₁, u₂, u₃, u₄})
    (h : Nonempty (SquareZeroExtensionProblem.CompatibleExtension.{v} S))
    (X Y : S.CompatibleExtension.{v}) :
    (@VSub.vsub
      (naiveCotangentExtOne S.A S.B S.N)
      (SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses S)
      (isomorphismClassesTorsor S h).toVSub
      (Quotient.mk
          (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid S) Y :
          SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses S)
      (Quotient.mk
          (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid S) X :
          SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses S) =
      (obstructionClass (comparisonDiagram X Y)).1)

Tag 0GPT, a lemma

Tag 0GPT in the Stacks Project.

Stacks.Deformation.squareZeroAlgebraExtensionClassesEquivExtOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/AlgebraExtensions.lean, line 149.

Isomorphism classes of square-zero extensions of an A-algebra B by a B-module N are canonically equivalent to Ext¹_B(NL_{B/A}, N).

public noncomputable def squareZeroAlgebraExtensionClassesEquivExtOne
    (A : Type uA) (B : Type uB) [CommRing A] [CommRing B] [Algebra A B]
    (N : Type uN) [AddCommGroup N] [Module B N] :
    SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{uA, uA, uB, uN,
        max uB uN}
        (algebraExtensionProblem A B N) ≃
      naiveCotangentExtOne A B N

Stacks.Deformation.squareZeroAlgebraExtensionClassesEquivExtOne_sub, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/AlgebraExtensions.lean, line 196. The attribute's comment: “canonical difference”.

The classification sends the difference between two square-zero extensions to the canonical obstruction class comparing them.

public theorem squareZeroAlgebraExtensionClassesEquivExtOne_sub
    (A : Type uA) (B : Type uB) [CommRing A] [CommRing B] [Algebra A B]
    (N : Type uN) [AddCommGroup N] [Module B N]
    (X Y : (algebraExtensionProblem A B N).CompatibleExtension.{max uB uN}) :
    squareZeroAlgebraExtensionClassesEquivExtOne A B N
        (Quotient.mk
          (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
            (algebraExtensionProblem A B N)) Y) -
      squareZeroAlgebraExtensionClassesEquivExtOne A B N
      (Quotient.mk
        (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
          (algebraExtensionProblem A B N)) X) =
      (obstructionClass (comparisonDiagram X Y)).1

Stacks.Deformation.squareZeroAlgebraExtensionClassesEquivExtOne_split_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/AlgebraExtensions.lean, line 217. The attribute's comment: “split extension”.

The canonical classification sends the split square-zero extension to zero.

public theorem squareZeroAlgebraExtensionClassesEquivExtOne_split_eq_zero
    (A : Type uA) (B : Type uB) [CommRing A] [CommRing B] [Algebra A B]
    (N : Type uN) [AddCommGroup N] [Module B N] :
    squareZeroAlgebraExtensionClassesEquivExtOne A B N
      (Quotient.mk
        (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
          (algebraExtensionProblem A B N)) (splitAlgebraExtension A B N)) = 0

Tag 0GPU, a remark

Tag 0GPU in the Stacks Project.

Algebra.Generators.exists_lift_and_cotangentMap_to_squareZeroKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/CotangentLift.lean, line 102. The attribute's comment: “lift_and_factor”.

A polynomial presentation of an algebra lifts through every square-zero extension, and the restriction of the lift to the relation ideal factors B-linearly through J / J².

theorem exists_lift_and_cotangentMap_to_squareZeroKernel
    {ι : Type w} (P : Algebra.Generators A B ι) (E : Algebra.Extension A B)
    (hE : E.ker ^ 2 = ⊥) :
    letI := Algebra.Extension.squareZeroKerModule E hE
    ∃ (f : P.toExtension.Hom E) (l : P.toExtension.Cotangent →ₗ[B] E.ker),
      ∀ x : P.toExtension.ker,
        (l (Algebra.Extension.Cotangent.mk x) : E.Ring) = f.toRingHom x

Stacks.Deformation.extensionClass_eq_conormalCokernelClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/PresentationExtensionClass.lean, line 673. The attribute's comment: “extension_class”.

Stacks 0GPU, the extension class. Let α : P → B be a presentation of the A-algebra B with relation ideal J, let 0 → N → B' → B → 0 be a square-zero extension of A-algebras, let α' : P → B' be an A-algebra lift of α, and let δ : J/J² → N be the B-linear factorisation of α'|_J. Then the classification of Stacks 0GPT, carried to the cokernel Coker(Hom_B(Ω_{P/A} ⊗_P B, N) → Hom_B(J/J², N)) which computes Ext¹_B(NL(α), N), sends the extension to the class of δ.

public theorem extensionClass_eq_conormalCokernelClass
    {ι : Type uι} (P : Algebra.Generators A B ι)
    (X : (algebraExtensionProblem A B N).CompatibleExtension.{max uB uN})
    (lift : P.Ring →ₐ[A] X.B')
    (hlift : ∀ p, X.toB (lift p) = algebraMap P.Ring B p)
    (δ : P.toExtension.Cotangent →ₗ[B] N)
    (hδ : ∀ y : P.toExtension.ker,
      kernelVal X (δ (Algebra.Extension.Cotangent.mk y)) = lift (y : P.toExtension.Ring))
    (ψ : P.toExtension.Hom (Algebra.Generators.self A B).toExtension) :
    presentationComparison P ψ
        (extCokernelIso A B N (squareZeroAlgebraExtensionClassesEquivExtOne A B N
          (Quotient.mk (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
            (algebraExtensionProblem A B N)) X))) =
      Submodule.Quotient.mk δ

NaiveCotangent.extOne_naiveCotangentComplex_addEquiv_cokernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/ExtCokernel.lean, line 120. The attribute's comment: “ext_cokernel”.

The comparison which computes the first Ext group of the naive cotangent complex of a polynomial presentation. On the right, the cokernel is represented as the quotient by the range of precomposition with the conormal differential.

It is the underlying additive equivalence of extOne_naiveCotangentComplex_linearEquiv_cokernel, so the two cannot drift apart; use that one for anything involving scalars.

public noncomputable def extOne_naiveCotangentComplex_addEquiv_cokernel
    {A : Type uA} {B : Type uB} {ι : Type uι} {N : Type uN}
    [CommRing A] [CommRing B] [Algebra A B]
    (P : Algebra.Generators A B ι) [AddCommGroup N] [Module B N] :
    DerivedCategory.Ext
        ((DerivedCategory.Q :
            CochainComplex (ModuleCat.{max uA uB uι uN} B) ℤ ⥤ _).obj
          (CochainComplex.mappingCone
            ((CochainComplex.singleFunctor (ModuleCat.{max uA uB uι uN} B) 0).map
              (ModuleCat.ofHom
                (ULift.moduleEquiv.{uB, max (max uA uB) uι,
                  max uA uB uι uN}.symm.toLinearMap.comp
                  ((NaiveCotangent.NL P).d.comp
                    ULift.moduleEquiv.{uB, max uA uι,
                      max uA uB uι uN}.toLinearMap))))))
        ((DerivedCategory.singleFunctor (ModuleCat.{max uA uB uι uN} B) 0).obj
          (ModuleCat.of B (ULift.{max uA uB uι uN} N))) 1 ≃+
      ((P.toExtension.Cotangent →ₗ[B] N) ⧸ LinearMap.range
        ((LinearMap.lcomp B N (NaiveCotangent.NL P).d) :
          (P.toExtension.CotangentSpace →ₗ[B] N) →ₗ[B]
            (P.toExtension.Cotangent →ₗ[B] N)))

Declarations registered for the tag:

Algebra.Extension.cotangentComplex registered with add_to_stacks in StacksFrontier/RingTheory/NaiveCotangent/ExtCokernel.lean, line 54 (StacksFrontier): “presentation_complex”. References: EGA IV (17.15.9); SGA 1 II (5.9), “more general”; SGA 6 0 (4.4), “special case”; SGA 6 VIII (2.1), “affine case”.

Tag 0GPV, a lemma

Tag 0GPV in the Stacks Project.

Stacks.Deformation.exists_compatible_algebraMap_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/AlgebraExtensionMaps.lean, line 500.

Stacks 0GPV. Given ring maps A → B → C, a B-module M, a C-module N, a B-linear map c : M → N, a square-zero extension 0 → M → B' → B → 0 of A-algebras with class ξ ∈ Ext¹_B(NL_{B/A}, M) and a square-zero extension 0 → N → C' → C → 0 of A-algebras with class ζ ∈ Ext¹_C(NL_{C/A}, N), there is an A-algebra map B' → C' compatible with B → C and with c if and only if ξ and ζ have the same image in Ext¹_B(NL_{B/A}, N).

public theorem exists_compatible_algebraMap_iff :
    (∃ h : X.B' →ₐ[A] Y.B',
        (∀ z : X.B', Y.toB (h z) = algebraMap B C (X.toB z)) ∧
          ∀ m : M, h (kernelInclusion X m) = kernelInclusion Y (c m)) ↔
      naiveCotangentExtOneMap A B c (squareZeroAlgebraExtensionClassesEquivExtOne A B M
          (Quotient.mk (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
            (algebraExtensionProblem A B M)) X))
        = naiveCotangentExtOneTowerMap A B C
          (squareZeroAlgebraExtensionClassesEquivExtOne A C N
            (Quotient.mk (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid
              (algebraExtensionProblem A C N)) Y))

Tag 0GPW, a remark

Tag 0GPW in the Stacks Project.

Stacks.Deformation.pullbackExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtensionPushoutPullback.lean, line 305. The attribute's comment: “the pullback extension B'₂ = C' ×_C B; all five rings and modules in one universe”.

The pullback extension B'₂ = C' ×_C B. Pulling the square-zero extension 0 → N → C' → C → 0 of A-algebras back along B → C gives a square-zero extension 0 → N → B'₂ → B → 0 of the A-algebra B by N.

public def pullbackExtension :
    (algebraExtensionProblem A B N).CompatibleExtension.{u}

Stacks.Deformation.pullbackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtensionPushoutPullback.lean, line 360. The attribute's comment: “the map B'₂ → C' of the second displayed diagram”.

The map B'₂ → C' of the remark's second displayed diagram: the first projection of the fibre product.

public def pullbackMap : ↥(pullbackSubalgebra A B C Y) →ₐ[A] Y.B'

Stacks.Deformation.pushoutExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtensionPushoutPullback.lean, line 631. The attribute's comment: “the pushout extension B'₁ = (N × B')/M; all five rings and modules in one universe”. References: EGA 0 (19.5.6.1), “partial”.

The pushout extension B'₁ = (N × B')/M. Pushing the square-zero extension 0 → M → B' → B → 0 of A-algebras out along c : M → N gives a square-zero extension 0 → N → B'₁ → B → 0 of the A-algebra B by N.

public def pushoutExtension : (algebraExtensionProblem A B N).CompatibleExtension.{u}

Stacks.Deformation.pushoutMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtensionPushoutPullback.lean, line 696. The attribute's comment: “the map B' → B'₁ of the first displayed diagram”.

The map B' → B'₁ of the remark's first displayed diagram: x ↦ [(0, x)].

public def pushoutMap : X.B' →ₐ[A] (pushoutExtension c X).B'

Stacks.Deformation.extClass_pushoutExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtensionPushoutPullback.lean, line 739. The attribute's comment: “B'₁ corresponds to the image of ξ under Ext¹_B(NL_{B/A}, M) → Ext¹_B(NL_{B/A}, N)”.

Stacks 0GPW. The pushout extension B'₁ corresponds, under the classification of Stacks 0GPT, to the image of the class of B' by the map Ext¹_B(NL_{B/A}, M) → Ext¹_B(NL_{B/A}, N) induced by c : M → N.

This is Stacks 0GPV for the trivial tower A → B → B, applied to the map B' → B'₁ produced by the construction, together with the fact that the restriction map for that tower is the identity.

public theorem extClass_pushoutExtension (c : M →ₗ[B] N)
    (X : (algebraExtensionProblem A B M).CompatibleExtension.{u}) :
    extClass (pushoutExtension c X) = naiveCotangentExtOneMap A B c (extClass X)

Stacks.Deformation.extClass_pullbackExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtensionPushoutPullback.lean, line 755. The attribute's comment: “B'₂ corresponds to the image of ζ under Ext¹_C(NL_{C/A}, N) → Ext¹_B(NL_{B/A}, N)”.

Stacks 0GPW. The pullback extension B'₂ corresponds, under the classification of Stacks 0GPT, to the image of the class of C' by the map Ext¹_C(NL_{C/A}, N) → Ext¹_B(NL_{B/A}, N).

This is Stacks 0GPV applied to the projection B'₂ → C', which is compatible with B → C and with the identity of N, together with the fact that the map on first Ext induced by the identity of N is the identity.

public theorem extClass_pullbackExtension
    (Y : (algebraExtensionProblem A C N).CompatibleExtension.{u}) :
    extClass (pullbackExtension A B C Y) = naiveCotangentExtOneTowerMap A B C (extClass Y)

Stacks.Deformation.isomorphic_pushoutExtension_pullbackExtension_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtensionPushoutPullback.lean, line 770. The attribute's comment: “a compatible A-algebra map B' → C' exists iff B'₁ and B'₂ are isomorphic”.

Stacks 0GPW, the diagram chase. There is an A-algebra map B' → C' compatible with B → C and with c : M → N if and only if the pushout B'₁ is isomorphic to the pullback B'₂ as A-algebra extensions of B by N.

The two directions are obtained from Stacks 0GPV together with the two class identifications above and the injectivity of the classification of Stacks 0GPT.

public theorem isomorphic_pushoutExtension_pullbackExtension_iff (c : M →ₗ[B] N)
    (X : (algebraExtensionProblem A B M).CompatibleExtension.{u})
    (Y : (algebraExtensionProblem A C N).CompatibleExtension.{u}) :
    SquareZeroExtensionProblem.CompatibleExtension.Isomorphic
        (pushoutExtension c X) (pullbackExtension A B C Y) ↔
      ∃ h : X.B' →ₐ[A] Y.B',
        (∀ z : X.B', Y.toB (h z) = algebraMap B C (X.toB z)) ∧
          ∀ m : M, h (kernelInclusion X m) = kernelInclusion Y (c m)

Tag 0GPX, a lemma

Tag 0GPX in the Stacks Project.

Stacks.Deformation.baseExtClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/SolutionsFibre.lean, line 130. The attribute's comment: “the class ξ of the thickening A', via Lemma 0GPT”.

The canonical class ξ ∈ Ext¹_A(NL_{A/A'}, I) of the square-zero thickening A': the value of the classification of Stacks 0GPT on baseExtension.

public def baseExtClass : naiveCotangentExtOne S.A' S.A S.I

Stacks.Deformation.solutionsFibre, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/SolutionsFibre.lean, line 279. The attribute's comment: “the fibre over the image of the class of the thickening”.

The fibre of Ext¹_B(NL_{B/A'}, N) → Ext¹_A(NL_{A/A'}, N) over the image of the canonical class ξ of the thickening A' under the map Ext¹_A(NL_{A/A'}, I) → Ext¹_A(NL_{A/A'}, N) induced by c : I → N.

public abbrev solutionsFibre

Stacks.Deformation.solutionsEquivFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/SolutionsFibre.lean, line 337. The attribute's comment: “solutions with middle ring in the universe max uB uN, as in Lemma 0GPT”.

Stacks 0GPX. Let 0 → I → A' → A → 0, A → B and c : I → N be as in Stacks 08S4, and let ξ ∈ Ext¹_A(NL_{A/A'}, I) be the class of the extension A' of A by I under Stacks 0GPT. The set of isomorphism classes of solutions of the extension problem is canonically bijective to the fibre of Ext¹_B(NL_{B/A'}, N) → Ext¹_A(NL_{A/A'}, N) over the image of ξ.

The bijection is the canonical one: it sends the class of a solution to the class of its underlying square-zero extension of the A'-algebra B by N, as recorded by solutionsEquivFibre_apply.

public def solutionsEquivFibre :
    SquareZeroExtensionProblem.CompatibleExtension.IsomorphismClasses.{u₁, u₂, u₃, u₄,
      max u₃ u₄} S ≃ solutionsFibre S

Stacks.Deformation.solutionsEquivFibre_apply, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/SolutionsFibre.lean, line 347. The attribute's comment: “the bijection sends a solution to the class of its underlying extension”.

The bijection of Stacks 0GPX sends the class of a solution to the class in Ext¹_B(NL_{B/A'}, N) of its underlying square-zero extension of the A'-algebra B by N.

public lemma solutionsEquivFibre_apply (P : S.CompatibleExtension.{max u₃ u₄}) :
    (solutionsEquivFibre S (Quotient.mk
      (SquareZeroExtensionProblem.CompatibleExtension.isomorphicSetoid S) P)).1
      = solutionExtClass S P

Tag 0GPY, a remark

Tag 0GPY in the Stacks Project.

Stacks.Deformation.naiveCotangentExtOneDerivedBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtBaseChange.lean, line 156. The attribute's comment: “Ext¹_A(NL_{A/A'}, N) = Ext¹_B(NL_{A/A'} ⊗^L_A B, N), via Tag 0GMT”.

Stacks 0GPY, first identification. For A' → A → B and a B-module M, extension classes of the naive cotangent complex of A over A' with coefficients in M regarded as an A-module are the same as extension classes over B of its derived base change. This is the adjunction of Stacks 0GMT.

public noncomputable def naiveCotangentExtOneDerivedBaseChangeEquiv
    (A' : Type u₁) (A : Type u₂) (B : Type u₃) [CommRing A'] [CommRing A] [CommRing B]
    [Algebra A' A] [Algebra A B] (M : ModuleCat.{max u₁ u₂ u₃ v} B) :
    DerivedCategory.Ext
        (DerivedCategory.Q.obj (naiveCotangentCochainComplex.{u₁, u₂, max u₃ v} A' A))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₁ u₂ u₃ v} A) 0).obj
          ((ModuleCat.restrictScalars (algebraMap A B)).obj M)) 1 ≃+
      DerivedCategory.Ext
        ((totalDerivedExtensionScalars.{u₂, u₃, max u₁ v} (algebraMap A B)).functor.obj
          (DerivedCategory.Q.obj (naiveCotangentCochainComplex.{u₁, u₂, max u₃ v} A' A)))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₁ u₂ u₃ v} B) 0).obj M) 1

Stacks.Deformation.naiveCotangentDerivedBaseChangeExtOneEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtBaseChange.lean, line 175. The attribute's comment: “Ext¹_B(NL_{A/A'} ⊗^L_A B, N) = Ext¹_B(NL_{A/A'} ⊗_A B, N), via Tag 0FUY”.

Stacks 0GPY, second identification. Extension classes over B out of the derived base change of the naive cotangent complex are the same as extension classes out of its termwise base change. The coefficient M, placed in degree 0 and shifted into degree -1, only sees the truncation τ_{≥ -1}, which the termwise base change computes by Stacks 0FUY.

public noncomputable def naiveCotangentDerivedBaseChangeExtOneEquiv
    (A' : Type u₁) (A : Type u₂) (B : Type u₃) [CommRing A'] [CommRing A] [CommRing B]
    [Algebra A' A] [Algebra A B] (M : ModuleCat.{max u₁ u₂ u₃ v} B) :
    letI : (ModuleCat.extendScalars.{u₂, u₃, max u₁ u₂ u₃ v} (algebraMap A B)).IsLeftAdjoint :=
      ModuleCat.instIsLeftAdjointExtendScalars.{u₂, u₃, max u₁ u₂ v} (algebraMap A B)
    DerivedCategory.Ext
        ((totalDerivedExtensionScalars.{u₂, u₃, max u₁ v} (algebraMap A B)).functor.obj
          (DerivedCategory.Q.obj (naiveCotangentCochainComplex.{u₁, u₂, max u₃ v} A' A)))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₁ u₂ u₃ v} B) 0).obj M) 1 ≃+
      DerivedCategory.Ext
        (DerivedCategory.Q.obj
          (((ModuleCat.extendScalars.{u₂, u₃, max u₁ u₂ u₃ v}
            (algebraMap A B)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
              (naiveCotangentCochainComplex.{u₁, u₂, max u₃ v} A' A)))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₁ u₂ u₃ v} B) 0).obj M) 1

Stacks.Deformation.naiveCotangentExtOneBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtBaseChange.lean, line 215.

Stacks 0GPY. For A' → A → B and a B-module M, the first extension group of the naive cotangent complex of A over A' with coefficients in M regarded as an A-module is canonically the first extension group over B of the termwise base change NL_{A/A'} ⊗_A B with coefficients in M.

public noncomputable def naiveCotangentExtOneBaseChangeEquiv
    (A' : Type u₁) (A : Type u₂) (B : Type u₃) [CommRing A'] [CommRing A] [CommRing B]
    [Algebra A' A] [Algebra A B] (M : ModuleCat.{max u₁ u₂ u₃ v} B) :
    letI : (ModuleCat.extendScalars.{u₂, u₃, max u₁ u₂ u₃ v} (algebraMap A B)).IsLeftAdjoint :=
      ModuleCat.instIsLeftAdjointExtendScalars.{u₂, u₃, max u₁ u₂ v} (algebraMap A B)
    DerivedCategory.Ext
        (DerivedCategory.Q.obj (naiveCotangentCochainComplex.{u₁, u₂, max u₃ v} A' A))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₁ u₂ u₃ v} A) 0).obj
          ((ModuleCat.restrictScalars (algebraMap A B)).obj M)) 1 ≃+
      DerivedCategory.Ext
        (DerivedCategory.Q.obj
          (((ModuleCat.extendScalars.{u₂, u₃, max u₁ u₂ u₃ v}
            (algebraMap A B)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
              (naiveCotangentCochainComplex.{u₁, u₂, max u₃ v} A' A)))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₁ u₂ u₃ v} B) 0).obj M) 1

Stacks.Deformation.naiveCotangentExtOneBaseChangeModuleEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/ExtBaseChange.lean, line 238. The attribute's comment: “for a module N and the Ext group naiveCotangentExtOne”.

Stacks 0GPY, stated for a B-module N and the Ext group Stacks.Deformation.naiveCotangentExtOne: the first extension group over A of the naive cotangent complex of A over A' with coefficients in N, which is an A-module by restriction of scalars, is the first extension group over B of NL_{A/A'} ⊗_A B.

public noncomputable def naiveCotangentExtOneBaseChangeModuleEquiv
    (A' : Type u₁) (A : Type u₂) (B : Type u₃) [CommRing A'] [CommRing A] [CommRing B]
    [Algebra A' A] [Algebra A B] (N : Type u₄) [AddCommGroup N] [Module B N] :
    letI : (ModuleCat.extendScalars.{u₂, u₃, max u₁ u₂ u₃ u₄} (algebraMap A B)).IsLeftAdjoint :=
      ModuleCat.instIsLeftAdjointExtendScalars.{u₂, u₃, max u₁ u₂ u₄} (algebraMap A B)
    letI : Module A (ULift.{u₃} N) := Module.compHom _ (algebraMap A B)
    naiveCotangentExtOne A' A (ULift.{u₃} N) ≃+
      DerivedCategory.Ext
        (DerivedCategory.Q.obj
          (((ModuleCat.extendScalars.{u₂, u₃, max u₁ u₂ u₃ u₄}
            (algebraMap A B)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
              (naiveCotangentCochainComplex.{u₁, u₂, max u₃ u₄} A' A)))
        ((DerivedCategory.singleFunctor (ModuleCat.{max u₁ u₂ u₃ u₄} B) 0).obj
          ((ModuleCat.uliftFunctor.{max u₁ u₂} B).obj
            (ModuleCat.of B (ULift.{u₃} N)))) 1

Tag 08S6, a lemma

Tag 08S6 in the Stacks Project.

Stacks.Deformation.nonempty_compatibleExtension_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/LocalCompleteIntersection.lean, line 674.

Stacks 08S6. If A → B is a local complete intersection ring map, then every square-zero extension problem over A' → A with target B and prescribed kernel map c : I → N has a solution.

public theorem nonempty_compatibleExtension_of_isLocalCompleteIntersection
    (S : SquareZeroExtensionProblem.{u₁, u₂, u₃, u₄})
    (h : (algebraMap S.A S.B).IsLocalCompleteIntersection) :
    Nonempty (S.CompatibleExtension.{max u₁ (max u₂ (max u₃ u₄))})

Sources

LeanStacks.Deformation.SquareZeroExtensionProblem.CompatibleExtension · Deformation.RingThickening.fittingMap_addTorsor_kaehlerDifferentialHom · Stacks.Deformation.obstructionClass · Stacks.Deformation.isomorphismClassesTorsor · Stacks.Deformation.isomorphismClasses_vsub_eq_obstructionClass · Stacks.Deformation.squareZeroAlgebraExtensionClassesEquivExtOne · Stacks.Deformation.squareZeroAlgebraExtensionClassesEquivExtOne_sub · Stacks.Deformation.squareZeroAlgebraExtensionClassesEquivExtOne_split_eq_zero

Section91.3 Thickenings of ringed spaces #

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

Tag 08KZ, a situation

Tag 08KZ in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/Thickening.lean, line 416. The attribute's comment: “the commutative square”.

A morphism of thickenings: a commutative square of ringed spaces whose horizontal arrows are thickenings.

structure MorphismOfThickenings

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.idealMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/Thickening.lean, line 465. The attribute's comment: “the canonical ideal map”.

The canonical map (f')^* J ⟶ I: after inclusion into 𝒪_{X'}, it is the restriction of (f')^♯ to the pullback of J.

noncomputable def idealMap (D : MorphismOfThickenings.{u}) :
    { g : (modulePullback D.f').obj D.idealJ ⟶ D.idealI //
      g ≫ kernel.ι (SheafOfModules.unitToPushforwardObjUnit (structureSheafHom D.i)) =
        D.ambientIdealMap }

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.firstOrderSurjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/Thickening.lean, line 544. The attribute's comment: “the first-order canonical map”.

The canonical reduction map (f')^* J ⟶ i_* f^* t^* J: the unit of i^* ⊣ i_*, followed by the pushforward of reducedPullbackComparison.

noncomputable def firstOrderSurjection (D : MorphismOfThickenings.{u})
    (_hi : IsFirstOrderThickening D.i) (_ht : IsFirstOrderThickening D.t) :
    (modulePullback D.f').obj D.idealJ ⟶ D.reducedPullbackIdeal

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.firstOrderSurjection_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/Thickening.lean, line 553. The attribute's comment: “surjectivity of the first-order canonical map”.

When both thickenings are first order, the canonical reduction map (f')^* J ⟶ i_* f^* t^* J is an epimorphism.

theorem firstOrderSurjection_epi (D : MorphismOfThickenings.{u})
    (hi : IsFirstOrderThickening D.i) (ht : IsFirstOrderThickening D.t) :
    Epi (D.firstOrderSurjection hi ht)

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.firstOrderIdealMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/Thickening.lean, line 566. The attribute's comment: “the first-order factorization”.

If both thickenings are first order, the canonical ideal map (f')^* J ⟶ I factors uniquely through the reduction (f')^* J ⟶ i_* f^* J, giving a map f^* J ⟶ I.

noncomputable def firstOrderIdealMap (D : MorphismOfThickenings.{u})
    (hi : IsFirstOrderThickening D.i) (ht : IsFirstOrderThickening D.t) :
    { g : D.reducedPullbackIdeal ⟶ D.idealI //
      D.firstOrderSurjection hi ht ≫ g = D.idealMap.1 ∧
        ∀ g' : D.reducedPullbackIdeal ⟶ D.idealI,
          D.firstOrderSurjection hi ht ≫ g' = D.idealMap.1 → g' = g }

AlgebraicGeometry.RingedSpaceThickening.exists_factorization_of_comp_idealι_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ThickeningTrivialization.lean, line 197. The attribute's comment: “factoring through a thickening”.

Stacks Project, Tag 08KZ. Let i : X ⟶ X' be a thickening and f : Y ⟶ X' a morphism of ringed spaces whose comorphism kills the kernel ideal ℐ = ker(i^♯). Then f factors through i.

The factorization of sheaves of modules exists because i^♯ is an epimorphism killed by ℐ, which is what Abelian.epiDesc supplies; exists_ringHom_of_additive_factorization upgrades its underlying additive map to a map of sheaves of rings.

theorem exists_factorization_of_comp_idealι_eq_zero
    {X Y X' : RingedSpace.{u, u}} (i : X ⟶ X') (f : Y ⟶ X')
    (hi : IsThickening i)
    (h : kernel.ι (SheafOfModules.unitToPushforwardObjUnit (structureSheafHom i)) ≫
      SheafOfModules.unitToPushforwardObjUnit (structureSheafHom f) = 0) :
    ∃ p : Y ⟶ X, p ≫ i = f

Tag 08L1, a definition

Tag 08L1 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.epi_baseToSourceIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/StrictThickening.lean, line 77. The attribute's comment: “surjectivity of the reduced canonical ideal map”.

For a strict morphism of thickenings the reduced canonical ideal map f^* t^* J ⟶ i^* I is surjective.

theorem epi_baseToSourceIdeal (D : MorphismOfThickenings.{u}) (hs : D.IsStrict) :
    Epi D.baseToSourceIdeal

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.IsStrict, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/Thickening.lean, line 599. The attribute's comment: “strict morphism of thickenings”.

A morphism of thickenings is strict when the canonical map (f')^* J ⟶ I of ideal sheaves is surjective, i.e. an epimorphism of sheaves of 𝒪_{X'}-modules.

noncomputable abbrev IsStrict (D : MorphismOfThickenings.{u}) : Prop

Tag 08L2, a lemma

Tag 08L2 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.isStrict_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/CartesianStrict.lean, line 284. The attribute's comment: “a cartesian square is strict”.

Stacks Project, Tag 08L2. A cartesian square of thickenings is strict.

For a point x of X' the test object testPoint x maps to X', and its composite with f' factors through the thickening t; the square, being cartesian, therefore lifts it to X, and the lift forces the comorphism of testPoint x to kill I. So the germ at x of a section of I is a germ of a section in the range of the ambient ideal map, and (f')^* J ⟶ I is locally surjective.

theorem isStrict_of_isPullback (hc : IsPullback D.i D.f D.f' D.t) : D.IsStrict

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.isStrict_iff_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/CartesianStrict.lean, line 329. The attribute's comment: “strict iff cartesian”.

Stacks Project, Tag 08L2. A morphism of thickenings of ringed spaces is strict if and only if its square is cartesian in the category of ringed spaces. The forward implication is isPullback_of_isStrict; the converse is isStrict_of_isPullback.

theorem isStrict_iff_isPullback : D.IsStrict ↔ IsPullback D.i D.f D.f' D.t

AlgebraicGeometry.RingedSpaceThickening.MorphismOfThickenings.isPullback_of_isStrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/StrictCartesian.lean, line 90. The attribute's comment: “a strict morphism has a cartesian square”.

Stacks Project, Tag 08L2. A strict morphism of thickenings has a cartesian square: both thickenings are monomorphisms, so uniqueness of a lift is automatic, and existence is the factorization of a test morphism through i supplied by exists_factorization_of_comp_idealι_eq_zero.

theorem isPullback_of_isStrict (D : MorphismOfThickenings.{u}) (hs : D.IsStrict) :
    IsPullback D.i D.f D.f' D.t

Sources

Section91.4 Modules on first order thickenings of ringed spaces #

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

Tag 08L4, an equation

Tag 08L4 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.firstOrderExtensionAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ModuleExtension.lean, line 616. The attribute's comment: “the canonical map”.

Stacks Project, Tag 08L4. The canonical map c_{ℱ'} : i^* ℐ ⊗_{𝒪_X} ℱ ⟶ 𝒦 of an extension 0 ⟶ i_* 𝒦 ⟶ ℱ' ⟶ i_* ℱ ⟶ 0 of 𝒪_{X'}-modules across a first order thickening i.

The bundled equation is the local lifting characterisation from the source: on an open set of X' over which a section s of i_* ℱ lifts to a section s' of ℱ', the image in ℱ' of c_{ℱ'}(a ⊗ s) is the scalar multiple a · s'.

noncomputable def firstOrderExtensionAction
    (F K : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} ⟨X.presheaf, X.IsSheaf⟩))
        (hi : IsFirstOrderThickening i)
    (E : CategoryTheory.Abelian.YonedaExtension
      ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0) :
    { c : (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
        ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj ((idealSheafPullback i))).obj (F)) ⟶ K //
      ∀ (U : Opens X') (a : (AlgebraicGeometry.SheafOfModules.idealSheaf i).val.obj (op U))
        (s : ((modulePushforward i).obj F).val.obj (op U)) (s' : E.Z.left.val.obj (op U)),
        (E.g.val.app (op U)).hom s' = s →
          (E.f.val.app (op U)).hom
              ((((modulePushforward i).map c).val.app (op U)).hom
                (((extensionTensorComparison i F).val.app (op U)).hom
                  (toTensorSheafSection X' (AlgebraicGeometry.SheafOfModules.idealSheaf i)
                    ((modulePushforward i).obj F) (op U)
                    (a ⊗ₜ[X'.presheaf.obj (op U)] s)))) =
            (show ((Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u}
                ⟨X'.presheaf, X'.IsSheaf⟩).obj.obj (op U) : Type u) from
              ((idealSheafι i).val.app (op U)).hom a) • s' }

Declarations registered for the tag:

CategoryTheory.Abelian.YonedaExtension, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/RingedSpaceThickening/ModuleExtension.lean, line 122 (StacksFrontier): “the short exact sequence”.

Tag 08L5, a lemma

Tag 08L5 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.ExtensionPair.extensionAction_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionActionNaturality.lean, line 249. The attribute's comment: “part (1): compatibility of the canonical maps”.

Stacks Project, Tag 08L5, part (1). If the middle terms of two extensions across a first order thickening are linked by a map φ' compatible with φ : ℱ ⟶ 𝒢 and ψ : 𝒦 ⟶ ℒ, then the canonical maps of the two extensions commute with 1 ⊗ φ and ψ.

theorem extensionAction_naturality (S : ExtensionPair.{u}) (c : CompatibleMap S) :
    (firstOrderExtensionAction S.i S.F S.K S.firstOrder S.firstExtension).val ≫ S.kernelMap =
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor ⟨((S.X)).presheaf, ((S.X)).IsSheaf⟩)).map (((𝟙 (idealSheafPullback S.i)), S.quotientMap) : (_, _) ⟶ (_, _))) ≫
        (firstOrderExtensionAction S.i S.G S.L S.firstOrder S.secondExtension).val

AlgebraicGeometry.RingedSpaceThickening.ExtensionPair.exists_compatibleMap_translate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionMaps.lean, line 143. The attribute's comment: “the action on compatible maps”.

Stacks Project, Tag 08L5. Translating a compatible map φ' by a map α : ℱ ⟶ ℒ, that is adding the composite ℱ' ⟶ i_* ℱ ⟶ i_* ℒ ⟶ 𝒢', again gives a compatible map. This is the action of Hom_{𝒪_X}(ℱ, ℒ) on the set of compatible maps.

theorem exists_compatibleMap_translate (c : CompatibleMap S) (α : S.F ⟶ S.L) :
    ∃ d : CompatibleMap S,
      d.hom = c.hom +
        S.firstExtension.g ≫ (modulePushforward S.i).map α ≫ S.secondExtension.f

AlgebraicGeometry.RingedSpaceThickening.ExtensionPair.existsUnique_translate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionMaps.lean, line 190. The attribute's comment: “freeness and transitivity of the action”.

Stacks Project, Tag 08L5. Any two compatible maps differ by a unique α : ℱ ⟶ ℒ. Together with exists_compatibleMap_translate this says that the set of compatible maps is, when nonempty, a principal homogeneous space under Hom_{𝒪_X}(ℱ, ℒ).

theorem existsUnique_translate (c d : CompatibleMap S) :
    ∃! α : S.F ⟶ S.L,
      d.hom = c.hom +
        S.firstExtension.g ≫ (modulePushforward S.i).map α ≫ S.secondExtension.f

Tag 08L6, a lemma

Tag 08L6 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.mapLiftingObstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/LiftingObstruction.lean, line 155. The attribute's comment: “the obstruction class and its vanishing criterion”.

The obstruction o(φ, ψ) ∈ Ext¹_{𝒪_X}(ℱ, ℒ) to lifting a pair of maps φ : ℱ ⟶ 𝒢 and ψ : 𝒦 ⟶ ℒ, compatible with the canonical maps of two extensions across a first order thickening, to a map of the extensions themselves: the class vanishes exactly when an 𝒪_{X'}-module map φ' : ℱ' ⟶ 𝒢' inducing ψ on kernels and φ on quotients exists.

noncomputable def mapLiftingObstruction
    [HasExt (SheafOfModules.{u} (structureSheafRing X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing X))]
    (hi : IsFirstOrderThickening i) (F K G L : SheafOfModules.{u} (structureSheafRing X))
    (E : CategoryTheory.Abelian.YonedaExtension
      ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0)
    (E' : CategoryTheory.Abelian.YonedaExtension
      ((modulePushforward i).obj G) ((modulePushforward i).obj L) 0)
    (φ : F ⟶ G) (ψ : K ⟶ L)
    (hcompat : (firstOrderExtensionAction i F K hi E).val ≫ ψ =
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
          ⟨((X)).presheaf, ((X)).IsSheaf⟩)).map (((𝟙 (idealSheafPullback i)), φ) :
          ((idealSheafPullback i), F) ⟶ ((idealSheafPullback i), G))) ≫
        (firstOrderExtensionAction i G L hi E').val) :
    { o : CategoryTheory.Abelian.zExt F L 1 //
      o = 0 ↔ ∃ φ' : E.Z.left ⟶ E'.Z.left,
        E.f ≫ φ' = (modulePushforward i).map ψ ≫ E'.f ∧
          φ' ≫ E'.g = E.g ≫ (modulePushforward i).map φ }

Tag 08L7, a lemma

Tag 08L7 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.extensionClassesWithAction_principalHomogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionClassesPrincipalHomogeneous.lean, line 83. The attribute's comment: “the whole lemma, for a first order thickening of ringed spaces: the isomorphism classes of extensions as in 08L4 with c_{ℱ'} = c, represented by their classes in Ext¹_{𝒪_{X'}}(i_* ℱ, i_* 𝒦), form a principal homogeneous space under Ext¹_{𝒪_X}(ℱ, 𝒦) acting through i_* by Baer sum”.

Stacks 08L7. Let i : (X, 𝒪_X) ⟶ (X', 𝒪_{X'}) be a first order thickening of ringed spaces, ℱ, 𝒦 two 𝒪_X-modules and c : ℐ ⊗_{𝒪_X} ℱ ⟶ 𝒦 an 𝒪_X-linear map. The isomorphism classes of extensions 0 ⟶ i_* 𝒦 ⟶ ℱ' ⟶ i_* ℱ ⟶ 0 of 𝒪_{X'}-modules with c_{ℱ'} = c (the set extensionClassesWithAction i F K hi c ⊆ Ext¹_{𝒪_{X'}}(i_* ℱ, i_* 𝒦)) form a principal homogeneous space under Ext¹_{𝒪_X}(ℱ, 𝒦), acting by ξ • η = η + i_* ξ:

the action preserves the set;

it is an action of the group Ext¹_{𝒪_X}(ℱ, 𝒦): 0 acts trivially and ξ + ξ' acts as ξ followed by ξ';

it is simply transitive: any two elements η, η' of the set satisfy η' = η + i_* ξ for exactly one ξ ∈ Ext¹_{𝒪_X}(ℱ, 𝒦).

So as soon as the set is nonempty (the source's hypothesis that some sequence (08L4) with c_{ℱ'} = c exists, hc), every point η₀ of it identifies it with Ext¹_{𝒪_X}(ℱ, 𝒦) via ξ ↦ η₀ + i_* ξ.

theorem extensionClassesWithAction_principalHomogeneous
    {X X' : RingedSpace.{u, u}} (i : X ⟶ X')
    (hi : AlgebraicGeometry.RingedSpaceThickening.IsFirstOrderThickening i)
    (F K : SheafOfModules.{u} (structureSheafRing X))
    [HasExt.{e} (SheafOfModules.{u} (structureSheafRing X))]
    [HasExt.{e} (SheafOfModules.{u} (structureSheafRing X'))]
    (c : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj
      ((idealSheafPullback i))).obj (F)) ⟶ K)
    (hc : ∃ E : CategoryTheory.Abelian.YonedaExtension
        ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0,
      (firstOrderExtensionAction i F K hi E).val = c) :
    haveI := preservesFiniteColimits_modulePushforward i hi.1
    haveI := preservesFiniteLimits_modulePushforward i
    (extensionClassesWithAction.{e} i F K hi c).Nonempty ∧
      (∀ η ∈ extensionClassesWithAction.{e} i F K hi c, ∀ ξ : Abelian.Ext.{e} F K 1,
        η + ξ.mapExactFunctor (modulePushforward i) ∈ extensionClassesWithAction.{e} i F K hi c) ∧
      (∀ η : Abelian.Ext.{e} ((modulePushforward i).obj F) ((modulePushforward i).obj K) 1,
        η + (0 : Abelian.Ext.{e} F K 1).mapExactFunctor (modulePushforward i) = η ∧
          ∀ ξ ξ' : Abelian.Ext.{e} F K 1,
            η + (ξ + ξ').mapExactFunctor (modulePushforward i) =
              (η + ξ.mapExactFunctor (modulePushforward i)) +
                ξ'.mapExactFunctor (modulePushforward i)) ∧
      ∀ η ∈ extensionClassesWithAction.{e} i F K hi c,
        ∀ η' ∈ extensionClassesWithAction.{e} i F K hi c,
          ∃! ξ : Abelian.Ext.{e} F K 1, η + ξ.mapExactFunctor (modulePushforward i) = η'

AlgebraicGeometry.RingedSpaceThickening.exists_extClass_add_of_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionClassification.lean, line 666. The attribute's comment: “the action of Ext¹_{𝒪_X}(ℱ, 𝒦): adding an extension of 𝒪_X-modules, read on X' as one whose middle term is a direct image, does not change the canonical map. SCOPE: this clause only; the simple transitivity of the action is existsUnique_extClass_sub_of_firstOrderExtensionAction_eq, and the identification of the subgroup of such classes with Ext¹_{𝒪_X}(ℱ, 𝒦) itself is not formalized here”.

Stacks 08L7, the action. Adding to an extension one whose middle term is a direct image does not change the canonical map: such an extension has vanishing canonical map (Stacks 08KS) and the canonical map is additive for Baer sums (AlgebraicGeometry.RingedSpaceThickening.exists_baerSum_firstOrderExtensionAction).

This is the source's "conversely, given such an extension ℰ we can add the extension ℰ to the 𝒪_{X'}-extension ℱ' without affecting the map c_{ℱ'}". By Stacks 08KS the extensions whose middle term is a direct image are exactly the extensions of 𝒪_X-modules, which is how Ext¹_{𝒪_X}(ℱ, 𝒦) acts.

theorem exists_extClass_add_of_essImage (hi : IsFirstOrderThickening i)
    (E₀ D : CategoryTheory.Abelian.YonedaExtension
      ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0)
    (hD : (modulePushforward i).essImage D.Z.left) :
    ∃ E : CategoryTheory.Abelian.YonedaExtension
        ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0,
      (CategoryTheory.Abelian.YonedaExtension.shortExact E).extClass =
          (CategoryTheory.Abelian.YonedaExtension.shortExact E₀).extClass +
            (CategoryTheory.Abelian.YonedaExtension.shortExact D).extClass ∧
        (firstOrderExtensionAction i F K hi E).val =
          (firstOrderExtensionAction i F K hi E₀).val

AlgebraicGeometry.RingedSpaceThickening.existsUnique_extClass_sub_of_firstOrderExtensionAction_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionClassification.lean, line 693. The attribute's comment: “simple transitivity: two extensions with the same canonical map differ by the class of exactly one extension whose middle term is a direct image, i.e. of an extension of 𝒪_X-modules. SCOPE: this clause only; the identification of the group of such classes with Ext¹_{𝒪_X}(ℱ, 𝒦) itself is not formalized here”.

Stacks 08L7, simple transitivity. Two extensions across the thickening with the same canonical map differ, in Ext¹_{𝒪_{X'}}(i_* ℱ, i_* 𝒦), by the class of exactly one extension whose middle term is a direct image — hence, by Stacks 08KS, by the class of an extension of 𝒪_X-modules.

This is the source's "the difference is an extension 0 → 𝒦 → ℰ → ℱ → 0 where ℰ is annihilated by ℐ, hence is an extension of 𝒪_X-modules". Uniqueness is uniqueness of a difference in the group Ext¹_{𝒪_{X'}}(i_* ℱ, i_* 𝒦).

theorem existsUnique_extClass_sub_of_firstOrderExtensionAction_eq (hi : IsFirstOrderThickening i)
    (E₀ E : CategoryTheory.Abelian.YonedaExtension
      ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0)
    (h : (firstOrderExtensionAction i F K hi E).val =
      (firstOrderExtensionAction i F K hi E₀).val) :
    ∃! ξ : CategoryTheory.Abelian.Ext.{w}
        ((modulePushforward i).obj F) ((modulePushforward i).obj K) 1,
      (CategoryTheory.Abelian.YonedaExtension.shortExact E).extClass =
          (CategoryTheory.Abelian.YonedaExtension.shortExact E₀).extClass + ξ ∧
        ∃ D : CategoryTheory.Abelian.YonedaExtension
            ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0,
          (CategoryTheory.Abelian.YonedaExtension.shortExact D).extClass = ξ ∧
            (modulePushforward i).essImage D.Z.left

AlgebraicGeometry.RingedSpaceThickening.existsUnique_ext_mapExactFunctor_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatLift.lean, line 295. The attribute's comment: “the identification of the group of classes whose extensions have a direct image as middle term with Ext¹_{𝒪_X}(ℱ, 𝒦) itself: such a class is i_* of exactly one class on X. SCOPE: this clause only; the action of those classes is exists_extClass_add_of_essImage and the simple transitivity is existsUnique_extClass_sub_of_firstOrderExtensionAction_eq”.

The classes in Ext¹_{𝒪_{X'}}(i_* ℱ, i_* 𝒦) whose extensions have a direct image as middle term are exactly the images of Ext¹_{𝒪_X}(ℱ, 𝒦) under i_*, each attained by exactly one class.

theorem existsUnique_ext_mapExactFunctor_eq (hi : IsThickening i)
    (ξ' : CategoryTheory.Abelian.Ext.{w}
      ((modulePushforward i).obj F) ((modulePushforward i).obj K) 1)
    (h : ∃ D : CategoryTheory.Abelian.YonedaExtension
        ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0,
      (CategoryTheory.Abelian.YonedaExtension.shortExact D).extClass = ξ' ∧
        (modulePushforward i).essImage D.Z.left) :
    ∃! ξ : CategoryTheory.Abelian.Ext.{w} F K 1,
      ξ.mapExactFunctor (modulePushforward i) = ξ'

Tag 08L8, a lemma

Tag 08L8 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.extensionExistenceObstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExistenceObstruction.lean, line 1055.

Stacks Project, Tag 08L8. The obstruction o(ℱ, 𝒦, c) ∈ Ext²_{𝒪_X}(ℱ, 𝒦) to the existence of an extension of 𝒪_{X'}-modules 0 ⟶ i_* 𝒦 ⟶ ℱ' ⟶ i_* ℱ ⟶ 0 as in Tag 08L4 whose canonical map c_{ℱ'} is a prescribed 𝒪_X-linear map c : ℐ ⊗_{𝒪_X} ℱ ⟶ 𝒦.

The class is AlgebraicGeometry.RingedSpaceThickening.obstructionClass, and the bundled property is the content of the lemma: it vanishes exactly when such an extension exists.

noncomputable def extensionExistenceObstruction
    [HasExt (SheafOfModules.{u} (structureSheafRing X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing X))]
    (hi : IsFirstOrderThickening i) (F K : SheafOfModules.{u} (structureSheafRing X))
    (c : (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj ((idealSheafPullback i))).obj (F)) ⟶ K) :
    { o : CategoryTheory.Abelian.zExt F K 2 //
      o = 0 ↔ ∃ E : CategoryTheory.Abelian.YonedaExtension
          ((modulePushforward i).obj F) ((modulePushforward i).obj K) 0,
        (firstOrderExtensionAction i F K hi E).val = c }

Tag 08L9, a remark

Tag 08L9 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.structureSheafSplitEpi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 345. The attribute's comment: “a trivialization splits the structure-sheaf map”.

Stacks 08L9. A trivialization of a thickening splits its structure-sheaf map: the structure-sheaf map 𝒪_X ⟶ π_* 𝒪_{X'} of the retraction, reindexed along AlgebraicGeometry.RingedSpaceThickening.retraction_opens_obj, is a section of i^♯ : 𝒪_{X'} ⟶ i_* 𝒪_X.

This is the step the source phrases as "using π^♯ to split the surjection 𝒪_{X'} ⟶ 𝒪_X". It is the converse of Deformation.RingThickening.retractionFromSplitting, and it supplies the CategoryTheory.SplitMono that Deformation.RingThickening.splittingFromTrivialization takes as a hypothesis — so the two together, and neither alone, give the source's "given π we obtain a splitting".

noncomputable def structureSheafSplitEpi : SplitEpi i.hom.c

AlgebraicGeometry.RingedSpaceThickening.trivializedThickeningEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivializedThickeningEquivalence.lean, line 946. The attribute's comment: “the category of trivialized first order thickenings of (X, 𝒪_X) is equivalent to the category of 𝒪_X-modules; morphisms of thickenings run in the geometric direction (X'₁ ⟶ X'₂ of ringed spaces, Stacks 08LD), so the module side carries ᵒᵖ”.

The category of trivialized first order thickenings of a ringed space (X, 𝒪_X) is equivalent to the opposite of the category of 𝒪_X-modules.

A trivialization π of a first order thickening i : X ⟶ X' splits the surjection 𝒪_{X'} ⟶ 𝒪_X, giving 𝒪_{X'} = 𝒪_X ⊕ ℐ as sheaves of algebras on X, and conversely such a splitting determines π. The equivalence sends an 𝒪_X-module 𝒢 to the trivial square-zero extension (X, 𝒪_X ⋉ 𝒢) with the zero section as trivialization, and a trivialized thickening back to its ideal read along the trivialization.

It is contravariant for the source's own convention for morphisms: TrivializedThickening X has its Hom in the geometric direction, a morphism of thickenings of (X, 𝒪_X) being a morphism X'₁ ⟶ X'₂ of ringed spaces (Stacks 08LD), and that is a morphism 𝒪_{X'₂} ⟶ 𝒪_{X'₁} of sheaves of algebras on X, hence a morphism ℐ₂ ⟶ ℐ₁ of the ideals (Stacks 08LC).

noncomputable def trivializedThickeningEquivalence (X : RingedSpace.{u, u}) :
    (SheafOfModules.{u} (structureSheafRing X))ᵒᵖ ≌ TrivializedThickening X

Deformation.RingThickening.splittingFromTrivialization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/TrivialThickening.lean, line 126. The attribute's comment: “splitting_from_trivialization”. References: EGA 0 (18.2.3), “special case”.

A trivialization identifies a first order thickening with the trivial square-zero extension by its kernel ideal.

noncomputable def splittingFromTrivialization
    (split : A ⟶ A') (π : SplitMono split)
    (h_sq : ∀ U : C, RingHom.ker (π.retraction.app U).hom ^ 2 = ⊥) :
  PresheafTrivialSquareZeroEquiv A' A π.retraction split

Deformation.RingThickening.retractionFromSplitting, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/TrivialThickening.lean, line 174. The attribute's comment: “trivialization_from_splitting”.

The section of the structure-sheaf map, transported along the inverse homeomorphism of the base map, defines a morphism of ringed spaces in the opposite direction.

noncomputable abbrev retractionFromSplitting {X X' : RingedSpace.{u, v}}
    (i : X ⟶ X') [IsIso i.hom.base]
    (splitting : SplitEpi i.hom.c) : X' ⟶ X

Deformation.RingThickening.retractionFromSplitting_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/TrivialThickening.lean, line 183. The attribute's comment: “trivialization_from_splitting”.

The morphism induced by a splitting of the structure-sheaf map retracts the original morphism.

theorem retractionFromSplitting_comp {X X' : RingedSpace.{u, v}}
    (i : X ⟶ X') [IsIso i.hom.base]
    (splitting : SplitEpi i.hom.c) :
    i ≫ retractionFromSplitting i splitting = 𝟙 X

Declarations registered for the tag:

CategoryTheory.SplitMono registered with add_to_stacks in StacksFrontier/Deformation/RingThickening/TrivialThickening.lean, line 58 (StacksFrontier): “trivial_thickening_and_trivialization”.
CategoryTheory.IsSplitMono registered with add_to_stacks in StacksFrontier/Deformation/RingThickening/TrivialThickening.lean, line 59 (StacksFrontier): “trivial_thickening_and_trivialization”. References: SGA 4 I (10.6).

Tag 08LA, an equation

Tag 08LA in the Stacks Project.

Declarations registered for the tag:

Deformation.RingThickening.splittingFromTrivialization, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/RingThickening/TrivialThickening.lean, line 202 (StacksFrontier): “the splitting determined by a trivialization”.
Deformation.RingThickening.PresheafTrivialSquareZeroEquiv, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/RingThickening/TrivialThickening.lean, line 204 (StacksFrontier): “the split square-zero extension it lands in”.

Tag 08LB, a remark

Tag 08LB in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.trivialExtensionModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 779. The attribute's comment: “part (1): the trivial extension ℱ'_{c,triv} = ℱ ⊕ 𝒦”.

Stacks Project, Tag 08LB, part (1). The trivial extension ℱ'_{c,triv} of ℱ by 𝒦 attached to c and a trivialization π: the direct sum ℱ ⊕ 𝒦, carried to X' by i_*, with the 𝒪_{X'}-module structure built from the splitting of Stacks 08LA and the map c,
r · (m, n) = (r m, r n + c(d r ⊗ m)),
where d r = r - π^♯(i^♯ r) is the derivation of the trivialization.

noncomputable def trivialExtensionModule : SheafOfModules.{u} (structureSheafRing X')

AlgebraicGeometry.RingedSpaceThickening.trivialExtensionModule_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 799. The attribute's comment: “part (1): the action of 𝒪_{X'} on ℱ ⊕ 𝒦”.

Stacks Project, Tag 08LB, part (1). The 𝒪_{X'}-module structure of the trivial extension: a section of 𝒪_{X'} acts diagonally on ℱ ⊕ 𝒦 and moves the ℱ-coordinate into the 𝒦-coordinate through c and the derivation of the trivialization. Together with AlgebraicGeometry.RingedSpaceThickening.trivialExtensionModule, whose sections over U are by construction the pairs ℱ(i^{-1}U) × 𝒦(i^{-1}U), this is the whole content of part (1).

theorem trivialExtensionModule_smul (U : (Opens X'.carrier)ᵒᵖ)
    (r : (structureSheafRing X').obj.obj U)
    (z : (trivialExtensionModule i π F K c hi).val.obj U) :
    r • z = (r • z.1, r • z.2 +
      extensionPairing i F K c U (trivializationDerivation i π hi.1.1 U r) z.1)

AlgebraicGeometry.RingedSpaceThickening.trivialExtensionShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 916. The attribute's comment: “part (2): the trivial extension is an extension as in 08L4”.

Stacks Project, Tag 08LB, part (2). The trivial extension sits in a short exact sequence 0 ⟶ i_* 𝒦 ⟶ ℱ'_{c,triv} ⟶ i_* ℱ ⟶ 0 of 𝒪_{X'}-modules: the inclusion of the second summand is a kernel of the projection onto the first.

theorem trivialExtensionShortComplex_shortExact :
    (trivialExtensionShortComplex i π F K c hi).ShortExact

AlgebraicGeometry.RingedSpaceThickening.trivialYonedaExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 932. The attribute's comment: “part (2): the trivial extension as a Yoneda extension”.

Stacks Project, Tag 08LB, part (2). The trivial extension, read as an extension of i_* ℱ by i_* 𝒦 in the sense of Stacks 08L4.

noncomputable def trivialYonedaExtension :
    CategoryTheory.Abelian.YonedaExtension ((modulePushforward i).obj F)
      ((modulePushforward i).obj K) 0

AlgebraicGeometry.RingedSpaceThickening.trivialYonedaExtension_action, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 954. The attribute's comment: “part (2'): the canonical map of the trivial extension is c”.

Stacks Project, Tag 08LB, part (2'). The canonical map of the trivial extension is the prescribed one: c_{ℱ'_{c,triv}} = c. This is what places ℱ'_{c,triv} in the set of extensions with c = c_{ℱ'} that part (4) of the remark puts in bijection with Ext¹_{𝒪_X}(ℱ, 𝒦).

theorem trivialYonedaExtension_action :
    (firstOrderExtensionAction i F K hi (trivialYonedaExtension i π F K c hi)).1 = c

AlgebraicGeometry.RingedSpaceThickening.splitRestriction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1002. The attribute's comment: “part (3): reading an extension as an 𝒪_X-module along the trivialization”.

Stacks Project, Tag 08LB, part (3). Reading a sheaf of 𝒪_{X'}-modules as a sheaf of 𝒪_X-modules along a trivialization: pushforward along the retraction.

This is the ringed-space form of the source's "use π^♯ : 𝒪_X ⟶ 𝒪_{X'} to think of ℱ' as an 𝒪_X-module". On a single site one would restrict scalars along π^♯ (Stacks.SheafOfModules.restrictScalarsSplitIso), but here X and X' carry different sites Opens X and Opens X', so the reindexing of opens along the homeomorphism π has to be carried along with the restriction of scalars — which is exactly what π_* does.

noncomputable abbrev splitRestriction :
    SheafOfModules.{u} (structureSheafRing X') ⥤ SheafOfModules.{u} (structureSheafRing X)

AlgebraicGeometry.RingedSpaceThickening.splitExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1048. The attribute's comment: “part (3): an extension read as a sequence of 𝒪_X-modules”.

Stacks Project, Tag 08LB, part (3). The extension 0 ⟶ i_* 𝒦 ⟶ ℱ' ⟶ i_* ℱ ⟶ 0 of 𝒪_{X'}-modules, read as a short complex of 𝒪_X-modules along the trivialization. Its outer terms are 𝒦 and ℱ themselves, by AlgebraicGeometry.RingedSpaceThickening.splitRestrictionIso.

noncomputable def splitExtension : ShortComplex (SheafOfModules.{u} (structureSheafRing X))

AlgebraicGeometry.RingedSpaceThickening.splitExtension_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1077. The attribute's comment: “part (3): the sequence read over 𝒪_X is short exact”.

Stacks Project, Tag 08LB, part (3). An extension across the thickening, read along the trivialization, is again short exact — which is what makes the class ξ_{ℱ'} available.

Pushforward along π.retraction is left exact because it is a right adjoint (RingedSpaceModuleAdjunction.modulePushforward_isRightAdjoint) and right exact because the base map of a trivialization is a homeomorphism (Stacks.ClosedImmersion.preservesFiniteColimits_modulePushforward_of_isIso_base), so the sequence maps across by CategoryTheory.ShortComplex.ShortExact.map_of_exact; the outer terms are then only reindexed by isomorphisms.

theorem splitExtension_shortExact : (splitExtension i π F K E).ShortExact

AlgebraicGeometry.RingedSpaceThickening.underlyingExtensionClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1093. The attribute's comment: “part (3): the class ξ_{ℱ'} of an extension”.

Stacks Project, Tag 08LB, part (3). The class ξ_{ℱ'} ∈ Ext¹_{𝒪_X}(ℱ, 𝒦) of an extension of ℱ by 𝒦 across a trivialized first order thickening of ringed spaces: the trivialization lets the extension be read as an extension of 𝒪_X-modules, and this is the class of that extension.

noncomputable def underlyingExtensionClass
    [HasExt.{e} (SheafOfModules.{u} (structureSheafRing X))] :
    CategoryTheory.Abelian.Ext F K 1

AlgebraicGeometry.RingedSpaceThickening.underlyingExtensionClass_trivialYonedaExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1197. The attribute's comment: “part (5): the trivial extension has class ξ_{ℱ'_{c,triv}} = 0”.

Stacks Project, Tag 08LB, part (5). The trivial extension maps to the zero class: ξ_{ℱ'_{c,triv}} = 0 in Ext¹_{𝒪_X}(ℱ, 𝒦).

Read along the trivialization the sequence 0 ⟶ 𝒦 ⟶ ℱ ⊕ 𝒦 ⟶ ℱ ⟶ 0 splits, because the derivation d kills every scalar pulled back along π and so the correction term c(d r ⊗ m) in the action disappears — the projection onto the 𝒦-summand, which is not 𝒪_{X'}-linear, becomes 𝒪_X-linear. A split short exact sequence has zero class by AlgebraicGeometry.RingedSpaceThickening.extClass_eq_zero_of_retraction.

theorem underlyingExtensionClass_trivialYonedaExtension
    [HasExt.{e} (SheafOfModules.{u} (structureSheafRing X))] :
    underlyingExtensionClass i π hi.1.1 F K (trivialYonedaExtension i π F K c hi) = 0

AlgebraicGeometry.RingedSpaceThickening.exists_iso_of_underlyingExtensionClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1380. The attribute's comment: “part (4): injectivity of ℱ' ↦ ξ_{ℱ'} — two extensions as in 08L4 with the same canonical map c and the same class ξ are isomorphic as extensions”.

Stacks Project, Tag 08LB, part (4). Injectivity of ℱ' ↦ ξ_{ℱ'} on isomorphism classes: two extensions across the thickening with the same canonical map and the same class ξ are isomorphic as extensions, by an isomorphism of their middle terms compatible with both end terms.

This is AlgebraicGeometry.RingedSpaceThickening.extClass_eq_of_underlyingExtensionClass_eq together with the fact that two short exact sequences with the same class in Ext¹ are isomorphic over the identity of both end terms (CategoryTheory.Abelian.Ext.extClass_surjective_and_eq_iff_iso_and_baerSum).

theorem exists_iso_of_underlyingExtensionClass_eq
    (E E' : Abelian.YonedaExtension ((modulePushforward i).obj F)
      ((modulePushforward i).obj K) 0)
    (hact : (firstOrderExtensionAction i F K hi E).val =
      (firstOrderExtensionAction i F K hi E').val)
    (hξ : underlyingExtensionClass i π hi.1.1 F K E =
      underlyingExtensionClass i π hi.1.1 F K E') :
    ∃ φ : E.Z.left ≅ E'.Z.left, E.f ≫ φ.hom = E'.f ∧ φ.hom ≫ E'.g = E.g

AlgebraicGeometry.RingedSpaceThickening.exists_yonedaExtension_underlyingExtensionClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1406. The attribute's comment: “part (4): surjectivity of ℱ' ↦ ξ_{ℱ'} — every class in Ext¹_{𝒪_X}(ℱ, 𝒦) is the class of an extension as in 08L4 with canonical map c”.

Stacks Project, Tag 08LB, part (4). Surjectivity of ℱ' ↦ ξ_{ℱ'}: every class η ∈ Ext¹_{𝒪_X}(ℱ, 𝒦) is the class ξ_{ℱ'} of an extension ℱ' as in Stacks 08L4 whose canonical map is the prescribed c.

Realize η as an extension of 𝒪_X-modules and push it forward along the thickening: its middle term is a direct image, so by Stacks 08L7 it can be added to the trivial extension ℱ'_{c,triv} of part (1) without changing the canonical map, which is c by part (2'). The class of the sum is 0 + η = η by part (5) and additivity.

theorem exists_yonedaExtension_underlyingExtensionClass_eq
    (c : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj
      ((idealSheafPullback i))).obj (F)) ⟶ K) (η : Abelian.Ext.{e} F K 1) :
    ∃ E : Abelian.YonedaExtension ((modulePushforward i).obj F)
        ((modulePushforward i).obj K) 0,
      (firstOrderExtensionAction i F K hi E).val = c ∧
        underlyingExtensionClass i π hi.1.1 F K E = η

AlgebraicGeometry.RingedSpaceThickening.bijective_underlyingExtensionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialExtension.lean, line 1470. The attribute's comment: “part (4): ℱ' ↦ ξ_{ℱ'} is a bijection from the isomorphism classes of extensions as in 08L4 with c = c_{ℱ'} onto Ext¹_{𝒪_X}(ℱ, 𝒦), the isomorphism classes being represented by their classes in Ext¹_{𝒪_{X'}}(i_* ℱ, i_* 𝒦)”.

Stacks Project, Tag 08LB, part (4). ℱ' ↦ ξ_{ℱ'} is a bijection from the isomorphism classes of extensions 0 ⟶ i_* 𝒦 ⟶ ℱ' ⟶ i_* ℱ ⟶ 0 as in Stacks 08L4 with c = c_{ℱ'} onto Ext¹_{𝒪_X}(ℱ, 𝒦).

The isomorphism classes are the elements of AlgebraicGeometry.RingedSpaceThickening.extensionClassesWithAction, i.e. are represented by their classes in Ext¹_{𝒪_{X'}}(i_* ℱ, i_* 𝒦), and the map is AlgebraicGeometry.RingedSpaceThickening.splitRestrictionExtHom, which on the class of ℱ' is ξ_{ℱ'} by AlgebraicGeometry.RingedSpaceThickening.underlyingExtensionClass_eq_splitRestrictionExtHom. The two halves of the statement, read on extensions rather than on classes, are AlgebraicGeometry.RingedSpaceThickening.exists_yonedaExtension_underlyingExtensionClass_eq and AlgebraicGeometry.RingedSpaceThickening.exists_iso_of_underlyingExtensionClass_eq.

theorem bijective_underlyingExtensionClass
    (c : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj
      ((idealSheafPullback i))).obj (F)) ⟶ K) :
    Function.Bijective (fun ξ : ↥(extensionClassesWithAction i F K hi c) =>
      splitRestrictionExtHom i π hi.1.1 F K ξ.1)

Tag 08LC, a remark

Tag 08LC in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.PushoutDescentData.extensionOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionPushoutDescent.lean, line 1383. The attribute's comment: “the canonical map on extensions, by pushout along the map of kernel modules”.

Stacks Project, Tag 08LC. The extension over the first thickening produced from an extension over the second: the pushout ℱ'₂ ⊔_{𝒦₂} 𝒦₁ carries an 𝒪_{X'}-module structure, built by descending the action of T = 𝒪'₂ ⋉ ℐ₁ twisted by c₁ along the locally surjective q : T ⟶ 𝒪_{X'}, and sits in a short exact sequence 0 → i_* 𝒦₁ → ℱ'₁ → i_* ℱ → 0 of 𝒪_{X'}-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 :
    CategoryTheory.Abelian.YonedaExtension ((modulePushforward i).obj dat.F)
      ((modulePushforward i).obj dat.K₁) 0

AlgebraicGeometry.RingedSpaceThickening.PushoutDescentData.extensionOne_action, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionPushoutDescent.lean, line 1471. The attribute's comment: “the canonical map of the pushed-out extension is c₁”.

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

theorem extensionOne_action :
    (firstOrderExtensionAction i dat.F dat.K₁ hi (dat.extensionOne E₂ hi hE₂)).val = dat.c₁

Tag 08LD, a remark

Tag 08LD in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.PushoutDescentData.underlyingExtensionClass_extensionOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/PushoutDescentClass.lean, line 233. The attribute's comment: “the square commutes for the extension Tag 08LC produces”.

Stacks Project, Tag 08LD. The square of the remark commutes for the extension that Tag 08LC produces: let h = SecondThickening.spaceHom be the morphism of first order thickenings of (X, 𝒪_X) that h^♯ presents, let both thickenings be trivialized by π₁ and π₂ with π₁ = h ≫ π₂, so that h is a morphism of trivialized thickenings, and let the square relating c₁, c₂, κ and ℐ₂ ⟶ ℐ₁ commute. If ℱ'₂ is an extension as in Tag 08L4 whose canonical map is c₂, then the class ξ of Tag 08LB of the extension AlgebraicGeometry.RingedSpaceThickening.PushoutDescentData.extensionOne that Tag 08LC produces from it is the image of ξ_{ℱ'₂} under functoriality of Ext¹_{𝒪_X}(ℱ, -) along κ.

Both extensions are members of the two sets the square relates: hE₂ says that the canonical map of ℱ'₂ is c₂, and PushoutDescentData.extensionOne_action says that the canonical map of the extension produced from it is c₁.

The hypothesis hc is the remark's commuting square, written with the induced map of ideals AlgebraicGeometry.RingedSpaceThickening.thickeningIdealMap. The field AlgebraicGeometry.RingedSpaceThickening.PushoutDescentData.comm of dat is the same square of the same remark, written on local pure tensors, which is the form the construction of Tag 08LC consumes; no cross-thickening comparison of the two canonical maps is available to pass between the two forms, so the square is assumed in both.

theorem underlyingExtensionClass_extensionOne
    [HasExt.{e} (SheafOfModules.{u} (structureSheafRing X))]
    (π₁ : SplitMono i) (π₂ : SplitMono S.hom)
    (hπ : π₁.retraction = S.spaceHom ≫ π₂.retraction)
    (hc : dat.c₂ ≫ dat.kernelMap =
      (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩)).map
        ((thickeningIdealMap i S.hom S.spaceHom S.comp_spaceHom, 𝟙 dat.F) : (_, _) ⟶ (_, _)) ≫
          dat.c₁) :
    underlyingExtensionClass i π₁ hi.1.1 dat.F dat.K₁ (dat.extensionOne E₂ hi hE₂) =
      (underlyingExtensionClass S.hom π₂ S.firstOrder.1.1 dat.F dat.K₂ E₂).comp
        (CategoryTheory.Abelian.Ext.mk₀ dat.kernelMap) (add_zero 1)

AlgebraicGeometry.RingedSpaceThickening.underlyingExtensionClass_eq_of_pushedExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivializedFunctoriality.lean, line 394. The attribute's comment: “the commutative square relating the two extension classes”.

For a morphism h : X'₁ ⟶ X'₂ of trivialized first order thickenings of (X, 𝒪_X) the square relating the extension classes commutes: if ℱ'₁ is the extension that the functoriality of Tag 08LC produces from ℱ'₂ and k : 𝒦₂ ⟶ 𝒦₁, then the class ξ_{ℱ'₁} of Tag 08LB is the image of ξ_{ℱ'₂} under functoriality of Ext¹_{𝒪_X}(ℱ, -) along k.

The hypotheses hc, hE₂ and hE₁ say that the two extensions are members of the two sets the square relates — that their canonical maps of Tag 08L4 are c₂ and c₁, compatibly with k. The identity of classes uses only the map of extensions w.

theorem underlyingExtensionClass_eq_of_pushedExtension (i₁ : X ⟶ X₁) (i₂ : X ⟶ X₂)
    (h : X₁ ⟶ X₂) (comm : i₁ ≫ h = i₂)
    (hi₁ : IsFirstOrderThickening i₁) (hi₂ : IsFirstOrderThickening i₂)
    (π₁ : SplitMono i₁) (π₂ : SplitMono i₂)
    (hπ : π₁.retraction = h ≫ π₂.retraction)
    (F K₁ K₂ : SheafOfModules.{u} (structureSheafRing X)) (k : K₂ ⟶ K₁)
    (c₁ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj
      ((idealSheafPullback i₁))).obj (F)) ⟶ K₁)
    (c₂ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X)).presheaf, ((X)).IsSheaf⟩).obj
      ((idealSheafPullback i₂))).obj (F)) ⟶ K₂)
    (_hc : c₂ ≫ k = ((Functor.uncurry.obj
      (Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X)).presheaf, ((X)).IsSheaf⟩)).map
        (((thickeningIdealMap i₁ i₂ h comm), (𝟙 F)) : (_, _) ⟶ (_, _))) ≫ c₁)
    (E₂ : CategoryTheory.Abelian.YonedaExtension ((modulePushforward i₂).obj F)
      ((modulePushforward i₂).obj K₂) 0)
    (_hE₂ : (firstOrderExtensionAction i₂ F K₂ hi₂ E₂).val = c₂)
    (E₁ : CategoryTheory.Abelian.YonedaExtension ((modulePushforward i₁).obj F)
      ((modulePushforward i₁).obj K₁) 0)
    (_hE₁ : (firstOrderExtensionAction i₁ F K₁ hi₁ E₁).val = c₁)
    (w : PushedExtension i₁ i₂ h comm F K₁ K₂ k E₂ E₁) :
    underlyingExtensionClass i₁ π₁ hi₁.1.1 F K₁ E₁ =
      (underlyingExtensionClass i₂ π₂ hi₂.1.1 F K₂ E₂).comp
        (CategoryTheory.Abelian.Ext.mk₀ k) (add_zero 1)

Tag 08LE, a remark

Tag 08LE in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.IsComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ThickeningSequence.lean, line 176. The attribute's comment: “complex of first order thickenings”.

Stacks Project, Tag 08LE. A sequence of first order thickenings of X is a complex when its induced maps on ideal modules compose to zero.

noncomputable abbrev IsComplex (S : FirstOrderThickeningSequence.{u}) : Prop

AlgebraicGeometry.RingedSpaceThickening.IsShortExact, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ThickeningSequence.lean, line 183. The attribute's comment: “short exact sequence of first order thickenings”.

Stacks Project, Tag 08LE. A sequence of first order thickenings of X is a short exact sequence when 0 ⟶ ℐ₃ ⟶ ℐ₂ ⟶ ℐ₁ ⟶ 0 is short exact as a sequence of 𝒪_X-modules.

noncomputable abbrev IsShortExact (S : FirstOrderThickeningSequence.{u}) : Prop

AlgebraicGeometry.RingedSpaceThickening.FirstOrderThickeningSequence.existsUnique_trivialization_of_isComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ThickeningTrivialization.lean, line 461. The attribute's comment: “canonical trivialization of a complex”.

Stacks Project, Tag 08LE. A complex of first order thickenings of (X, 𝒪_X) canonically trivializes its first thickening: the composite X₁ ⟶ X₃ factors uniquely through i₃ : X ⟶ X₃, and the factor π : X₁ ⟶ X is a retraction of i₁.

theorem existsUnique_trivialization_of_isComplex (hS : IsComplex S) :
    ∃! π : S.X₁ ⟶ S.X, (S.i₁ ≫ π = 𝟙 S.X) ∧ (π ≫ S.i₃ = S.f₁₂ ≫ S.f₂₃)

Tag 08LF, a remark

Tag 08LF in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.boundary_underlyingExtensionClass_eq_obstructionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/RestrictedExtensionAction.lean, line 356.

Stacks Project, Tag 08LF. Let (X, 𝒪_X) be a ringed space, ℱ an 𝒪_X-module and X'₁ ⟶ X'₂ ⟶ X'₃ a complex of first order thickenings of (X, 𝒪_X) (Tag 08LE), with ideals ℐᵢ. Let cᵢ : ℐᵢ ⊗_{𝒪_X} ℱ ⟶ 𝒦ᵢ be maps and 0 ⟶ 𝒦₃ ⟶ 𝒦₂ ⟶ 𝒦₁ ⟶ 0 a short exact sequence of 𝒪_X-modules for which the two squares of the remark commute. Let ℱ'₂ be an extension 0 ⟶ 𝒦₂ ⟶ ℱ'₂ ⟶ ℱ ⟶ 0 as in Tag 08L4 over X'₂ with c_{ℱ'₂} = c₂, and let ℱ'₁ be the extension over X'₁ that the functoriality of Tag 08LC produces from it. That functoriality carries ℱ'₂ to an extension as in Tag 08L4 over X'₁ together with a map of extensions w from ℱ'₂, which is 𝒦₂ ⟶ 𝒦₁ on kernels and the identity on ℱ; the statement is made for every extension ℱ'₁ over X'₁ receiving such a map, so in particular for the one of Tag 08LC (which in addition has c_{ℱ'₁} = c₁, a property the identity of classes does not use).

Then the boundary map ∂ : Ext¹_{𝒪_X}(ℱ, 𝒦₁) ⟶ Ext²_{𝒪_X}(ℱ, 𝒦₃) of 0 ⟶ 𝒦₃ ⟶ 𝒦₂ ⟶ 𝒦₁ ⟶ 0 — Yoneda composition with the class of that sequence — sends the class ξ_{ℱ'₁} of Tag 08LB, formed with the canonical splitting π of Tag 08LE, to the obstruction class o(ℱ, 𝒦₃, c₃) of Tag 08L8.

The first compatibility square of the remark, relating c₂, c₁ and 𝒦₂ ⟶ 𝒦₁, is what makes Tag 08LC applicable; once ℱ'₁ and w are given it is not needed for the identity of classes, so it is not a hypothesis here. It is a hypothesis of the version for the extension that Tag 08LC constructs, boundary_underlyingExtensionClass_extensionOne_eq_obstructionClass, where it is the input of that construction; the map c₁ enters only through that square, so it does not appear here either.

theorem boundary_underlyingExtensionClass_eq_obstructionClass
    (S : FirstOrderThickeningSequence.{u})
    [HasExt (SheafOfModules.{u} (structureSheafRing S.X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing S.X))]
    (hS : IsComplex S) (F K₁ K₂ K₃ : SheafOfModules.{u} (structureSheafRing S.X))
    (k₃₂ : K₃ ⟶ K₂) (k₂₁ : K₂ ⟶ K₁) (hk : k₃₂ ≫ k₂₁ = 0)
    (hK : (ShortComplex.mk k₃₂ k₂₁ hk).ShortExact)
    (c₂ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨S.X.presheaf, S.X.IsSheaf⟩).obj
      (idealSheafPullback S.i₂)).obj F) ⟶ K₂)
    (c₃ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨S.X.presheaf, S.X.IsSheaf⟩).obj
      (idealSheafPullback S.i₃)).obj F) ⟶ K₃)
    (hc₃₂ : c₃ ≫ k₃₂ =
      ((Functor.uncurry.obj
        (Stacks.SheafOfModules.Tensor.sheafTensor ⟨S.X.presheaf, S.X.IsSheaf⟩)).map
        (((thickeningIdealMap S.i₂ S.i₃ S.f₂₃ S.comm₂₃), (𝟙 F)) : (_, _) ⟶ (_, _))) ≫ c₂)
    (E₂ : CategoryTheory.Abelian.YonedaExtension ((modulePushforward S.i₂).obj F)
      ((modulePushforward S.i₂).obj K₂) 0)
    (hE₂ : (firstOrderExtensionAction S.i₂ F K₂ S.firstOrder₂ E₂).val = c₂)
    (E₁ : CategoryTheory.Abelian.YonedaExtension ((modulePushforward S.i₁).obj F)
      ((modulePushforward S.i₁).obj K₁) 0)
    (w : PushedExtension S.i₁ S.i₂ S.f₁₂ S.comm₁₂ F K₁ K₂ k₂₁ E₂ E₁) :
    (underlyingExtensionClass S.i₁ (S.trivialization hS) S.firstOrder₁.1.1 F K₁ E₁).comp
        hK.extClass (by decide) =
      obstructionClass S.i₃ S.firstOrder₃ F K₃ c₃

AlgebraicGeometry.RingedSpaceThickening.boundary_underlyingExtensionClass_extensionOne_eq_obstructionClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/RestrictedExtensionAction.lean, line 601.

Stacks Project, Tag 08LF, for the extension ℱ'₁ that Tag 08LC constructs. Let X'₁ ⟶ X'₂ ⟶ X'₃ be a complex of first order thickenings of (X, 𝒪_X) (Tag 08LE), with X'₂ presented on the space of X'₁ as in Tag 08LC, and let (𝒦ᵢ, cᵢ), a short exact sequence 0 ⟶ 𝒦₃ ⟶ 𝒦₂ ⟶ 𝒦₁ ⟶ 0 and the two commutative squares be as in the remark. For an extension ℱ'₂ over X'₂ as in Tag 08L4 with c_{ℱ'₂} = c₂, let ℱ'₁ be the extension over X'₁ that the functoriality of Tag 08LC produces (PushoutDescentData.extensionOne). Then the boundary map Ext¹_{𝒪_X}(ℱ, 𝒦₁) ⟶ Ext²_{𝒪_X}(ℱ, 𝒦₃) sends ξ_{ℱ'₁}, formed with the canonical splitting of Tag 08LE, to the obstruction class o(ℱ, 𝒦₃, c₃) of Tag 08L8.

theorem boundary_underlyingExtensionClass_extensionOne_eq_obstructionClass
    {X₁ : RingedSpace.{u, u}} {i : X ⟶ X₁} (hi : IsFirstOrderThickening i)
    (ST : SecondThickening i) (i₃ : X ⟶ X₃) (hi₃ : IsFirstOrderThickening i₃)
    (f₂₃ : ST.space ⟶ X₃) (comm₂₃ : ST.hom ≫ f₂₃ = i₃)
    (idealMap₂₁ : (modulePullback ST.hom).obj (AlgebraicGeometry.SheafOfModules.idealSheaf ST.hom) ⟶
      (modulePullback i).obj (AlgebraicGeometry.SheafOfModules.idealSheaf i))
    (idealMap₃₂ : (modulePullback i₃).obj (AlgebraicGeometry.SheafOfModules.idealSheaf i₃) ⟶
      (modulePullback ST.hom).obj (AlgebraicGeometry.SheafOfModules.idealSheaf ST.hom))
    [HasExt (SheafOfModules.{u} (structureSheafRing X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing X))]
    (hS : IsComplex (ST.thickeningSequence hi i₃ hi₃ f₂₃ comm₂₃ idealMap₂₁ idealMap₃₂))
    (F K₁ K₂ K₃ : SheafOfModules.{u} (structureSheafRing X))
    (k₃₂ : K₃ ⟶ K₂) (k₂₁ : K₂ ⟶ K₁) (hk : k₃₂ ≫ k₂₁ = 0)
    (hK : (ShortComplex.mk k₃₂ k₂₁ hk).ShortExact)
    (c₁ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩).obj
      (idealSheafPullback i)).obj F) ⟶ K₁)
    (c₂ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩).obj
      (idealSheafPullback ST.hom)).obj F) ⟶ K₂)
    (c₃ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩).obj
      (idealSheafPullback i₃)).obj F) ⟶ K₃)
    (hc₂₁ : c₂ ≫ k₂₁ =
      ((Functor.uncurry.obj
        (Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩)).map
        (((thickeningIdealMap i ST.hom ST.toSpace ST.comp_toSpace), (𝟙 F)) :
          (_, _) ⟶ (_, _))) ≫ c₁)
    (hc₃₂ : c₃ ≫ k₃₂ =
      ((Functor.uncurry.obj
        (Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩)).map
        (((thickeningIdealMap ST.hom i₃ f₂₃ comm₂₃), (𝟙 F)) : (_, _) ⟶ (_, _))) ≫ c₂)
    (E₂ : CategoryTheory.Abelian.YonedaExtension ((modulePushforward ST.hom).obj F)
      ((modulePushforward ST.hom).obj K₂) 0)
    (hE₂ : (firstOrderExtensionAction ST.hom F K₂ ST.firstOrder E₂).val = c₂) :
    (underlyingExtensionClass i
        ((ST.thickeningSequence hi i₃ hi₃ f₂₃ comm₂₃ idealMap₂₁ idealMap₃₂).trivialization hS)
        hi.1.1 F K₁
        ((PushoutDescentData.ofSquare ST F K₁ K₂ c₁ c₂ k₂₁ hc₂₁).extensionOne E₂ hi hE₂)).comp
        hK.extClass (by decide) =
      obstructionClass i₃ hi₃ F K₃ c₃

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

Stacks Project, Tag 08LF. Let (X, 𝒪_X) be a ringed space, ℱ an 𝒪_X-module, and let X'₁ ⟶ X'₂ ⟶ X'₃ be a complex of first order thickenings of (X, 𝒪_X), with π the canonical trivialization of i₁ (Tag 08LE). Let (𝒦ᵢ, cᵢ) be pairs with cᵢ : ℐᵢ ⊗_{𝒪_X} ℱ ⟶ 𝒦ᵢ and let 0 ⟶ 𝒦₃ ⟶ 𝒦₂ ⟶ 𝒦₁ ⟶ 0 be a short exact sequence of 𝒪_X-modules making the two squares _hc₂₁ and hc₃₂ of the remark commute. Let ℱ'₂ be an extension as in Tag 08L4 over X'₂ with c_{ℱ'₂} = c₂ and let ℱ'₁ be the extension over X'₁ that Tag 08LC produces from it, exhibited by the map of extensions w and the pushout square hw.

Then the boundary map ∂ : Ext¹_{𝒪_X}(ℱ, 𝒦₁) ⟶ Ext²_{𝒪_X}(ℱ, 𝒦₃) of 0 ⟶ 𝒦₃ ⟶ 𝒦₂ ⟶ 𝒦₁ ⟶ 0 — Yoneda composition with the class of that sequence — carries ξ_{ℱ'₁} of Tag 08LB to the obstruction class o(ℱ, 𝒦₃, c₃) of Tag 08L8.

The hypothesis hrestrict is not derived in this development; see the Scope section of the module docstring. The hypotheses _hS, _hc₂₁, _hE₂ and _hE₁ are part of the situation of the remark but are not used: the complex condition enters only through hπ, which is what the canonical trivialization of Tag 08LE supplies, and the canonical maps of ℱ'₂ and ℱ'₁ enter only through hrestrict and w.

theorem boundary_underlyingExtensionClass (S : FirstOrderThickeningSequence.{u})
    [HasExt (SheafOfModules.{u} (structureSheafRing S.X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing S.X))]
    (_hS : IsComplex S) (π : SplitMono S.i₁)
    (hπ : π.retraction ≫ S.i₃ = S.f₁₂ ≫ S.f₂₃)
    (F K₁ K₂ K₃ : SheafOfModules.{u} (structureSheafRing S.X))
    (k₃₂ : K₃ ⟶ K₂) (k₂₁ : K₂ ⟶ K₁) (hk : k₃₂ ≫ k₂₁ = 0)
    (hK : (ShortComplex.mk k₃₂ k₂₁ hk).ShortExact)
    (c₁ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((S.X)).presheaf, ((S.X)).IsSheaf⟩).obj
      ((idealSheafPullback S.i₁))).obj (F)) ⟶ K₁)
    (c₂ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((S.X)).presheaf, ((S.X)).IsSheaf⟩).obj
      ((idealSheafPullback S.i₂))).obj (F)) ⟶ K₂)
    (c₃ : (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((S.X)).presheaf, ((S.X)).IsSheaf⟩).obj
      ((idealSheafPullback S.i₃))).obj (F)) ⟶ K₃)
    (_hc₂₁ : c₂ ≫ k₂₁ =
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨((S.X)).presheaf, ((S.X)).IsSheaf⟩)).map
        (((thickeningIdealMap S.i₁ S.i₂ S.f₁₂ S.comm₁₂), (𝟙 F)) : (_, _) ⟶ (_, _))) ≫ c₁)
    (hc₃₂ : c₃ ≫ k₃₂ =
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨((S.X)).presheaf, ((S.X)).IsSheaf⟩)).map
        (((thickeningIdealMap S.i₂ S.i₃ S.f₂₃ S.comm₂₃), (𝟙 F)) : (_, _) ⟶ (_, _))) ≫ c₂)
    (E₂ : CategoryTheory.Abelian.YonedaExtension ((modulePushforward S.i₂).obj F)
      ((modulePushforward S.i₂).obj K₂) 0)
    (_hE₂ : (firstOrderExtensionAction S.i₂ F K₂ S.firstOrder₂ E₂).val = c₂)
    (E₁ : CategoryTheory.Abelian.YonedaExtension ((modulePushforward S.i₁).obj F)
      ((modulePushforward S.i₁).obj K₁) 0)
    (_hE₁ : (firstOrderExtensionAction S.i₁ F K₁ S.firstOrder₁ E₁).val = c₁)
    (w : PushedExtension S.i₁ S.i₂ S.f₁₂ S.comm₁₂ F K₁ K₂ k₂₁ E₂ E₁)
    (hw : IsPushout E₂.f ((modulePushforward S.i₂).map k₂₁ ≫
        (thickeningPushforwardComp S.i₁ S.i₂ S.f₁₂ S.comm₁₂).inv.app K₁) w.hom
        ((modulePushforward S.f₁₂).map E₁.f))
    (hrestrict : (firstOrderExtensionAction S.i₃ F K₂ S.firstOrder₃
        (sequenceRestrictedExtension S F K₂ E₂)).val =
      ((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨((S.X)).presheaf, ((S.X)).IsSheaf⟩)).map
        (((thickeningIdealMap S.i₂ S.i₃ S.f₂₃ S.comm₂₃), (𝟙 F)) : (_, _) ⟶ (_, _))) ≫ c₂) :
    (underlyingExtensionClass S.i₁ π S.firstOrder₁.1.1 F K₁ E₁).comp hK.extClass (by decide) =
      obstructionClass S.i₃ S.firstOrder₃ F K₃ c₃

Sources

LeanAlgebraicGeometry.RingedSpaceThickening.firstOrderExtensionAction · CategoryTheory.Abelian.YonedaExtension · AlgebraicGeometry.RingedSpaceThickening.ExtensionPair.extensionAction_naturality · AlgebraicGeometry.RingedSpaceThickening.ExtensionPair.exists_compatibleMap_translate · AlgebraicGeometry.RingedSpaceThickening.ExtensionPair.existsUnique_translate · AlgebraicGeometry.RingedSpaceThickening.mapLiftingObstruction · AlgebraicGeometry.RingedSpaceThickening.extensionClassesWithAction_principalHomogeneous · AlgebraicGeometry.RingedSpaceThickening.exists_extClass_add_of_essImage

Section91.5 Infinitesimal deformations of modules on ringed spaces #

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

Tag 08LH, a lemma

Tag 08LH in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.mapLift_isPrincipalHomogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/MapLift.lean, line 360.

Stacks Project, Tag 08LH. Let i : X ⟶ X' be a first-order thickening of ringed spaces with ideal ℐ, let ℱ' and 𝒢' be 𝒪_{X'}-modules and let φ : i^* ℱ' ⟶ i^* 𝒢'. If φ lifts to X', its lifts form a principal homogeneous space under Hom_{𝒪_X}(i^* ℱ', ℐ𝒢'): any two lifts differ by exactly one element of that group.

The difference of two lifts is killed by 𝒢' ⟶ i_* i^* 𝒢', so it factors uniquely through ℐ𝒢', and infinitesimalHomEquiv turns that factorization into the translating element.

theorem mapLift_isPrincipalHomogeneous (hi : IsFirstOrderThickening i)
    (F' G' : SheafOfModules.{u} (structureSheafRing X'))
    (φ : (modulePullback i).obj F' ⟶ (modulePullback i).obj G')
    (_hne : Nonempty (MapLift i F' G' φ)) :
    ∀ φ₁ φ₂ : MapLift i F' G' φ,
      ∃! δ : InfinitesimalHom i F' G',
        infinitesimalHomEquiv i hi F' G' δ ≫ infinitesimalι i G' + φ₁.1 = φ₂.1

AlgebraicGeometry.RingedSpaceThickening.exists_addTorsor_mapLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/MapLiftTorsor.lean, line 168.

Stacks Project, Tag 08LH. Let i : X ⟶ X' be a first-order thickening of ringed spaces with ideal ℐ, let ℱ' and 𝒢' be 𝒪_{X'}-modules, ℱ = i^* ℱ', 𝒢 = i^* 𝒢', and let φ : ℱ ⟶ 𝒢 be 𝒪_X-linear. If the set of lifts of φ to an 𝒪_{X'}-linear map φ' : ℱ' ⟶ 𝒢' (those with i^* φ' = φ) is nonempty, it is a principal homogeneous space under Hom_{𝒪_X}(ℱ, ℐ𝒢'), where ℐ𝒢' is the image of the ideal action ℐ ⊗ 𝒢' ⟶ 𝒢' read as an 𝒪_X-module: there is a torsor structure in which δ acts on a lift φ' by adding the 𝒪_{X'}-linear map ℱ' ⟶ ℐ𝒢' ⟶ 𝒢' corresponding to δ.

theorem exists_addTorsor_mapLift (hi : IsFirstOrderThickening i)
    (F' G' : SheafOfModules.{u} (structureSheafRing X'))
    (φ : (modulePullback i).obj F' ⟶ (modulePullback i).obj G')
    (hne : Nonempty (MapLift i F' G' φ)) :
    ∃ t : AddTorsor
        ((modulePullback i).obj F' ⟶ (modulePullback i).obj (Abelian.image (idealAction i G')))
        (MapLift i F' G' φ),
      ∀ (δ : (modulePullback i).obj F' ⟶
          (modulePullback i).obj (Abelian.image (idealAction i G')))
        (φ' : MapLift i F' G' φ),
        (t.vadd δ φ').1 =
          φ'.1 + idealMultipleHomEquiv i hi F' G' δ ≫ Abelian.image.ι (idealAction i G')

Tag 08LI, a lemma

Tag 08LI in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.isFlatOver_iff_baseToInfinitesimal_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatCriterion.lean, line 1799. The attribute's comment: “flatness criterion”. References: SGA 3 XV (2.7), “more general”.

Stacks Project, Tag 08LI. For a strict morphism of first-order thickenings of ringed spaces and an 𝒪_{X'}-module ℱ' whose restriction ℱ = i^* ℱ' is flat over S, the module ℱ' is flat over S' if and only if the canonical map f^* 𝒥 ⊗_{𝒪_X} ℱ ⟶ ℐℱ' is an isomorphism.

One direction is baseToInfinitesimal_isIso_of_isFlatOver: flatness makes the ideal action injective, and the map in question is i^* of an epimorphism which that injectivity turns into an isomorphism. For the other, invertibility makes the action of (f')^* 𝒥 on ℱ' a monomorphism, hence injective on every stalk after base change; the flatness of ℱ over S supplies the quotient hypothesis of the square-zero local criterion, and strictness is what identifies the relevant quotient of 𝒪_{X',x} with 𝒪_{X,x}.

theorem isFlatOver_iff_baseToInfinitesimal_isIso (D : MorphismOfThickenings.{u})
    (hi : IsFirstOrderThickening D.i) (ht : IsFirstOrderThickening D.t) (hs : D.IsStrict)
    (F' : SheafOfModules.{u} (structureSheafRing D.X'))
    (hF : AlgebraicGeometry.IsFlatOver D.f ((modulePullback D.i).obj F')) :
    AlgebraicGeometry.IsFlatOver D.f' F' ↔ IsIso (baseToInfinitesimal D F')

AlgebraicGeometry.RingedSpaceThickening.baseToSourceIdealTensor_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatCriterion.lean, line 1886. The attribute's comment: “first isomorphism in the final assertion”.

Stacks Project, Tag 08LI. Under the hypotheses of the criterion and flatness of ℱ' over S', the reduced canonical ideal map tensored with ℱ is an isomorphism: it is an epimorphism by strictness, and a monomorphism because the composite with the ideal action is one.

theorem baseToSourceIdealTensor_isIso (D : MorphismOfThickenings.{u})
    (hi : IsFirstOrderThickening D.i) (ht : IsFirstOrderThickening D.t) (hs : D.IsStrict)
    (F' : SheafOfModules.{u} (structureSheafRing D.X'))
    (hF : AlgebraicGeometry.IsFlatOver D.f ((modulePullback D.i).obj F'))
    (hF' : AlgebraicGeometry.IsFlatOver D.f' F') :
    IsIso (baseToSourceIdealTensor D F')

AlgebraicGeometry.RingedSpaceThickening.sourceIdealActionImage_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatCriterion.lean, line 1906. The attribute's comment: “second isomorphism in the final assertion”.

Stacks Project, Tag 08LI. Under the hypotheses of the criterion and flatness of ℱ' over S', the ideal action on the reduced source identifies i^* ℐ ⊗_{𝒪_X} ℱ with the ideal multiple ℐℱ'.

theorem sourceIdealActionImage_isIso (D : MorphismOfThickenings.{u})
    (hi : IsFirstOrderThickening D.i) (ht : IsFirstOrderThickening D.t) (hs : D.IsStrict)
    (F' : SheafOfModules.{u} (structureSheafRing D.X'))
    (hF : AlgebraicGeometry.IsFlatOver D.f ((modulePullback D.i).obj F'))
    (hF' : AlgebraicGeometry.IsFlatOver D.f' F') :
    IsIso (sourceIdealActionImage D F')

Tag 08LJ, a lemma

Tag 08LJ in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.mapLift_isTorsor_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatCriterion.lean, line 2039.

Stacks Project, Tag 08LJ. Let (f, f') be a morphism of thickenings with i a first order thickening, let ℱ' and 𝒢' be 𝒪_{X'}-modules, set ℱ = i^* ℱ' and 𝒢 = i^* 𝒢', and let φ : ℱ ⟶ 𝒢 be 𝒪_X-linear. If 𝒢' is flat over S' and (f, f') is strict, the lifts of φ to an 𝒪_{X'}-linear φ' : ℱ' ⟶ 𝒢' form, when nonempty, a principal homogeneous space under Hom_{𝒪_X}(ℱ, 𝒢 ⊗_{𝒪_X} f^* 𝒥), which acts through infinitesimalTensorIso: each δ translates a lift to a lift, and any two lifts are translated to one another by exactly one δ.

The group acts because i^* is additive and kills a map through ℐ𝒢', which is modulePullback_map_add_comp_infinitesimalι. That the action is simply transitive is Stacks 08LH, which gives the same conclusion for Hom_{𝒪_X}(ℱ, ℐ𝒢'), transported along Stacks 08LI, which identifies ℐ𝒢' with 𝒢 ⊗_{𝒪_X} f^* 𝒥.

theorem mapLift_isTorsor_tensor (D : MorphismOfThickenings.{u})
    (hi : IsFirstOrderThickening D.i) (hs : D.IsStrict)
    (F' G' : SheafOfModules.{u} (structureSheafRing D.X'))
    (hG' : AlgebraicGeometry.IsFlatOver D.f' G')
    (φ : (modulePullback D.i).obj F' ⟶ (modulePullback D.i).obj G')
    (hne : Nonempty (MapLift D.i F' G' φ)) :
    (∀ (δ : (modulePullback D.i).obj F' ⟶ restrictionTensorBaseIdeal D G')
        (φ₁ : MapLift D.i F' G' φ),
        (modulePullback D.i).map
            (infinitesimalHomEquiv D.i hi F' G'
                  (δ ≫ (infinitesimalTensorIso D hs G' hG').hom) ≫ infinitesimalι D.i G' +
                φ₁.1) =
          φ) ∧
      ∀ φ₁ φ₂ : MapLift D.i F' G' φ,
        ∃! δ : (modulePullback D.i).obj F' ⟶ restrictionTensorBaseIdeal D G',
          infinitesimalHomEquiv D.i hi F' G'
                (δ ≫ (infinitesimalTensorIso D hs G' hG').hom) ≫ infinitesimalι D.i G' + φ₁.1 =
              φ₂.1

Tag 08LK, a lemma

Tag 08LK in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.exists_derivedMapLiftingObstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DerivedLiftingObstruction.lean, line 149.

Stacks Project, Tag 08LK. Let i : (X, 𝒪_X) ⟶ (X', 𝒪_{X'}) be a first order thickening of ringed spaces with ideal ℐ, let ℱ' and 𝒢' be 𝒪_{X'}-modules and let φ : i^* ℱ' ⟶ i^* 𝒢' be 𝒪_X-linear. There is a class o(φ) ∈ Ext¹_{𝒪_X}(Li^* ℱ', ℐ𝒢') whose vanishing is necessary and sufficient for φ to lift to an 𝒪_{X'}-linear map ℱ' ⟶ 𝒢'.

theorem exists_derivedMapLiftingObstruction (hi : IsFirstOrderThickening i)
    (F' G' : SheafOfModules.{u} (structureSheafRing X'))
    (φ : (modulePullback i).obj F' ⟶ (modulePullback i).obj G') :
    ∃ o : DerivedCategory.Ext
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback i).obj
          ((DerivedCategory.singleFunctor _ 0).obj F'))
        ((DerivedCategory.singleFunctor _ 0).obj (infinitesimalPartOnSource i G')) 1,
      (o = 0 ↔ Nonempty (MapLift i F' G' φ))

Tag 08LL, a lemma

Tag 08LL in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.mapLiftObstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/MapLiftObstruction.lean, line 405. The attribute's comment: “the obstruction class”.

Stacks Project, Tag 08LL. The obstruction class o(φ) ∈ Ext¹_{𝒪_X}(ℱ, 𝒢 ⊗_{𝒪_X} f^* 𝒥) to lifting an 𝒪_X-linear φ : ℱ ⟶ 𝒢 between the restrictions of two 𝒪_{X'}-modules flat over S', across a strict morphism of thickenings whose upper arrow is a first order thickening.

It is the class of Stacks 08L6 for the two kernel extensions of Stacks 08LM and the pair (φ, 1 ⊗ φ), carried into the source's group along the identification idealTensorIsoRestrictionTensorBaseIdeal of Stacks 08LI. Its vanishing criterion is AlgebraicGeometry.RingedSpaceThickening.mapLiftObstruction_eq_zero_iff.

noncomputable def mapLiftObstruction (hi : IsFirstOrderThickening D.i) (hs : D.IsStrict)
    (F' G' : SheafOfModules.{u} (structureSheafRing D.X'))
    (hF' : AlgebraicGeometry.IsFlatOver D.f' F')
    (hG' : AlgebraicGeometry.IsFlatOver D.f' G')
    (φ : (modulePullback D.i).obj F' ⟶ (modulePullback D.i).obj G') :
    CategoryTheory.Abelian.zExt ((modulePullback D.i).obj F')
      (restrictionTensorBaseIdeal D G') 1

AlgebraicGeometry.RingedSpaceThickening.mapLiftObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/MapLiftObstruction.lean, line 419. The attribute's comment: “the vanishing criterion”.

Stacks Project, Tag 08LL. The vanishing of the obstruction class o(φ) is necessary and sufficient for φ to lift to an 𝒪_{X'}-linear map φ' : ℱ' ⟶ 𝒢', that is one with i^* φ' = φ.

theorem mapLiftObstruction_eq_zero_iff (hi : IsFirstOrderThickening D.i) (hs : D.IsStrict)
    (F' G' : SheafOfModules.{u} (structureSheafRing D.X'))
    (hF' : AlgebraicGeometry.IsFlatOver D.f' F')
    (hG' : AlgebraicGeometry.IsFlatOver D.f' G')
    (φ : (modulePullback D.i).obj F' ⟶ (modulePullback D.i).obj G') :
    mapLiftObstruction hi hs F' G' hF' hG' φ = 0 ↔ Nonempty (MapLift D.i F' G' φ)

AlgebraicGeometry.RingedSpaceThickening.exists_mapLiftObstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/MapLiftObstruction.lean, line 451.

Stacks Project, Tag 08LL. Let (f, f') be a morphism of thickenings of ringed spaces whose upper arrow i : X ⟶ X' is a first order thickening, let ℱ' and 𝒢' be 𝒪_{X'}-modules, put ℱ = i^* ℱ' and 𝒢 = i^* 𝒢', and let φ : ℱ ⟶ 𝒢 be 𝒪_X-linear. Assume ℱ' and 𝒢' are flat over S' and that (f, f') is strict. Then there exists
o(φ) ∈ Ext¹_{𝒪_X}(ℱ, 𝒢 ⊗_{𝒪_X} f^* 𝒥)
whose vanishing is a necessary and sufficient condition for the existence of an 𝒪_{X'}-linear map φ' : ℱ' ⟶ 𝒢' with i^* φ' = φ.

The source asserts existence of the class, not uniqueness, and that is what is stated here; the class itself is AlgebraicGeometry.RingedSpaceThickening.mapLiftObstruction and its criterion AlgebraicGeometry.RingedSpaceThickening.mapLiftObstruction_eq_zero_iff.

theorem exists_mapLiftObstruction (hi : IsFirstOrderThickening D.i) (hs : D.IsStrict)
    (F' G' : SheafOfModules.{u} (structureSheafRing D.X'))
    (hF' : AlgebraicGeometry.IsFlatOver D.f' F')
    (hG' : AlgebraicGeometry.IsFlatOver D.f' G')
    (φ : (modulePullback D.i).obj F' ⟶ (modulePullback D.i).obj G') :
    ∃ o : CategoryTheory.Abelian.zExt ((modulePullback D.i).obj F')
        (restrictionTensorBaseIdeal D G') 1,
      (o = 0 ↔ Nonempty (MapLift D.i F' G' φ))

Tag 08LM, a lemma

Tag 08LM in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.flatLiftClassDifference_isPrincipalHomogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatLiftTorsor.lean, line 148.

Let (f, f') be a strict morphism of first order thickenings of ringed spaces and let ℱ be an 𝒪_X-module flat over S. The isomorphism classes of pairs (ℱ', α) of an 𝒪_{X'}-module ℱ' flat over S' and an isomorphism α : i^* ℱ' ≅ ℱ form a principal homogeneous space under Ext¹_{𝒪_X}(ℱ, ℐ ⊗_{𝒪_X} ℱ): the difference AlgebraicGeometry.RingedSpaceThickening.flatLiftClassDifference is additive, and for every class b the map a ↦ d(a, b) is a bijection onto Ext¹_{𝒪_X}(ℱ, ℐ ⊗_{𝒪_X} ℱ). When there is no flat lift both conditions hold vacuously.

theorem flatLiftClassDifference_isPrincipalHomogeneous (hi : IsFirstOrderThickening D.i)
    (ht : IsFirstOrderThickening D.t) (hs : D.IsStrict)
    {F : SheafOfModules.{u} (structureSheafRing D.X)} (hF : AlgebraicGeometry.IsFlatOver D.f F) :
    (∀ a b c : FlatLiftClass D F,
      flatLiftClassDifference hi hs F a b + flatLiftClassDifference hi hs F b c =
        flatLiftClassDifference hi hs F a c) ∧
      ∀ b : FlatLiftClass D F,
        Function.Bijective fun a : FlatLiftClass D F => flatLiftClassDifference hi hs F a b

Tag 08LN, a lemma

Tag 08LN in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.nonempty_flatLift_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatLiftExistence.lean, line 516.

Stacks Project, Tag 08LN. Let (f, f') be a strict morphism of first order thickenings of ringed spaces and let ℱ be an 𝒪_X-module flat over S. There is an 𝒪_{X'}-module ℱ' flat over S' with i^* ℱ' ≅ ℱ if and only if the canonical map f^* 𝒥 ⊗_{𝒪_X} ℱ ⟶ ℐ ⊗_{𝒪_X} ℱ is an isomorphism and the class o(ℱ, ℐ ⊗_{𝒪_X} ℱ, 1) ∈ Ext²_{𝒪_X}(ℱ, ℐ ⊗_{𝒪_X} ℱ) of Stacks 08L8 is zero.

The pair (ℱ', α) of the source is AlgebraicGeometry.RingedSpaceThickening.FlatLift, and the obstruction class is AlgebraicGeometry.RingedSpaceThickening.obstructionClass for the coefficient module ℐ ⊗_{𝒪_X} ℱ and the normalization c = 1.

theorem nonempty_flatLift_iff (D : MorphismOfThickenings.{u})
    [HasExt (SheafOfModules.{u} (structureSheafRing D.X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing D.X))]
    (hi : IsFirstOrderThickening D.i) (ht : IsFirstOrderThickening D.t) (hs : D.IsStrict)
    (F : SheafOfModules.{u} (structureSheafRing D.X))
    (hF : AlgebraicGeometry.IsFlatOver D.f F) :
    Nonempty (FlatLift D F) ↔
      IsIso (baseIdealTensorComparison D F) ∧
        obstructionClass D.i hi F (idealTensor D F) (𝟙 (idealTensor D F)) = 0

Sources

LeanAlgebraicGeometry.RingedSpaceThickening.mapLift_isPrincipalHomogeneous · AlgebraicGeometry.RingedSpaceThickening.exists_addTorsor_mapLift · AlgebraicGeometry.RingedSpaceThickening.isFlatOver_iff_baseToInfinitesimal_isIso · AlgebraicGeometry.RingedSpaceThickening.baseToSourceIdealTensor_isIso · AlgebraicGeometry.RingedSpaceThickening.sourceIdealActionImage_isIso · AlgebraicGeometry.RingedSpaceThickening.mapLift_isTorsor_tensor · AlgebraicGeometry.RingedSpaceThickening.exists_derivedMapLiftingObstruction · AlgebraicGeometry.RingedSpaceThickening.mapLiftObstruction

Section91.6 Application to flat modules on flat thickenings of ringed spaces #

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

Tag 08VR, a lemma

Tag 08VR in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.FlatModuleDeformation.nonempty_flatLift_iff_flatDeformationObstruction_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatModuleDeformation.lean, line 244. The attribute's comment: “clause (1)”.

Stacks Project, Tag 08VR, clause (1). Let (f, f') be a strict morphism of first order thickenings of ringed spaces with f' flat, and let ℱ be an 𝒪_X-module flat over S. There is an 𝒪_{X'}-module ℱ' flat over S' with i^* ℱ' ≅ ℱ if and only if the class o(ℱ, f^* 𝒥 ⊗_{𝒪_X} ℱ, 1) of Stacks 08L8 vanishes.

This is Stacks 08LN read through the identification ℐ = f^* 𝒥 (isIso_baseToSourceIdeal_of_isFlat), which makes its first condition automatic.

theorem nonempty_flatLift_iff_flatDeformationObstruction_eq_zero
    (hi : IsFirstOrderThickening D.i) (ht : IsFirstOrderThickening D.t) (hs : D.IsStrict)
    (hf' : AlgebraicGeometry.IsFlat D.f') (F : SheafOfModules.{u} (structureSheafRing D.X))
    (hF : AlgebraicGeometry.IsFlatOver D.f F) :
    Nonempty (FlatLift D F) ↔
      flatDeformationObstruction D hi (isIso_baseToSourceIdeal_of_isFlat D hs hf') F = 0

AlgebraicGeometry.RingedSpaceThickening.FlatModuleDeformation.flatLiftClassDifferenceBase_isPrincipalHomogeneous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatModuleDeformation.lean, line 294. The attribute's comment: “clause (2)”.

Stacks Project, Tag 08VR, clause (2). Let (f, f') be a strict morphism of first order thickenings of ringed spaces with f' flat, and let ℱ be an 𝒪_X-module flat over S. The isomorphism classes of lifts of ℱ to 𝒪_{X'}-modules flat over S' form a principal homogeneous space under Ext¹_{𝒪_X}(ℱ, f^* 𝒥 ⊗_{𝒪_X} ℱ): the difference flatLiftClassDifferenceBase is additive, and for every class b the map a ↦ d(a, b) is a bijection onto Ext¹_{𝒪_X}(ℱ, f^* 𝒥 ⊗_{𝒪_X} ℱ). When no lift exists both conditions hold vacuously.

This is Stacks 08LM read through the identification ℐ = f^* 𝒥.

theorem flatLiftClassDifferenceBase_isPrincipalHomogeneous (hi : IsFirstOrderThickening D.i)
    (ht : IsFirstOrderThickening D.t) (hs : D.IsStrict) (hf' : AlgebraicGeometry.IsFlat D.f')
    {F : SheafOfModules.{u} (structureSheafRing D.X)} (hF : AlgebraicGeometry.IsFlatOver D.f F) :
    (∀ a b c : FlatLiftClass D F,
      flatLiftClassDifferenceBase D hi hs (isIso_baseToSourceIdeal_of_isFlat D hs hf') F a b +
          flatLiftClassDifferenceBase D hi hs (isIso_baseToSourceIdeal_of_isFlat D hs hf') F b c =
        flatLiftClassDifferenceBase D hi hs (isIso_baseToSourceIdeal_of_isFlat D hs hf') F a c) ∧
      ∀ b : FlatLiftClass D F, Function.Bijective fun a : FlatLiftClass D F =>
        flatLiftClassDifferenceBase D hi hs (isIso_baseToSourceIdeal_of_isFlat D hs hf') F a b

AlgebraicGeometry.RingedSpaceThickening.FlatModuleDeformation.exists_identityLiftAut_equiv_ext_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatModuleDeformation.lean, line 444. The attribute's comment: “clause (3)”.

Stacks Project, Tag 08VR, clause (3). Given a lift ℱ' of ℱ to an 𝒪_{X'}-module flat over S', the set of automorphisms of ℱ' which pull back to the identity of ℱ is canonically isomorphic to Ext⁰_{𝒪_X}(ℱ, f^* 𝒥 ⊗_{𝒪_X} ℱ): the class ξ corresponds to the automorphism 1 + ε_ξ, where ε_ξ is ξ ∈ Hom_{𝒪_X}(ℱ, f^* 𝒥 ⊗_{𝒪_X} ℱ) read through Stacks 08LJ as an endomorphism ℱ' ⟶ ℐℱ' ⟶ ℱ'.

theorem exists_identityLiftAut_equiv_ext_zero [CategoryTheory.HasExt.{w}
      (SheafOfModules.{u} (structureSheafRing D.X))]
    (hi : IsFirstOrderThickening D.i) (hs : D.IsStrict)
    {F : SheafOfModules.{u} (structureSheafRing D.X)} (A : FlatLift D F) :
    ∃ e : { φ : A.module' ≅ A.module' // (modulePullback D.i).map φ.hom = 𝟙 ((modulePullback D.i).obj A.module') } ≃
        CategoryTheory.Abelian.Ext.{w} F (baseIdealTensor D F) 0,
      ∀ φ, φ.1.hom = 𝟙 A.module' +
        liftInfinitesimalEndo D hi hs A (CategoryTheory.Abelian.Ext.homEquiv₀ (e φ))

Tag 08VS, a situation

Tag 08VS in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.FlatShortExactThickeningDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatThickeningSituation.lean, line 46. The attribute's comment: “the situation”.

Two short exact sequences of first order thickenings, one over the other, with strict and flat vertical arrows, together with a module on the middle upper space which is flat over the middle lower space.

structure FlatShortExactThickeningDiagram

Tag 08VT, a lemma

Tag 08VT in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.boundary_flatLiftClassDifferenceBase_eq_flatDeformationObstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatThickeningBoundary.lean, line 250. The attribute's comment: “the boundary of the difference of π^* ℱ and h^* ℱ'₂ is the obstruction to lifting ℱ to an 𝒪'₃-module flat over S'₃, difference in the order (h^* ℱ'₂, π^* ℱ); inputs of the source are hypotheses -- the 08VQ identifications ℐᵢ = f^* 𝒥ᵢ, as 08VR already carries them, the short exactness of the tensored ideal sequence, and 08LF's own hrestrict -- each named in the Scope section of the module docstring”.

In the situation of Stacks 08VS the two 𝒪'₁-modules π^* ℱ and h^* ℱ'₂ are flat over S'₁ and restrict to ℱ on X, so Stacks 08VR clause (2) attaches to them a difference θ ∈ Ext¹_{𝒪_X}(ℱ, f^* 𝒥₁ ⊗_{𝒪_X} ℱ). The boundary of θ along 0 ⟶ f^* 𝒥₃ ⊗ ℱ ⟶ f^* 𝒥₂ ⊗ ℱ ⟶ f^* 𝒥₁ ⊗ ℱ ⟶ 0 is the obstruction of Stacks 08VR clause (1) to lifting ℱ to an 𝒪'₃-module flat over S'₃.

The difference is taken in the order (h^* ℱ'₂, π^* ℱ); the other order negates both it and its boundary. The hypotheses carrying inputs of the source are described in the Scope section of the module docstring.

theorem boundary_flatLiftClassDifferenceBase_eq_flatDeformationObstruction
    (D : FlatShortExactThickeningDiagram.{u})
    [CategoryTheory.HasExt.{w} (SheafOfModules.{u} (structureSheafRing D.upper.X))]
    [CategoryTheory.HasExt.{w} (SheafOfModules.{u} (structureSheafRing D.upper.X₁))]
    [HasDerivedCategory.{w'} (SheafOfModules.{u} (structureSheafRing D.upper.X))]
    (hI₁ : IsIso D.morphism₁.baseToSourceIdeal)
    (hI₂ : IsIso D.morphism₂.baseToSourceIdeal)
    (hI₃ : IsIso D.morphism₃.baseToSourceIdeal)
    (k₃₂ : baseIdealTensor D.morphism₃ D.restriction ⟶
      baseIdealTensor D.morphism₂ D.restriction)
    (k₂₁ : baseIdealTensor D.morphism₂ D.restriction ⟶
      baseIdealTensor D.morphism₁ D.restriction)
    (hk : k₃₂ ≫ k₂₁ = 0) (hK : (ShortComplex.mk k₃₂ k₂₁ hk).ShortExact)
    (hk₃₂ : (baseIdealTensorIso D.morphism₃ hI₃ D.restriction).inv ≫ k₃₂ =
      D.idealTensorTransition₃₂ ≫ (baseIdealTensorIso D.morphism₂ hI₂ D.restriction).inv)
    (hk₂₁ : (baseIdealTensorIso D.morphism₂ hI₂ D.restriction).inv ≫ k₂₁ =
      D.idealTensorTransition₂₁ ≫ (baseIdealTensorIso D.morphism₁ hI₁ D.restriction).inv)
    (Aπ Bh : FlatLift D.morphism₁ D.restriction)
    (hAπ : underlyingExtensionClass D.upper.i₁ D.trivialization D.upper.firstOrder₁.1.1
      D.restriction (idealTensor D.morphism₁ D.restriction)
      (Aπ.kernelExtension D.upper.firstOrder₁ D.isStrict₁) = 0)
    (w : PushedExtension D.upper.i₁ D.upper.i₂ D.upper.f₁₂ D.upper.comm₁₂ D.restriction
      (idealTensor D.morphism₁ D.restriction) (idealTensor D.morphism₂ D.restriction)
      D.idealTensorTransition₂₁
      (D.liftOfModule₂.kernelExtension D.upper.firstOrder₂ D.isStrict₂)
      (Bh.kernelExtension D.upper.firstOrder₁ D.isStrict₁))
    (hw : IsPushout (D.liftOfModule₂.kernelExtension D.upper.firstOrder₂ D.isStrict₂).f
      ((modulePushforward D.upper.i₂).map D.idealTensorTransition₂₁ ≫
        (thickeningPushforwardComp D.upper.i₁ D.upper.i₂ D.upper.f₁₂ D.upper.comm₁₂).inv.app
          (idealTensor D.morphism₁ D.restriction))
      w.hom ((modulePushforward D.upper.f₁₂).map
        (Bh.kernelExtension D.upper.firstOrder₁ D.isStrict₁).f))
    (hrestrict : (firstOrderExtensionAction D.upper.i₃ D.restriction
        (idealTensor D.morphism₂ D.restriction) D.upper.firstOrder₃
        (sequenceRestrictedExtension D.upper D.restriction
          (idealTensor D.morphism₂ D.restriction)
          (D.liftOfModule₂.kernelExtension D.upper.firstOrder₂ D.isStrict₂))).val =
      D.idealTensorTransition₃₂) :
    (flatLiftClassDifferenceBase D.morphism₁ D.upper.firstOrder₁ D.isStrict₁ hI₁ D.restriction
          (Quotient.mk (flatLiftSetoid D.morphism₁ D.restriction) Bh)
          (Quotient.mk (flatLiftSetoid D.morphism₁ D.restriction) Aπ)).comp
        hK.extClass (by decide) =
      flatDeformationObstruction D.morphism₃ D.upper.firstOrder₃ hI₃ D.restriction

AlgebraicGeometry.RingedSpaceThickening.FlatShortExactThickeningDiagram.boundary_difference_trivialLift_pulledLift_eq_flatDeformationObstruction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/FlatThickeningBoundaryUnconditional.lean, line 100.

In Situation Stacks 08VS — a commutative diagram of short exact sequences of first order thickenings X'₁ ⟶ X'₂ ⟶ X'₃ of X over S'₁ ⟶ S'₂ ⟶ S'₃ of S, with every (f, f'ᵢ) strict and every f'ᵢ flat, and an 𝒪'₂-module ℱ'₂ flat over S'₂ with ℱ = ℱ'₂|_X — let π : X'₁ ⟶ X be the canonical splitting of Stacks 08LE. Then π^* ℱ and h^* ℱ'₂ are 𝒪'₁-modules flat over S'₁ (the first two conjuncts); they restrict to ℱ on X through i₁^* π^* ℱ ≅ (i₁ ≫ π)^* ℱ = ℱ and i₁^* h^* ℱ'₂ ≅ (i₁ ≫ h)^* ℱ'₂ = ℱ, which makes them the flat lifts trivialLift and pulledLift. Their difference θ ∈ Ext¹_{𝒪_X}(ℱ, f^* 𝒥₁ ⊗_{𝒪_X} ℱ), the difference of Stacks 08VR (2) of the two isomorphism classes, has for boundary along 0 ⟶ f^* 𝒥₃ ⊗ ℱ ⟶ f^* 𝒥₂ ⊗ ℱ ⟶ f^* 𝒥₁ ⊗ ℱ ⟶ 0 — the sequence induced by the lower row, short exact by baseTransition_shortExact — the obstruction of Stacks 08VR (1) to lifting ℱ to an 𝒪'₃-module flat over S'₃.

The difference is taken in the order (h^* ℱ'₂, π^* ℱ).

theorem boundary_difference_trivialLift_pulledLift_eq_flatDeformationObstruction
    [CategoryTheory.HasExt.{w} (SheafOfModules.{u} (structureSheafRing D.upper.X))]
    [CategoryTheory.HasExt.{w} (SheafOfModules.{u} (structureSheafRing D.upper.X₁))]
    [HasDerivedCategory.{w'} (SheafOfModules.{u} (structureSheafRing D.upper.X))] :
    AlgebraicGeometry.IsFlatOver D.f₁
        ((modulePullback D.trivialization.retraction).obj D.restriction) ∧
      AlgebraicGeometry.IsFlatOver D.f₁ ((modulePullback D.upper.f₁₂).obj D.module₂) ∧
      (flatLiftClassDifferenceBase D.morphism₁ D.upper.firstOrder₁ D.isStrict₁
          D.isIso_baseToSourceIdeal₁ D.restriction
          (Quotient.mk (flatLiftSetoid D.morphism₁ D.restriction) D.pulledLift)
          (Quotient.mk (flatLiftSetoid D.morphism₁ D.restriction) D.trivialLift)).comp
          D.baseTransition_shortExact.extClass (by decide) =
        flatDeformationObstruction D.morphism₃ D.upper.firstOrder₃ D.isIso_baseToSourceIdeal₃
          D.restriction

Sources

LeanAlgebraicGeometry.RingedSpaceThickening.FlatModuleDeformation.nonempty_flatLift_iff_flatDeformationObstruction_eq_zero · AlgebraicGeometry.RingedSpaceThickening.FlatModuleDeformation.flatLiftClassDifferenceBase_isPrincipalHomogeneous · AlgebraicGeometry.RingedSpaceThickening.FlatModuleDeformation.exists_identityLiftAut_equiv_ext_zero · AlgebraicGeometry.RingedSpaceThickening.FlatShortExactThickeningDiagram · AlgebraicGeometry.RingedSpaceThickening.boundary_flatLiftClassDifferenceBase_eq_flatDeformationObstruction ·

AlgebraicGeometry.RingedSpaceThickening.FlatShortExactThickeningDiagram.boundary_difference_trivialLift_pulledLift_eq_flatDeformationObstruction

Section91.7 Deformations of ringed spaces and the naive cotangent complex #

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

Tag 08U7, an equation

Tag 08U7 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.DeformationSolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DeformationDiagram.lean, line 60. The attribute's comment: “the deformation problem to solve”.

A solution of the first order deformation problem for a fixed first order thickening t : S ⟶ S', morphism f : X ⟶ S, 𝒪_X-module 𝒢 and prescribed map c : f^* t^* 𝒥 ⟶ 𝒢: a first order thickening i : X ⟶ X' and a morphism f' : X' ⟶ S' over t, together with an identification of the ideal of i with 𝒢 under which the vertical map on ideals induced by f' is exactly c.

structure DeformationSolution {X S S' : RingedSpace.{u, u}} (t : S ⟶ S')
    (ht : IsFirstOrderThickening t) (f : X ⟶ S)
    (G : SheafOfModules.{u} (structureSheafRing X))
    (c : (modulePullback f).obj
      ((modulePullback t).obj (AlgebraicGeometry.SheafOfModules.idealSheaf t)) ⟶ G)

Tag 08U8, a lemma

Tag 08U8 in the Stacks Project.

Stacks.SheafOfModules.presentationNaiveCotangentExtZeroAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangentExtZero.lean, line 120. The attribute's comment: “clause (2): the identification of the acting group Hom(H^0(NL(α)), G) = Hom(Omega_{B/A}, G) with Ext^0(NL(α), G), for NL(α) the naive cotangent complex of a polynomial presentation of a homomorphism of sheaves of rings on a site — the form the source's diagram takes after its own reduction to sheaves on one space. No hypothesis beyond the source. The remaining two links of the source's display, the adjunction Hom(Omega_{X_1/S_1}, g_ G_2) = Hom(g^ Omega_{X_1/S_1}, G_2) and the passage from NL(α) to Lg^* NL_{X_1/S_1}, are not proved here; clause (1) and the principal homogeneous space structure itself are elsewhere”.

The identification of Ext⁰_B(NL(α), 𝒢) with Hom_B(Ω_{B/A}, 𝒢), for NL(α) the naive cotangent complex of a polynomial presentation of B over A.

noncomputable def presentationNaiveCotangentExtZeroAddEquiv :
    presentationNaiveCotangentExt.{v, u, w, z, t} J A B a E α G 0 ≃+
      (moduleOfDifferentialsOfSite.{v, u, w, z} A B a ⟶ G)

AlgebraicGeometry.RingedSpaceThickening.DeformationIdealDiagram.lifting_obstruction_and_torsor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DeformationLiftingObstruction.lean, line 273. References: EGA 0 (20.1.3), “more general”; EGA IV (16.5.14), “more general”.

Stacks Project, Tag 08U8. In the situation of Stacks 08U9 — a commutative cube of ringed spaces whose horizontal arrows are first order thickenings, with 𝒢_j = Ker(i_j^♯), a g-map ν : 𝒢₁ ⟶ 𝒢₂, and front and back solutions of Stacks 08U7 making the diagram of ideal rows of Stacks 08UA commute (D : DeformationIdealDiagram):

the canonical element D.obstructionClass of Ext¹_{𝒪_{X₂}}(Lg^*NL_{X₁/S₁}, 𝒢₂) vanishes if and only if there is a morphism of ringed spaces X'₂ ⟶ X'₁ fitting into (08U9) compatibly with ν;

if there is such a morphism, the set of all of them is a principal homogeneous space under Hom_{𝒪_{X₁}}(Ω_{X₁/S₁}, g_*𝒢₂): the action liftAct (given by the source's formula, liftAct_spec) is trivial at 0, additive, and simply transitive, and is the action of an AddTorsor structure on the set.

The other two spellings of the acting group in the source's display are identified with this one by actingGroupPullbackAddEquiv (Hom_{𝒪_{X₂}}(g^*Ω_{X₁/S₁}, 𝒢₂)) and extZeroDerivedPullbackNaiveCotangentAddEquiv (Ext⁰_{𝒪_{X₂}}(Lg^*NL_{X₁/S₁}, 𝒢₂)).

theorem lifting_obstruction_and_torsor :
    (D.obstructionClass = 0 ↔ Nonempty D.Lifts) ∧
      (∀ φ : D.Lifts, D.liftAct 0 φ = φ) ∧
      (∀ (φ : D.Lifts) (θ θ' : D.ActingGroup),
        D.liftAct θ' (D.liftAct θ φ) = D.liftAct (θ + θ') φ) ∧
      (∀ φ ψ : D.Lifts, ∃! θ : D.ActingGroup, D.liftAct θ φ = ψ) ∧
      (∀ _φ₀ : D.Lifts, ∃ T : AddTorsor D.ActingGroup D.Lifts,
        ∀ (θ : D.ActingGroup) (φ ψ : D.Lifts), T.vadd θ φ = ψ ↔ D.liftAct θ φ = ψ)

AlgebraicGeometry.RingedSpaceThickening.liftingObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentLiftingObstruction.lean, line 245. The attribute's comment: “clause (1): the class of Step 1 of the source's proof and its vanishing criterion, with the underlying spaces of the diagram identified as in the source's reduction, the two-term structure of NL(α) supplied as the distinguished triangle of NaiveCotangentTwoTerm, and the content of Steps 1 to 3 — the bijection between morphisms X'₂ ⟶ X'₁ fitting into the diagram and factorizations of the difference map through the degree 0 term — carried as the hypothesis e”.

Stacks Project, Tag 08U8, clause (1). In the situation of the source's diagram, reduced as in its proof to sheaves of rings on one space, the class in Ext¹(NL(α), 𝒢₂) of the difference homomorphism ξ of Step 1 vanishes if and only if there is a morphism X'₂ ⟶ X'₁ fitting into the diagram compatibly with ν.

theorem liftingObstruction_eq_zero_iff (P : NaiveCotangentTwoTerm single) (G : M)
    (ξ : P.conormal ⟶ G) {Lift : Type*} (e : Lift ≃ {θ : P.base ⟶ G // P.d ≫ θ = ξ}) :
    liftingObstruction P G ξ = 0 ↔ Nonempty Lift

AlgebraicGeometry.RingedSpaceThickening.liftTranslate_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentLiftingObstruction.lean, line 290. The attribute's comment: “clause (2): triviality of the action of 0 in the principal homogeneous space structure under Hom(H⁰(NL(α)), 𝒢₂)”.

Stacks Project, Tag 08U8, clause (2). The zero homomorphism acts trivially on the morphisms X'₂ ⟶ X'₁ fitting into the source's diagram.

theorem liftTranslate_zero (p : Lift) : liftTranslate P G ξ e 0 p = p

AlgebraicGeometry.RingedSpaceThickening.liftTranslate_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentLiftingObstruction.lean, line 297. The attribute's comment: “clause (2): additivity of the action in the principal homogeneous space structure under Hom(H⁰(NL(α)), 𝒢₂)”.

Stacks Project, Tag 08U8, clause (2). Translation of the morphisms X'₂ ⟶ X'₁ fitting into the source's diagram is additive in the translating homomorphism.

theorem liftTranslate_add (a b : cokernel P.d ⟶ G) (p : Lift) :
    liftTranslate P G ξ e a (liftTranslate P G ξ e b p) = liftTranslate P G ξ e (a + b) p

AlgebraicGeometry.RingedSpaceThickening.existsUnique_liftTranslate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentLiftingObstruction.lean, line 311. The attribute's comment: “clause (2): the morphisms X'₂ ⟶ X'₁ fitting into the diagram are a principal homogeneous space under Hom(H⁰(NL(α)), 𝒢₂), the acting group being written as the Hom out of the cokernel of the differential of NL(α); its further identification with Hom(g^Ω_{X₁/S₁}, 𝒢₂) and with Ext⁰(Lg^NL_{X₁/S₁}, 𝒢₂) is not proved here”.

Stacks Project, Tag 08U8, clause (2). The morphisms X'₂ ⟶ X'₁ fitting into the source's diagram compatibly with ν form a principal homogeneous space under Hom(H⁰(NL(α)), 𝒢₂) = Hom(Ω_{X₁/S₁}, 𝒢₂): any one of them is carried to any other by exactly one homomorphism.

theorem existsUnique_liftTranslate (p q : Lift) :
    ∃! a : cokernel P.d ⟶ G, liftTranslate P G ξ e a p = q

Tag 08U9, an equation

Tag 08U9 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.DeformationCube, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DeformationDiagram.lean, line 110. The attribute's comment: “the displayed commutative diagram of ringed spaces”.

The commutative diagram of morphisms of ringed spaces comparing two deformation situations: a square i₂ : X₂ ⟶ X₂' over t₂ : S₂ ⟶ S₂' at the back, a square i₁ : X₁ ⟶ X₁' over t₁ : S₁ ⟶ S₁' at the front, and comparison morphisms g : X₂ ⟶ X₁, h : S₂ ⟶ S₁, h' : S₂' ⟶ S₁' making the four closed faces commute. There is no comparison X₂' ⟶ X₁'.

structure DeformationCube

Tag 08UA, an equation

Tag 08UA in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.DeformationIdealDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DeformationDiagram.lean, line 216. The attribute's comment: “the displayed commutative diagram of the four ideal rows”.

The commutative diagram of the four short exact ideal rows attached to a deformation cube whose horizontal arrows are first order thickenings: modules 𝒢₁, 𝒢₂ identifying the ideals of i₁ and i₂, prescribed maps c₁, c₂ making front and back solutions of the deformation problem, and a g-map ν : 𝒢₁ ⟶ 𝒢₂ compatible with the comparison DeformationCube.baseIdealMap of the ideals of t₁ and t₂.

structure DeformationIdealDiagram

Tag 08UB, a lemma

Tag 08UB in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.exists_conormalRepresentative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentConormalRepresentation.lean, line 197. The attribute's comment: “over a ringed space, in the two-term idiom of NaiveCotangentTwoTerm: the class of a conormal homomorphism of a family of generators produced with it, transported to 𝖭𝖫_{X/S}”.

Stacks Project, Tag 08UB. Every class of Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢) is the class of a homomorphism δ : 𝒥/𝒥² ⟶ 𝒢 out of the conormal sheaf of a suitable family of generators α : ℰ ⟶ 𝒪_X of 𝒪_X over f⁻¹𝒪_S, transported to 𝖭𝖫_{X/S} through the quasi-isomorphism of Stacks 08TL.

The family of generators comes with the class and is not a refinement of a prescribed one; that is all the source gives, and it is all that is needed where the acting group of the torsor of Stacks 08UC is the presentation-free Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢).

theorem exists_conormalRepresentative (ξ : relativeObj f ⟶ shiftedSingleObj G) :
    ∃ (E : Functor (Opens X.carrier)ᵒᵖ (Type u))
      (α : E ⟶ underlyingPresheaf (Opens.grothendieckTopology X.carrier) X.sheaf)
      (hsurj : Presheaf.IsLocallySurjective (Opens.grothendieckTopology X.carrier)
        (generatorsPresentation f E α).hom),
      letI : Presheaf.IsLocallySurjective (Opens.grothendieckTopology X.carrier)
        (generatorsPresentation f E α).hom := hsurj
      ∃ δ : (twoTerm f E α).conormal ⟶ G,
        (naiveCotangentIso f E α).inv ≫ (twoTerm f E α).conormalExtClass G δ = ξ

Stacks.SheafOfModules.ConormalRepresentative.exists_enlargement_conormalExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/NaiveCotangentExtClassRepresentation.lean, line 44. The attribute's comment: “on the site of open sets of a topological space, the setting of the statement; the family of generators and the homomorphism are produced by the proof”.

Stacks Project, Tag 08UB. Let 𝒜 ⟶ ℬ be a homomorphism of sheaves of commutative rings on a topological space, let 𝒢 be a ℬ-module and let ξ be a first Ext class of NL_{ℬ/𝒜} with values in 𝒢. There is a family of generators α : ℰ ⟶ ℬ presenting ℬ over 𝒜 for which ξ, restricted along the canonical comparison map NL(α) ⟶ NL_{ℬ/𝒜}, is the class of a homomorphism ℐ/ℐ² ⟶ 𝒢 out of the conormal sheaf.

theorem exists_enlargement_conormalExtClass
    [HasWeakSheafify (Opens.grothendieckTopology X) CommRingCat.{max w u}]
    [(Opens.grothendieckTopology X).HasSheafCompose
      (forget₂ CommRingCat.{max w u} RingCat.{max w u})]
    (A B : Sheaf (Opens.grothendieckTopology X) CommRingCat.{max w u}) (a : A ⟶ B)
    [HasSheafify (Opens.grothendieckTopology X) AddCommGrpCat.{max w u}]
    [(Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{max w u}]
    [HasDerivedCategory.{w} (SheafOfModules.{max w u} (Stacks.SheafOfModules.Tensor.ringSheaf B))]
    (G : SheafOfModules.{max w u} (Stacks.SheafOfModules.Tensor.ringSheaf B))
    (ξ : DerivedCategory.Ext (DerivedCategory.Q.obj
        (Stacks.SheafOfModules.naiveCotangentComplex.{u, u, max w u, w}
          (Opens.grothendieckTopology X) A B a))
      ((DerivedCategory.singleFunctor _ 0).obj G) 1) :
    ∃ (E : Sheaf (Opens.grothendieckTopology X) (Type (max w u)))
      (α : E.obj ⟶ underlyingPresheaf (Opens.grothendieckTopology X) B)
      (hsurj : Presheaf.IsLocallySurjective (Opens.grothendieckTopology X)
        (Stacks.SheafOfModules.presentation (Opens.grothendieckTopology X) A B a E.obj α).hom),
      letI : Presheaf.IsLocallySurjective (Opens.grothendieckTopology X)
        (Stacks.SheafOfModules.presentation (Opens.grothendieckTopology X) A B a E.obj α).hom :=
        hsurj
      ∃ f : (Stacks.SheafOfModules.presentationConormalSequence.{u, u, max w u, w}
          (Opens.grothendieckTopology X) A B a E.obj α).X₁ ⟶ G,
        DerivedCategory.Q.map
            (Stacks.SheafOfModules.naiveCotangentComplexComparison.{u, u, max w u, w}
              (Opens.grothendieckTopology X) A B a E.obj α) ≫ ξ =
          Stacks.SheafOfModules.presentationConormalExtClass.{u, u, w, w}
            (Opens.grothendieckTopology X) A B a E.obj α G f

Tag 08UC, a lemma

Tag 08UC in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.exists_addTorsor_solutionClasses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SolutionClassesPrincipalHomogeneous.lean, line 171. The attribute's comment: “at any model of D(𝒪_X), with the canonical Ext¹(NL_{X/S}, 𝒢); the separating element of two classes is their difference class and ξ acts on [X'] by [X'_ξ]”.

Stacks Project, Tag 08UC. If there exists a solution to the deformation problem (91.7.0.1) of Stacks 08U7, then the set of isomorphism classes of solutions is principal homogeneous under Ext¹_{𝒪_X}(NL_{X/S}, 𝒢).

The statement holds at every model H of the derived category D(𝒪_X), with the canonical group Stacks.SheafOfModules.naiveCotangentExt of the homomorphism f⁻¹𝒪_S ⟶ 𝒪_X in degree one. The set of isomorphism classes is SolutionClasses t ht f G c, the quotient of the solutions by Isomorphic (some morphism of solutions — a morphism of the deformed spaces under X, over S', and the identity on 𝒢 — is an isomorphism). "Principal homogeneous" is Mathlib's AddTorsor: an action of the group which is free and transitive, the unique element carrying one class to another being -ᵥ. The structure is not an arbitrary one: the element separating the classes of X'₁ and X'₂ is the difference class o(X'₁, X'₂) of the two solutions (the class of the square-zero extension of f⁻¹𝒪_S-algebras which is their difference, read in the model H), and ξ acts on the class of X' by the class of the solution X'_ξ of the source's proof.

theorem exists_addTorsor_solutionClasses (h : Nonempty (DeformationSolution t ht f G c)) :
    ∃ T : AddTorsor (modelExtOneNaiveCotangent H f G) (SolutionClasses t ht f G c),
      letI := T
      (∀ Q₁ Q₂ : DeformationSolution t ht f G c,
        ((⟦Q₁⟧ : SolutionClasses t ht f G c) -ᵥ ⟦Q₂⟧) =
          extOneNaiveCotangentModelAddEquiv f G (differenceClass Q₁ Q₂)) ∧
      ∀ (ξ : modelExtOneNaiveCotangent H f G) (Q : DeformationSolution t ht f G c),
        ξ +ᵥ (⟦Q⟧ : SolutionClasses t ht f G c) =
          ⟦solutionTwist Q ((extOneNaiveCotangentModelAddEquiv f G).symm ξ)⟧

AlgebraicGeometry.RingedSpaceThickening.isomorphic_iff_nonempty_solutionHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SolutionIsomorphism.lean, line 405. The attribute's comment: “the step of the proof that the obstruction to a morphism of solutions is the obstruction to an isomorphism; the full statement is exists_addTorsor_solutionClasses”.

Stacks Project, Tag 08UC, the half asserting that the obstruction separates isomorphism classes. Two solutions of the deformation problem of Tag 08U7 are isomorphic exactly when there is a morphism of solutions between them: by SolutionHom.isIso_hom 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 Tag 08U8, which obstructs a morphism of solutions, thereby obstructs an isomorphism.

The other half of the tag — that the isomorphism classes form a principal homogeneous space under Ext¹_{𝒪_X}(NL_{X/S}, 𝒢) — is not claimed here; the full statement of the tag is exists_addTorsor_solutionClasses in StacksFrontier/Deformation/RingedSpaceThickening/SolutionClassesPrincipalHomogeneous.lean.

theorem isomorphic_iff_nonempty_solutionHom (Q₁ Q₂ : DeformationSolution t ht f G c) :
    Isomorphic Q₁ Q₂ ↔ Nonempty (SolutionHom Q₁ Q₂)

Tag 0GPZ, a lemma

Tag 0GPZ in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.SquareZeroAlgebraExtension.isomorphismClassesEquivExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SquareZeroAlgebraExtensionClassification.lean, line 340.

Let f : (X, 𝒪_X) ⟶ (S, 𝒪_S) be a morphism of ringed spaces and 𝒢 an 𝒪_X-module. The set of isomorphism classes of extensions 0 ⟶ 𝒢 ⟶ 𝒪_{X'} ⟶ 𝒪_X ⟶ 0 of f⁻¹𝒪_S-algebras with 𝒢 an ideal of square zero is canonically bijective to Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢).

The bijection is the class map of Stacks 0GQ0: an extension goes to the class of the homomorphism 𝒥/𝒥² ⟶ 𝒢 of the presentation of 𝒪_X by the sheaf of sets underlying 𝒪_{X'}, read through the quasi-isomorphism of Stacks 08TL (isomorphismClassesEquivExt_apply).

def isomorphismClassesEquivExt : IsomorphismClasses f G ≃ extOneNaiveCotangent f G

AlgebraicGeometry.RingedSpaceThickening.trivialSolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SquareZeroExtensionClasses.lean, line 172. The attribute's comment: “the existence of a solution: the trivial extension 𝒪_X ⋉ 𝒢; not the bijection with Ext¹, which needs the torsor statement of 08UC”.

The trivial square-zero extension is a solution of the problem of Stacks 08U7 over the identity thickening of the base: X' = (X, 𝒪_X ⋉ 𝒢) is a first order thickening of X over S whose ideal is 𝒢. This is the base point the torsor of Stacks 08UC needs.

def trivialSolution (ht : IsFirstOrderThickening (𝟙 S)) (f : X ⟶ S)
    (G : SheafOfModules.{u} (structureSheafRing X)) :
    DeformationSolution (𝟙 S) ht f G 0

AlgebraicGeometry.RingedSpaceThickening.nonempty_deformationSolution, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SquareZeroExtensionClasses.lean, line 192. The attribute's comment: “the existence of a solution, which is what the torsor of 08UC requires of the type of solutions; not the bijection with Ext¹”.

The deformation problem of Stacks 08U7 over the identity thickening of the base has a solution, namely the trivial square-zero extension. This is the source's "there exists a solution", i.e. what [Nonempty Sol] asks of SolutionObstruction.addTorsor.

instance nonempty_deformationSolution {ht : IsFirstOrderThickening (𝟙 S)} {f : X ⟶ S}
    {G : SheafOfModules.{u} (structureSheafRing X)} :
    Nonempty (DeformationSolution (𝟙 S) ht f G 0)

AlgebraicGeometry.RingedSpaceThickening.classesEquivExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SquareZeroExtensionClasses.lean, line 232. The attribute's comment: “the bijection, subject to four conditions on the type of solutions that remain inputs — the fields of SolutionObstruction: the difference cocycle xi of two solutions, its additivity hxi, the pushout construction realizing every class as a difference, and the representation rep of every class by a conormal homomorphism (08UB, whose change of presentation is 08TL). The two-term complex P is arbitrary, so the acting group is the Ext¹ of P — for P the complex of a fixed presentation α, that of α rather than Ext¹(NL_{X/S}, 𝒢), whose identification is 08TL”.

Stacks Project, Tag 0GPZ. The isomorphism classes of square-zero extensions 0 ⟶ 𝒢 ⟶ 𝒪_{X'} ⟶ 𝒪_X ⟶ 0 of f⁻¹𝒪_S-algebras — equivalently, of first order thickenings i : X ⟶ X' over S with Ker(i^♯) ≅ 𝒢, i.e. of solutions of the problem of Stacks 08U7 over the identity thickening of the base — are in bijection with Ext¹(NL(α), 𝒢).

The bijection is the torsor of Stacks 08UC evaluated at the base point supplied by the trivial extension 𝒪_X ⋉ 𝒢: a class q goes to the obstruction class separating it from the class of 𝒪_X ⋉ 𝒢, and a class ξ of Ext¹ goes to the class of the solution obtained from 𝒪_X ⋉ 𝒢 by twisting with ξ. The four fields of SolutionObstruction remain inputs; see the implementation notes of this file and of StacksFrontier/Deformation/RingedSpaceThickening/SolutionTorsor.lean.

def classesEquivExt (P : NaiveCotangentTwoTerm single)
    (xi : DeformationSolution (𝟙 S) ht f G 0 → DeformationSolution (𝟙 S) ht f G 0 →
      (P.conormal ⟶ G))
    (hxi : ∀ Q₁ Q₂ Q₃ : DeformationSolution (𝟙 S) ht f G 0, xi Q₁ Q₂ + xi Q₂ Q₃ = xi Q₁ Q₃)
    (rep : ∀ ξ : P.obj ⟶ (single.obj G)⟦(1 : ℤ)⟧,
      { δ : P.conormal ⟶ G // liftingObstruction P G δ = ξ })
    (pushout : ∀ (Q : DeformationSolution (𝟙 S) ht f G 0) (δ : P.conormal ⟶ G),
      { Q' : DeformationSolution (𝟙 S) ht f G 0 // xi Q Q' = δ }) :
    (liftingObstructionSolution P G xi hxi rep pushout).IsomorphismClasses ≃
      (P.obj ⟶ (single.obj G)⟦(1 : ℤ)⟧)

AlgebraicGeometry.RingedSpaceThickening.classesEquivExtRelative, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SquareZeroExtensionClassesRelative.lean, line 102. The attribute's comment: “the bijection, unconditional, with the acting group of the tag: Ext¹(𝖭𝖫_{X/S}, 𝒢) itself. The set counted is the classes of square-zero extensions of f⁻¹𝒪_S-algebras under equality of their class in that group; a morphism of extensions forces that equality by extClass_eq_extClass_of_hom, and that the converse holds too — so that the relation is isomorphism of extensions — is clause (1) of 08U8, a separate tag, not reproved here”.

Stacks Project, Tag 0GPZ. The classes of square-zero extensions 0 ⟶ 𝒢 ⟶ 𝒪_{X'} ⟶ 𝒪_X ⟶ 0 of f⁻¹𝒪_S-algebras are in bijection with Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢), by sending an extension to its class.

Both halves are proved. Injectivity is by construction: the classes are the quotient of the type of extensions by equality of their class in Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢), a relation which a morphism of extensions forces by AlgebraicGeometry.RingedSpaceThickening.extClassDiff_eq_zero_of_hom and which is read as the vanishing of an obstruction class over a common refinement by ...extClassDiff_eq_zero_iff_pairRefinement. Surjectivity is ...exists_extension_extClass_eq: the square-zero pushout of a presentation along a conormal homomorphism representing the class, which exists by Stacks 08UB.

The acting group is the group of the tag, and the bijection is the one of the torsor addTorsorExtensionClasses read at a base point.

def classesEquivExtRelative :
    ExtensionClasses (realizeExtClassDiff (f := f) (G := G)) ≃
      (PresentedSquareZeroExtension.relativeObj f ⟶
        PresentedSquareZeroExtension.shiftedSingleObj G)

Stacks.Deformation.TrivialSqZero.isFirstOrderThickening_thickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialSquareZeroThickening.lean, line 165. The attribute's comment: “the solution 𝒢 ⊕ 𝒪_X of the proof: it is a first order thickening of X; not the bijection with Ext¹, which needs the torsor statement of 08UC”.

i : X ⟶ X' is a first order thickening: the square of the kernel ideal of i^♯ over an open is generated by products of sections killed by i^♯, all of which vanish.

theorem isFirstOrderThickening_thickening : IsFirstOrderThickening (thickening X G)

Stacks.Deformation.TrivialSqZero.idealSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialSquareZeroThickening.lean, line 371. The attribute's comment: “the solution 𝒢 ⊕ 𝒪_X of the proof: the identification of 𝒢 with Ker(i^♯); not the bijection with Ext¹, which needs the torsor statement of 08UC”.

The ideal of the trivial square-zero thickening is 𝒢: the canonical isomorphism Ker(i^♯) ≅ i_* 𝒢 of 𝒪_{X'}-modules coming from the kernel property of the inclusion.

def idealSheafIso :
    AlgebraicGeometry.SheafOfModules.idealSheaf (thickening X G) ≅
      (modulePushforward (thickening X G)).obj G

Stacks.Deformation.TrivialSqZero.thickening_comp_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/TrivialSquareZeroThickening.lean, line 395. The attribute's comment: “the solution 𝒢 ⊕ 𝒪_X of the proof: the thickening is a thickening over S; not the bijection with Ext¹, which needs the torsor statement of 08UC”.

i : X ⟶ X' is a morphism over S.

theorem thickening_comp_over (f : X ⟶ S) : thickening X G ≫ over (G := G) f = f

Tag 0GQ0, a remark

Tag 0GQ0 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.AlgebraSquareZeroExtension.lift_comp_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionPresentation.lean, line 351. The attribute's comment: “the commutative diagram over 𝒪_{X'} ⟶ 𝒪_X for the choice of sheaf of sets ℰ that the source gives, namely the one underlying 𝒪_{X'} with α' the identity”.

The map determined by α' followed by the reduction 𝒪_{X'} ⟶ 𝒪_X is the presentation attached to α.

theorem lift_comp_reduction : P.lift ≫ P.reduction = P.presentation

AlgebraicGeometry.RingedSpaceThickening.AlgebraSquareZeroExtension.presentation_isLocallySurjective, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionPresentation.lean, line 356. The attribute's comment: “surjectivity of f⁻¹𝒪_S[ℰ] ⟶ 𝒪_X, which is what makes 𝖭𝖫(α) defined”.

The presentation f⁻¹𝒪_S[ℰ] ⟶ 𝒪_X is surjective.

instance presentation_isLocallySurjective :
    Presheaf.IsLocallySurjective (Opens.grothendieckTopology X.carrier) P.presentation.hom

AlgebraicGeometry.RingedSpaceThickening.AlgebraSquareZeroExtension.conormalToIdeal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionPresentation.lean, line 377. The attribute's comment: “the map 𝒥/𝒥² ⟶ 𝒢 determined by α'; not the resulting element of Ext¹_{𝒪_X}(𝖭𝖫(α), 𝒢), whose agreement with the class of 𝒪_{X'} under the bijection of 0GPZ is not proved here”.

The map 𝒥/𝒥² ⟶ 𝒢 determined by α'.

abbrev conormalToIdeal :
    conormalSheaf.{u, u, u, u} (Opens.grothendieckTopology X.carrier)
      (freeAlgebraSheaf (Opens.grothendieckTopology X.carrier) (inverseImageBaseRing f)
        P.generators) X.sheaf P.presentation ⟶ G

AlgebraicGeometry.RingedSpaceThickening.AlgebraSquareZeroExtension.naiveCotangentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionPresentation.lean, line 405. The attribute's comment: “the identification 𝖭𝖫_{X/S} ≅ 𝖭𝖫(α) in D(𝒪_X) for the chosen ℰ, by 08TL”.

The identification 𝖭𝖫(α) ≅ 𝖭𝖫_{X/S} in D(𝒪_X) given by the canonical comparison map.

def naiveCotangentIso :
    DerivedCategory.Q.obj P.naiveCotangentComplex ≅
      DerivedCategory.Q.obj (Stacks.SheafOfModules.naiveCotangentComplex.{u, u, u, u}
        (Opens.grothendieckTopology X.carrier) (inverseImageBaseRing f) X.sheaf
        (structureRingMap f))

AlgebraicGeometry.RingedSpaceThickening.SquareZeroAlgebraExtension.isomorphismClassesEquivExt_mk_eq_presented, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionPresentationRemark.lean, line 108.

Stacks Project, Tag 0GQ0. Let 0 ⟶ 𝒢 ⟶ 𝒪_{X'} ⟶ 𝒪_X ⟶ 0 be an extension of f⁻¹𝒪_S-algebras with 𝒢 an ideal of square zero, and let ℰ be any (pre)sheaf of sets with a commutative diagram α' : ℰ ⟶ 𝒪_{X'}, α : ℰ ⟶ 𝒪_X over the reduction (hα) such that f⁻¹𝒪_S[ℰ] ⟶ 𝒪_X is surjective, with kernel 𝒥. The map f⁻¹𝒪_S[ℰ] ⟶ 𝒪_{X'} determined by α' induces 𝒥/𝒥² ⟶ 𝒢 (conormalToIdeal); its class in Ext¹_{𝒪_X}(𝖭𝖫(α), 𝒢) (conormalExtClass on 𝖭𝖫(α) = (𝒥/𝒥² ⟶ Ω ⊗ 𝒪_X)), carried to Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢) along the identification 𝖭𝖫(α) ≅ 𝖭𝖫_{X/S} of Stacks 08TL (naiveCotangentIso), is the element the canonical bijection of Stacks 0GPZ attaches to the class of 𝒪_{X'}.

theorem isomorphismClassesEquivExt_mk_eq_presented (P : SquareZeroAlgebraExtension f G)
    (E : Functor (Opens X.carrier)ᵒᵖ (Type u))
    (α : E ⟶ underlyingPresheaf (Opens.grothendieckTopology X.carrier) X.sheaf)
    (α' : E ⟶ underlyingPresheaf (Opens.grothendieckTopology X.carrier) P.sheaf)
    (hα : α' ≫ P.generatorsMap = α)
    [Presheaf.IsLocallySurjective (Opens.grothendieckTopology X.carrier)
      (generatorsPresentation f E α).hom] :
    (PresentedSquareZeroExtension.naiveCotangentIso f E α).inv ≫
        (PresentedSquareZeroExtension.twoTerm f E α).conormalExtClass G
          (P.withGenerators E α α' hα).conormalToIdeal =
      isomorphismClassesEquivExt f G ⟦P⟧

Tag 0GQ1, a lemma

Tag 0GQ1 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.nonempty_compatibleMorphism_iff_pullbackExtClass_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/CompatibleMorphismExtClass.lean, line 363.

Stacks Project, Tag 0GQ1. Let f : (X, 𝒪_X) ⟶ (S, 𝒪_S) and g : (Y, 𝒪_Y) ⟶ (X, 𝒪_X) be morphisms of ringed spaces, ℱ an 𝒪_X-module, 𝒢 an 𝒪_Y-module and c : ℱ ⟶ g_*𝒢 a g-map. Let P : 0 ⟶ ℱ ⟶ 𝒪_{X'} ⟶ 𝒪_X ⟶ 0 be an extension of f⁻¹𝒪_S-algebras corresponding to ξ ∈ Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, ℱ) and Q : 0 ⟶ 𝒢 ⟶ 𝒪_{Y'} ⟶ 𝒪_Y ⟶ 0 an extension of g⁻¹f⁻¹𝒪_S-algebras corresponding to ζ ∈ Ext¹_{𝒪_Y}(𝖭𝖫_{Y/S}, 𝒢) under the bijections of Stacks 0GPZ. Then there is an S-morphism g' : Y' ⟶ X' compatible with g and c if and only if ξ and ζ map to the same element of Ext¹_{𝒪_Y}(Lg^*𝖭𝖫_{X/S}, 𝒢): ξ through Lg^* and the coefficient map Lg^*ℱ ⟶ g^*ℱ ⟶ 𝒢 (the last map the adjoint of c), and ζ through the canonical map Lg^*𝖭𝖫_{X/S} ⟶ 𝖭𝖫_{Y/S}.

theorem nonempty_compatibleMorphism_iff_pullbackExtClass_eq (P : SquareZeroAlgebraExtension f F)
    (Q : SquareZeroAlgebraExtension (g ≫ f) G) (c : F ⟶ (modulePushforward g).obj G) :
    Nonempty (CompatibleMorphism P Q c) ↔
      pullbackExtClass g f (((modulePullbackPushforwardAdjunction g).homEquiv _ _).symm c)
          (isomorphismClassesEquivExt f F (Quotient.mk _ P)) =
        restrictDerivedExtClass (derivedPullbackNaiveCotangentMap g f)
          (isomorphismClassesEquivExt (g ≫ f) G (Quotient.mk _ Q))

AlgebraicGeometry.RingedSpaceThickening.exists_compatibleLift_iff_eq_pullbackExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DerivedExtensionClassCriterion.lean, line 92. The attribute's comment: “the criterion for the DERIVED pullback Lf^*𝖭𝖫_{S/S'} of the source's statement, with the image of ξ the constructed map pullbackExtClass. Carried, exactly as in the degreewise form: the two-term structure P with hP, the bijection e of Steps 1 to 3 of 08U8, and hcompat, the 0GPZ/08U8 compatibility whose statement and proof the source omits”.

For the derived pullback Lf^*𝖭𝖫_{S/S'}: a lift compatible with f and the prescribed map c exists if and only if the class of the extension 𝒪_{X'}, restricted along a comparison q : Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'}, agrees with the image pullbackExtClass f t c xi of ξ ∈ Ext¹_{𝒪_S}(𝖭𝖫_{S/S'}, 𝒥) in Ext¹_{𝒪_X}(Lf^*𝖭𝖫_{S/S'}, 𝒢). The compatible lifts are the type Lift, identified by e with the factorizations of the difference homomorphism δ through the degree 0 term, and hcompat says that the difference of the two classes is the obstruction class.

theorem exists_compatibleLift_iff_eq_pullbackExtClass {f : X ⟶ S} {t : S ⟶ S'}
    {J : SheafOfModules.{u} (structureSheafRing S)} {G : SheafOfModules.{u} (structureSheafRing X)}
    (c : (modulePullback f).obj J ⟶ G)
    (q : derivedPullbackNaiveCotangent f t ⟶ relativeNaiveCotangentObj (f ≫ t))
    (P : NaiveCotangentTwoTerm
      (DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0))
    (hP : P.obj = derivedPullbackNaiveCotangent f t)
    (δ : P.conormal ⟶ G) {Lift : Type*}
    (e : Lift ≃ {θ : P.base ⟶ G // P.d ≫ θ = δ})
    (xi : extOneNaiveCotangent t J) (ζ : extOneNaiveCotangent (f ≫ t) G)
    (hcompat : eqToHom hP ≫ (pullbackExtClass f t c xi - restrictDerivedExtClass q ζ) =
      P.conormalExtClass G δ) :
    Nonempty Lift ↔ pullbackExtClass f t c xi = restrictDerivedExtClass q ζ

AlgebraicGeometry.RingedSpaceThickening.isSolutionClass_iff_eq_pullbackExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DerivedExtensionClassCriterion.lean, line 141. The attribute's comment: “the criterion for the DERIVED pullback, read on isomorphism classes of extensions: this is the hcrit hypothesis of solutionsEquivExtFibre, proved rather than assumed. Carried are the two-term structure P with hP, the per-class bijections e of Steps 1 to 3 of 08U8, the per-class 0GPZ/08U8 compatibilities, and the 0GPZ bijection E”.

Read on isomorphism classes: a class of square-zero extensions of f^{-1}𝒪_{S'}-algebras is a class of solutions of Stacks 08U7 exactly when its image under E restricts, along a comparison q : Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'}, to the image of ξ in Ext¹_{𝒪_X}(Lf^*𝖭𝖫_{S/S'}, 𝒢). Here P with hP is a two-term structure of Lf^*𝖭𝖫_{S/S'}, e and hcompat are the per-class bijections and compatibilities of exists_compatibleLift_iff_eq_pullbackExtClass, and E is the bijection of Stacks 0GPZ.

theorem isSolutionClass_iff_eq_pullbackExtClass
    (E : Quotient r ≃ extOneNaiveCotangent (f ≫ t) G)
    (q : derivedPullbackNaiveCotangent f t ⟶ relativeNaiveCotangentObj (f ≫ t))
    (xi : extOneNaiveCotangent t (baseIdealOnReduction t))
    (P : NaiveCotangentTwoTerm
      (DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0))
    (hP : P.obj = derivedPullbackNaiveCotangent f t)
    (δ : Quotient r → (P.conormal ⟶ G))
    (e : ∀ p : Quotient r, SolutionInClass ht c r p ≃
      {θ : P.base ⟶ G // P.d ≫ θ = δ p})
    (hcompat : ∀ p : Quotient r, eqToHom hP ≫
      (pullbackExtClass f t c xi - restrictDerivedExtClass q (E p)) =
        P.conormalExtClass G (δ p))
    (p : Quotient r) :
    ExtensionOverBase.IsSolutionClass ht c r p ↔
      restrictDerivedExtClass q (E p) = pullbackExtClass f t c xi

AlgebraicGeometry.RingedSpaceThickening.pulledNaiveCotangentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionClassComparison.lean, line 76. The attribute's comment: “the canonical comparison g^𝖭𝖫_{X/S} ⟶ 𝖭𝖫_{Y/S} along which ζ is read, for the degreewise pullback; the derived pullback Lg^𝖭𝖫_{X/S} of the source's statement is not used”.

The canonical comparison g^*𝖭𝖫_{X/S} ⟶ 𝖭𝖫_{Y/S}: the identification of g^*𝖭𝖫_{X/S} with the base change of 𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, followed by the canonical base-change map for g⁻¹f⁻¹𝒪_S ⟶ g⁻¹𝒪_X ⟶ 𝒪_Y.

def pulledNaiveCotangentComparison (g : Y ⟶ X) (f : X ⟶ S) :
    pulledNaiveCotangentComplex.{u} g f ⟶ relativeNaiveCotangentComplex g f

AlgebraicGeometry.RingedSpaceThickening.restrictExtClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionClassComparison.lean, line 105. The attribute's comment: “the map Ext¹(𝖭𝖫_{Y/S}, 𝒢) ⟶ Ext¹(g^*𝖭𝖫_{X/S}, 𝒢) in which ζ is read, the second of the two maps the source's proof constructs; the first, which goes through the derived pullback of 06YJ and the g-map c, is not constructed here”.

The map Ext¹_{𝒪_Y}(𝖭𝖫_{Y/S}, 𝒢) ⟶ Ext¹_{𝒪_Y}(g^*𝖭𝖫_{X/S}, 𝒢): precomposition with the canonical comparison of the naive cotangent complexes.

def restrictExtClass (ζ : relativeExtGroup g f G) : pulledExtGroup g f G

AlgebraicGeometry.RingedSpaceThickening.exists_compatibleLift_iff_eq_restrictExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionClassComparison.lean, line 124. The attribute's comment: “the equivalence, deduced from clause (1) of 08U8: the two Ext¹ classes agree exactly when a compatible S-morphism exists. The two-term structure of g^𝖭𝖫_{X/S} is now constructed rather than assumed, by pulledNaiveCotangentTwoTerm. Two conditions remain inputs: (i) the bijection e between the compatible S-morphisms and the factorizations of the difference homomorphism — Steps 1 to 3 of 08U8, an input there too — and (ii) hcompat, the compatibility between the constructions in the proofs of 0GPZ and 08U8 whose statement and proof the source omits. The class read off from ξ is taken as its image in Ext¹(g^𝖭𝖫_{X/S}, 𝒢); the first of the source's two maps is not constructed here”.

An S-morphism Y' ⟶ X' compatible with g and the g-map c exists if and only if ξ = restrictExtClass g f G ζ in Ext¹_{𝒪_Y}(g^*𝖭𝖫_{X/S}, 𝒢).

Here δ : g^*(𝒥/𝒥²) ⟶ 𝒢 is a homomorphism out of the conormal term of the two-term structure AlgebraicGeometry.RingedSpaceThickening.pulledNaiveCotangentTwoTerm g f. The theorem takes as hypotheses a bijection e between the type Lift of compatible morphisms and the factorizations of δ through the degree 0 term g^*Ω, and the identity hcompat: the difference ξ - restrictExtClass g f G ζ is the obstruction class of δ.

theorem exists_compatibleLift_iff_eq_restrictExtClass
    (δ : (pulledNaiveCotangentTwoTerm g f).conormal ⟶ G) {Lift : Type*}
    (e : Lift ≃ {θ : (pulledNaiveCotangentTwoTerm g f).base ⟶ G //
      (pulledNaiveCotangentTwoTerm g f).d ≫ θ = δ})
    (ξ : pulledExtGroup g f G) (ζ : relativeExtGroup g f G)
    (hcompat : ξ - restrictExtClass g f G ζ =
      (pulledNaiveCotangentTwoTerm g f).conormalExtClass G δ) :
    Nonempty Lift ↔ ξ = restrictExtClass g f G ζ

AlgebraicGeometry.RingedSpaceThickening.eq_restrictExtClass_iff_exists_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/ExtensionClassComparisonUnconditional.lean, line 149. The attribute's comment: “the equivalence with every input removed: the two Ext¹ classes agree exactly when their difference is the class of a homomorphism δ out of the conormal term of g^𝖭𝖫_{X/S} which factors through the degree 0 term. The binders are g, f, 𝒢 and the two classes alone — there is no type of compatible morphisms, no bijection e and no compatibility hcompat — and this implies exists_compatibleLift_iff_eq_restrictExtClass of ExtensionClassComparison.lean for every choice of those four. The right hand side is the condition that Steps 1 to 3 of the proof of 08U8 identify with the existence of a compatible S-morphism Y' ⟶ X'; that identification is a separate result of the source, so the left hand side of the source's own equivalence is read here through it. The comparison group is the Ext¹ of the DEGREEWISE pullback g^𝖭𝖫_{X/S} rather than of the derived pullback Lg^*𝖭𝖫_{X/S} of the source's statement, and ξ is a FREE ELEMENT of that group rather than the image of the class of the extension of 𝒪_X: the first of the source's two maps, which would carry that class in, is absent here”.

Stacks Project, Tag 0GQ1, with every input removed. The two classes agree in Ext¹_{𝒪_Y}(g^*𝖭𝖫_{X/S}, 𝒢) if and only if their difference is the class of a homomorphism δ out of the conormal term of g^*𝖭𝖫_{X/S} which factors through the degree 0 term.

The right hand side is the condition that Steps 1 to 3 of the proof of Stacks 08U8 identify with the existence of a compatible S-morphism Y' ⟶ X'. Compared with exists_compatibleLift_iff_eq_restrictExtClass the homomorphism δ, the type Lift, the bijection e and the compatibility hcompat are all gone: the only binders are g, f, 𝒢 and the two classes. That statement follows from this one for every choice of them.

theorem eq_restrictExtClass_iff_exists_factorization
    (ξ : pulledExtGroup g f G) (ζ : relativeExtGroup g f G) :
    ξ = restrictExtClass g f G ζ ↔
      ∃ δ : (pulledNaiveCotangentTwoTerm g f).conormal ⟶ G,
        ξ - restrictExtClass g f G ζ =
            (pulledNaiveCotangentTwoTerm g f).conormalExtClass G δ ∧
          Nonempty { θ : (pulledNaiveCotangentTwoTerm g f).base ⟶ G //
            (pulledNaiveCotangentTwoTerm g f).d ≫ θ = δ }

Tag 0GQ2, a remark

Tag 0GQ2 in the Stacks Project.

Stacks.Deformation.InverseImageExtension.Data.pullbackExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageExtensionComparison.lean, line 231. The attribute's comment: “the pullback extension 𝒪'₂ = 𝒪_{Y'} ×_{𝒪_Y} g⁻¹𝒪_X, with the second displayed diagram its projections. Carried: that g⁻¹𝒪_{X'} is an extension of g⁻¹𝒪_X by g⁻¹ℱ, and that 𝒢 is the square-zero ideal of 𝒪_{Y'} with its 𝒪_Y-action”.

Stacks 0GQ2, the second construction: pulling the extension 0 ⟶ 𝒢 ⟶ 𝒪_{Y'} ⟶ 𝒪_Y ⟶ 0 back along g^♯ : g^{-1}𝒪_X ⟶ 𝒪_Y gives an extension 0 ⟶ 𝒢 ⟶ 𝒪'₂ ⟶ g^{-1}𝒪_X ⟶ 0 of g^{-1}f^{-1}𝒪_S-algebras, with 𝒪'₂ = 𝒪_{Y'} ×_{𝒪_Y} g^{-1}𝒪_X the fibre product of sheaves of rings and the remark's second displayed diagram its two projections.

def pullbackExtension : AlgebraExtension S A (d.u ≫ d.π) d.N.val.presheaf

Stacks.Deformation.InverseImageExtension.Data.pushoutExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageExtensionComparison.lean, line 325. The attribute's comment: “the pushout extension 𝒪'₁ of g⁻¹𝒪_{X'} along c, with the first displayed diagram its comparison with g⁻¹𝒪_{X'}. Carried: that g⁻¹𝒪_{X'} is an extension of g⁻¹𝒪_X by g⁻¹ℱ, the ideal being Ker π”.

Stacks 0GQ2, the first construction: pushing the extension 0 ⟶ g^{-1}ℱ ⟶ g^{-1}𝒪_{X'} ⟶ g^{-1}𝒪_X ⟶ 0 out along c : g^{-1}ℱ ⟶ 𝒢 gives an extension 0 ⟶ 𝒢 ⟶ 𝒪'₁ ⟶ g^{-1}𝒪_X ⟶ 0 of g^{-1}f^{-1}𝒪_S-algebras, with the remark's first displayed diagram its comparison with g^{-1}𝒪_{X'}.

def pushoutExtension [K.WEqualsLocallyBijective CommRingCat.{u}] :
    AlgebraExtension S A (d.u ≫ d.π) d.N.val.presheaf

Stacks.Deformation.InverseImageExtension.Data.nonempty_compatibleHom_iff_isomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageExtensionComparison.lean, line 661. The attribute's comment: “the diagram chase: a compatible S-morphism Y' → X' exists iff 𝒪'₁ ≅ 𝒪'₂ as g⁻¹f⁻¹𝒪_S-algebra extensions of g⁻¹𝒪_X by 𝒢. Carried: that g⁻¹𝒪_{X'} is an extension of g⁻¹𝒪_X by g⁻¹ℱ, and that 𝒢 is the square-zero ideal of 𝒪_{Y'} with its 𝒪_Y-action”.

Stacks 0GQ2, the criterion. An S-morphism Y' → X' compatible with g and c exists if and only if the pushout 𝒪'₁ and the pullback 𝒪'₂ are isomorphic as g^{-1}f^{-1}𝒪_S-algebra extensions of g^{-1}𝒪_X by 𝒢.

theorem nonempty_compatibleHom_iff_isomorphic :
    Nonempty d.CompatibleHom ↔
      AlgebraExtension.Isomorphic d.pushoutExtension d.pullbackExtension

AlgebraicGeometry.RingedSpaceThickening.inverseImageNaiveCotangentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageNaiveCotangentIso.lean, line 592.

The identification g⁻¹𝖭𝖫_{X/S} = 𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}: the canonical map π^*𝖭𝖫_{X/S} ⟶ 𝖭𝖫_{g⁻¹𝒪_X/(g ∘ f)⁻¹𝒪_S} of naive cotangent complexes, as an isomorphism of complexes of g⁻¹𝒪_X-modules.

def inverseImageNaiveCotangentIso :
    ((modulePullback (inverseImageProj g)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (show CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ from
          PresentedSquareZeroExtension.relativeComplex f) ≅
      (show CochainComplex
            (SheafOfModules.{u} (structureSheafRing (inverseImageRingedSpace g))) ℤ from
          PresentedSquareZeroExtension.relativeComplex (inverseImageProj g ≫ f))

AlgebraicGeometry.RingedSpaceThickening.isomorphismClassesEquivExt_inverseImagePushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageNaiveCotangentIso.lean, line 635.

The class, under the bijection of Stacks 0GPZ for the ringed space (Y, g⁻¹𝒪_X) over S, of the pushout 𝒪'₁ of 0 ⟶ g⁻¹ℱ ⟶ g⁻¹𝒪_{X'} ⟶ g⁻¹𝒪_X ⟶ 0 along c : g⁻¹ℱ ⟶ 𝒢 is the image of the class ξ of 𝒪_{X'} (under the bijection of Stacks 0GPZ for X over S): g⁻¹ξ pushed along c^♭ : g⁻¹ℱ ⟶ 𝒢, read in Ext¹_{g⁻¹𝒪_X}(𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, 𝒢) through the identification 𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S} = g⁻¹𝖭𝖫_{X/S} of Stacks 08TM.

theorem isomorphismClassesEquivExt_inverseImagePushout (P : SquareZeroAlgebraExtension f F)
    (c : F ⟶ (modulePushforward g).obj G) :
    SquareZeroAlgebraExtension.isomorphismClassesEquivExt (inverseImageSpaceHom f g)
        (restrictedModule g G) (Quotient.mk _ (inverseImagePushout G P c)) =
      inverseImageXiMap c
        (SquareZeroAlgebraExtension.isomorphismClassesEquivExt f F (Quotient.mk _ P))

AlgebraicGeometry.RingedSpaceThickening.isomorphismClassesEquivExt_inverseImagePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningClasses.lean, line 431.

The class of 𝒪'₂. The class, under the bijection of Stacks 0GPZ for the ringed space (Y, g⁻¹𝒪_X) over S, of the pullback 𝒪'₂ = 𝒪_{Y'} ×_{𝒪_Y} g⁻¹𝒪_X is the image of the class ζ of 𝒪_{Y'} (under the bijection of Stacks 0GPZ for Y over S) by the canonical map Ext¹_{𝒪_Y}(𝖭𝖫_{Y/S}, 𝒢) ⟶ Ext¹_{g⁻¹𝒪_X}(𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, 𝒢).

theorem isomorphismClassesEquivExt_inverseImagePullback
    {G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (J := Opens.grothendieckTopology Y.carrier) Y.sheaf)}
    (Q : SquareZeroAlgebraExtension (g ≫ f) G) :
    SquareZeroAlgebraExtension.isomorphismClassesEquivExt (inverseImageSpaceHom f g)
        (restrictedModule g G) (Quotient.mk _ (inverseImagePullback Q)) =
      inverseImageExtMap
        (SquareZeroAlgebraExtension.isomorphismClassesEquivExt (g ≫ f) G (Quotient.mk _ Q))

AlgebraicGeometry.RingedSpaceThickening.inverseImageExtEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningExtIdentification.lean, line 628.

The identification Ext¹_{𝒪_Y}(Lg^*𝖭𝖫_{X/S}, 𝒢) = Ext¹_{g⁻¹𝒪_X}(𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, 𝒢) of Stacks 0GQ2. Through Lg^* = Lι^* ∘ π^* along g = π ∘ ι, the tensor–hom adjunction Lι^* ⊣ Rι_* = ι_* (restriction of scalars along g^♯ : g⁻¹𝒪_X ⟶ 𝒪_Y), and the identification g⁻¹𝖭𝖫_{X/S} = 𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S} (inverseImageNaiveCotangentIso).

def inverseImageExtEquiv :
    extOnePulledNaiveCotangent g f G ≃
      extOneNaiveCotangent (inverseImageSpaceHom f g) (restrictedModule g G)

AlgebraicGeometry.RingedSpaceThickening.inverseImageExtEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningExtIdentification.lean, line 640.

The identification inverseImageExtEquiv is the explicit composite: the transposition liftProjTransport along the adjunction Lι^* ⊣ ι_*, preceded by g⁻¹𝖭𝖫_{X/S} = 𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S} and followed by ι_*(𝒢[1]) = (ι_*𝒢)[1].

theorem inverseImageExtEquiv_apply (z : extOnePulledNaiveCotangent g f G) :
    inverseImageExtEquiv f g G z =
      (DerivedCategory.Q.mapIso (inverseImageNaiveCotangentIso f g)).inv ≫
        liftProjTransport g (PresentedSquareZeroExtension.relativeComplex f) z ≫
        liftShiftSingleIso.hom

AlgebraicGeometry.RingedSpaceThickening.inverseImageExtEquiv_restrictDerivedExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningExtIdentification.lean, line 661.

The image of ζ through Ext¹_{𝒪_Y}(Lg^*𝖭𝖫_{X/S}, 𝒢) is its image in Ext¹_{g⁻¹𝒪_X}(𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, 𝒢).

theorem inverseImageExtEquiv_restrictDerivedExtClass (ζ : extOneNaiveCotangent (g ≫ f) G) :
    inverseImageExtEquiv f g G
        (restrictDerivedExtClass (derivedPullbackNaiveCotangentMap g f) ζ) =
      inverseImageExtMap ζ

AlgebraicGeometry.RingedSpaceThickening.inverseImageExtEquiv_pullbackExtClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningExtIdentification.lean, line 959.

The image of ξ through Ext¹_{𝒪_Y}(Lg^*𝖭𝖫_{X/S}, 𝒢) is its image in Ext¹_{g⁻¹𝒪_X}(𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, 𝒢).

theorem inverseImageExtEquiv_pullbackExtClass (P : SquareZeroAlgebraExtension f F)
    (c : F ⟶ (modulePushforward g).obj G) :
    inverseImageExtEquiv f g G (pullbackExtClass g f (LiftGluing.cAdj g c) P.extClass) =
      inverseImageXiMap c P.extClass

AlgebraicGeometry.RingedSpaceThickening.nonempty_compatibleMorphism_iff_isomorphismClassesEquivExt_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningExtIdentification.lean, line 972.

Stacks 0GQ2, the classification. By the diagram chase and the bijection of Stacks 0GPZ for the ringed space (Y, g⁻¹𝒪_X) over S, an S-morphism Y' ⟶ X' compatible with g and c exists if and only if the extensions 𝒪'₁ and 𝒪'₂ have the same class in Ext¹_{g⁻¹𝒪_X}(𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, 𝒢).

theorem nonempty_compatibleMorphism_iff_isomorphismClassesEquivExt_eq
    (P : SquareZeroAlgebraExtension f F) (Q : SquareZeroAlgebraExtension (g ≫ f) G)
    (c : F ⟶ (modulePushforward g).obj G) :
    Nonempty (CompatibleMorphism P Q c) ↔
      SquareZeroAlgebraExtension.isomorphismClassesEquivExt (inverseImageSpaceHom f g)
          (restrictedModule g G) (Quotient.mk _ (inverseImagePushout G P c)) =
        SquareZeroAlgebraExtension.isomorphismClassesEquivExt (inverseImageSpaceHom f g)
          (restrictedModule g G) (Quotient.mk _ (inverseImagePullback Q))

AlgebraicGeometry.RingedSpaceThickening.nonempty_compatibleMorphism_iff_images_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningExtIdentification.lean, line 989.

Stacks 0GQ2, the final deduction. An S-morphism Y' ⟶ X' compatible with g and c exists if and only if ξ and ζ have the same image in Ext¹_{𝒪_Y}(Lg^*𝖭𝖫_{X/S}, 𝒢): through the identification Ext¹_{g⁻¹𝒪_X}(𝖭𝖫_{g⁻¹𝒪_X/g⁻¹f⁻¹𝒪_S}, 𝒢) = Ext¹_{𝒪_Y}(Lg^*𝖭𝖫_{X/S}, 𝒢) (inverseImageExtEquiv), the class of 𝒪'₁ is the image of ξ and the class of 𝒪'₂ is the image of ζ, so this is nonempty_compatibleMorphism_iff_isomorphismClassesEquivExt_eq.

theorem nonempty_compatibleMorphism_iff_images_eq
    (P : SquareZeroAlgebraExtension f F) (Q : SquareZeroAlgebraExtension (g ≫ f) G)
    (c : F ⟶ (modulePushforward g).obj G) :
    Nonempty (CompatibleMorphism P Q c) ↔
      pullbackExtClass g f (LiftGluing.cAdj g c)
          (SquareZeroAlgebraExtension.isomorphismClassesEquivExt f F (Quotient.mk _ P)) =
        restrictDerivedExtClass (derivedPullbackNaiveCotangentMap g f)
          (SquareZeroAlgebraExtension.isomorphismClassesEquivExt (g ≫ f) G (Quotient.mk _ Q))

AlgebraicGeometry.RingedSpaceThickening.inverseImagePushout, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningRemark.lean, line 275.

The extension 𝒪'₁ of Stacks 0GQ2: the pushout of 0 ⟶ g⁻¹ℱ ⟶ g⁻¹𝒪_{X'} ⟶ g⁻¹𝒪_X ⟶ 0 along c : g⁻¹ℱ ⟶ 𝒢, an extension 0 ⟶ 𝒢 ⟶ 𝒪'₁ ⟶ g⁻¹𝒪_X ⟶ 0 of g⁻¹f⁻¹𝒪_S-algebras, that is, a square-zero extension over the ringed space (Y, g⁻¹𝒪_X) and its morphism to S. Here g⁻¹ℱ is the kernel of the inverse image g⁻¹𝒪_{X'} ⟶ g⁻¹𝒪_X of the reduction, and c on it is idealMap.

def inverseImagePushout :
    SquareZeroAlgebraExtension (inverseImageSpaceHom f g) (restrictedModule g G)

AlgebraicGeometry.RingedSpaceThickening.inverseImagePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningRemark.lean, line 335.

The extension 𝒪'₂ of Stacks 0GQ2: the pullback of 0 ⟶ 𝒢 ⟶ 𝒪_{Y'} ⟶ 𝒪_Y ⟶ 0 along g^♯ : g⁻¹𝒪_X ⟶ 𝒪_Y, the extension 0 ⟶ 𝒢 ⟶ 𝒪_{Y'} ×_{𝒪_Y} g⁻¹𝒪_X ⟶ g⁻¹𝒪_X ⟶ 0 of g⁻¹f⁻¹𝒪_S-algebras; its two projections are the second displayed diagram.

def inverseImagePullback :
    SquareZeroAlgebraExtension (inverseImageSpaceHom f g) (restrictedModule g G)

AlgebraicGeometry.RingedSpaceThickening.nonempty_compatibleMorphism_iff_nonempty_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/InverseImageThickeningRemark.lean, line 558.

Stacks 0GQ2, the diagram chase. An S-morphism Y' ⟶ X' compatible with g and c exists if and only if 𝒪'₁ and 𝒪'₂ are isomorphic as g⁻¹f⁻¹𝒪_S-algebra extensions of g⁻¹𝒪_X by 𝒢.

theorem nonempty_compatibleMorphism_iff_nonempty_iso :
    Nonempty (CompatibleMorphism P Q c) ↔
      Nonempty (inverseImagePushout G P c ≅ inverseImagePullback Q)

Tag 0GQ3, a lemma

Tag 0GQ3 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.DeformationSolution.isomorphismClassesEquivExtFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DeformationSolutionExtFibre.lean, line 95.

Let t : (S, 𝒪_S) ⟶ (S', 𝒪_{S'}) be a first order thickening, 𝒥 = Ker(t^♯) (baseIdealModule), f : (X, 𝒪_X) ⟶ (S, 𝒪_S), 𝒢 an 𝒪_X-module and c : 𝒥 ⟶ 𝒢 as in (08U7): here c is given, as in DeformationSolution, by c' : f^*t^*Ker(t^♯) ⟶ 𝒢, and is f^*𝒥 ≅ f^*t^*Ker(t^♯) ⟶ 𝒢 (baseIdealIsoPullback). Let ξ ∈ Ext¹_{𝒪_S}(𝖭𝖫_{S/S'}, 𝒥) be the element corresponding to the extension 𝒪_{S'} of 𝒪_S by 𝒥 via Stacks 0GPZ (baseClass). The set of isomorphism classes of solutions of (08U7) (first order thickenings X ⟶ X' with a morphism of thickenings to S ⟶ S', Ker ≅ 𝒢 and inducing c, up to the isomorphism Isomorphic of Stacks 08UC) is canonically bijective to the fibre of

Ext¹_{𝒪_X}(𝖭𝖫_{X/S'}, 𝒢) ⟶ Ext¹_{𝒪_X}(Lf^*𝖭𝖫_{S/S'}, 𝒢)

over the image of ξ: the map is precomposition with the canonical comparison Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} (through the derived pullback Lf^* of Stacks 06YJ), and the image of ξ is Lf^*ξ pushed along Lf^*𝒥 ⟶ f^*𝒥 ⟶ 𝒢 (pullbackExtClass). The bijection sends a solution X' to the class, under Stacks 0GPZ for X ⟶ S', of 𝒪_{X'} read as an extension of f⁻¹𝒪_{S'}-algebras (DeformationSolution.isomorphismClassesEquivExtFibre_mk).

def DeformationSolution.isomorphismClassesEquivExtFibre :
    Quotient (DeformationSolution.isomorphicSetoid ht f G c') ≃
      {z : extOneNaiveCotangent (f ≫ t) G //
        restrictDerivedExtClass (derivedPullbackNaiveCotangentMap f t) z =
          pullbackExtClass f t ((modulePullback f).map (baseIdealIsoPullback ht).hom ≫ c')
            (baseClass ht)}

AlgebraicGeometry.RingedSpaceThickening.solutionsEquivDerivedExtFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DerivedExtensionClassCriterion.lean, line 173. The attribute's comment: “the canonical bijection from isomorphism classes of solutions of 08U7 to the fibre of Ext¹(𝖭𝖫_{X/S'}, 𝒢) ⟶ Ext¹(Lf^*𝖭𝖫_{S/S'}, 𝒢) over the image of ξ, by the constructed map [X'] ↦ E [𝒪_{X'}]. Carried: the 0GPZ bijection E, the comparison q, and the inputs P, hP, δ, e, hcompat of the 0GQ1 criterion — which is proved here, not assumed”.

In the situation of Stacks 08U7, with ξ the class of the extension 𝒪_{S'} of 𝒪_S by 𝒥, the isomorphism classes of solutions are canonically bijective to the fibre of

Ext¹_{𝒪_X}(𝖭𝖫_{X/S'}, 𝒢) ⟶ Ext¹_{𝒪_X}(Lf^*𝖭𝖫_{S/S'}, 𝒢)

over the image of ξ, by the map [X'] ↦ E [𝒪_{X'}]. Here E is the bijection of Stacks 0GPZ, q the comparison of naive cotangent complexes, and P, hP, δ, e, hcompat the inputs of isSolutionClass_iff_eq_pullbackExtClass.

def solutionsEquivDerivedExtFibre
    (E : Quotient r ≃ extOneNaiveCotangent (f ≫ t) G)
    (q : derivedPullbackNaiveCotangent f t ⟶ relativeNaiveCotangentObj (f ≫ t))
    (xi : extOneNaiveCotangent t (baseIdealOnReduction t))
    (P : NaiveCotangentTwoTerm
      (DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0))
    (hP : P.obj = derivedPullbackNaiveCotangent f t)
    (δ : Quotient r → (P.conormal ⟶ G))
    (e : ∀ p : Quotient r, SolutionInClass ht c r p ≃
      {θ : P.base ⟶ G // P.d ≫ θ = δ p})
    (hcompat : ∀ p : Quotient r, eqToHom hP ≫
      (pullbackExtClass f t c xi - restrictDerivedExtClass q (E p)) =
        P.conormalExtClass G (δ p)) :
    Quotient (solutionSetoid ht c r) ≃
      {z : extOneNaiveCotangent (f ≫ t) G //
        restrictDerivedExtClass q z = pullbackExtClass f t c xi}

AlgebraicGeometry.RingedSpaceThickening.solutionsEquivDerivedExtFibre_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/DerivedExtensionClassCriterion.lean, line 197. The attribute's comment: “the canonicity of the bijection: it is the constructed map [X'] ↦ E [𝒪_{X'}], sending the class of a solution to the class of its underlying extension read through the 0GPZ bijection, rather than an unspecified bijection of the two sides”.

The bijection solutionsEquivDerivedExtFibre sends the class of a solution X' to E [𝒪_{X'}].

theorem solutionsEquivDerivedExtFibre_apply
    (E : Quotient r ≃ extOneNaiveCotangent (f ≫ t) G)
    (q : derivedPullbackNaiveCotangent f t ⟶ relativeNaiveCotangentObj (f ≫ t))
    (xi : extOneNaiveCotangent t (baseIdealOnReduction t))
    (P : NaiveCotangentTwoTerm
      (DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0))
    (hP : P.obj = derivedPullbackNaiveCotangent f t)
    (δ : Quotient r → (P.conormal ⟶ G))
    (e : ∀ p : Quotient r, SolutionInClass ht c r p ≃
      {θ : P.base ⟶ G // P.d ≫ θ = δ p})
    (hcompat : ∀ p : Quotient r, eqToHom hP ≫
      (pullbackExtClass f t c xi - restrictDerivedExtClass q (E p)) =
        P.conormalExtClass G (δ p))
    (s : Quotient (solutionSetoid ht c r)) :
    (solutionsEquivDerivedExtFibre ht c r E q xi P hP δ e hcompat s).1 =
      solutionClassToExtClass ht c r E s

Tag 0GQ4, a remark

Tag 0GQ4 in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.naiveCotangentRemarkArrows, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentRemarkConditional.lean, line 69.

The two maps Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S} in D(𝒪_X). The first is the canonical map of Stacks 0GQ1 through the derived pullback of Stacks 06YJ, the second is induced by the tower (f ≫ t)^{-1}𝒪_{S'} ⟶ f^{-1}𝒪_S ⟶ 𝒪_X.

def naiveCotangentRemarkArrows (f : X ⟶ S) (t : S ⟶ S') :
    ComposableArrows (DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) 2

AlgebraicGeometry.RingedSpaceThickening.DeformationSolution.nonempty_iff_obstructionExtClass_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentRemarkConditional.lean, line 135.

In the situation of Stacks 0GQ3 (a first order thickening t : S ⟶ S' with ideal 𝒥, f : X ⟶ S, an 𝒪_X-module 𝒢 and c : f^*𝒥 ⟶ 𝒢, here f^*𝒥 ≅ f^*t^*Ker(t^♯) ⟶ 𝒢 with c'), let ξ be the class of the extension 𝒪_{S'} of 𝒪_S by 𝒥 under Stacks 0GPZ (baseClass). If the two maps Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S} form a distinguished triangle with some connecting map w, then a solution of (08U7) exists if and only if the image of ξ in Ext²_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢) — the image of ξ in Ext¹_{𝒪_X}(Lf^*𝖭𝖫_{S/S'}, 𝒢) (pullbackExtClass) composed with w — vanishes.

theorem DeformationSolution.nonempty_iff_obstructionExtClass_eq_zero
    (w : relativeNaiveCotangentObj f ⟶ (derivedPullbackNaiveCotangent f t)⟦(1 : ℤ)⟧)
    (htri : Triangle.mk (derivedPullbackNaiveCotangentMap f t)
        (relativeNaiveCotangentObjMap f t) w ∈
      distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))) :
    Nonempty (DeformationSolution t ht f G c') ↔
      obstructionExtClass w (pullbackExtClass f t
        ((modulePullback f).map (baseIdealIsoPullback ht).hom ≫ c') (baseClass ht)) = 0

AlgebraicGeometry.RingedSpaceThickening.naiveCotangentRemark_closeToDistinguishedTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentRemarkTriangle.lean, line 1236.

Stacks Project, Tag 0GQ4, what the remark's two maps Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S} satisfy: they are close to forming a distinguished triangle, by Stacks 0E1Z. Precisely:

the composite Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S} vanishes in D(𝒪_X);

the first map factors as the comparison Lf^*𝖭𝖫_{S/S'} ⟶ f^*𝖭𝖫_{S/S'} of Stacks 06YJ (an isomorphism on H⁰) followed by the canonical map f^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'};

the second map sits in a distinguished triangle C[-1] ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S} ⟶ C, with C the cone of 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S};

the canonical map f^*𝖭𝖫_{S/S'} ⟶ C[-1] of Stacks 0E1Z lifts f^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} along C[-1] ⟶ 𝖭𝖫_{X/S'}, is an isomorphism on H⁰ and is surjective on H⁻¹.

So the maps form a distinguished triangle exactly when the comparison with the cone is an isomorphism; the remark only says they are close to one, and nothing more is claimed.

theorem naiveCotangentRemark_closeToDistinguishedTriangle :
    derivedPullbackNaiveCotangentMap f t ≫ relativeNaiveCotangentObjMap f t = 0 ∧
    remarkPullbackComparison f t ≫ remarkPulledMap f t = derivedPullbackNaiveCotangentMap f t ∧
    IsIso ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) 0).map
      (remarkPullbackComparison f t)) ∧
    remarkConeTriangle f t ∈ distTriang _ ∧
    (remarkConeTriangle f t).mor₂ = relativeNaiveCotangentObjMap f t ∧
    remarkConeMap f t ≫ (remarkConeTriangle f t).mor₁ = remarkPulledMap f t ∧
    IsIso ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) 0).map
      (remarkConeMap f t)) ∧
    Epi ((DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing X)) (-1)).map
      (remarkConeMap f t))

AlgebraicGeometry.RingedSpaceThickening.naiveCotangentCompComplexMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentTriangleObstruction.lean, line 138. The attribute's comment: “the second map of complexes of the remark, 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S}”.

The map of complexes 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S}: the canonical map of a tower of sheaves of rings on X, taken at (f ≫ t)^{-1}𝒪_{S'} ⟶ f^{-1}𝒪_S ⟶ 𝒪_X.

public def naiveCotangentCompComplexMap (f : X ⟶ S) (t : S ⟶ S') :
    RingedSpace.naiveCotangentComplex (f ≫ t) ⟶ RingedSpace.naiveCotangentComplex f

AlgebraicGeometry.RingedSpaceThickening.derivedPullbackNaiveCotangentChain, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentTriangleObstruction.lean, line 154. The attribute's comment: “the remark's chain Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S}, with q carried”.

The chain Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S}, composed in D(𝒪_X): the first map is the given comparison q, the second is relativeNaiveCotangentObjMap.

public def derivedPullbackNaiveCotangentChain {f : X ⟶ S} {t : S ⟶ S'}
    (q : derivedPullbackNaiveCotangent f t ⟶ relativeNaiveCotangentObj (f ≫ t)) :
    derivedPullbackNaiveCotangent f t ⟶ relativeNaiveCotangentObj f

AlgebraicGeometry.RingedSpaceThickening.nonempty_deformationSolution_iff_obstruction_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/NaiveCotangentTriangleObstruction.lean, line 216. The attribute's comment: “the conditional: given the triangle, ξ's image in Ext² obstructs 08U7”.

In the situation of Stacks 0GQ3, given that the two maps Lf^*𝖭𝖫_{S/S'} ⟶ 𝖭𝖫_{X/S'} ⟶ 𝖭𝖫_{X/S} form a distinguished triangle with connecting morphism w, the deformation problem of Stacks 08U7 has a solution exactly when the image of ξ in Ext²_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢) vanishes; that image is therefore the obstruction.

The triangle is a hypothesis, not a claim: the source only says that the two maps are close to forming a distinguished triangle, and its conclusion is drawn under that assumption. The remaining arguments are those of solutionsEquivDerivedExtFibre, which supplies the bijection of Stacks 0GQ3 between isomorphism classes of solutions and the fibre over the image of ξ.

public theorem nonempty_deformationSolution_iff_obstruction_eq_zero
    (E : Quotient r ≃ extOneNaiveCotangent (f ≫ t) G)
    (q : derivedPullbackNaiveCotangent f t ⟶ relativeNaiveCotangentObj (f ≫ t))
    (xi : extOneNaiveCotangent t (baseIdealOnReduction t))
    (P : NaiveCotangentTwoTerm
      (DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0))
    (hP : P.obj = derivedPullbackNaiveCotangent f t)
    (δ : Quotient r → (P.conormal ⟶ G))
    (e : ∀ p : Quotient r, SolutionInClass ht c r p ≃
      {θ : P.base ⟶ G // P.d ≫ θ = δ p})
    (hcompat : ∀ p : Quotient r, eqToHom hP ≫
      (pullbackExtClass f t c xi - restrictDerivedExtClass q (E p)) =
        P.conormalExtClass G (δ p))
    (w : relativeNaiveCotangentObj f ⟶ (derivedPullbackNaiveCotangent f t)⟦(1 : ℤ)⟧)
    (htri : Triangle.mk q (relativeNaiveCotangentObjMap f t) w ∈
      distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))) :
    Nonempty (DeformationSolution t ht f G c) ↔
      obstructionExtClass w (pullbackExtClass f t c xi) = 0

Sources

LeanAlgebraicGeometry.RingedSpaceThickening.DeformationSolution · Stacks.SheafOfModules.presentationNaiveCotangentExtZeroAddEquiv · AlgebraicGeometry.RingedSpaceThickening.DeformationIdealDiagram.lifting_obstruction_and_torsor · AlgebraicGeometry.RingedSpaceThickening.liftingObstruction_eq_zero_iff · AlgebraicGeometry.RingedSpaceThickening.liftTranslate_zero · AlgebraicGeometry.RingedSpaceThickening.liftTranslate_add · AlgebraicGeometry.RingedSpaceThickening.existsUnique_liftTranslate · AlgebraicGeometry.RingedSpaceThickening.DeformationCube

Section91.8 Deformations of schemes #

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

Tag 0D14, a lemma

Tag 0D14 in the Stacks Project.

Stacks.Thickenings.FlatDeformation.exists_addTorsor_classes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FlatDeformation/Torsor.lean, line 223. References: SGA 7 VI (4.16), “(b), special case”.

Let S ⊂ S' be a first order thickening of schemes (t : S ⟶ S' a closed immersion whose ideal sheaf squares to zero) and let f : X ⟶ S be flat. Suppose there exist a flat morphism f' : X' ⟶ S' and an isomorphism a : X ≅ X' ×_{S'} S over S (a FlatDeformation t f, recording a through i = pr₁ ∘ a and the cartesian square IsPullback i f f' t; FlatDeformation.ofPair and FlatDeformation.a pass between the two). Then the set of isomorphism classes of such pairs (FlatDeformation.Classes t f; by FlatDeformation.nonempty_iso_iff two pairs are isomorphic exactly when there is e : X'₁ ≅ X'₂ over S' with (e ×_{S'} S) ∘ a₁ = a₂) is principal homogeneous under Ext¹_{𝒪_X}(NL_{X/S}, f^*𝒞_{S/S'}) (Scheme.naiveCotangentExt f _ 1, with pullbackConormalModule f t = f^*𝒞_{S/S'}).

The action is as follows: a pair is the same thing as a solution of the square-zero extension problem 0 ⟶ f^*𝒞_{S/S'} ⟶ 𝒪_{X'} ⟶ 𝒪_X ⟶ 0 over 0 ⟶ 𝒞_{S/S'} ⟶ 𝒪_{S'} ⟶ 𝒪_S ⟶ 0 (solutionOf, with the ideal of X in X' identified with f^*𝒞_{S/S'} by [Stacks Project, Tag 063Y]), and ξ sends the class of (f'₁, a₁) to the class of (f'₂, a₂) exactly when the obstruction class of [Stacks Project, Tag 08UG] separating the two solutions is ξ, which is the action of [Stacks Project, Tag 08UK]. The relation is independent of the reference pair D₀ used to write down the extension problem.

theorem exists_addTorsor_classes [Flat f]
    (hne : Nonempty (FlatDeformation t f)) :
    ∃ T : AddTorsor (Scheme.naiveCotangentExt f (pullbackConormalModule f t) 1)
        (Classes t f),
      ∀ (ξ : Scheme.naiveCotangentExt f (pullbackConormalModule f t) 1)
        (D₀ D₁ D₂ : FlatDeformation t f),
        T.vadd ξ (Quotient.mk (setoid t f) D₁) = Quotient.mk (setoid t f) D₂ ↔
          CompatibleFirstOrderThickening.pairObstruction (solutionOf hst D₀ D₁)
              (solutionOf hst D₀ D₂) =
            extIso f (pullbackConormalModule f t) 1 ξ

Stacks.Thickenings.flatThickeningAutEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FlatThickeningAutomorphisms.lean, line 488.

[Stacks Project, Tag 0D14], part (2). Let S ⊂ S' be a first order thickening of schemes, let f : X ⟶ S be a morphism, let f' : X' ⟶ S' be flat and let i : X ⟶ X' make the square cartesian, so that X = X' ×_{S'} S over S. Then the set of automorphisms φ : X' ⟶ X' over S' which reduce to the identity on X' ×_{S'} S is

Ext⁰_{𝒪_X}(NL_{X/S}, f^*𝒞_{S/S'}).

The bijection is not merely asserted: its value on a class ξ is the morphism Stacks.Thickenings.autOfHom for the 𝒪_X-linear map Stacks.Thickenings.flatThickeningActingGroupAddEquiv ... ξ : Ω_{X/S} ⟶ 𝒞_{X/X'}, whose comorphism is g ↦ g + α(d_{X/S}(i^♯ g)) by Stacks.Thickenings.flatThickeningAutEquiv_apply_appLE. In particular the identity automorphism corresponds to 0 (Stacks.Thickenings.autOfHom_zero) and composition to addition (Stacks.Thickenings.autOfHom_add), so the bijection is an isomorphism of groups.

def flatThickeningAutEquiv (i : X ⟶ X') (t : S ⟶ S')
    [AlgebraicGeometry.IsClosedImmersion t] (f : X ⟶ S) (f' : X' ⟶ S') [Flat f']
    (hst : t.ker ^ 2 = ⊥) (sq : IsPullback i f f' t) :
    AlgebraicGeometry.Scheme.naiveCotangentExt f (pullbackConormalModule f t) 0 ≃
      {φ : X' ≅ X' // i ≫ φ.hom = i ∧ φ.hom ≫ f' = f'}

Sources

LeanStacks.Thickenings.FlatDeformation.exists_addTorsor_classes · Stacks.Thickenings.flatThickeningAutEquiv

Section91.9 Thickenings of ringed topoi #

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

Tag 08M7, a situation

Tag 08M7 in the Stacks Project.

Deformation.ToposThickening.IsThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickenings.lean, line 119. The attribute's comment: “the horizontal arrows are thickenings”.

Stacks 08M7. A thickening of ringed topoi: the underlying geometric morphism is an equivalence of topoi, the structure map is locally surjective, and its kernel ideal is locally nilpotent. This is the hypothesis the source places on the horizontal arrows of a morphism of thickenings.

def IsThickening (i : RingedToposHom X Y) : Prop

Deformation.ToposThickening.IdealOfThickening, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickenings.lean, line 127. The attribute's comment: “the defining ideal of a thickening”.

Stacks 08M7. The defining ideal I = Ker(i^♯) ⊂ O' of a thickening i, presented as a sheaf of O'-modules together with an inclusion into O' whose sections are exactly the sections killed by the structure map.

structure IdealOfThickening (i : RingedToposHom X Y)

Deformation.ToposThickening.IsThickening.of_firstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickenings.lean, line 194. The attribute's comment: “a first order thickening is a thickening”.

Stacks 08M7. A first order thickening of ringed topoi in the sense of Stacks 08MB is a thickening: its structure map is locally surjective by assumption and its square-zero kernel is in particular locally nilpotent.

theorem IsThickening.of_firstOrderThickening {i : RingedToposHom X Y}
    (h : FirstOrderThickening i) : IsThickening i

Deformation.ToposThickening.IsFirstOrderThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickenings.lean, line 203. The attribute's comment: “first order thickening, as a property”.

Stacks 08M7. A first order thickening of ringed topoi, as a property of a morphism: a thickening whose kernel ideal is square zero. This is the predicate form of the structure Deformation.ToposThickening.FirstOrderThickening of Stacks 08MB, which in addition names the ideal.

def IsFirstOrderThickening (i : RingedToposHom X Y) : Prop

Deformation.ToposThickening.IsFirstOrderThickening.of_firstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickenings.lean, line 215. The attribute's comment: “08MB implies the property”.

Stacks 08M7. A first order thickening in the sense of Stacks 08MB has the property of being a first order thickening: its kernel is the square-zero ideal it names.

theorem IsFirstOrderThickening.of_firstOrderThickening {i : RingedToposHom X Y}
    (h : FirstOrderThickening i) : IsFirstOrderThickening i

Deformation.ToposThickening.MorphismOfThickenings, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickenings.lean, line 236. The attribute's comment: “the commutative square”.

Stacks 08M7. A morphism of thickenings of ringed topoi: a commutative square of morphisms of ringed topoi whose horizontal arrows i and t are thickenings, together with their defining ideals I = Ker(i^♯) ⊂ O' and J = Ker(t^♯) ⊂ O_{B'}.

structure MorphismOfThickenings

Deformation.ToposThickening.MorphismOfThickenings.firstOrderSurjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsFirstOrder.lean, line 314. The attribute's comment: “the first order reduction of the pullback of the lower ideal; the two upper topoi share their section universe, as the closed immersion carried by AlgebraicGeometry.ClosedRingedImmersion requires, the two lower ones staying independent”.

Stacks 08M7. The canonical reduction map (f')^*J ⟶ f^*J of a morphism of thickenings of ringed topoi, with the target read as the O'-module i_*f^*t^*J: the unit of i^* ⊣ i_*, followed by the direct image of the canonical comparison Deformation.ToposThickening.MorphismOfThickenings.pullbackComparison of the two iterated pullbacks around the square.

The map needs no hypothesis on the square. When the upper arrow is a first order thickening it is an epimorphism, by Deformation.ToposThickening.MorphismOfThickenings.firstOrderSurjection_epi.

What is proved here is an epimorphism with a unique factorization, and not the source's assertion, which is an equality (f')^*J = f^*J of the two pullbacks. The equality is not available under the hypotheses of Situation 91.9.1. By Deformation.ToposThickening.IsThickening.essImage_pushforwardModules_iff this map is an isomorphism exactly when I annihilates (f')^*J; and what annihilates (f')^*J is the ideal J·O' generated by the image of J under (f')^♯, since a product of two sections of J is zero. So the source's equality amounts to J·O' = I, which is the strictness Deformation.ToposThickening.MorphismOfThickenings.IsStrict of Stacks 08M9 — a further hypothesis that Situation 91.9.1 does not make. The source also identifies the equivalent topoi of the two thickenings, which this development does not do. (That reading of the source's equality is a remark, not a formalized equivalence; nothing below depends on it.)

Nothing of the tag is lost by proving the epimorphism instead. The source uses the equality only to turn the induced map (f')^*J ⟶ I into a map f^*J ⟶ I, and an epimorphism does exactly that: it admits at most one such map, and Deformation.ToposThickening.MorphismOfThickenings.firstOrderIdealMap exhibits one, so the source's map is obtained and is unique.

noncomputable def firstOrderSurjection :
    (pullbackModules D.f'.toModulesHom).obj D.idealJ.I ⟶ D.reducedPullbackIdeal

Deformation.ToposThickening.MorphismOfThickenings.firstOrderSurjection_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsFirstOrder.lean, line 330. The attribute's comment: “surjectivity of the first order reduction; the two upper topoi share their section universe, as the closed immersion carried by AlgebraicGeometry.ClosedRingedImmersion requires, the two lower ones staying independent”.

Stacks 08M7. When both thickenings are first order the canonical reduction map (f')^*J ⟶ f^*J is surjective: the unit of i^* ⊣ i_* is an epimorphism at every module, and the second factor is the direct image of an isomorphism.

First-orderness of t is not consumed: it is what makes t^*J the ideal J read on Sh(B), and that identification is built into reducedPullbackIdeal.

theorem firstOrderSurjection_epi (hi : IsFirstOrderThickening D.i)
    (_ht : IsFirstOrderThickening D.t) : Epi D.firstOrderSurjection

Deformation.ToposThickening.MorphismOfThickenings.firstOrderIdealMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsFirstOrder.lean, line 348. The attribute's comment: “the first order factorization of the induced map of defining ideals; the two upper topoi share their section universe, as the closed immersion carried by AlgebraicGeometry.ClosedRingedImmersion requires, the two lower ones staying independent”.

Stacks 08M7. When both thickenings are first order the induced map of defining ideals (f')^*J ⟶ I factors uniquely through the canonical reduction (f')^*J ⟶ f^*J, giving the source's map f^*J ⟶ I.

The factorization exists because the unit of i^* ⊣ i_* at I is an isomorphism, I being annihilated by itself; it is unique because the reduction is an epimorphism.

noncomputable def firstOrderIdealMap (hi : IsFirstOrderThickening D.i)
    (ht : IsFirstOrderThickening D.t) :
    { g : D.reducedPullbackIdeal ⟶ D.idealI.I //
      D.firstOrderSurjection ≫ g = D.idealMap ∧
        ∀ g' : D.reducedPullbackIdeal ⟶ D.idealI.I,
          D.firstOrderSurjection ≫ g' = D.idealMap → g' = g }

Deformation.ToposThickening.MorphismOfThickenings.canonicalIdealMap_existsUnique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsIdealMap.lean, line 248. The attribute's comment: “the canonical map of defining ideals”.

Stacks 08M7. There is exactly one map of O'-modules (f')^*J ⟶ I whose composite into O' is the structure map of f' applied to the inclusion of J.

Existence is the factorisation of Stacks.SheafOfModules.existsUnique_factorThrough: every local section of (f')^*J, read in O', is killed by i^♯, hence lies in I. Uniqueness is the sectionwise injectivity of I ⟶ O'.

theorem canonicalIdealMap_existsUnique :
    ∃! φ : (D.f'.toModulesHom.pullbackModules).obj D.idealJ.I ⟶ D.idealI.I,
      D.IsCanonicalIdealMap φ

Deformation.ToposThickening.MorphismOfThickenings.idealMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsIdealMap.lean, line 258. The attribute's comment: “the induced map of defining ideals”.

Stacks 08M7. The induced map of defining ideals (f')^*J ⟶ I of a morphism of thickenings of ringed topoi.

noncomputable def idealMap : (D.f'.toModulesHom.pullbackModules).obj D.idealJ.I ⟶ D.idealI.I

Deformation.ToposThickening.MorphismOfThickenings.idealMap_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsIdealMap.lean, line 264. The attribute's comment: “the induced map of defining ideals is the normalised one”.

Stacks 08M7. The induced map of defining ideals has the normalisation that characterises it.

theorem idealMap_spec : D.IsCanonicalIdealMap D.idealMap

Deformation.ToposThickening.MorphismOfThickenings.homEquiv_idealMap_comp_incl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsIdealMap.lean, line 276. The attribute's comment: “the induced map of defining ideals is the structure map of f' on J”.

Stacks 08M7. The induced map of defining ideals, read on the target topos: its adjoint transpose, composed with the inclusion of I into O', is the structure map of f' applied to the inclusion of J into O_{B'}. This is the source's own description of the map.

theorem homEquiv_idealMap_comp_incl :
    (pullbackAdjPushforwardModules D.f').homEquiv D.idealJ.I
        (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf (J := X'.J)) X'.O))
        (D.idealMap ≫ D.idealI.incl) =
      D.idealJ.incl ≫ unitStructureMap D.f'

Deformation.ToposThickening.MorphismOfThickenings.pullbackComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsIdealMap.lean, line 329. The attribute's comment: “the canonical comparison of the two iterated pullbacks around the square”.

Stacks 08M7. The canonical comparison of the two iterated pullbacks around the square: pulling back along f' and then i is pulling back along t and then f.

Each side is a composite of left adjoints, so it is the mate of the corresponding comparison of iterated direct images, which is AlgebraicGeometry.RingedToposHom.pushforwardModulesCompIso; the two are then joined by the commutativity of the square, the pullback functor depending on the morphism of ringed topoi only through its value.

noncomputable def pullbackComparison :
    D.f'.toModulesHom.pullbackModules ⋙ D.i.toModulesHom.pullbackModules ≅
      D.t.toModulesHom.pullbackModules ⋙ D.f.toModulesHom.pullbackModules

Tag 08M9, a definition

Tag 08M9 in the Stacks Project.

Deformation.ToposThickening.MorphismOfThickenings.IsStrict, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/MorphismOfThickeningsIdealMap.lean, line 296. The attribute's comment: “strict morphism of thickenings”.

Stacks 08M9. A morphism of thickenings of ringed topoi is strict when its induced map of defining ideals (f')^*J ⟶ I is surjective, i.e. an epimorphism of sheaves of O'-modules.

def IsStrict : Prop

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

91.2 Deformations of rings and… to 91.9 Thickenings of ringed topoi

Section91.2 Deformations of rings and the naive cotangent complex#

Tag 08S4, an equation

Tag 08S5, a lemma

Tag 08S7, a lemma

Tag 0GPT, a lemma

Tag 0GPU, a remark

Tag 0GPV, a lemma

Tag 0GPW, a remark

Tag 0GPX, a lemma

Tag 0GPY, a remark

Tag 08S6, a lemma

Sources

Section91.3 Thickenings of ringed spaces#

Tag 08KZ, a situation

Tag 08L1, a definition

Tag 08L2, a lemma

Sources

Section91.4 Modules on first order thickenings of ringed spaces#

Tag 08L4, an equation

Tag 08L5, a lemma

Tag 08L6, a lemma

Tag 08L7, a lemma

Tag 08L8, a lemma

Tag 08L9, a remark

Tag 08LA, an equation

Tag 08LB, a remark

Tag 08LC, a remark

Tag 08LD, a remark

Tag 08LE, a remark

Tag 08LF, a remark

Sources

Section91.5 Infinitesimal deformations of modules on ringed spaces#

Tag 08LH, a lemma

Tag 08LI, a lemma

Tag 08LJ, a lemma

Tag 08LK, a lemma

Tag 08LL, a lemma

Tag 08LM, a lemma

Tag 08LN, a lemma

Sources

Section91.6 Application to flat modules on flat thickenings of ringed spaces#

Tag 08VR, a lemma

Tag 08VS, a situation

Tag 08VT, a lemma

Sources

Section91.7 Deformations of ringed spaces and the naive cotangent complex#

Tag 08U7, an equation

Tag 08U8, a lemma

Tag 08U9, an equation

Tag 08UA, an equation

Tag 08UB, a lemma

Tag 08UC, a lemma

Tag 0GPZ, a lemma

Tag 0GQ0, a remark

Tag 0GQ1, a lemma

Tag 0GQ2, a remark

Tag 0GQ3, a lemma

Tag 0GQ4, a remark

Sources

Section91.8 Deformations of schemes#

Tag 0D14, a lemma

Sources

Section91.9 Thickenings of ringed topoi#

Tag 08M7, a situation

Tag 08M9, a definition

Sources

Section91.2 Deformations of rings and the naive cotangent complex #

Section91.3 Thickenings of ringed spaces #

Section91.4 Modules on first order thickenings of ringed spaces #

Section91.5 Infinitesimal deformations of modules on ringed spaces #

Section91.6 Application to flat modules on flat thickenings of ringed spaces #

Section91.7 Deformations of ringed spaces and the naive cotangent complex #

Section91.8 Deformations of schemes #

Section91.9 Thickenings of ringed topoi #