92.18 The cotangent complex to 92.28 Fibre products of…

Section92.18 The cotangent complex #

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

Tag 08SR, a definition

Tag 08SR in the Stacks Project.

CategoryTheory.Sheaf.standardResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Morphisms/StandardResolution.lean, line 193.

Stacks 08SR. The standard resolution of a morphism A ⟶ B of sheaves of commutative rings is the augmentation obtained by evaluating the free-forgetful standard resolution at the A-algebra B.

noncomputable def standardResolution {A B : Sheaf J CommRingCat.{max u v w}} (f : A ⟶ B) :
    SimplicialObject.Augmented (Under A)

Tag 08SS, a definition

Tag 08SS in the Stacks Project.

CategoryTheory.Sheaf.cotangentSimplicialModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/CotangentComplex.lean, line 329. The attribute's comment: “the simplicial module”.

Stacks 08SS. The canonical simplicial sheaf of B-modules Ω_{P_•/A} ⊗_{P_•} B of the standard resolution.

noncomputable def cotangentSimplicialModule : CotangentSimplicialModuleData J f

CategoryTheory.Sheaf.cotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/CotangentComplex.lean, line 334. The attribute's comment: “the associated complex”.

Stacks 08SS. The cotangent complex of a morphism of sheaves of commutative rings.

noncomputable def cotangentComplex : CochainComplex (targetModules J B) ℤ

CategoryTheory.Sheaf.cotangentComplexDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/CotangentComplex.lean, line 340. The attribute's comment: “the derived object”.

Stacks 08SS. The cotangent complex regarded as an object of the derived category.

noncomputable abbrev cotangentComplexDerived [HasDerivedCategory.{t} (targetModules J B)] :
    DerivedCategory (targetModules J B)

CategoryTheory.Sheaf.cotangentComplex_isZero_pos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/CotangentComplex.lean, line 356. The attribute's comment: “the positive-degree terms”.

Stacks 08SS. The cotangent complex is zero in positive cohomological degrees.

theorem cotangentComplex_isZero_pos (m : ℤ) (hm : 0 < m) :
    IsZero ((cotangentComplex J f).X m)

CategoryTheory.Sheaf.cotangentComplex_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/CotangentComplex.lean, line 366. The attribute's comment: “the differential”.

Stacks 08SS. The differential is the alternating sum of the face maps, transported through the canonical degree isomorphisms.

theorem cotangentComplex_d (n : ℕ) :
    (cotangentComplex J f).d (-((n + 1 : ℕ) : ℤ)) (-(n : ℤ)) =
      (cotangentComplex_degreeIso J f (n + 1)).hom ≫
        AlgebraicTopology.AlternatingFaceMapComplex.objD
          (cotangentSimplicialModule J f).object n ≫
      (cotangentComplex_degreeIso J f n).inv

Tag 08SV, a lemma

Tag 08SV in the Stacks Project.

CategoryTheory.Sheaf.inverseImageCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/InverseImageCotangentComplex.lean, line 743. The attribute's comment: “for an arbitrary morphism of topoi, with the object, arrow and section universes of the two sites independent”.

Stacks 08SV. The inverse image of the cotangent complex of a homomorphism of sheaves of commutative rings along a morphism of topoi is the cotangent complex of its inverse image: f⁻¹L_{B/A} = L_{f⁻¹B/f⁻¹A}.

noncomputable def inverseImageCotangentComplexIso :
    ((inverseImageTargetModules.{u, v, w, u', v', w'} J K f).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj (cotangentComplex.{u', v', w'} K a) ≅
      cotangentComplex.{u, v, w} J (f.inverseImageRing.map a)

Tag 08SW, a lemma

Tag 08SW in the Stacks Project.

CategoryTheory.Sheaf.sectionwiseCotangentCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/SectionwiseCotangentComplex.lean, line 274. The attribute's comment: “the presheaf U ↦ H^i(L_{B(U)/A(U)}); not its sheafification”.

The sectionwise cotangent cohomology presheaf U ↦ H^i(L_{B(U)/A(U)}): the cotangent cohomology groups of the ring maps on sections, with the maps induced by the restriction squares as restriction maps.

noncomputable def sectionwiseCotangentCohomology (i : ℤ) : Cᵒᵖ ⥤ AddCommGrpCat.{max u v w}

CategoryTheory.Sheaf.cohomologySheafification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/SectionwiseCotangentComplexIso.lean, line 380. The attribute's comment: “the whole lemma: the sheaf associated to the presheaf U ↦ H^i(L_{B(U)/A(U)}) is H^i(L_{B/A}), by the canonical identification — sectionwiseComplexIso, which sectionwiseComplexIso_hom_unit shows is induced by the comparison maps L_{B(U)/A(U)} ⟶ L_{B/A}(U) of Remark 08SX. CARRIES NOTHING beyond the ambient variables: arbitrary site, arbitrary Grothendieck topology, arbitrary homomorphism of sheaves of commutative rings, every i, with the section universe a free parameter. The module-level form, before the structure over B is forgotten, is cohomologySheafIso”.

For a homomorphism A ⟶ B of sheaves of commutative rings on a site, the cohomology sheaf H^i(L_{B/A}) of the cotangent complex is the sheaf associated to the presheaf U ↦ H^i(L_{B(U)/A(U)}) formed from the cotangent complexes of the ring maps on sections.

The presheaf is CategoryTheory.Sheaf.sectionwiseCotangentCohomology, whose sections over U are H^i(L_{B(U)/A(U)}) by CategoryTheory.Sheaf.sectionwiseCotangentCohomology_obj and whose restriction maps are those of the restriction squares; the sheafification is taken in abelian sheaves, and CategoryTheory.Sheaf.cohomologySheafIso is the same identification before the module structure over B is forgotten. The identification is the canonical one: it comes from CategoryTheory.Sheaf.sectionwiseComplexIso, which by CategoryTheory.Sheaf.sectionwiseComplexIso_hom_unit is induced by the canonical comparison maps L_{B(U)/A(U)} ⟶ L_{B/A}(U) of Remark 08SX.

noncomputable def cohomologySheafification (i : ℤ) :
    (presheafToSheaf J AddCommGrpCat.{max u v w}).obj (sectionwiseCotangentCohomology J f i) ≅
      (SheafOfModules.toSheaf (Stacks.SheafOfModules.Tensor.ringSheaf.{u, v, max u v w} B)).obj
        ((cotangentComplex J f).homology i)

Tag 08SX, a remark

Tag 08SX in the Stacks Project.

CategoryTheory.Sheaf.sectionsCotangentComplexComparison_restriction_degree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/SectionsComparisonNaturality.lean, line 405. The attribute's comment: “CLAUSE (2), the compatibility with the restriction maps of the site, in every cohomological degree. Remark 08SX makes three assertions: that for every U there is a canonical map L_{B(U)/A(U)} ⟶ L_{B/A}(U), that these maps are compatible with the restriction maps, and that L_{B/A} is the sheafification of U ↦ L_{B(U)/A(U)}. The first is sectionsCotangentComplexComparison, whose attribute records that only that clause is claimed and that this one needs naturality in U of sectionsComonadLax, hence of resolutionSectionsComparison — which is what is proved here, as resolutionSectionsComparison_restriction_square, and propagated to the complex. CARRIES NOTHING beyond the ambient variables of the comparison itself: arbitrary site, arbitrary Grothendieck topology, arbitrary morphism of sheaves of commutative rings, arbitrary g. No sheaf-condition, smallness or site hypothesis is added, because the proof is a variables-to-variables induction over the standard resolution tower. The SHEAFIFICATION clause (3) is not claimed here; it is sectionwiseComplexIso of StacksFrontier/Cotangent/SheavesOfRings/SectionwiseCotangentComplexIso.lean”.

In each cohomological degree j, the canonical maps L_{B(U)/A(U)} ⟶ L_{B/A}(U) commute with the restriction maps along g : U ⟶ V.

theorem sectionsCotangentComplexComparison_restriction_degree {U V : Cᵒᵖ} (g : U ⟶ V) (j : ℤ) :
    (sectionsCotangentComplexComparison J f U).f j ≫
        ((cotangentComplex J f).X j).val.map g =
      (CommAlgCat.squareCotangentComplexMap.{max u v w, max u v w, max u v w}
          (sectionsRestrictionSquare J f g)).f j ≫
        (ModuleCat.restrictScalars (sectionsRestrictionSquare J f g).map).map
          ((sectionsCotangentComplexComparison J f V).f j)

CategoryTheory.Sheaf.sectionsCotangentComplexComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/SectionsCotangentComparison.lean, line 899. The attribute's comment: “the canonical map L_{B(U)/A(U)} ⟶ L_{B/A}(U); not the sheafification clause”.

The canonical map L_{B(U)/A(U)} ⟶ L_{B/A}(U) of complexes of B(U)-modules: the comparison of standard resolutions, base-changed on differentials, pushed through the alternating-face-map complex and through the reindexing which places simplicial degree n in cohomological degree -n.

noncomputable def sectionsCotangentComplexComparison (U : Cᵒᵖ) :
    CommAlgCat.cotangentComplex.{max u v w, max u v w} (A.obj.obj U)
        (sectionsAlgebra J f U) ⟶
      ((moduleSections J f U).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (cotangentComplex J f)

CategoryTheory.Sheaf.isIso_sheafify_sectionwiseCotangentTermComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/SectionwiseSheafification.lean, line 858. The attribute's comment: “the third assertion, in each degree and in sheaves of B-modules: the degree-j term of L_{B/A} is the sheafification of the presheaf of B-modules U ↦ L^j_{B(U)/A(U)} along the canonical maps of the first assertion”.

In every degree j, the term of the cotangent complex L_{B/A} of a homomorphism of sheaves of rings is the sheafification of the presheaf of B-modules U ↦ L^j_{B(U)/A(U)} of the terms of the cotangent complexes of the ring maps on sections, along the canonical maps L_{B(U)/A(U)} ⟶ L_{B/A}(U): the adjunct of the canonical map out of the sheafification is an isomorphism.

theorem isIso_sheafify_sectionwiseCotangentTermComparison (j : ℤ) :
    IsIso ((PresheafOfModules.sheafificationHomEquiv.{max u v w}
      (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf.{u, v, max u v w} B).obj)).symm
        (sectionwiseCotangentTermComparison J f j))

CategoryTheory.Sheaf.sheafifiedSectionwiseCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/SectionwiseSheafification.lean, line 1005. The attribute's comment: “the third assertion: L_{B/A} is the sheafification of U ↦ L_{B(U)/A(U)}, the sheafification of the presheaf of complexes of abelian groups U ↦ L_{B(U)/A(U)} being isomorphic to L_{B/A} along the canonical maps of the first assertion; degreewise, in sheaves of B-modules, this is isIso_sheafify_sectionwiseCotangentTermComparison”.

The cotangent complex L_{B/A} of a homomorphism of sheaves of rings is the sheafification of the rule U ↦ L_{B(U)/A(U)}: the sheafification of the presheaf of complexes of abelian groups U ↦ L_{B(U)/A(U)} is isomorphic to L_{B/A}, by the canonical maps followed by the counit of sheafification.

noncomputable def sheafifiedSectionwiseCotangentComplexIso :
    ((presheafToSheaf J AddCommGrpCat.{max u v w}).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (sectionwiseCotangentPresheafComplex J f) ≅ cotangentComplexAb J f

Tag 08UR, a lemma

Tag 08UR in the Stacks Project.

CategoryTheory.Sheaf.cotangentComplex_homologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/HomologyZero.lean, line 579.

The zeroth homology of the cotangent complex of a morphism of sheaves of commutative rings on a site is its sheaf of relative differentials, the sheaf of modules corepresenting the relative derivations.

noncomputable def cotangentComplex_homologyZeroIso :
    (cotangentComplex J f).homology 0 ≅
      (AlgebraicGeometry.SheafOfModules.derivationsFunctor.{max u v w} A B f).coreprX

Tag 08SY, a lemma

Tag 08SY in the Stacks Project.

CategoryTheory.Sheaf.prodCotangentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/ProductRings.lean, line 192. The attribute's comment: “the comparison map”.

The canonical comparison map L_{B ⨯ B'/A} ⟶ L_{B/A} ⊕ L_{B'/A} of complexes of sheaves of B ⨯ B'-modules: the pairing of the two maps of cotangent complexes induced by the two projection squares, each summand read over B ⨯ B' by restriction of scalars along the corresponding projection.

noncomputable def prodCotangentComparison :
    cotangentComplex.{u, v, w} J (prodRingHom J f f') ⟶ prodCotangentSum J f f'

CategoryTheory.Sheaf.prodCotangentComparisonDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/ProductRings.lean, line 257. The attribute's comment: “the comparison map in the derived category”.

The comparison map L_{B ⨯ B'/A} ⟶ L_{B/A} ⊕ L_{B'/A} read in the derived category D(B ⨯ B').

noncomputable abbrev prodCotangentComparisonDerived
    [HasDerivedCategory.{t} (targetModules.{u, v, w} J (B ⨯ B'))] :
    cotangentComplexDerived.{u, v, w, t} J (prodRingHom J f f') ⟶
      DerivedCategory.Q.obj (prodCotangentSum J f f')

CategoryTheory.Sheaf.isIso_prodCotangentComparisonDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/ProductRingsSectionwise.lean, line 555. The attribute's comment: “the lemma: the canonical map L_{B×B'/A} → L_{B/A} ⊕ L_{B'/A}, the pairing of the maps induced by the two projections, is an isomorphism in D(B×B'), for an arbitrary site and arbitrary homomorphisms A → B, A → B' of sheaves of rings”.

Let C be a site and let A ⟶ B, A ⟶ B' be homomorphisms of sheaves of commutative rings on C. Then the canonical map L_{B ⨯ B'/A} ⟶ L_{B/A} ⊕ L_{B'/A} (CategoryTheory.Sheaf.prodCotangentComparisonDerived, the pairing of the maps of cotangent complexes induced by the two projections) is an isomorphism in D(B ⨯ B').

theorem isIso_prodCotangentComparisonDerived
    [HasDerivedCategory.{t} (targetModules.{u, v, w} J (B ⨯ B'))] :
    IsIso (prodCotangentComparisonDerived.{u, v, w, t} J f f')

Tag 08SZ, a lemma

Tag 08SZ in the Stacks Project.

CategoryTheory.Sheaf.baseChangedCotangentComplexDerivedIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/BaseChangedCotangentDerived.lean, line 184. The attribute's comment: “the first vertex: L_{B/A} ⊗^L_B D, the derived pullback along h : B ⟶ D of the cotangent complex, is the class of its degreewise base change, the first vertex of the triangle of CategoryTheory.Sheaf.exists_distTriang_towerCotangent; on any site”.

The first vertex of the triangle of Tag 08SZ is L_{B/A} ⊗^L_B D. The complex L_{B/A} ⊗_B D, the degreewise base change of the cotangent complex of A ⟶ B, represents the derived base change of L_{B/A} along h : B ⟶ D: the cotangent complex is K-flat with flat terms, so its derived pullback is computed degreewise (Tag 06YY), and degreewise pullback along the change of coefficient rings is extension of scalars.

def baseChangedCotangentComplexDerivedIso :
    (towerDerivedBaseChange.{u, v, w} J h).obj
        (DerivedCategory.Q.obj (cotangentComplex.{u, v, w} J g)) ≅
      DerivedCategory.Q.obj (baseChangedCotangentComplex.{u, v, w} J g h)

CategoryTheory.Sheaf.towerCotangentBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/FundamentalTriangle.lean, line 284. The attribute's comment: “the first displayed arrow L_{B/A} ⊗_B C ⟶ L_{C/A}, with the DEGREEWISE tensor product in place of the derived one — the two agree only once the terms of L_{B/A} are known to be locally free, which is not proved here and for which no derived extension of scalars for sheaves of modules on a site exists in this library. Distinguishedness of the triangle is not claimed by this declaration”.

Stacks Project, Tag 08SZ, the first displayed arrow. The canonical map L_{B/A} ⊗_B D ⟶ L_{D/A} of complexes of sheaves of D-modules: the transpose, along the extension–restriction adjunction for sheaves of modules, of the B-linear map of cotangent complexes attached to the square (𝟙 A, h) of the tower.

The tensor product in the source is the degreewise one, not the derived one; see the module documentation.

noncomputable def towerCotangentBaseChange :
    baseChangedCotangentComplex.{u, v, w} J g h ⟶ cotangentComplex.{u, v, w} J (g ≫ h)

CategoryTheory.Sheaf.towerCotangentChangeOfBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/FundamentalTriangle.lean, line 310. The attribute's comment: “the second displayed arrow L_{C/A} ⟶ L_{C/B}, unconditionally and with no identification intervening. Distinguishedness of the triangle is not claimed by this declaration”.

Stacks Project, Tag 08SZ, the second displayed arrow. The canonical change-of-base-ring map L_{D/A} ⟶ L_{D/B} of complexes of sheaves of D-modules: the map of cotangent complexes attached to the square (g, 𝟙 D) of the tower. Restriction of scalars along the identity of D is the identity functor, so no identification intervenes between the stated target and L_{D/B}.

noncomputable def towerCotangentChangeOfBase :
    cotangentComplex.{u, v, w} J (g ≫ h) ⟶ cotangentComplex.{u, v, w} J h

CategoryTheory.Sheaf.exists_distTriang_cotangentComplexDerived_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/FundamentalTriangle.lean, line 368. The attribute's comment: “the distinguished triangle, under ONE carried hypothesis the source lacks: the short exact sequence S, hS realizing the two canonical arrows (hf, hg) on the three vertices (e₁, e₂, e₃) — the sheaf-level analogue of Tag 08SD, absent from this library, as are Tag 08SE and the ISOMORPHISM of Tag 08SY. The first vertex carries the DEGREEWISE tensor product in place of the derived one”.

Stacks Project, Tag 08SZ, under one carried hypothesis. Let A ⟶ B ⟶ D be homomorphisms of sheaves of commutative rings on a site. Then there is a distinguished triangle

L_{B/A} ⊗_B D ⟶ L_{D/A} ⟶ L_{D/B} ⟶ (L_{B/A} ⊗_B D)[1]

in D(D) whose first two arrows are the two canonical maps CategoryTheory.Sheaf.towerCotangentBaseChange and CategoryTheory.Sheaf.towerCotangentChangeOfBase constructed above.

The hypothesis carried is the sheaf-level differential short exact sequence of the source's proof (Tag 08SD): a short complex S of cochain complexes of sheaves of D-modules that is short exact (hS), whose three terms are the three vertices (e₁, e₂, e₃) and whose two maps are the two canonical arrows (hf, hg). The source identifies the third term using Tag 08SE and reduces to the case of an injective B ⟶ D using the isomorphism of Tag 08SY.

The first vertex carries the degreewise, not the derived, tensor product; see the module documentation.

theorem exists_distTriang_cotangentComplexDerived_of_shortExact
    [HasDerivedCategory.{t} (targetModules.{u, v, w} J D)]
    (S : ShortComplex (CochainComplex (targetModules.{u, v, w} J D) ℤ)) (hS : S.ShortExact)
    (e₁ : S.X₁ ≅ baseChangedCotangentComplex.{u, v, w} J g h)
    (e₂ : S.X₂ ≅ cotangentComplex.{u, v, w} J (g ≫ h))
    (e₃ : S.X₃ ≅ cotangentComplex.{u, v, w} J h)
    (hf : S.f = e₁.hom ≫ towerCotangentBaseChange.{u, v, w} J g h ≫ e₂.inv)
    (hg : S.g = e₂.hom ≫ towerCotangentChangeOfBase.{u, v, w} J g h ≫ e₃.inv) :
    ∃ δ : cotangentComplexDerived.{u, v, w, t} J h ⟶
        (DerivedCategory.Q.obj (baseChangedCotangentComplex.{u, v, w} J g h))⟦(1 : ℤ)⟧,
      Triangle.mk (DerivedCategory.Q.map (towerCotangentBaseChange.{u, v, w} J g h))
          (DerivedCategory.Q.map (towerCotangentChangeOfBase.{u, v, w} J g h)) δ ∈
        distTriang (DerivedCategory (targetModules.{u, v, w} J D))

CategoryTheory.Sheaf.exists_distTriang_towerCotangent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/FundamentalTriangleGeneral.lean, line 565. The attribute's comment: “the distinguished triangle L_{B/A} ⊗^L_B D → L_{D/A} → L_{D/B} → (L_{B/A} ⊗^L_B D)[1] with the canonical first two arrows, in D(D), on any site; the first vertex is identified with L_{B/A} ⊗^L_B D by CategoryTheory.Sheaf.baseChangedCotangentComplexDerivedIso”.

Stacks 08SZ, the fundamental triangle. Let A ⟶ B ⟶ D be homomorphisms of sheaves of commutative rings on a site. The triangle

L_{B/A} ⊗_B D ⟶ L_{D/A} ⟶ L_{D/B} ⟶ (L_{B/A} ⊗_B D)[1]

with first two arrows CategoryTheory.Sheaf.towerCotangentBaseChange and CategoryTheory.Sheaf.towerCotangentChangeOfBase is distinguished in D(D); its first vertex is L_{B/A} ⊗^L_B D by CategoryTheory.Sheaf.baseChangedCotangentComplexDerivedIso.

This is the argument of the source: the homomorphism B ⟶ B × D, b ↦ (b, h b), is injective on sections, so the triangle of A ⟶ B ⟶ B × D is distinguished (CategoryTheory.Sheaf.exists_distTriang_towerCotangent_of_injective), and the exact second summand functor Mod(B × D) ⥤ Mod(D) carries it to the triangle of A ⟶ B ⟶ D.

theorem exists_distTriang_towerCotangent
    [HasDerivedCategory.{t} (targetModules.{u, v, w} J D)] :
    ∃ δ : cotangentComplexDerived.{u, v, w, t} J h ⟶
        (DerivedCategory.Q.obj (baseChangedCotangentComplex.{u, v, w} J g h))⟦(1 : ℤ)⟧,
      Triangle.mk (DerivedCategory.Q.map (towerCotangentBaseChange.{u, v, w} J g h))
          (DerivedCategory.Q.map (towerCotangentChangeOfBase.{u, v, w} J g h)) δ ∈
        distTriang (DerivedCategory (targetModules.{u, v, w} J D))

Tag 08T0, a lemma

Tag 08T0 in the Stacks Project.

CategoryTheory.Sheaf.stalkCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/StalkCotangentComplex.lean, line 152. The attribute's comment: “for a point whose universe of sets is the universe of the sections of the two sheaves of rings, as in 08SV, and with the point read as a morphism of topoi out of the sheaves for the trivial topology on the one-point site, taken in the universes of the objects and the morphisms of the site. Both sides are cotangent complexes of a homomorphism of sheaves of commutative rings, the right-hand one on the one-point site rather than of the homomorphism of stalk rings itself: the identification of sheaves of modules on the one-point site with modules over the stalk ring is not used. The identification of that topos with sets is pointToposEquiv, of the inverse image along it with the stalk functor is pointToposMorphismInverseImageIso, of the inverse image of the sheaves of rings with the stalk rings is pointInverseImageRingIso, and of the terms of the left-hand side with the stalks of the terms of the cotangent complex is pointStalkModuleSheafIso”.

The stalk of the cotangent complex of a homomorphism of sheaves of commutative rings on a site at a point of the site is the cotangent complex of the induced homomorphism of stalks: (L_{B/A})_p = L_{B_p/A_p}.

noncomputable def stalkCotangentComplexIso :
    ((inverseImageTargetModules.{u, v, w, u, v, w}
            (⊥ : GrothendieckTopology (PointSite.{v, u})) J
            (pointToposMorphism.{u, v, w} J p)).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj (cotangentComplex.{u, v, w} J a) ≅
      cotangentComplex.{u, v, w} (⊥ : GrothendieckTopology (PointSite.{v, u}))
        ((pointToposMorphism.{u, v, w} J p).inverseImageRing.map a)

Tag 08US, a lemma

Tag 08US in the Stacks Project.

CategoryTheory.Sheaf.naiveComparisonNegOne_conormalClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonArrow.lean, line 526. The attribute's comment: “the degree -1 component of the canonical map L_{B/A} → NL_{B/A}, with its value [d₀ x - d₁ x] on a pure differential. Hypotheses beyond the source: the naive cotangent complex is realized as the conormal sequence of the presentation P₀ ⟶ B by the degree-zero term of the standard resolution, and the identification of that presentation with Stacks.Sites.FreeAlgebra.canonicalPresentation is not carried. The identification of the naive complex with the truncation τ_{≥ -1} L_{B/A} is NOT proved: the source proves it by comparison with the chaotic topology, and that comparison is not carried. Tag 08TZ, which it uses, IS formalized, as Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso”.

Stacks 08US, the degree -1 component of the canonical map. On the pure differential d x of a local section x of P₁, the comparison is the class of d₀ x - d₁ x in I/I²; the general local section d x ⊗ b goes to b times that class.

theorem naiveComparisonNegOne_conormalClass (U : Cᵒᵖ)
    (x : (resolutionTerm J f (op ⦋1⦌)).obj.obj U) :
    (naiveComparisonNegOne J f).val.app U
        (((cotangentSimplicialModule J f).universalDerivation (op ⦋1⦌)).d x) =
      conormalClassSection J f U (faceDifference J f U x)

CategoryTheory.Sheaf.naiveComparisonNegOne_comp_conormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonArrow.lean, line 576. The attribute's comment: “the lower commuting square: the degree -1 component composed with the differential of the naive cotangent complex is the difference of the two faces composed with the degree-zero component. Hypotheses beyond the source: the naive cotangent complex is realized as the conormal sequence of the presentation P₀ ⟶ B by the degree-zero term of the standard resolution, and the differential of L_{B/A} appears as the difference of the two face maps of the base-changed simplicial module rather than transported through CategoryTheory.Sheaf.cotangentComplex_degreeIso”.

Stacks 08US, the lower commuting square. Following the degree -1 component by the differential I/I² ⟶ B ⊗_{P₀} Ω_{P₀/A} of the naive cotangent complex is the difference of the two faces Ω_{P₁/A} ⊗ B ⇉ Ω_{P₀/A} ⊗ B followed by the degree-zero component. The difference of the two faces is the differential of the cotangent complex out of degree -1, so this is the lower square of the comparison diagram: the differential of the naive complex sends [d₀ x - d₁ x] to 1 ⊗ d(d₀ x - d₁ x).

theorem naiveComparisonNegOne_comp_conormal :
    naiveComparisonNegOne J f ≫ (naiveSequence J f).f =
      (cotangentSimplicialModule J f).object.δ 0 ≫ naiveComparisonZero J f -
        (cotangentSimplicialModule J f).object.δ 1 ≫ naiveComparisonZero J f

CategoryTheory.Sheaf.naiveComparisonNegOne_faceSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonArrow.lean, line 636. The attribute's comment: “the upper commuting square: the degree -1 component annihilates the alternating sum of the three faces, which is the differential of L_{B/A} into degree -1, the naive cotangent complex being zero in degree -2. Hypotheses beyond the source: the naive cotangent complex is realized as the conormal sequence of the presentation P₀ ⟶ B by the degree-zero term of the standard resolution, and the differential of L_{B/A} appears as the alternating sum of the face maps of the base-changed simplicial module rather than transported through CategoryTheory.Sheaf.cotangentComplex_degreeIso”.

Stacks 08US, the upper commuting square. The degree -1 component annihilates the alternating sum of the three faces Ω_{P₂/A} ⊗ B ⟶ Ω_{P₁/A} ⊗ B, which is the differential of the cotangent complex into degree -1. The naive cotangent complex is zero in degree -2, so this is exactly the commutation of the comparison with that differential.

theorem naiveComparisonNegOne_faceSum :
    ((cotangentSimplicialModule J f).object.δ (0 : Fin 3) -
        (cotangentSimplicialModule J f).object.δ (1 : Fin 3) +
        (cotangentSimplicialModule J f).object.δ (2 : Fin 3)) ≫
      naiveComparisonNegOne J f = 0

CategoryTheory.Sheaf.naiveCotangentComplexIsoCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonCanonical.lean, line 283. The attribute's comment: “the naive cotangent complex of the presentation P₀ = A[B] is the naive cotangent complex NL_{B/A} of Tag 08TW”.

The naive cotangent complex of the presentation P₀ ⟶ B is the naive cotangent complex NL_{B/A} of Tag 08TW, through the isomorphism P₀ ≅ A[B] of A-algebras over B.

noncomputable def naiveCotangentComplexIsoCanonical :
    naiveCotangentComplex.{u, v, w} J f ≅
      Stacks.SheafOfModules.naiveCotangentComplex.{v, u, max u v w, u} J A B f

CategoryTheory.Sheaf.canonicalNaiveComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonCanonical.lean, line 397. The attribute's comment: “the canonical map L_{B/A} → NL_{B/A}, into the naive cotangent complex Stacks.SheafOfModules.naiveCotangentComplex of Tag 08TW”.

Stacks 08US, the canonical map. The canonical map L_{B/A} ⟶ NL_{B/A} from the cotangent complex to the naive cotangent complex of Tag 08TW: d x ⊗ b ↦ b · [d₀ x - d₁ x] in degree -1 and d p ⊗ b ↦ b ⊗ d p in degree 0 (CategoryTheory.Sheaf.naiveComparison), read in NL_{B/A} through the isomorphism P₀ ≅ A[B] of A-algebras over B.

noncomputable def canonicalNaiveComparison :
    cotangentComplex.{u, v, w} J f ⟶
      Stacks.SheafOfModules.naiveCotangentComplex.{v, u, max u v w, u} J A B f

CategoryTheory.Sheaf.canonicalNaiveComparison_isIso_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonCanonical.lean, line 410. The attribute's comment: “the canonical map identifies the naive cotangent complex NL_{B/A} of Tag 08TW with the truncation τ_{≥ -1} L_{B/A}: it is an isomorphism on the cohomology sheaf of every degree ≥ -1, the naive complex having no terms outside degrees -1 and 0”.

Stacks 08US. The canonical map L_{B/A} ⟶ NL_{B/A} into the naive cotangent complex of Tag 08TW is an isomorphism on the cohomology sheaf of every degree ≥ -1. Since NL_{B/A} has no terms outside degrees -1 and 0 (Stacks.SheafOfModules.naiveCotangentComplex_isZero_X), this says that the canonical map identifies the naive cotangent complex with the truncation τ_{≥ -1} L_{B/A}.

theorem canonicalNaiveComparison_isIso_homologyMap (i : ℤ) (hi : -1 ≤ i) :
    IsIso (HomologicalComplex.homologyMap (canonicalNaiveComparison J f) i)

CategoryTheory.Sheaf.naiveComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposNaiveComparison.lean, line 226. The attribute's comment: “the canonical map L_{B/A} → NL_{B/A} as a map of complexes, assembled from the degreewise comparison and its two squares. Hypotheses beyond the source: the naive cotangent complex is realized as the conormal sequence of the presentation P₀ ⟶ B by the degree-zero term of the standard resolution, and the identification of that presentation with Stacks.Sites.FreeAlgebra.canonicalPresentation is not carried”.

The canonical map of complexes L_{B/A} ⟶ NL_{B/A}: it is d x ⊗ b ↦ b · [d₀ x - d₁ x] in degree -1, it is d p ⊗ b ↦ b ⊗ d p in degree 0, and it is zero in every other degree, the naive cotangent complex having no other terms.

noncomputable def naiveComparison :
    cotangentComplex.{u, v, w} J f ⟶ naiveCotangentComplex.{u, v, w} J f

CategoryTheory.Sheaf.naiveComparison_isIso_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposNaiveComparison.lean, line 281. The attribute's comment: “the identification of the naive cotangent complex with the truncation τ_{≥ -1} L_{B/A}, stated as: the canonical map is an isomorphism on the cohomology sheaf of every degree ≥ -1, the naive complex having no cohomology below degree -1 by CategoryTheory.Sheaf.naiveCotangentComplex_isZero_homology. Hypotheses carried: homologyZeroIsIso and homologyNegOneIsIso, the isomorphisms on H⁰ and on H^{-1}, which are the final step of the source's proof — the comparison with the chaotic topology, reducing them to the ring-level map of Tag 08UP and transporting along the inverse-image isomorphism of Tag 08TZ. That tag IS carried as an isomorphism of complexes, Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso; what is not carried is the comparison with the chaotic topology”.

If the canonical map L_{B/A} ⟶ NL_{B/A} is an isomorphism on the cohomology sheaves of degrees 0 and -1 (the hypotheses homologyZeroIsIso and homologyNegOneIsIso), then it is an isomorphism on the cohomology sheaf of every degree ≥ -1. Since the naive cotangent complex has no cohomology below degree -1, this says that the canonical map identifies NL_{B/A} with the truncation τ_{≥ -1} L_{B/A}.

theorem naiveComparison_isIso_homologyMap
    (homologyZeroIsIso :
      IsIso (HomologicalComplex.homologyMap (naiveComparison.{u, v, w} J f) 0))
    (homologyNegOneIsIso :
      IsIso (HomologicalComplex.homologyMap (naiveComparison.{u, v, w} J f) (-1)))
    (i : ℤ) (hi : -1 ≤ i) :
    IsIso (HomologicalComplex.homologyMap (naiveComparison.{u, v, w} J f) i)

Sources

LeanCategoryTheory.Sheaf.standardResolution · CategoryTheory.Sheaf.cotangentSimplicialModule · CategoryTheory.Sheaf.cotangentComplex · CategoryTheory.Sheaf.cotangentComplexDerived · CategoryTheory.Sheaf.cotangentComplex_isZero_pos · CategoryTheory.Sheaf.cotangentComplex_d · CategoryTheory.Sheaf.inverseImageCotangentComplexIso · CategoryTheory.Sheaf.sectionwiseCotangentCohomology

Section92.19 The Atiyah class of a sheaf of modules #

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

Tag 09DG, an equation

Tag 09DG in the Stacks Project.

AlgebraicGeometry.SheafOfModules.exists_shortExact_principalPartsSequence', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsJet.lean, line 1178. The attribute's comment: “the sequence for a term of the standard resolution”. References: SGA 6 II (AppII.1.2.4), “n = 1”.

The sequence of principal parts is a short exact sequence.

theorem exists_shortExact_principalPartsSequence' :
    ∃ h : (principalPartsInclusion.{v, u, w, m} φ).app F ≫
        (principalPartsProjection.{v, u, w, m}
          (underlyingRingSheafMapOfSite φ) 1).app F = 0,
      (ShortComplex.mk ((principalPartsInclusion.{v, u, w, m} φ).app F)
        ((principalPartsProjection.{v, u, w, m}
          (underlyingRingSheafMapOfSite φ) 1).app F) h).ShortExact

CategoryTheory.Sheaf.resolutionPrincipalPartsShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/AtiyahClass.lean, line 134.

Stacks 09DG. The extension of principal parts of a term of the standard resolution is short exact: 0 ⟶ Ω_{P_n/A} ⊗_{P_n} F ⟶ P¹_{P_n/A}(F) ⟶ F ⟶ 0.

theorem resolutionPrincipalPartsShortComplex_shortExact (n : SimplexCategoryᵒᵖ)
    (F : targetModules J B) :
    (resolutionPrincipalPartsShortComplex J f n F).ShortExact

Tag 09DH, an equation

Tag 09DH in the Stacks Project.

CategoryTheory.Sheaf.atiyahTriangle_distinguished_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/AtiyahClass.lean, line 194. The attribute's comment: “the distinguished triangle; M, G, hS, e₁ and e₃ carry the inputs the library does not yet have — the category of simplicial P_•-modules known to be abelian, the functor Lπ_! of Tag 09D3, the simplicial short exact sequence of Tag 09DG, and the identifications of Tags 08PU and 08QE. See the implementation notes”.

Stacks 09DH. The Atiyah triangle of a sheaf of B-modules, written with its first and third terms replaced by objects identified with them: for L identified with Lπ_!(Ω_{P_•/A} ⊗_{P_•} F) and N identified with Lπ_!(F), the sequence L ⟶ Lπ_!(P¹_{P_•/A}(F)) ⟶ N ⟶ L[1] is a distinguished triangle in D(B).

theorem atiyahTriangle_distinguished_of_iso
    (G : DerivedCategory M ⥤ DerivedCategory (targetModules J B))
    [G.CommShift ℤ] [G.IsTriangulated] {S : ShortComplex M} (hS : S.ShortExact)
    (L N : DerivedCategory (targetModules J B))
    (e₁ : (atiyahTriangle J G hS).obj₁ ≅ L) (e₃ : (atiyahTriangle J G hS).obj₃ ≅ N) :
    Triangle.mk (e₁.inv ≫ (atiyahTriangle J G hS).mor₁)
        ((atiyahTriangle J G hS).mor₂ ≫ e₃.hom)
        (e₃.inv ≫ (atiyahTriangle J G hS).mor₃ ≫
          (shiftFunctor (DerivedCategory (targetModules J B)) (1 : ℤ)).map e₁.hom) ∈
      distinguishedTriangles

CategoryTheory.Sheaf.sheafAtiyahTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/AtiyahClassDefinite.lean, line 280.

[Stacks, Tag 09DH], Equation 92.19.0.2. For a homomorphism f : 𝒜 ⟶ ℬ of sheaves of commutative rings on a site and a sheaf of ℬ-modules ℱ,

L_{ℬ/𝒜} ⊗^𝐋_ℬ ℱ ⟶ Lπ_!(P¹_{𝒫/π^{-1}𝒜}(ℱ)) ⟶ ℱ ⟶ (L_{ℬ/𝒜} ⊗^𝐋_ℬ ℱ)[1]

is a distinguished triangle in D(ℬ).

theorem sheafAtiyahTriangle_distinguished (F : SheafOfModules.{u} (targetRing J (B := B))) :
    sheafAtiyahTriangle J f F ∈ distinguishedTriangles

Tag 09DI, a definition

Tag 09DI in the Stacks Project.

CategoryTheory.Sheaf.atiyahClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/AtiyahClass.lean, line 214. The attribute's comment: “the Atiyah class, as the last arrow of the triangle of Tag 09DH; M, G, hS, e₁ and e₃ carry the same five inputs the library does not yet have that atiyahTriangle_distinguished_of_iso carries, so N stands for F and L for L_{B/A} ⊗_B^L F. See the implementation notes”.

Stacks 09DI. The Atiyah class of a sheaf of B-modules: the map F ⟶ L_{B/A} ⊗_B^L F[1], realised as the last arrow N ⟶ L[1] of the Atiyah triangle of Tag 09DH, read through the identifications of its first and third terms.

def atiyahClass (G : DerivedCategory M ⥤ DerivedCategory (targetModules J B))
    [G.CommShift ℤ] [G.IsTriangulated] {S : ShortComplex M} (hS : S.ShortExact)
    (L N : DerivedCategory (targetModules J B))
    (e₁ : (atiyahTriangle J G hS).obj₁ ≅ L) (e₃ : (atiyahTriangle J G hS).obj₃ ≅ N) :
    N ⟶ L⟦(1 : ℤ)⟧

CategoryTheory.Sheaf.sheafAtiyahClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/AtiyahClassDefinite.lean, line 250.

[Stacks, Tag 09DI], Definition 92.19.1: the Atiyah class of a sheaf of modules. For a homomorphism f : 𝒜 ⟶ ℬ of sheaves of commutative rings on a site and a sheaf of ℬ-modules ℱ, the Atiyah class of ℱ is the morphism

ℱ ⟶ (L_{ℬ/𝒜} ⊗^𝐋_ℬ ℱ)[1]

of D(ℬ) which is the last arrow of the triangle (92.19.0.2) of [Stacks, Tag 09DH]: the image under the Lπ_! of Remark 09D3 of the short exact sequence of first principal parts of the standard resolution (Tag 09DG), read through the identifications CategoryTheory.Sheaf.atiyahTriangleFirstTermIso and CategoryTheory.Sheaf.atiyahTriangleThirdTermIso of its outer terms.

def sheafAtiyahClass (F : SheafOfModules.{u} (targetRing J (B := B))) :
    DerivedCategory.Q.obj
        ((HomologicalComplex.single (SheafOfModules.{u} (targetRing J (B := B)))
          (ComplexShape.up ℤ) 0).obj F) ⟶
      (((derivedTensorProductFunctor B).obj
          (DerivedCategory.Q.obj (cotangentComplex.{u, u, u} J f))).obj
        (DerivedCategory.Q.obj
          ((HomologicalComplex.single (Stacks.DerivedTensor.RingedSite.Modules B)
            (ComplexShape.up ℤ) 0).obj F)))⟦(1 : ℤ)⟧

Sources

LeanAlgebraicGeometry.SheafOfModules.exists_shortExact_principalPartsSequence' · CategoryTheory.Sheaf.resolutionPrincipalPartsShortComplex_shortExact · CategoryTheory.Sheaf.atiyahTriangle_distinguished_of_iso · CategoryTheory.Sheaf.sheafAtiyahTriangle_distinguished · CategoryTheory.Sheaf.atiyahClass · CategoryTheory.Sheaf.sheafAtiyahClass

Section92.20 The cotangent complex of a morphism of ringed spaces #

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

Tag 08UU, a definition

Tag 08UU in the Stacks Project.

Stacks.Sheaves.RingedSpaceCotangent.cotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpace.lean, line 90. The attribute's comment: “the complex L_f”.

The cotangent complex L_{X/S} of a morphism of ringed spaces f : X ⟶ S: the cotangent complex of the morphism of sheaves of commutative rings f⁻¹𝒪_S ⟶ 𝒪_X on the site of open subsets of X.

noncomputable def cotangentComplex (f : X ⟶ S) :
    CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ

Stacks.Sheaves.RingedSpaceCotangent.cotangentComplexDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpace.lean, line 103. The attribute's comment: “the object L_f of the derived category of O_X-modules”.

L_{X/S} regarded as an object of the derived category of sheaves of 𝒪_X-modules.

noncomputable abbrev cotangentComplexDerived (f : X ⟶ S)
    [HasDerivedCategory.{t} (SheafOfModules.{u} (structureSheafRing X))] :
    DerivedCategory (SheafOfModules.{u} (structureSheafRing X))

Tag 08UV, a lemma

Tag 08UV in the Stacks Project.

Stacks.Sheaves.RingedSpaceCotangent.cotangentComplex_homologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpace.lean, line 127.

Stacks 08UV. The zeroth cohomology of the cotangent complex of a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (S, 𝒪_S) is its sheaf of relative differentials: H⁰(L_{X/S}) ≅ Ω_{X/S}. Both sheaves of 𝒪_X-modules corepresent the relative derivations of 𝒪_X over f⁻¹𝒪_S, so they are canonically isomorphic.

noncomputable def cotangentComplex_homologyZeroIso (f : X ⟶ S) :
    (cotangentComplex f).homology 0 ≅ moduleOfDifferentials f

Tag 08T4, a lemma

Tag 08T4 in the Stacks Project.

Stacks.Sheaves.RingedSpaceCotangent.baseStructureMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceFundamentalTriangle.lean, line 165. The attribute's comment: “the canonical tower of inverse images, whose fundamental triangle is the triangle of this tag”.

Stacks Project, Tag 08T4, the tower. The structure map of g ∘ f factors through the structure map of f by baseStructureMap, so that (g ∘ f)⁻¹𝒪_Z ⟶ f⁻¹𝒪_Y ⟶ 𝒪_X is a tower of sheaves of commutative rings on X whose composite is the structure map of g ∘ f.

theorem baseStructureMap_comp (f : X ⟶ Y) (g : Y ⟶ Z) :
    baseStructureMap f g ≫ inverseImageStructureMap f = inverseImageStructureMap (f ≫ g)

Stacks.Sheaves.RingedSpaceCotangent.cotangentChangeOfBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceFundamentalTriangle.lean, line 221. The attribute's comment: “the second displayed arrow L_{X/Z} ⟶ L_{X/Y}, unconditionally. Distinguishedness of the triangle is not claimed by this declaration”.

Stacks Project, Tag 08T4, the second displayed arrow L_{X/Z} ⟶ L_{X/Y}: the change-of-base-ring map of Tag 08SZ for the tower (g ∘ f)⁻¹𝒪_Z ⟶ f⁻¹𝒪_Y ⟶ 𝒪_X.

def cotangentChangeOfBase (f : X ⟶ Y) (g : Y ⟶ Z) :
    (cotangentComplex (f ≫ g) : CochainComplex (structureModules X) ℤ) ⟶
      cotangentComplex f

Stacks.Sheaves.RingedSpaceCotangent.exists_distTriang_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceFundamentalTriangle.lean, line 285. The attribute's comment: “the triangle with FIRST VERTEX THE DEGREEWISE base change L_{f⁻¹O_Y/(g∘f)⁻¹O_Z} ⊗_{f⁻¹O_Y} O_X, not Lf^* L_{Y/Z}, and under the ONE carried hypothesis of Tag 08SZ: the short exact sequence S/hS, the sheaf-level analogue of Tag 08SD, absent from this library. See the docstring above”.

Stacks Project, Tag 08T4, under one carried hypothesis. For morphisms of ringed spaces f : X ⟶ Y and g : Y ⟶ Z the triangle

L_{f⁻¹𝒪_Y/(g ∘ f)⁻¹𝒪_Z} ⊗_{f⁻¹𝒪_Y} 𝒪_X ⟶ L_{X/Z} ⟶ L_{X/Y} ⟶ ⋯

on the two canonical arrows cotangentBaseChange and cotangentChangeOfBase is distinguished in D(𝒪_X).

The hypothesis carried is the one carried by Tag 08SZ, in the same shape: a short complex S of complexes of sheaves of 𝒪_X-modules that is short exact (hS), whose three terms are the three vertices (e₁, e₂, e₃) and whose two maps are the two canonical arrows (hf, hg). See the "What is proved and what is not" section of the module documentation.

theorem exists_distTriang_of_shortExact (f : X ⟶ Y) (g : Y ⟶ Z)
    (S : ShortComplex (CochainComplex (structureModules X) ℤ))
    (hS : S.ShortExact) (e₁ : S.X₁ ≅ baseChangedCotangentComplex f g)
    (e₂ : S.X₂ ≅ cotangentComplex (f ≫ g)) (e₃ : S.X₃ ≅ cotangentComplex f)
    (hf : S.f = e₁.hom ≫ cotangentBaseChange f g ≫ e₂.inv)
    (hg : S.g = e₂.hom ≫ cotangentChangeOfBase f g ≫ e₃.inv) :
    ∃ δ : (DerivedCategory.Q (C := structureModules X)).obj (cotangentComplex f) ⟶
        ((DerivedCategory.Q (C := structureModules X)).obj
          (baseChangedCotangentComplex f g))⟦(1 : ℤ)⟧,
      Triangle.mk ((DerivedCategory.Q (C := structureModules X)).map (cotangentBaseChange f g))
          ((DerivedCategory.Q (C := structureModules X)).map (cotangentChangeOfBase f g)) δ ∈
        distTriang (DerivedCategory (structureModules X))

Stacks.Sheaves.RingedSpaceCotangent.exists_distTriang_degreewisePullback_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceFundamentalTriangle.lean, line 325. The attribute's comment: “the triangle with first vertex the DEGREEWISE pullback f^ L_{Y/Z}, not Lf^ L_{Y/Z}; the two agree in D(O_X) exactly when L_{Y/Z} is K-flat, which is NOT proved here. TWO carried hypotheses: e is Tag 08SV for this tower, S/hS is what Tag 08SZ carries. See the docstring above and the module documentation”.

Stacks Project, Tag 08T4, under two carried hypotheses. For morphisms of ringed spaces f : X ⟶ Y and g : Y ⟶ Z the triangle

f^*L_{Y/Z} ⟶ L_{X/Z} ⟶ L_{X/Y} ⟶ f^*L_{Y/Z}[1]

is distinguished in D(𝒪_X), its first arrow being the base-change arrow of Tag 08SZ for the tower read on f^*L_{Y/Z} and its second the canonical map cotangentChangeOfBase.

Two hypotheses are carried. e is Tag 08SV for the tower: the degreewise pullback of L_{Y/Z} is the first vertex L_{f⁻¹𝒪_Y/(g ∘ f)⁻¹𝒪_Z} ⊗_{f⁻¹𝒪_Y} 𝒪_X of the triangle of Tag 08SZ. The short exact sequence S, hS is the hypothesis Tag 08SZ itself carries. The first vertex is the degreewise pullback f^*L_{Y/Z}; it is Lf^*L_{Y/Z} as soon as L_{Y/Z} is K-flat, by isIso_derivedPullbackComparison_cotangentComplex. See the "What is proved and what is not" section of the module documentation.

theorem exists_distTriang_degreewisePullback_of_shortExact (f : X ⟶ Y) (g : Y ⟶ Z)
    (e : degreewisePullbackCotangentComplex f g ≅ baseChangedCotangentComplex f g)
    (S : ShortComplex (CochainComplex (structureModules X) ℤ))
    (hS : S.ShortExact) (e₁ : S.X₁ ≅ baseChangedCotangentComplex f g)
    (e₂ : S.X₂ ≅ cotangentComplex (f ≫ g)) (e₃ : S.X₃ ≅ cotangentComplex f)
    (hf : S.f = e₁.hom ≫ cotangentBaseChange f g ≫ e₂.inv)
    (hg : S.g = e₂.hom ≫ cotangentChangeOfBase f g ≫ e₃.inv) :
    ∃ δ : (DerivedCategory.Q (C := structureModules X)).obj (cotangentComplex f) ⟶
        ((DerivedCategory.Q (C := structureModules X)).obj
          (degreewisePullbackCotangentComplex f g))⟦(1 : ℤ)⟧,
      Triangle.mk ((DerivedCategory.Q (C := structureModules X)).map
            (e.hom ≫ cotangentBaseChange f g))
          ((DerivedCategory.Q (C := structureModules X)).map (cotangentChangeOfBase f g)) δ ∈
        distTriang (DerivedCategory (structureModules X))

Stacks.Sheaves.RingedSpaceCotangent.sheafPullbackCompIso_hom_app_comp_inverseImageStructureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceTransitivityTriangle.lean, line 133. The attribute's comment: “the tower (g ∘ f)⁻¹O_Z = f⁻¹g⁻¹O_Z ⟶ f⁻¹O_Y ⟶ O_X of the proof: the structure map of g ∘ f is the composite of the tower”.

The structure map of g ∘ f is the structure map of g pulled back along f followed by the structure map of f, across (g ∘ f)⁻¹𝒪_Z ≅ f⁻¹g⁻¹𝒪_Z (Tag 008I).

theorem sheafPullbackCompIso_hom_app_comp_inverseImageStructureMap (f : X ⟶ Y) (g : Y ⟶ Z) :
    (sheafPullbackCompIso f.hom.base g.hom.base CommRingCat.{u}).hom.app Z.sheaf ≫
        (TopCat.Sheaf.pullback CommRingCat.{u} f.hom.base).map (inverseImageStructureMap g) ≫
          inverseImageStructureMap f =
      inverseImageStructureMap (f ≫ g)

Stacks.Sheaves.RingedSpaceCotangent.transitivityUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceTransitivityTriangle.lean, line 330. The attribute's comment: “the canonical first arrow Lf^* L_{Y/Z} ⟶ L_{X/Z} of the triangle”.

The first arrow Lf^* L_{Y/Z} ⟶ L_{X/Z} of the transitivity triangle: the first arrow of the triangle of Tag 08V1 for the presented morphisms of ringed topoi, read through derivedPullbackCotangentComplexIso and compCotangentComplexIsoRingedTopos.

def transitivityUnit (f : X ⟶ Y) (g : Y ⟶ Z) :
    (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).obj
        (cotangentComplexDerived g) ⟶ cotangentComplexDerived (f ≫ g)

Stacks.Sheaves.RingedSpaceCotangent.transitivityCounit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceTransitivityTriangle.lean, line 342. The attribute's comment: “the canonical second arrow L_{X/Z} ⟶ L_{X/Y} of the triangle”.

The second arrow L_{X/Z} ⟶ L_{X/Y} of the transitivity triangle: the second arrow of the triangle of Tag 08V1 for the presented morphisms of ringed topoi, read through compCotangentComplexIsoRingedTopos and cotangentComplexIsoRingedTopos.

def transitivityCounit (f : X ⟶ Y) (g : Y ⟶ Z) :
    cotangentComplexDerived (f ≫ g) ⟶ cotangentComplexDerived f

Stacks.Sheaves.RingedSpaceCotangent.exists_distTriang_transitivity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceTransitivityTriangle.lean, line 359.

The transitivity triangle. Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of ringed spaces. The canonical triangle

Lf^* L_{Y/Z} ⟶ L_{X/Z} ⟶ L_{X/Y} ⟶ Lf^* L_{Y/Z}[1]

is distinguished in D(𝒪_X). Here L_{X/S} is the cotangent complex of Definition 08UU, Lf^* is the derived pullback of Tag 06YJ, and the two arrows are transitivityUnit and transitivityCounit, those of the fundamental triangle of the tower (g ∘ f)⁻¹𝒪_Z = f⁻¹g⁻¹𝒪_Z ⟶ f⁻¹𝒪_Y ⟶ 𝒪_X (Tags 08SZ and 08V1).

theorem exists_distTriang_transitivity (f : X ⟶ Y) (g : Y ⟶ Z) :
    ∃ δ : cotangentComplexDerived f ⟶
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).obj
          (cotangentComplexDerived g))⟦(1 : ℤ)⟧,
      Triangle.mk (transitivityUnit f g) (transitivityCounit f g) δ ∈
        distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))

Tag 08UW, a lemma

Tag 08UW in the Stacks Project.

Stacks.Sheaves.RingedSpaceCotangent.canonicalNaiveComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceCanonicalNaiveComparison.lean, line 62. The attribute's comment: “the canonical map L_{X/Y} → NL_{X/Y}, into the naive cotangent complex AlgebraicGeometry.RingedSpace.naiveCotangentComplex of Tag 08TN; the special case of the map of Tag 08US”.

The canonical map L_{X/S} ⟶ NL_{X/S} from the cotangent complex of a morphism of ringed spaces to its naive cotangent complex AlgebraicGeometry.RingedSpace.naiveCotangentComplex: the canonical map CategoryTheory.Sheaf.canonicalNaiveComparison for the morphism of sheaves of rings f⁻¹𝒪_S ⟶ 𝒪_X.

noncomputable def canonicalNaiveComparison (f : X ⟶ S) :
    cotangentComplex f ⟶ RingedSpace.naiveCotangentComplex f

Stacks.Sheaves.RingedSpaceCotangent.canonicalNaiveComparison_isIso_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceCanonicalNaiveComparison.lean, line 75. The attribute's comment: “the canonical map identifies the naive cotangent complex NL_{X/Y} with the truncation τ_{≥ -1} L_{X/Y}: it is an isomorphism on the cohomology sheaf of every degree ≥ -1, the naive complex having no terms outside degrees -1 and 0; the special case of Tag 08US”.

The canonical map L_{X/S} ⟶ NL_{X/S} is an isomorphism on the cohomology sheaf of every degree ≥ -1. Since NL_{X/S} has no terms outside degrees -1 and 0 (AlgebraicGeometry.RingedSpace.naiveCotangentComplex_isZero_X), the canonical map identifies the naive cotangent complex with the truncation τ_{≥ -1} L_{X/S}.

theorem canonicalNaiveComparison_isIso_homologyMap (f : X ⟶ S) (i : ℤ) (hi : -1 ≤ i) :
    IsIso (HomologicalComplex.homologyMap (canonicalNaiveComparison f) i)

Stacks.Sheaves.RingedSpaceCotangent.naiveComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceNaiveComparison.lean, line 116. The attribute's comment: “the canonical map L_{X/Y} → NL_{X/Y} as a morphism of cochain complexes of sheaves of O_X-modules, with both of its components pinned by the lemmas below. Hypotheses beyond the source: NL_{X/Y} is realized as the two-term complex of the conormal sequence of the presentation P₀ ⟶ O_X by the degree-zero term of the standard resolution, whose free algebra is spelled by CategoryTheory.Sheaf.freeAlgebraSheaf; the identification of that model with the one of AlgebraicGeometry.RingedSpace.naiveCotangentComplex is not carried. The second half of the tag, that this map identifies the naive cotangent complex with the truncation tau_{>=-1} L_{X/Y}, is NOT proved and is nowhere assumed”.

The canonical chain map L_{X/S} ⟶ NL_{X/S} of a morphism of ringed spaces: CategoryTheory.Sheaf.naiveComparison at the morphism of sheaves of rings f⁻¹𝒪_S ⟶ 𝒪_X.

noncomputable def naiveComparison (f : X ⟶ S) :
    cotangentComplex f ⟶ naivePresentationComplex f

Stacks.Sheaves.RingedSpaceCotangent.naiveComparison_f_negOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceNaiveComparison.lean, line 127. The attribute's comment: “the degree -1 component of the canonical map is the comparison arrow Omega_{P_1} ⊗ O_X → I/I², so the map is the canonical one. Same hypotheses as Stacks.Sheaves.RingedSpaceCotangent.naiveComparison”.

The degree -1 component of the canonical map is the comparison arrow CategoryTheory.Sheaf.naiveComparisonNegOne for the morphism of sheaves of rings f⁻¹𝒪_S ⟶ 𝒪_X.

theorem naiveComparison_f_negOne (f : X ⟶ S) :
    (naiveComparison f).f (-1) ≫ (naivePresentationComplexXNegOneIso f).hom =
      (CategoryTheory.Sheaf.cotangentComplex_degreeIso (Opens.grothendieckTopology X.carrier)
          (inverseImageStructureMap f) 1).hom ≫
        CategoryTheory.Sheaf.naiveComparisonNegOne (Opens.grothendieckTopology X.carrier)
          (inverseImageStructureMap f)

Stacks.Sheaves.RingedSpaceCotangent.naiveComparison_f_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceNaiveComparison.lean, line 142. The attribute's comment: “the degree 0 component of the canonical map is the comparison arrow Omega_{P_0} ⊗ O_X → O_X ⊗ Omega_{P_0}, so the map is the canonical one. Same hypotheses as Stacks.Sheaves.RingedSpaceCotangent.naiveComparison”.

The degree 0 component of the canonical map is the comparison arrow CategoryTheory.Sheaf.naiveComparisonZero for the morphism of sheaves of rings f⁻¹𝒪_S ⟶ 𝒪_X.

theorem naiveComparison_f_zero (f : X ⟶ S) :
    (naiveComparison f).f 0 ≫ (naivePresentationComplexXZeroIso f).hom =
      (CategoryTheory.Sheaf.cotangentComplex_degreeIso (Opens.grothendieckTopology X.carrier)
          (inverseImageStructureMap f) 0).hom ≫
        CategoryTheory.Sheaf.naiveComparisonZero (Opens.grothendieckTopology X.carrier)
          (inverseImageStructureMap f)

Stacks.Sheaves.RingedSpaceCotangent.naiveComparison_f_negOne_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceNaiveComparison.lean, line 162. The attribute's comment: “the value of the canonical map on local sections in degree -1: the pure differential d x goes to the class of d_0 x - d_1 x in I/I². Same hypotheses as Stacks.Sheaves.RingedSpaceCotangent.naiveComparison”.

On local sections over an open U the degree -1 component of the canonical map sends the pure differential d x of a section x of P₁ to the class of d₀ x - d₁ x in I/I².

theorem naiveComparison_f_negOne_apply (f : X ⟶ S) (U : (Opens X.carrier)ᵒᵖ)
    (x : (CategoryTheory.Sheaf.resolutionTerm (Opens.grothendieckTopology X.carrier)
      (inverseImageStructureMap f) (op ⦋1⦌)).obj.obj U) :
    ((CategoryTheory.Sheaf.cotangentComplex_degreeIso (Opens.grothendieckTopology X.carrier)
          (inverseImageStructureMap f) 1).inv ≫ (naiveComparison f).f (-1) ≫
        (naivePresentationComplexXNegOneIso f).hom).val.app U
        (((CategoryTheory.Sheaf.cotangentSimplicialModule
          (Opens.grothendieckTopology X.carrier)
          (inverseImageStructureMap f)).universalDerivation (op ⦋1⦌)).d x) =
      CategoryTheory.Sheaf.conormalClassSection (Opens.grothendieckTopology X.carrier)
        (inverseImageStructureMap f) U
        (CategoryTheory.Sheaf.faceDifference (Opens.grothendieckTopology X.carrier)
          (inverseImageStructureMap f) U x)

Stacks.Sheaves.RingedSpaceCotangent.isIso_homologyMap_naiveComparison_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedSpaceNaiveComparisonHomologyZero.lean, line 44. The attribute's comment: “the degree-zero clause of the second assertion: the canonical map L_{X/Y} → NL_{X/Y} is an isomorphism on the degree-zero cohomology sheaf, both sides being Omega_{X/Y}. NL_{X/Y} is realized as the two-term complex of the conormal sequence of the presentation P₀ ⟶ O_X by the degree-zero term of the standard resolution, as for Stacks.Sheaves.RingedSpaceCotangent.naiveComparison”.

The canonical map L_{X/S} ⟶ NL_{X/S} is an isomorphism on the degree-zero cohomology sheaf, both sides being the sheaf of relative differentials Ω_{X/S}.

theorem isIso_homologyMap_naiveComparison_zero (f : X ⟶ S) :
    IsIso (HomologicalComplex.homologyMap (naiveComparison f) 0)

Sources

Section92.21 Deformations of ringed spaces and the cotangent complex #

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

Tag 08UY, an equation

Tag 08UY 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 same displayed deformation problem for ringed spaces”.

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 08UZ, a lemma

Tag 08UZ in the Stacks Project.

AlgebraicGeometry.RingedSpaceThickening.solutionClassesCotangentAddTorsor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/CotangentDeformationClassesTorsor.lean, line 75. The attribute's comment: “clause (2): if a solution of 08UY exists, the set of isomorphism classes of solutions is principal homogeneous under Ext¹(L_{X/S}, 𝒢)”. References: SGA 7 VI (4.16), “more general”.

Stacks Project, Tag 08UZ, clause (2). If there exists a solution of the deformation problem of Stacks 08UY, then the set of isomorphism classes of solutions is principal homogeneous under Ext¹_{𝒪_X}(L_{X/S}, 𝒢), as Mathlib's AddTorsor.

The set of isomorphism classes is SolutionClasses t ht f G c, the Quotient of the solutions by Isomorphic. The structure is the one of Stacks 08UC (solutionClassesAddTorsor) under Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢), read through the identification Ext¹_{𝒪_X}(𝖭𝖫_{X/S}, 𝒢) = Ext¹_{𝒪_X}(L_{X/S}, 𝒢) of Stacks 08UW (naiveExtCotangentAddEquiv). hne is the source's "if there exists a solution".

noncomputable def solutionClassesCotangentAddTorsor
    (hne : Nonempty (DeformationSolution t ht f G c)) :
    AddTorsor (cotangentExt f G 1) (SolutionClasses t ht f G c)

AlgebraicGeometry.RingedSpaceThickening.cotangentObstruction_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/CotangentObstruction.lean, line 339. The attribute's comment: “clause (1): there is a canonical element ξ ∈ Ext²(L_{X/S}, 𝒢) whose vanishing is a sufficient and necessary condition for the existence of a solution to (08UY)”.

Stacks Project, Tag 08UZ, clause (1). Let t : S ⟶ S' be a first order thickening of ringed spaces with ideal 𝒥, f : X ⟶ S a morphism of ringed spaces, 𝒢 an 𝒪_X-module and c : f^* t^* 𝒥 ⟶ 𝒢 the prescribed map on ideals (the setup of Stacks 08UY). The canonical class ξ = cotangentObstruction f G ht c ∈ Ext²_{𝒪_X}(L_{X/S}, 𝒢) vanishes if and only if the deformation problem (08UY) has a solution.

The proof is the source's: by Stacks 0GQ3 (realized here through square-zero extensions of (f ∘ t)⁻¹𝒪_{S'}-algebras with bijective ideal, exists_ideal_bijective_extClass_eq, and the correspondence DeformationSolution.toAlgebraExtension / toDeformationSolution with solutions) a solution exists exactly when ξ' = c ∘ κ ∈ Ext¹(L_{A/A'} ⊗_A 𝒪_X, 𝒢) comes from Ext¹(L_{X/S'}, 𝒢) = Ext¹(𝖭𝖫_{X/S'}, 𝒢) (Stacks 08UW), and the long exact sequence of the distinguished triangle of Stacks 08T4 identifies those classes with the ones whose image in Ext²(L_{X/S}, 𝒢) vanishes.

theorem cotangentObstruction_eq_zero_iff :
    cotangentObstruction f G ht c = 0 ↔ Nonempty (DeformationSolution t ht f G c)

AlgebraicGeometry.RingedSpaceThickening.DeformationSolution.solutionAutMulEquivCotangentExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingedSpaceThickening/SolutionAutomorphismGroup.lean, line 233. The attribute's comment: “clause (3): the group of automorphisms of a solution X' fitting into (08UY), under composition, is isomorphic to the additive group Ext^0(L_{X/S}, G)”.

Stacks Project, Tag 08UZ, clause (3). Given a solution X' of the deformation problem of (08UY), the group of automorphisms of X' fitting into that diagram is canonically isomorphic to Ext⁰_{𝒪_X}(L_{X/S}, 𝒢).

The automorphisms in question are the SolutionHom Q Q: morphisms of the deformed space under X, over S', and the identity on the prescribed ideal 𝒢. Every one is invertible by SolutionHom.isIso_hom, so these are the automorphisms of X' in the diagram; they form a group under composition (SolutionHom.instGroup, with SolutionHom.mul_hom, SolutionHom.one_hom, SolutionHom.inv_hom). The isomorphism is a group isomorphism onto the additive group Ext⁰_{𝒪_X}(L_{X/S}, 𝒢), written multiplicatively. Its underlying bijection is solutionHomEquivCotangentExt: an automorphism is x ↦ x + δ(x) for a unique relative derivation δ of 𝒪_X over f⁻¹𝒪_S with values in 𝒢, and these derivations are Hom_{𝒪_X}(Ω_{X/S}, 𝒢) = Ext⁰_{𝒪_X}(L_{X/S}, 𝒢). Composition goes to addition because (id + δ₁) ∘ (id + δ₂) = id + δ₁ + δ₂, the ideal having square zero (toDerivation_mul).

noncomputable def solutionAutMulEquivCotangentExt :
    SolutionHom Q Q ≃* Multiplicative (cotangentExt f G 0)

Sources

LeanAlgebraicGeometry.RingedSpaceThickening.DeformationSolution · AlgebraicGeometry.RingedSpaceThickening.solutionClassesCotangentAddTorsor · AlgebraicGeometry.RingedSpaceThickening.cotangentObstruction_eq_zero_iff · AlgebraicGeometry.RingedSpaceThickening.DeformationSolution.solutionAutMulEquivCotangentExt

Section92.22 The cotangent complex of a morphism of ringed topoi #

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

Tag 08SU, a definition

Tag 08SU in the Stacks Project.

AlgebraicGeometry.RingedToposHom.cotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposCotangentComplex.lean, line 58.

Stacks 08SU. The cotangent complex L_f = L_{𝒪_C/f⁻¹𝒪_D} of a morphism of ringed topoi (f, f♯) : (Sh(C), 𝒪_C) ⟶ (Sh(D), 𝒪_D): the cotangent complex of the inverse-image form f⁻¹𝒪_D ⟶ 𝒪_C of its structure map.

noncomputable def cotangentComplex :
    CochainComplex (Sheaf.targetModules.{u, v, w} X.J X.O) ℤ

AlgebraicGeometry.RingedToposHom.cotangentComplexDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposCotangentComplex.lean, line 65. The attribute's comment: “the derived object”.

Stacks 08SU. The cotangent complex of a morphism of ringed topoi, regarded as an object of the derived category of sheaves of 𝒪_C-modules.

noncomputable abbrev cotangentComplexDerived
    [HasDerivedCategory.{t} (Sheaf.targetModules.{u, v, w} X.J X.O)] :
    DerivedCategory (Sheaf.targetModules.{u, v, w} X.J X.O)

Tag 08V0, a lemma

Tag 08V0 in the Stacks Project.

AlgebraicGeometry.RingedToposHom.cotangentComplex_homologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposHomologyZero.lean, line 106.

Stacks 08V0. The zeroth homology of the cotangent complex of a morphism of ringed topoi is its sheaf of relative differentials: H⁰(L_f) = Ω_f.

noncomputable def cotangentComplex_homologyZeroIso :
    (f.cotangentComplex).homology 0 ≅ f.differentials

Tag 08V1, a lemma

Tag 08V1 in the Stacks Project.

AlgebraicGeometry.RingedToposHom.exists_distTriang_transitivity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposTransitivityTriangleDerived.lean, line 330.

Stacks 08V1. Let f : (Sh(C₁), 𝒪₁) ⟶ (Sh(C₂), 𝒪₂) and g : (Sh(C₂), 𝒪₂) ⟶ (Sh(C₃), 𝒪₃) be morphisms of ringed topoi. The canonical triangle

Lf^* L_g ⟶ L_{g ∘ f} ⟶ L_f ⟶ Lf^* L_g[1]

is distinguished in D(𝒪₁). Its first two arrows are transitivityUnit and transitivityCounit, those of the fundamental triangle of the tower (g ∘ f)⁻¹𝒪₃ = f⁻¹g⁻¹𝒪₃ ⟶ f⁻¹𝒪₂ ⟶ 𝒪₁ of Tag 08SZ; its first vertex is the derived pullback of L_g, which L_g being a bounded above complex of flat modules computes degreewise as L_{f⁻¹𝒪₂/f⁻¹g⁻¹𝒪₃} ⊗_{f⁻¹𝒪₂} 𝒪₁ (Tags 06YY and 08SV).

theorem exists_distTriang_transitivity :
    ∃ δ : G.cotangentComplexDerived ⟶ ((derivedPullback G).obj F.cotangentComplexDerived)⟦(1 : ℤ)⟧,
      Triangle.mk (transitivityUnit F G) (transitivityCounit F G) δ ∈
        distTriang (DerivedCategory (Sheaf.targetModules.{u, v, w} X.J X.O))

Tag 08V2, a lemma

Tag 08V2 in the Stacks Project.

AlgebraicGeometry.RingedToposHom.canonicalNaiveComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonCanonical.lean, line 440. The attribute's comment: “the canonical map L_f → NL_f of a morphism of ringed topoi, into the naive cotangent complex NL_{𝒪_C/f⁻¹𝒪_D} of Tag 08TW”.

Stacks 08V2, the canonical map. The canonical map L_f ⟶ NL_f of a morphism of ringed topoi (f, f♯) : (Sh(C), 𝒪_C) ⟶ (Sh(D), 𝒪_D), into NL_f = NL_{𝒪_C/f⁻¹𝒪_D} of Tag 08TW: the special case at f⁻¹𝒪_D ⟶ 𝒪_C of the map of Tag 08US.

noncomputable def canonicalNaiveComparison :
    f.cotangentComplex ⟶
      Stacks.SheafOfModules.naiveCotangentComplex.{v, u, max u v w, u} X.J _ X.O
        f.fSharpInverseImage

AlgebraicGeometry.RingedToposHom.canonicalNaiveComparison_isIso_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/NaiveComparisonCanonical.lean, line 452. The attribute's comment: “the canonical map identifies the naive cotangent complex NL_f with the truncation τ_{≥ -1} L_f: it is an isomorphism on the cohomology sheaf of every degree ≥ -1, the naive complex having no terms outside degrees -1 and 0; the special case of Tag 08US”.

Stacks 08V2. The canonical map L_f ⟶ NL_f is an isomorphism on the cohomology sheaf of every degree ≥ -1; since NL_f has no terms outside degrees -1 and 0, it identifies the naive cotangent complex with the truncation τ_{≥ -1} L_f.

theorem canonicalNaiveComparison_isIso_homologyMap (i : ℤ) (hi : -1 ≤ i) :
    IsIso (HomologicalComplex.homologyMap f.canonicalNaiveComparison i)

AlgebraicGeometry.RingedToposHom.naiveComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposNaiveComparison.lean, line 352. The attribute's comment: “the canonical map L_f → NL_f of a morphism of ringed topoi, as a map of complexes of sheaves of 𝒪_C-modules. Hypotheses beyond the source: NL_f is realized as the conormal sequence of the presentation P₀ ⟶ 𝒪_C by the degree-zero term of the standard resolution of f⁻¹𝒪_D ⟶ 𝒪_C, and the identification of that presentation with Stacks.Sites.FreeAlgebra.canonicalPresentation is not carried, so the map is not transported to Stacks.SheafOfModules.naiveCotangentComplex. The second assertion of the tag, that this map identifies NL_f with the truncation τ_{≥ -1} L_f, is the separate carrier AlgebraicGeometry.RingedToposHom.naiveComparison_isIso_homologyMap”.

The canonical map L_f ⟶ NL_f from the cotangent complex of a morphism of ringed topoi to its naive cotangent complex: CategoryTheory.Sheaf.naiveComparison at the inverse-image form f⁻¹𝒪_D ⟶ 𝒪_C of the structure map. It is d x ⊗ b ↦ b · [d₀ x - d₁ x] in degree -1, it is d p ⊗ b ↦ b ⊗ d p in degree 0, and it is zero in every other degree.

noncomputable def naiveComparison : f.cotangentComplex ⟶ f.naiveCotangentComplex

AlgebraicGeometry.RingedToposHom.naiveComparison_isIso_homologyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposNaiveComparison.lean, line 370. The attribute's comment: “the second assertion of the tag: the canonical map identifies NL_f with the truncation τ_{≥ -1} L_f, stated as: it is an isomorphism on the cohomology sheaf of every degree ≥ -1, the naive complex having no cohomology below degree -1 by AlgebraicGeometry.RingedToposHom.naiveCotangentComplex_isZero_homology. Hypotheses carried: homologyZeroIsIso and homologyNegOneIsIso, the isomorphisms on H⁰ and on H^{-1}, which are the final step of the proof of Tag 08US that this tag is the special case of — the comparison with the chaotic topology, reducing them to the ring-level map of Tag 08UP and transporting along the inverse-image isomorphism of Tag 08TZ. That tag IS carried as an isomorphism of complexes, Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso; what is not carried is the comparison with the chaotic topology”.

If the canonical map L_f ⟶ NL_f is an isomorphism on the cohomology sheaves of degrees 0 and -1 (the hypotheses homologyZeroIsIso and homologyNegOneIsIso), then it is an isomorphism on the cohomology sheaf of every degree ≥ -1. Since NL_f has no cohomology below degree -1, by AlgebraicGeometry.RingedToposHom.naiveCotangentComplex_isZero_homology, this says that the canonical map identifies the naive cotangent complex with the truncation τ_{≥ -1} L_f.

theorem naiveComparison_isIso_homologyMap
    (homologyZeroIsIso : IsIso (HomologicalComplex.homologyMap f.naiveComparison 0))
    (homologyNegOneIsIso : IsIso (HomologicalComplex.homologyMap f.naiveComparison (-1)))
    (i : ℤ) (hi : -1 ≤ i) :
    IsIso (HomologicalComplex.homologyMap f.naiveComparison i)

Sources

Section92.23 Deformations of ringed topoi and the cotangent complex #

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

Tag 08V4, an equation

Tag 08V4 in the Stacks Project.

Deformation.ToposThickening.ArbitrarySiteExtensionProblem.CompatibleFirstOrderThickening, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/UniversalFirstOrder/ArbitrarySite.lean, line 167. The attribute's comment: “the same square-zero extension problem, as stated in the Cotangent chapter”.

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

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

Declarations registered for the tag:

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/ToposThickening/UniversalFirstOrder/ArbitrarySite.lean, line 90 (StacksFrontier): “the displayed diagram, same-site presentation”.

Tag 08V5, a lemma

Tag 08V5 in the Stacks Project.

Deformation.ToposThickening.RingedToposExtensionProblem.nonempty_iff_obstructionClass_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/CotangentObstructionExistence.lean, line 326. The attribute's comment: “(1): the element obstructionClass of Ext²_O(L_f, G), the image of the class of c under the connecting morphism of the fundamental triangle of f⁻¹O_{B'} → f⁻¹O_B → O, vanishes exactly when a solution exists”.

Stacks 08V5 (1): a solution of the square-zero extension problem exists if and only if the obstruction class in Ext²_O(L_f, G) vanishes.

theorem nonempty_iff_obstructionClass_eq_zero :
    Nonempty S.CompatibleFirstOrderThickening ↔ S.obstructionClass = 0

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.autEquivDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionAutomorphisms.lean, line 419. The attribute's comment: “clause (3), the automorphism group of a solution, computed for the concrete group of section-wise derivations of the solution rather than Ext⁰_O(L_f, G); that identification is not proved, as in the library's Stacks 08UG and Stacks 08UK”.

Stacks Project, Tag 08V5, clause (3). The automorphisms of a solution of the square-zero extension problem of [Stacks Project, Tag 08V4] fitting into that diagram are canonically bijective to the derivations of that solution — section-wise maps from its thickened structure sheaf to the prescribed module G satisfying the Leibniz rule and vanishing on G and on the image of f⁻¹O_{B'}. With autEquivDerivation_mul this is an isomorphism of groups.

The source writes the group as Ext⁰_O(L_f, G); that identification is not proved here, and the three steps separating the two readings are recorded in the implementation notes of this file.

public noncomputable def autEquivDerivation (P : S.CompatibleFirstOrderThickening) :
    P.AutomorphismGroup ≃ Derivation P

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.autEquivDerivation_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionAutomorphisms.lean, line 445. The attribute's comment: “clause (3), that the canonical bijection of autEquivDerivation between the automorphisms of a solution and its section-wise derivations is a group isomorphism; the group is not identified with Ext⁰_O(L_f, G), as in the library's Stacks 08UG and Stacks 08UK”.

Stacks Project, Tag 08V5, clause (3). The canonical bijection between the automorphisms of a solution and the derivations of that solution is an isomorphism of groups: composition of automorphisms is addition of derivations.

public theorem autEquivDerivation_mul (P : S.CompatibleFirstOrderThickening)
    (a b : P.AutomorphismGroup) :
    autEquivDerivation P (a * b) = autEquivDerivation P a + autEquivDerivation P b

Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.autMulEquivExtZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/ToposThickening/SolutionAutomorphismsExt.lean, line 483. The attribute's comment: “clause (3): given a solution, its automorphisms fitting into the diagram of 08V4 form a group canonically isomorphic to Ext⁰_O(L_f, G)”.

Given a solution P of a square-zero extension problem of ringed topoi, the group of automorphisms of P fitting into the diagram of the problem is canonically isomorphic to Ext⁰_O(L_f, G): an automorphism a goes to the class whose degree-zero homology Ω_f = H⁰(L_f) ⟶ G sends d(x mod G) to the section of G by which a(x) differs from x; composition of automorphisms goes to addition of classes.

noncomputable def autMulEquivExtZero :
    P.AutomorphismGroup ≃* Multiplicative (S.f.cotangentExt (targetG S) 0)

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

Stacks 08V5, clause (2): if the square-zero extension problem has a solution, the isomorphism classes of solutions are a principal homogeneous space under Ext¹_O(L_f, G).

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

Sources

LeanDeformation.ToposThickening.ArbitrarySiteExtensionProblem.CompatibleFirstOrderThickening · Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening · Deformation.ToposThickening.RingedToposExtensionProblem.nonempty_iff_obstructionClass_eq_zero · Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.autEquivDerivation · Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.autEquivDerivation_mul · Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.autMulEquivExtZero · Deformation.ToposThickening.RingedToposExtensionProblem.CompatibleFirstOrderThickening.isomorphismClassesAddTorsor

Section92.24 The cotangent complex of a morphism of schemes #

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

Tag 08T2, a definition

Tag 08T2 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.cotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeCotangentComplex.lean, line 116.

Stacks 08T2. The cotangent complex L_{X/Y} of a morphism of schemes f : X ⟶ Y: the cotangent complex of f read as a morphism of the Zariski ringed topoi of X and Y, a complex of sheaves of 𝒪_X-modules.

noncomputable def cotangentComplex :
    CochainComplex
      (Sheaf.targetModules (Opens.grothendieckTopology ↥X) X.zariskiRingedTopos.O) ℤ

AlgebraicGeometry.Scheme.Hom.cotangentComplexDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeCotangentComplex.lean, line 124. The attribute's comment: “the derived object”.

Stacks 08T2. The cotangent complex L_{X/Y} of a morphism of schemes, regarded as an object of the derived category of sheaves of 𝒪_X-modules.

noncomputable abbrev cotangentComplexDerived
    [HasDerivedCategory.{u} (Sheaf.targetModules (Opens.grothendieckTopology ↥X)
      X.zariskiRingedTopos.O)] :
    DerivedCategory
      (Sheaf.targetModules (Opens.grothendieckTopology ↥X) X.zariskiRingedTopos.O)

Tag 08T3, a lemma

Tag 08T3 in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.affineCotangentComparison_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/AffineCotangentComparisonIsIso.lean, line 251. The attribute's comment: “the whole lemma, in one covering statement: (1) the canonical map, pinned as the adjunct under the tilde-Gamma adjunction of the canonical map L_{B/A} -> Gamma(L_{X/Y}|_U) built from A -> (f^{-1}O_Y)(U) and Remark 08SX; (2) it is an isomorphism in D(O_U); (3) it is compatible with restriction to smaller affine opens U' of X and opens V' of Y. Hypotheses: exactly the source's, U and V affine with f(U) inside V”.

Stacks Project, Tag 08T3.

Let f : X ⟶ Y be a morphism of schemes and let U = Spec B ⊂ X and V = Spec A ⊂ Y be affine opens with f(U) ⊂ V, so that B = 𝒪_X(U) and A = 𝒪_Y(V). The map of complexes AlgebraicGeometry.Scheme.Hom.affineCotangentComparison f hU e : ~(L_{B/A}) ⟶ L_{X/Y}|_U satisfies the three assertions of the lemma:

it is the canonical map: in every degree it is the adjunct, under the universal property of ~ (Tag 01I7), of the canonical map L_{B/A} ⟶ Γ(L_{X/Y}|_U), AlgebraicGeometry.Scheme.Hom.gammaCotangentComparison, which is the map L_{B/A} ⟶ L_{𝒪_X(U)/(f⁻¹𝒪_Y)(U)} induced by A ⟶ (f⁻¹𝒪_Y)(U) followed by the canonical map L_{𝒪_X(U)/(f⁻¹𝒪_Y)(U)} ⟶ L_{X/Y}(U) of Remark 08SX;

it is an isomorphism in D(𝒪_U);

it is compatible with restricting to smaller affine opens U' ⊂ U of X and V' ⊂ V of Y with f(U') ⊂ V': the square formed by the canonical maps for (U, V) and (U', V') and the two restriction maps commutes.

theorem affineCotangentComparison_spec [HasDerivedCategory.{w} (Spec Γ(X, U)).Modules] :
    (∀ j : ℤ, (tilde.adjunction (R := Γ(X, U))).homEquiv _ _
        ((affineCotangentComparison f hU e).f j) = (gammaCotangentComparison f hU e).f j) ∧
    IsIso (DerivedCategory.Q.map (affineCotangentComparison f hU e)) ∧
    ∀ {U' : X.Opens} (hU' : IsAffineOpen U') {V' : Y.Opens} (e' : U' ≤ f ⁻¹ᵁ V')
      (hUle : U' ≤ U) (hVle : V' ≤ V),
      affineCotangentComparison f hU e ≫
          Stacks.AffineCotangentSheaf.restrictedCotangentRestriction f hU hU' hUle =
        Stacks.AffineCotangentSheaf.tildeCotangentRestriction f e e' hUle hVle ≫
          ((Scheme.Modules.pushforward
            (Stacks.AffineCotangentSheaf.specRestriction hUle)).mapHomologicalComplex
              (ComplexShape.up ℤ)).map (affineCotangentComparison f hU' e')

Stacks.AffineCotangentSheaf.affineCotangentComparison_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/AffineCotangentRestrictionSheaf.lean, line 396. The attribute's comment: “ASSERTION 3 ONLY, and AS SHEAVES: the canonical map of this tag, ~(L_{O_X(U)/O_Y(V)}) -> L_{X/Y}|_U, is compatible with restriction along affine opens U' <= U and opens V' <= V, as an EQUALITY of maps of complexes of sheaves of O_{Spec O_X(U)}-modules -- not a Nonempty and not the sectionwise statement. The two vertical maps of the square are tildeCotangentRestriction and restrictedCotangentRestriction; the latter is the genuine sheaf restriction map, which restrictionUnit_app_app proves acts on sections as presheaf.map (homOfLE _).op. CARRIED: IsAffineOpen U and IsAffineOpen U', which are the source's own hypotheses -- the comparison map is only defined for an affine open -- and nothing else; IsAffineOpen V and IsAffineOpen V' are NOT carried, so this is more general than the source in the base variables. ASSERTIONS 1 AND 2 ARE NOT CLAIMED HERE”.

Stacks 08T3, assertion 3, as sheaves. For a morphism of schemes f : X ⟶ Y, affine opens U' ≤ U of X and opens V' ≤ V of Y with f(U) ⊂ V and f(U') ⊂ V', the canonical map ~(L_{𝒪_X(U)/𝒪_Y(V)}) ⟶ L_{X/Y}|_U of Tag 08T3 is compatible with restriction: writing ρ : Spec 𝒪_X(U') ⟶ Spec 𝒪_X(U) for the morphism induced by restriction, the square formed by the two comparison maps and the two restriction maps commutes as an equality of maps of complexes of 𝒪_{Spec 𝒪_X(U)}-modules.

theorem affineCotangentComparison_restriction (e : U ≤ f ⁻¹ᵁ V) (e' : U' ≤ f ⁻¹ᵁ V')
    (hUle : U' ≤ U) (hVle : V' ≤ V) :
    affineCotangentComparison f hU e ≫ restrictedCotangentRestriction f hU hU' hUle =
      tildeCotangentRestriction f e e' hUle hVle ≫
        ((Scheme.Modules.pushforward (specRestriction hUle)).mapHomologicalComplex
          (ComplexShape.up ℤ)).map (affineCotangentComparison f hU' e')

Tag 08V6, a lemma

Tag 08V6 in the Stacks Project.

AlgebraicGeometry.SchemeOverRing.constantComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeOverRing.lean, line 226. The attribute's comment: “the canonical comparison L_{O_X/const Lambda} ⟶ L_{X/Spec Lambda} of the tag, constructed unconditionally as the change-of-base arrow of Tag 08SZ for the tower const Lambda ⟶ p^-1 O_{Spec Lambda} ⟶ O_X, with the constant sheaf being Mathlib's constantSheaf and the target the cotangent complex of p of Tag 08UU (cotangentComplexRelative_eq). That it is an ISOMORPHISM is NOT claimed by this declaration; see isIso_constantComparison_iff and the module documentation”.

The canonical comparison L_{𝒪_X/Λ̲} ⟶ L_{X/Spec Λ}: the change-of-base-ring map of the tower Λ̲ ⟶ p⁻¹𝒪_{Spec Λ} ⟶ 𝒪_X.

def constantComparison : cotangentComplexConstant Λ p ⟶ cotangentComplexRelative Λ p

AlgebraicGeometry.SchemeOverRing.isIso_constantComparison_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeOverRing.lean, line 245. The attribute's comment: “the REDUCTION of the tag, not the tag: an IFF between the comparison being an isomorphism in D(O_X) and the vanishing of the first vertex of the fundamental triangle, the pullback of the source's L_q. The vanishing -- the source's Tag 08T0 plus Tag 08R2 step -- is NOT proved here and is not assumed either; it is the right-hand side. ONE carried hypothesis, exactly the one Tag 08SZ carries: the short exact sequence S/hS realizing the two canonical arrows (hf, hg) on the three vertices (e1, e2, e3), the sheaf-level analogue of Tag 08SD, absent from this library. See the module documentation”.

Granted the short exact sequence Tag 08SZ carries for the tower Λ̲ ⟶ p⁻¹𝒪_{Spec Λ} ⟶ 𝒪_X, the canonical comparison L_{𝒪_X/Λ̲} ⟶ L_{X/Spec Λ} is an isomorphism in D(𝒪_X) exactly when the first vertex L_{p⁻¹𝒪_{Spec Λ}/Λ̲} ⊗_{p⁻¹𝒪_{Spec Λ}} 𝒪_X of the fundamental triangle vanishes there.

The hypothesis carried is the one Tag 08SZ carries, in the same shape: a short complex S of complexes of sheaves of 𝒪_X-modules that is short exact (hS), whose three terms are the three vertices (e₁, e₂, e₃) and whose two maps are the two canonical arrows (hf, hg).

theorem isIso_constantComparison_iff
    [HasDerivedCategory.{t} (CategoryTheory.Sheaf.targetModules.{u, u, u}
      (Opens.grothendieckTopology ↥X) (structureSheafOfSite X))]
    (S : ShortComplex (CochainComplex
      (CategoryTheory.Sheaf.targetModules.{u, u, u} (Opens.grothendieckTopology ↥X)
        (structureSheafOfSite X)) ℤ))
    (hS : S.ShortExact) (e₁ : S.X₁ ≅ pullbackCotangentComplex Λ p)
    (e₂ : S.X₂ ≅ cotangentComplexConstant Λ p)
    (e₃ : S.X₃ ≅ cotangentComplexRelative Λ p)
    (hf : S.f = e₁.hom ≫ CategoryTheory.Sheaf.towerCotangentBaseChange.{u, u, u}
      (Opens.grothendieckTopology ↥X) (constantToPullback Λ p)
      (pullbackStructureMap Λ p) ≫ e₂.inv)
    (hg : S.g = e₂.hom ≫ constantComparison Λ p ≫ e₃.inv) :
    IsIso ((DerivedCategory.Q (C := CategoryTheory.Sheaf.targetModules.{u, u, u}
          (Opens.grothendieckTopology ↥X) (structureSheafOfSite X))).map
        (constantComparison Λ p)) ↔
      IsZero ((DerivedCategory.Q (C := CategoryTheory.Sheaf.targetModules.{u, u, u}
        (Opens.grothendieckTopology ↥X) (structureSheafOfSite X))).obj
          (pullbackCotangentComplex Λ p))

AlgebraicGeometry.SchemeOverRing.isIso_constantComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeOverRingComparison.lean, line 227. The attribute's comment: “L_{X/Spec Lambda} = L_{O_X/const Lambda} in D(O_X) for a scheme X over a ring Lambda, const Lambda the constant sheaf with value Lambda on X: the canonical comparison L_{O_X/const Lambda} ⟶ L_{X/Spec Lambda} (constantComparison) is an isomorphism in D(O_X)”.

Stacks Project, Tag 08V6. Let Λ be a ring and let X be a scheme over Λ. Then L_{X/Spec Λ} = L_{𝒪_X/Λ̲} in D(𝒪_X), where Λ̲ is the constant sheaf with value Λ on X: the canonical comparison L_{𝒪_X/Λ̲} ⟶ L_{X/Spec Λ}, the change-of-base map of the tower Λ̲ ⟶ p⁻¹𝒪_{Spec Λ} ⟶ 𝒪_X, is an isomorphism in the derived category.

theorem isIso_constantComparison
    [HasDerivedCategory.{t} (CategoryTheory.Sheaf.targetModules.{u, u, u}
      (Opens.grothendieckTopology ↥X) (structureSheafOfSite X))] :
    IsIso ((DerivedCategory.Q (C := CategoryTheory.Sheaf.targetModules.{u, u, u}
      (Opens.grothendieckTopology ↥X) (structureSheafOfSite X))).map (constantComparison Λ p))

Sources

LeanAlgebraicGeometry.Scheme.Hom.cotangentComplex · AlgebraicGeometry.Scheme.Hom.cotangentComplexDerived · AlgebraicGeometry.Scheme.Hom.affineCotangentComparison_spec · Stacks.AffineCotangentSheaf.affineCotangentComparison_restriction · AlgebraicGeometry.SchemeOverRing.constantComparison · AlgebraicGeometry.SchemeOverRing.isIso_constantComparison_iff · AlgebraicGeometry.SchemeOverRing.isIso_constantComparison

Section92.25 The cotangent complex of a scheme over a ring #

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

Tag 08V8, an equation

Tag 08V8 in the Stacks Project.

AlgebraicGeometry.PolynomialChart, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialChart.lean, line 50.

A commutative diagram U ⟶ A ⟶ Spec Λ, U ⟶ X ⟶ Spec Λ, where U is an open subscheme of X and A is an affine space over Spec Λ.

structure PolynomialChart (Λ : Type u) [CommRing Λ] (X : Scheme.{u})
    (structureMap : X ⟶ Spec (CommRingCat.of Λ))

Tag 08V9, a lemma

Tag 08V9 in the Stacks Project.

AlgebraicGeometry.PolynomialChart.openFunctor_isFibered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/PolynomialChartFibred.lean, line 101.

Stacks 08V9. Polynomial charts over X form a category fibred over the Zariski category of X.

instance openFunctor_isFibered (Λ : Type u) [CommRing Λ] (X : Scheme.{u})
    (structureMap : X ⟶ Spec (CommRingCat.of Λ)) :
    (openFunctor (Λ := Λ) (X := X) (structureMap := structureMap)).IsFibered

Tag 08VA, an equation

Tag 08VA in the Stacks Project.

AlgebraicGeometry.PolynomialChart.piSchemesDiagram, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/PolynomialChartRingedTopoi.lean, line 694.

Stacks 08VA. The diagram of ringed topoi of the polynomial charts of a scheme over a ring, with all of its arrows pinned to the canonical ones.

def piSchemesDiagram : PiSchemesDiagram.{u, w} Λ X structureMap

Tag 08VB, a remark

Tag 08VB in the Stacks Project.

AlgebraicGeometry.PolynomialChart.standardResolutionChart_computes_derivedLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/StandardResolutionChartsLowerShriek.lean, line 85.

Stacks 08VB. Let X be a scheme over a ring Λ, and for an open U ⊆ X let P_{•,U} be the standard resolution of 𝒪_X(U) over Λ and A_{•,U} = Spec(P_{•,U}), the functorial cosimplicial charts standardResolutionChart. Then:

the fibre category of C_{X/Λ} over U is C_{𝒪_X(U)/Λ}, and A_{•,U} is a cosimplicial object of it (standardResolutionFibreChart) which is as in Stacks 08Q9: every simplicial set Mor(A_{•,U}, W) is homotopy equivalent to a point;

for every abelian sheaf F on C_{X/Λ} the cohomology groups of the complex of presheaves U ↦ F(A_{•,U}) compute the homology of F on the fibre category over U;

their sheafification computes L_nπ_!(F);

the complex of sheaves whose term in degree -n is the sheafification of U ↦ F(A_{n,U}) computes Lπ_!(F).

theorem standardResolutionChart_computes_derivedLowerShriek :
    (∀ U : X.Opens, Nonempty ((openFunctor (Λ := Λ) (X := X)
        (structureMap := structureMap)).Fiber U ≌
      CommAlgCat.polynomialSite Λ ((openAlgebra Λ X structureMap).obj (op U)))) ∧
    (∀ (U : X.Opens) (W : (openFunctor (Λ := Λ) (X := X) (structureMap := structureMap)).Fiber U),
      ∃ f : (standardResolutionFibreChart Λ X structureMap U).op ⋙ yoneda.obj W ⟶
          (Functor.const SimplexCategoryᵒᵖ).obj PUnit.{u + 1},
        SimplicialObject.homotopyEquivalences (Type u) f) ∧
    (∀ (F : Sheaf (fibredCategorySituation Λ X structureMap).topology AddCommGrpCat.{u + 1})
      (U : (fibredCategorySituation Λ X structureMap).base.C) (n : ℕ),
      Nonempty (((((fibredCategorySituation Λ X structureMap).pointMooreComplex
          (standardResolutionChart Λ X structureMap :
            (fibredCategorySituation Λ X structureMap).base.C ⥤
              CosimplicialObject (fibredCategorySituation Λ X structureMap).C)).obj
            F.obj).homology n).obj (op U) ≅
        Stacks.CategoryHomology.categoryHomology.{u + 1, u + 1}
          ((fibredCategorySituation Λ X structureMap).smallFiberRestriction F.obj U) n)) ∧
    (∀ (F : Sheaf (fibredCategorySituation Λ X structureMap).topology AddCommGrpCat.{u + 1})
      (n : ℕ),
      Nonempty ((DerivedCategory.homologyFunctor _ (-(n : ℤ))).obj
          ((fibredCategorySituation Λ X structureMap).derivedAbelianLowerShriek.obj
            ((DerivedCategory.singleFunctor _ 0).obj F)) ≅
        (presheafToSheaf (fibredCategorySituation Λ X structureMap).base.J
          AddCommGrpCat.{u + 1}).obj
          ((((fibredCategorySituation Λ X structureMap).pointMooreComplex
            (standardResolutionChart Λ X structureMap :
              (fibredCategorySituation Λ X structureMap).base.C ⥤
                CosimplicialObject (fibredCategorySituation Λ X structureMap).C)).obj
              F.obj).homology n))) ∧
    (∀ F : Sheaf (fibredCategorySituation Λ X structureMap).topology AddCommGrpCat.{u + 1},
      Nonempty ((fibredCategorySituation Λ X structureMap).derivedAbelianLowerShriek.obj
          ((DerivedCategory.singleFunctor _ 0).obj F) ≅
        DerivedCategory.Q.obj ((fibredCategorySituation Λ X structureMap).pointSheafComplex
          (standardResolutionChart Λ X structureMap :
            (fibredCategorySituation Λ X structureMap).base.C ⥤
              CosimplicialObject (fibredCategorySituation Λ X structureMap).C) F.obj)))

Tag 08T9, a lemma

Tag 08T9 in the Stacks Project.

AlgebraicGeometry.PolynomialChart.hasLeftDerivedFunctor_horizontalModuleInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ChartSiteHorizontalDerivedPullback.lean, line 267. The attribute's comment: “the first link of the chain L_{X/Λ} = Lπ_!(Li^Ω_{𝒪/Λ̲}) = Lπ_!(i^Ω_{𝒪/Λ̲}) = Lπ_!(Ω_{𝒪/Λ̲} ⊗_𝒪 π⁻¹𝒪_X): the existence of the total left derived functor Li^* of the module pullback along the horizontal arrow of the diagram of Tag 08VA, on the chart site itself”.

Li^* exists on the site of polynomial charts. Degreewise i^* followed by localization to the derived category has a total left derived functor with respect to the quasi-isomorphisms of complexes of 𝒪-modules.

On the small model this is the derived pullback of Tag 06YY along a change of coefficient rings; the quasi-isomorphisms of the chart site are the inverse image of those of the small model, and total left derived functors are preserved by conjugation by equivalences.

theorem hasLeftDerivedFunctor_horizontalModuleInverseImage :
    ((horizontalModuleInverseImage.{u, u + 1} Λ X structureMap).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).HasLeftDerivedFunctor
      (HomotopyCategory.quasiIso (_root_.SheafOfModules.{u + 1}
        ((Stacks.SheafOfModules.Tensor.ringSheaf.{u + 1, u, u + 1}
            (J := (topology Λ X structureMap)))
          (affineSheaf.{u, u + 1} Λ X structureMap))) (ComplexShape.up ℤ))

AlgebraicGeometry.PolynomialChart.derivedLowerShriekInverseImageDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeCotangentChartSite.lean, line 256. The attribute's comment: “second isomorphism Lπ_!(Li^Ω_{𝒪/Λ̲}) = Lπ_!(i^Ω_{𝒪/Λ̲}), induced by the canonical map Li^Ω ⟶ i^Ω, an isomorphism since Ω_{𝒪/Λ̲} is flat”.

Stacks Project, Tag 08T9, the second isomorphism Lπ_!(Li^*Ω_{𝒪/Λ̲}) ≅ Lπ_!(i^*Ω_{𝒪/Λ̲}): Lπ_! applied to the canonical map Li^*Ω_{𝒪/Λ̲} ⟶ i^*Ω_{𝒪/Λ̲}, an isomorphism because Ω_{𝒪/Λ̲} is a flat 𝒪-module (derivedHorizontalInverseImageDifferentialsIso).

def derivedLowerShriekInverseImageDifferentialsIso :
    (chartDerivedLowerShriek Λ X structureMap).obj
        ((derivedHorizontalInverseImage Λ X structureMap).obj
          ((DerivedCategory.singleFunctor _ 0).obj
            (chartDifferentials.{u, u + 1} Λ X structureMap))) ≅
      (chartDerivedLowerShriek Λ X structureMap).obj
        ((DerivedCategory.singleFunctor _ 0).obj
          (pulledBackDifferentials.{u, u + 1} Λ X structureMap))

AlgebraicGeometry.PolynomialChart.derivedLowerShriekPulledBackDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeCotangentChartSite.lean, line 273. The attribute's comment: “third isomorphism Lπ_!(i^Ω_{𝒪/Λ̲}) = Lπ_!(Ω_{𝒪/Λ̲} ⊗_𝒪 𝒪̲_X), induced by the canonical identification of i^ with extension of scalars along i♯”.

Stacks Project, Tag 08T9, the third isomorphism Lπ_!(i^*Ω_{𝒪/Λ̲}) ≅ Lπ_!(Ω_{𝒪/Λ̲} ⊗_𝒪 𝒪̲_X): Lπ_! applied to the canonical identification of the pullback i^*Ω_{𝒪/Λ̲} with the extension of scalars of Ω_{𝒪/Λ̲} along i♯ (pulledBackDifferentialsIsoBaseChange).

def derivedLowerShriekPulledBackDifferentialsIso :
    (chartDerivedLowerShriek Λ X structureMap).obj
        ((DerivedCategory.singleFunctor _ 0).obj
          (pulledBackDifferentials.{u, u + 1} Λ X structureMap)) ≅
      (chartDerivedLowerShriek Λ X structureMap).obj
        ((DerivedCategory.singleFunctor _ 0).obj
          (chartDifferentialsBaseChange Λ X structureMap))

AlgebraicGeometry.PolynomialChart.cotangentComplexIsoDerivedLowerShriekInverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SchemeCotangentChartSite.lean, line 301. The attribute's comment: “first isomorphism L_{X/Λ} = Lπ_!(Li^*Ω_{𝒪/Λ̲}) in D(𝒪_X), for the site of polynomial charts of a scheme X over a ring Λ, with L_{X/Λ} the cotangent complex of X ⟶ Spec Λ and D(𝒪_X) taken in the coefficient universe of the chart topos; built from the canonical maps of the proof: flatness of Ω, Tag 08VB, Tag 08SX and the Tag 08V6 comparison”.

Stacks Project, Tag 08T9, the first isomorphism L_{X/Λ} ≅ Lπ_!(Li^*Ω_{𝒪/Λ̲}) in D(𝒪_X), for the site of polynomial charts of Tag 08VA of a scheme X over a ring Λ. Here L_{X/Λ} = L_{X/Spec Λ} is the cotangent complex of the structure morphism (SchemeOverRing.cotangentComplexRelative, Tag 08UU), read in the coefficient universe of the chart topos through chartBaseLift; Ω_{𝒪/Λ̲} is chartDifferentials; Li^* is derivedHorizontalInverseImage; and Lπ_! is chartDerivedLowerShriek.

It is the composite of the canonical maps of the source's proof, read from right to left: Li^*Ω ⟶ i^*Ω (an isomorphism because Ω_{𝒪/Λ̲} is flat), i^*Ω ≅ Ω ⊗_𝒪 𝒪̲_X, the identification of Lπ_!(Ω ⊗_𝒪 𝒪̲_X) with the complex of the standard resolutions (Tag 08VB at module coefficients), the identification of that complex with the sheafification of U ↦ L_{𝒪_X(U)/Λ} and with L_{𝒪_X/Λ̲} (Tag 08SX), and the comparison map L_{𝒪_X/Λ̲} ⟶ L_{X/Spec Λ}, a quasi-isomorphism by Tag 08V6.

def cotangentComplexIsoDerivedLowerShriekInverseImage :
    DerivedCategory.Q.obj (((chartBaseLift Λ X structureMap).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj (SchemeOverRing.cotangentComplexRelative Λ structureMap)) ≅
      (chartDerivedLowerShriek Λ X structureMap).obj
        ((derivedHorizontalInverseImage Λ X structureMap).obj
          ((DerivedCategory.singleFunctor _ 0).obj
            (chartDifferentials.{u, u + 1} Λ X structureMap)))

Sources

LeanAlgebraicGeometry.PolynomialChart · AlgebraicGeometry.PolynomialChart.openFunctor_isFibered · AlgebraicGeometry.PolynomialChart.piSchemesDiagram · AlgebraicGeometry.PolynomialChart.standardResolutionChart_computes_derivedLowerShriek · AlgebraicGeometry.PolynomialChart.hasLeftDerivedFunctor_horizontalModuleInverseImage · AlgebraicGeometry.PolynomialChart.derivedLowerShriekInverseImageDifferentialsIso · AlgebraicGeometry.PolynomialChart.derivedLowerShriekPulledBackDifferentialsIso · AlgebraicGeometry.PolynomialChart.cotangentComplexIsoDerivedLowerShriekInverseImage

Section92.26 The cotangent complex of a morphism of algebraic spaces #

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

Tag 08VD, a definition

Tag 08VD in the Stacks Project.

AlgebraicGeometry.Space.cotangentComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/CotangentComplex.lean, line 114.

Stacks Project, Tag 08VD. The cotangent complex L_{X/Y} of a morphism f : X ⟶ Y of algebraic spaces over a scheme S: the cotangent complex of the canonical morphism of ringed topoi f_small between the small étale sites of X and Y, that is, the cotangent complex of the map of sheaves of commutative rings f_small⁻¹𝒪_Y ⟶ 𝒪_X on the small étale site of X.

It is a complex of modules over 𝒪_X, so it depends on X alone.

noncomputable abbrev cotangentComplex (f : X ⟶ Y) :
    CochainComplex (smallEtaleModulesULift B S hS X) ℤ

AlgebraicGeometry.Space.cotangentComplexDerived, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/CotangentComplex.lean, line 123. The attribute's comment: “the derived object”.

Stacks Project, Tag 08VD. The cotangent complex L_{X/Y} regarded as an object of the derived category D(𝒪_X).

noncomputable abbrev cotangentComplexDerived (f : X ⟶ Y)
    [HasDerivedCategory.{t} (smallEtaleModulesULift B S hS X)] :
    DerivedCategory (smallEtaleModulesULift B S hS X)

Tag 08VE, a lemma

Tag 08VE in the Stacks Project.

AlgebraicGeometry.Space.etaleRestrictionCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/EtaleRestriction.lean, line 395.

For a commutative diagram of algebraic spaces over a scheme S
U --g--> V
|p       |q
X --f--> Y
with p and q étale, the restriction of the cotangent complex L_{X/Y} to the small étale site of U is the cotangent complex L_{U/V}:

L_{X/Y}|_{U_étale} = L_{U/V}.

Formation of the cotangent complex commutes with inverse image (Stacks 08SV), and the structure maps of f and of g are carried to one another by the comparisons of Stacks 03LV and Stacks 03G8, which commute by AlgebraicGeometry.Space.etaleRestrictionCotangentSquare; square functoriality of the cotangent complex then transports the complex.

noncomputable def etaleRestrictionCotangentComplexIso {p : U ⟶ X} {f : X ⟶ Y} {g : U ⟶ V}
    {q : V ⟶ Y} (hp : IsEtale B S hS p.hom) (hq : IsEtale B S hS q.hom) (h : p ≫ f = g ≫ q) :
    ((etaleRestrictModules B S hS p hp).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (cotangentComplex B S hS f) ≅
      cotangentComplex B S hS g

Tag 08VF, a lemma

Tag 08VF in the Stacks Project.

AlgebraicGeometry.Space.quasiIso_representedCotangentComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/RepresentableComparison.lean, line 303. The attribute's comment: “the canonical map ε^*L_{X₀/Y₀} ⟶ L_{X/Y} is a quasi-isomorphism, for the morphism of algebraic spaces represented by a morphism T₁ ⟶ T₂ of the big fppf site over S (so X and Y are represented by the schemes X₀, Y₀ underlying T₁, T₂); ε is the comparison of Section 071P (representedToZariskiRingedToposHom), L_{X₀/Y₀} the cotangent complex of Definition 08T2 lifted to the universe of the small étale site, ε^* the degreewise pullback of sheaves of modules along ε. The map is representedCotangentComparison; its transpose is the functoriality of the cotangent complex over the square of Remark 08GH (towerCotangentUnit_comp_representedBaseChangedComparison)”.

Stacks 08VF. Let f : X ⟶ Y be the morphism of algebraic spaces over S represented by a morphism T₁ ⟶ T₂ of the big fppf site, so that X and Y are representable by the schemes X₀ and Y₀ underlying T₁ and T₂. Then the canonical map ε^*L_{X₀/Y₀} ⟶ L_{X/Y} (AlgebraicGeometry.Space.representedCotangentComparison) is a quasi-isomorphism.

The source's proof checks this on stalks at geometric points; here the map is factored through the two canonical arrows of the fundamental triangles of Stacks 08SZ, and the two vertices that must vanish, L_{𝒪_X/ε⁻¹𝒪_{X₀}} and L_{f_small⁻¹𝒪_Y/ε⁻¹f₀⁻¹𝒪_{Y₀}} ⊗ 𝒪_X, vanish because their stalks at the geometric points are the cotangent complexes of the strict henselizations 𝒪_{X₀,x} ⟶ 𝒪_{X,x̄} and 𝒪_{Y₀,y} ⟶ 𝒪_{Y,ȳ} (Stacks 04K5, 08T0, 05V1, 04KF, 08R2); this is the content of Lemma 08UN that the source invokes.

theorem quasiIso_representedCotangentComparison :
    QuasiIso (representedCotangentComparison B S hS h)

AlgebraicGeometry.Space.representedCotangentComplexDerivedIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/RepresentableComparison.lean, line 323. The attribute's comment: “the canonical identification ε^*L_{X₀/Y₀} ≅ L_{X/Y} in D(𝒪_X), for the morphism of algebraic spaces represented by a morphism T₁ ⟶ T₂ of the big fppf site over S, as the image in the derived category of the canonical map representedCotangentComparison; any derived category of Mod(𝒪_X) may be used”.

Stacks 08VF. The canonical identification L_{X/Y} = ε^*L_{X₀/Y₀} in D(𝒪_X), for the morphism f : X ⟶ Y of algebraic spaces represented by a morphism T₁ ⟶ T₂ of the big fppf site over S: the image in the derived category of the canonical map AlgebraicGeometry.Space.representedCotangentComparison, which is a quasi-isomorphism (AlgebraicGeometry.Space.quasiIso_representedCotangentComparison).

noncomputable def representedCotangentComplexDerivedIso
    [HasDerivedCategory.{t}
      (smallEtaleModulesULift B S hS ⟨yoneda.obj T₁, isAlgebraicSpace_yoneda B S hS T₁⟩)] :
    DerivedCategory.Q.obj (representedPulledBackCotangentComplex B S hS h) ≅
      cotangentComplexDerived B S hS (representedSpaceMap B S hS h)

Tag 08VG, a lemma

Tag 08VG in the Stacks Project.

AlgebraicGeometry.RingedToposHom.cotangentComplexOverConstantRingIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/ConstantBaseRing.lean, line 255. The attribute's comment: “an isomorphism in D(𝒪_X) rather than an equality of complexes, as the source's own proof produces. L_{X/Spec(Λ)} is the cotangent complex of the morphism of ringed topoi (Tag 08SU) and L_{𝒪_X/Λ̲} is the cotangent complex of Λ̲ ⟶ 𝒪_X with Λ̲ the constant sheaf of Mathlib's constantSheaf, so no identification of Λ̲ with an iterated inverse image is used. TWO carried hypotheses, both inputs of the source's argument and neither the conclusion: (1) the short exact sequence S, hS, e₁, e₂, e₃ giving the fundamental triangle of Tag 08SZ for the tower Λ̲ ⟶ G⁻¹𝒪_Y ⟶ 𝒪_X, carried in the same shape and for the same reason as in Tag 08V1 (the sheaf-level analogue of Tag 08SD is absent here); (2) hv, the acyclicity of the FIRST vertex L_{G⁻¹𝒪_Y/Λ̲} ⊗ 𝒪_X, which is the source's L_q = 0 for q : Spec(Λ)_étale ⟶ (*, Λ) pulled back to X — firstVertexOverInverseImageBaseIso proves that a first vertex over an inverse-image base is G^*G⁻¹L_{𝒪_Y/Λ_Y} — and which the source obtains from Tags 04K5, 08T0, 04KF and 08R2, none of which this library has in a form applying to acyclicity of a complex of sheaves of modules on a site. The conclusion's two objects do not occur in either hypothesis. What is proved: the passage from the short exact sequence to a distinguished triangle, the identification of the first vertex over an inverse-image base through Tag 08SV, and the degeneration of the triangle. The first vertex carries the DEGREEWISE extension of scalars, as in Tag 08V1”.

Stacks 08VG. Let Λ be a commutative ring and let X be a space over Λ, with structure morphism G : X ⟶ Y of ringed topoi and with b : Λ̲ ⟶ G⁻¹𝒪_Y the Λ-algebra structure of its base, Λ̲ being the constant sheaf with value Λ on the site of X. Then

L_{X/Y} ≅ L_{𝒪_X/Λ̲}

in D(𝒪_X): the cotangent complex of the morphism agrees with the cotangent complex of the homomorphism of sheaves of rings Λ̲ ⟶ 𝒪_X.

Two hypotheses are carried, both inputs of the source's proof: the fundamental triangle of the tower Λ̲ ⟶ G⁻¹𝒪_Y ⟶ 𝒪_X, in the shape Tag 08V1 carries it, and the acyclicity hv of its first vertex, which is the source's L_q = 0 pulled back to X by firstVertexOverInverseImageBaseIso. See the module documentation.

def cotangentComplexOverConstantRingIso
    (b : X.constantRing Λ ⟶ G.toToposHom.inverseImageRing.obj Y.O)
    (S : ShortComplex (CochainComplex (Sheaf.targetModules.{u, v, w} X.J X.O) ℤ))
    (hS : S.ShortExact)
    (e₁ : S.X₁ ≅ firstVertexOverBase G b)
    (e₂ : S.X₂ ≅ cotangentComplexOverBase G b)
    (e₃ : S.X₃ ≅ G.cotangentComplex)
    (hv : IsZero (DerivedCategory.Q.obj (firstVertexOverBase G b))) :
    G.cotangentComplexDerived ≅ DerivedCategory.Q.obj (cotangentComplexOverBase G b)

AlgebraicGeometry.Space.cotangentComplexOverConstantSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/ConstantBaseRing.lean, line 759. The attribute's comment: “an isomorphism in D(𝒪_X), as the source's proof produces. Λ̲ is Mathlib's constantSheaf with value Λ on X_et, and Λ̲ ⟶ 𝒪_X is the canonical map, adjoint to the structure map Λ → Γ(X, 𝒪_X), global sections being taken at the terminal object of the spaces-étale site of X (Stacks 03G1). Both cotangent complexes are formed after lifting sections to universe u + 1 (SheafOfModules.sheafULift), the universe in which Tag 08VD defines L_{X/Spec Λ}.”.

Let Λ be a ring and X an algebraic space over Λ, with structure morphism p : X ⟶ Spec Λ. Let Λ̲ be the constant sheaf with value Λ on X_et and Λ̲ ⟶ 𝒪_X its canonical map, the one adjoint to the structure map Λ → Γ(X, 𝒪_X) (AlgebraicGeometry.Space.constantStructureMapOfSpace). Then the cotangent complex of Λ̲ ⟶ 𝒪_X is isomorphic in D(𝒪_X) to the cotangent complex L_{X/Spec Λ} of Tag 08VD.

The tower Λ̲ ⟶ p⁻¹𝒪_{Spec Λ} ⟶ 𝒪_X composes to the canonical map (AlgebraicGeometry.Space.towerConstantLower_comp_towerUpper); its fundamental triangle (Tag 08SZ) has first vertex L_{p⁻¹𝒪/Λ̲} ⊗ 𝒪_X, which vanishes stalkwise: at a geometric point its stalk is the base change of the cotangent complex of the germ map Λ → 𝒪_{Spec Λ, p(x̄)}, a strict henselization of a localization of Λ (Tags 04KF, 08R2).

def cotangentComplexOverConstantSheafIso
    [HasDerivedCategory.{t} (smallEtaleModulesULift B (Spec (CommRingCat.of Λ)) hS X)] :
    DerivedCategory.Q.obj (CategoryTheory.Sheaf.cotangentComplex.{u + 1, u, u}
        (smallEtaleRingedTopos B (Spec (CommRingCat.of Λ)) hS X).J
        ((SheafOfModules.sheafULift.{u, u + 1, u}
          (smallEtaleRingedTopos B (Spec (CommRingCat.of Λ)) hS X).J).map
          (constantStructureMapOfSpace Λ B hS X))) ≅
      cotangentComplexDerived B (Spec (CommRingCat.of Λ)) hS (structureToSpec Λ B hS X)

Sources

LeanAlgebraicGeometry.Space.cotangentComplex · AlgebraicGeometry.Space.cotangentComplexDerived · AlgebraicGeometry.Space.etaleRestrictionCotangentComplexIso · AlgebraicGeometry.Space.quasiIso_representedCotangentComparison · AlgebraicGeometry.Space.representedCotangentComplexDerivedIso · AlgebraicGeometry.RingedToposHom.cotangentComplexOverConstantRingIso · AlgebraicGeometry.Space.cotangentComplexOverConstantSheafIso

Section92.27 The cotangent complex of an algebraic space over a ring #

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

Tag 08VI, an equation

Tag 08VI in the Stacks Project.

AlgebraicGeometry.Space.PolynomialChart, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialChartSpace.lean, line 77. The attribute's comment: “the objects of the category C_{X/Λ}”.

A commutative square U ⟶ A ⟶ Spec Λ, U ⟶ X ⟶ Spec Λ, in which U ⟶ X is an object of the small étale site of the algebraic space X and A is an affine space over Spec Λ.

structure PolynomialChart (hX : IsAlgebraicSpace B (Spec (CommRingCat.of Λ)) hS X)

AlgebraicGeometry.Space.PolynomialChart.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialChartSpace.lean, line 108. The attribute's comment: “the morphisms of the category C_{X/Λ}”.

A morphism of polynomial charts is a commutative diagram over both the algebraic space X and Spec Λ.

structure Hom (P Q : PolynomialChart Λ B hS X hX)

AlgebraicGeometry.Space.PolynomialChart.openFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialChartSpace.lean, line 147. The attribute's comment: “the forgetful functor to the small étale site”.

The functor sending a polynomial chart (U ⟶ A) to the object U ⟶ X of the small étale site of X.

def openFunctor :
    PolynomialChart Λ B hS X hX ⥤ SmallEtale B (Spec (CommRingCat.of Λ)) hS X

Tag 08VJ, a lemma

Tag 08VJ in the Stacks Project.

AlgebraicGeometry.Space.PolynomialChart.openFunctor_isFibered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/PolynomialChartSpaceFibred.lean, line 115.

Stacks 08VJ. The category C_{X/Λ} of polynomial charts of an algebraic space X over Λ is fibred over the small étale site of X.

noncomputable instance openFunctor_isFibered (Λ : Type u) [CommRing Λ] (B : BigFppfSite.{u})
    (hS : B.Contains (Spec (CommRingCat.of Λ)))
    (X : (BigFppfOver B (Spec (CommRingCat.of Λ)) hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (CommRingCat.of Λ)) hS X) :
    (openFunctor (Λ := Λ) (B := B) (hS := hS) (X := X) (hX := hX)).IsFibered

Tag 08VK, an equation

Tag 08VK in the Stacks Project.

AlgebraicGeometry.Space.PolynomialChart.piSpacesDiagram, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/PolynomialChartSpaceRingedTopoi.lean, line 620.

The diagram of ringed topoi of the polynomial charts of an algebraic space over a ring, with all of its arrows pinned to the canonical ones.

def piSpacesDiagram [HasWeakSheafify (topology Λ B hS X hX) CommRingCat.{u}] :
    PiSpacesDiagram Λ B hS X hX

Tag 08VL, a remark

Tag 08VL in the Stacks Project.

AlgebraicGeometry.Space.PolynomialChart.standardResolutionChart_computes_derivedAbelianLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/PolynomialChartSpaceStandardResolution.lean, line 253.

Stacks 08VL. Let X be an algebraic space over a ring Λ, let C_{X/Λ} be its category of polynomial charts, fibred over X_étale, and let π : Sh(C_{X/Λ}) ⟶ Sh(X_étale) be the induced morphism of topoi. For an object U of X_étale let P_{•,U} be the standard resolution of 𝒪_X(U) over Λ and 𝐀_{•,U} = Spec(P_{•,U}) (standardResolutionChart). Then:

the fibre of C_{X/Λ} over U is the site C_{𝒪_X(U)/Λ}, and through this identification 𝐀_{•,U} is the cosimplicial object of P_{•,U};

𝐀_{•,U} is a cosimplicial object of the fibre over U, functorially in U;

it is a cosimplicial object as in Cohomology on Sites, Lemma 08Q9: every simplicial set Mor(𝐀_{•,U}, W) is homotopy equivalent to a singleton;

for every abelian sheaf ℱ on C_{X/Λ}, the homology at U of the complex of presheaves U ↦ ℱ(𝐀_{•,U}) is the homology H_n(C_U, ℱ|_{C_U}) of ℱ on the fibre category;

its sheafified homology computes L_nπ_!(ℱ);

the complex of sheaves whose term in degree -n is the sheafification of U ↦ ℱ(𝐀_{n,U}) computes Lπ_!(ℱ).

theorem standardResolutionChart_computes_derivedAbelianLowerShriek :
    (∀ U : SmallEtale B (Spec (CommRingCat.of Λ)) hS X,
      ∃ e : (openFunctor (Λ := Λ) (B := B) (hS := hS) (X := X) (hX := hX)).Fiber U ≌
          CommAlgCat.polynomialSite Λ (sectionsAlgebra Λ B hS X U),
        Nonempty (standardChartCosimplicialObject Λ B hS X hX U ⋙ e.functor ≅
          CommAlgCat.resolutionCosimplicialObject
            (CommAlgCat.standardResolution.{u, u} Λ (sectionsAlgebra Λ B hS X U)).hom
            (CommAlgCat.standardResolution_isResolution.{u, u} Λ
              (sectionsAlgebra Λ B hS X U)).isPolynomialAlgebra)) ∧
    (standardResolutionChart Λ B hS X hX : (fibredCategorySituation Λ B hS X hX).base.C ⥤
        CosimplicialObject (fibredCategorySituation Λ B hS X hX).C) ⋙
      (Functor.whiskeringRight SimplexCategory (fibredCategorySituation Λ B hS X hX).C
        (fibredCategorySituation Λ B hS X hX).base.C).obj
          (fibredCategorySituation Λ B hS X hX).p =
      Functor.const SimplexCategory ∧
    (∀ (U : (fibredCategorySituation Λ B hS X hX).base.C)
      (W : (fibredCategorySituation Λ B hS X hX).p.Fiber U),
      ∃ f : (Functor.Fiber.inducedFunctor (Functor.congr_obj
            (standardResolutionChart_comp_whiskeringRight Λ B hS X hX) U)).op ⋙
            yoneda.obj W ⟶
          (Functor.const SimplexCategoryᵒᵖ).obj PUnit.{u + 1},
        SimplicialObject.homotopyEquivalences (Type u) f) ∧
    ∀ F : Sheaf (fibredCategorySituation Λ B hS X hX).topology AddCommGrpCat.{u + 1},
      (∀ (U : (fibredCategorySituation Λ B hS X hX).base.C) (n : ℕ),
        Nonempty (((((fibredCategorySituation Λ B hS X hX).pointMooreComplex
            (standardResolutionChart Λ B hS X hX)).obj F.obj).homology n).obj (op U) ≅
          Stacks.CategoryHomology.categoryHomology.{u + 1, u + 1}
            ((fibredCategorySituation Λ B hS X hX).smallFiberRestriction F.obj U) n)) ∧
      (∀ n : ℕ, Nonempty ((DerivedCategory.homologyFunctor _ (-(n : ℤ))).obj
          ((fibredCategorySituation Λ B hS X hX).derivedAbelianLowerShriek.obj
            ((DerivedCategory.singleFunctor _ 0).obj F)) ≅
        (presheafToSheaf (fibredCategorySituation Λ B hS X hX).base.J AddCommGrpCat.{u + 1}).obj
          ((((fibredCategorySituation Λ B hS X hX).pointMooreComplex
            (standardResolutionChart Λ B hS X hX)).obj F.obj).homology n))) ∧
      Nonempty ((fibredCategorySituation Λ B hS X hX).derivedAbelianLowerShriek.obj
          ((DerivedCategory.singleFunctor _ 0).obj F) ≅
        DerivedCategory.Q.obj ((fibredCategorySituation Λ B hS X hX).pointSheafComplex
          (standardResolutionChart Λ B hS X hX) F.obj))

Tag 08VM, a lemma

Tag 08VM in the Stacks Project.

AlgebraicGeometry.Space.PolynomialChart.derivedLowerShriekInverseImageDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/SpaceCotangentChartSite.lean, line 193. The attribute's comment: “second isomorphism Lπ_!(Li^Ω_{𝒪/Λ̲}) = Lπ_!(i^Ω_{𝒪/Λ̲}) for an algebraic space X over Λ, induced by the canonical map Li^Ω ⟶ i^Ω, an isomorphism since Ω_{𝒪/Λ̲} is flat”.

Stacks Project, Tag 08VM, the second isomorphism Lπ_!(Li^*Ω_{𝒪/Λ̲}) ≅ Lπ_!(i^*Ω_{𝒪/Λ̲}): Lπ_! applied to the canonical map Li^*Ω_{𝒪/Λ̲} ⟶ i^*Ω_{𝒪/Λ̲}, an isomorphism because Ω_{𝒪/Λ̲} is a flat 𝒪-module (derivedHorizontalInverseImageDifferentialsIso).

def derivedLowerShriekInverseImageDifferentialsIso :
    (chartDerivedLowerShriek Λ B hS X hX).obj
        ((derivedHorizontalInverseImage Λ B hS X hX).obj
          ((DerivedCategory.singleFunctor _ 0).obj (chartDifferentials Λ B hS X hX))) ≅
      (chartDerivedLowerShriek Λ B hS X hX).obj
        ((DerivedCategory.singleFunctor _ 0).obj (pulledBackDifferentials Λ B hS X hX))

AlgebraicGeometry.Space.PolynomialChart.derivedLowerShriekPulledBackDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/SpaceCotangentChartSite.lean, line 208. The attribute's comment: “third isomorphism Lπ_!(i^Ω_{𝒪/Λ̲}) = Lπ_!(Ω_{𝒪/Λ̲} ⊗_𝒪 𝒪̲_X) for an algebraic space X over Λ, induced by the canonical identification of i^ with extension of scalars along i♯”.

Stacks Project, Tag 08VM, the third isomorphism Lπ_!(i^*Ω_{𝒪/Λ̲}) ≅ Lπ_!(Ω_{𝒪/Λ̲} ⊗_𝒪 𝒪̲_X): Lπ_! applied to the canonical identification of the pullback i^*Ω_{𝒪/Λ̲} with the extension of scalars of Ω_{𝒪/Λ̲} along i♯ (pulledBackDifferentialsIsoBaseChange).

def derivedLowerShriekPulledBackDifferentialsIso :
    (chartDerivedLowerShriek Λ B hS X hX).obj
        ((DerivedCategory.singleFunctor _ 0).obj (pulledBackDifferentials Λ B hS X hX)) ≅
      (chartDerivedLowerShriek Λ B hS X hX).obj
        ((DerivedCategory.singleFunctor _ 0).obj (chartDifferentialsBaseChange Λ B hS X hX))

AlgebraicGeometry.Space.PolynomialChart.cotangentComplexIsoDerivedLowerShriekInverseImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/SpaceCotangentChartSite.lean, line 266. The attribute's comment: “first isomorphism L_{X/Λ} = Lπ_!(Li^*Ω_{𝒪/Λ̲}) in D(𝒪_X), for the site of polynomial charts of an algebraic space X over a ring Λ, with L_{X/Λ} the cotangent complex of X ⟶ Spec Λ (Tag 08VD, sections lifted to the universe of the site); built from the canonical maps of the proof: flatness of Ω, Tag 08VL, Tag 08SX and Tag 08VG”.

Stacks Project, Tag 08VM, the first isomorphism L_{X/Λ} ≅ Lπ_!(Li^*Ω_{𝒪/Λ̲}) in D(𝒪_X), for the site of polynomial charts of Section 08VJ of an algebraic space X over a ring Λ. Here L_{X/Λ} = L_{X/Spec Λ} is the cotangent complex of the structure morphism (AlgebraicGeometry.Space.cotangentComplexDerived, Tag 08VD); Ω_{𝒪/Λ̲} is chartDifferentials; Li^* is derivedHorizontalInverseImage; and Lπ_! is chartDerivedLowerShriek.

It is the composite of the canonical maps of the source's proof, read from right to left: Li^*Ω ⟶ i^*Ω (an isomorphism because Ω_{𝒪/Λ̲} is flat), i^*Ω ≅ Ω ⊗_𝒪 𝒪̲_X, the identification of Lπ_!(Ω ⊗_𝒪 𝒪̲_X) with the complex of the standard resolutions (Tag 08VL at module coefficients), the identification of that complex with the sheafification of U ↦ L_{𝒪_X(U)/Λ} and with L_{𝒪_X/Λ̲} (Tag 08SX), and the isomorphism L_{𝒪_X/Λ̲} ≅ L_{X/Spec Λ} of Tag 08VG for the canonical map Λ̲ ⟶ 𝒪_X, which restricts on sections to the structure maps of the étale charts (toSheafify_comp_constantStructureMapOfSpace).

def cotangentComplexIsoDerivedLowerShriekInverseImage :
    cotangentComplexDerived B (Spec (CommRingCat.of Λ)) hS (structureToSpec Λ B hS ⟨X, hX⟩) ≅
      (chartDerivedLowerShriek Λ B hS X hX).obj
        ((derivedHorizontalInverseImage Λ B hS X hX).obj
          ((DerivedCategory.singleFunctor _ 0).obj (chartDifferentials Λ B hS X hX)))

Sources

Section92.28 Fibre products of algebraic spaces and the cotangent complex #

Section 92.28 of the Stacks Project, Tag 09DJ. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09DK, an equation

Tag 09DK in the Stacks Project.

CategoryTheory.Triangulated.nonempty_upperRightCorner, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/UpperRightCorner.lean, line 160. The attribute's comment: “existence of the upper right corner, in a triangulated category”.

Stacks 09DK. Two distinguished triangles sharing their middle vertex have an upper right corner: an object E turning both the top row A₁ ⟶ C₂ ⟶ E and the right column A₂ ⟶ C₁ ⟶ E of the diagram into distinguished triangles, with the remaining square commutative.

This is the nine diagram of Tag 05R0 applied to the lower left square of the diagram, whose left column and bottom row are the contractible triangles 0 ⟶ A₁ ⟶ A₁ and 0 ⟶ A₂ ⟶ A₂; the square commutes because both of its composites leave a zero object. The identity second arrow of each contractible triangle is what identifies the first arrow of the third row with α₁ ≫ β₂ and the first arrow of the third column with α₂ ≫ β₁.

theorem nonempty_upperRightCorner (h₁ : Triangle.mk α₁ β₁ γ₁ ∈ distTriang D)
    (h₂ : Triangle.mk α₂ β₂ γ₂ ∈ distTriang D) :
    Nonempty (UpperRightCorner α₁ β₁ α₂ β₂)

CategoryTheory.Triangulated.UpperRightCorner.ofBiprodCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Triangulated/UpperRightCorner.lean, line 180. The attribute's comment: “the cone of the direct sum as an upper right corner, in a triangulated category”.

Stacks 09DK. Any cone of the map A₁ ⊞ A₂ ⟶ M out of the direct sum, with components the first arrows α₁ and α₂ of the two given triangles, is an upper right corner.

The two arrows into the cone come from the octahedron axiom for the two factorizations of biprod.desc α₁ α₂ through the biproduct inclusions: factoring through biprod.inr has A₁ as the cone of the first map and C₂ as the cone of the composite, so the octahedron is the top row, and factoring through biprod.inl has A₂ and C₁, so the octahedron is the right column. In each case the first arrow of the octahedron becomes the required composite after precomposition with the complementary inclusion.

noncomputable def UpperRightCorner.ofBiprodCone (h₁ : Triangle.mk α₁ β₁ γ₁ ∈ distTriang D)
    (h₂ : Triangle.mk α₂ β₂ γ₂ ∈ distTriang D) {E : D} {ε : M ⟶ E}
    {ζ : E ⟶ (A₁ ⊞ A₂)⟦(1 : ℤ)⟧}
    (hE : Triangle.mk (biprod.desc α₁ α₂) ε ζ ∈ distTriang D) :
    UpperRightCorner α₁ β₁ α₂ β₂

AlgebraicGeometry.Space.fibreProductCotangentCorner, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/FibreProductCorner.lean, line 148. The attribute's comment: “the diagram for a commutative square, in particular for the two projections of a fibre product; E is the cone of the map out of the direct sum”.

Stacks 09DK. Let p : W ⟶ X and q : W ⟶ Y be morphisms of algebraic spaces over S with p ≫ f = q ≫ g for morphisms f : X ⟶ Z and g : Y ⟶ Z, for instance the two projections of W = X ×_Z Y. In D(𝒪_W) the diagram
Lp^*L_{X/Z} ──────▶ L_{W/Y} ──────▶ E
     ‖                ▲             ▲
Lp^*L_{X/Z} ──────▶ L_{W/Z} ──────▶ L_{W/X}
                      ▲             ▲
                Lq^*L_{Y/Z} ═════ Lq^*L_{Y/Z}
exists: its middle row is the transitivity triangle of Stacks 08V1 for W ⟶ X ⟶ Z, its middle column the one for W ⟶ Y ⟶ Z, and the object E of the upper right corner, with its two incoming and two outgoing arrows, turns the top row and the right column into distinguished triangles and makes the remaining square commute. The value of the definition is that upper right corner, together with the distinguishedness of the two middle triangles and the triangle Lp^*L_{X/Z} ⊕ Lq^*L_{Y/Z} ⟶ L_{W/Z} ⟶ E ⟶, which exhibits E as the cone of the map out of the direct sum.

noncomputable def fibreProductCotangentCorner (h : p ≫ f = q ≫ g) :
    { E : Triangulated.UpperRightCorner (transitivityUnit p f) (transitivityCounit p f)
          (fibreProductColumnUnit h) (fibreProductColumnCounit h) //
      (∃ δ : cotangentComplexDerived B S hS p ⟶
          ((derivedPullbackULift p).obj (cotangentComplexDerived B S hS f))⟦(1 : ℤ)⟧,
        Triangle.mk (transitivityUnit p f) (transitivityCounit p f) δ ∈
          distTriang (DerivedCategory (smallEtaleModulesULift B S hS W))) ∧
      (∃ δ : cotangentComplexDerived B S hS q ⟶
          ((derivedPullbackULift q).obj (cotangentComplexDerived B S hS g))⟦(1 : ℤ)⟧,
        Triangle.mk (fibreProductColumnUnit h) (fibreProductColumnCounit h) δ ∈
          distTriang (DerivedCategory (smallEtaleModulesULift B S hS W))) ∧
      ∃ (ε : cotangentComplexDerived B S hS (p ≫ f) ⟶ E.obj)
        (ζ : E.obj ⟶ ((derivedPullbackULift p).obj (cotangentComplexDerived B S hS f) ⊞
          (derivedPullbackULift q).obj (cotangentComplexDerived B S hS g))⟦(1 : ℤ)⟧),
        Triangle.mk (fibreProductBiprodMap h) ε ζ ∈
          distTriang (DerivedCategory (smallEtaleModulesULift B S hS W)) }

AlgebraicGeometry.Space.fiberProductCotangentCorner, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/FibreProductCorner.lean, line 182. The attribute's comment: “the diagram for the fibre product X ×_Z Y and its two projections”.

Stacks 09DK, for the fibre product X ×_Z Y of algebraic spaces (Stacks 02X2) with its projections p and q: the diagram of AlgebraicGeometry.Space.fibreProductCotangentCorner in D(𝒪_{X ×_Z Y}), built on the transitivity triangles of X ×_Z Y ⟶ X ⟶ Z and X ×_Z Y ⟶ Y ⟶ Z.

noncomputable def fiberProductCotangentCorner

Tag 09DL, a lemma

Tag 09DL in the Stacks Project.

AlgebraicGeometry.Space.fiberProduct_cotangentComplex_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/FibreProductTorIndependent.lean, line 332.

Stacks 09DL. Let X ⟶ Z and Y ⟶ Z be morphisms of algebraic spaces over S, and let W = X ×_Z Y with projections p and q. If X and Y are Tor independent over Z, then the object E of Stacks 09DK, i.e. any object fitting into the upper right corner of its diagram, is zero, and the canonical map Lp^*L_{X/Z} ⊕ Lq^*L_{Y/Z} ⟶ L_{W/Z} is an isomorphism, so that L_{X ×_Z Y/Z} ≅ Lp^*L_{X/Z} ⊕ Lq^*L_{Y/Z}.

theorem fiberProduct_cotangentComplex_of_torIndependent (f : X ⟶ Z) (g : Y ⟶ Z)
    (hTor : TorIndependent X.2 Y.2 Z.2 f.hom g.hom) :
    (∀ E : Triangulated.UpperRightCorner (transitivityUnit (ObjectProperty.homMk (pullback.fst
        f.hom g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ X) f) (transitivityCounit
            (ObjectProperty.homMk (pullback.fst f.hom g.hom) : (AlgebraicSpaces.fiberProduct B S hS
                f g) ⟶ X) f)
      (fibreProductColumnUnit (AlgebraicSpaces.isPullback_fiberProduct B S hS f g).w)
      (fibreProductColumnCounit (AlgebraicSpaces.isPullback_fiberProduct B S hS f g).w),
      IsZero E.obj) ∧
    IsIso (fibreProductBiprodMap (AlgebraicSpaces.isPullback_fiberProduct B S hS f g).w)

Tag 09DM, a lemma

Tag 09DM in the Stacks Project.

AlgebraicGeometry.Space.upperRightCorner_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/FibreProductCornerCohomology.lean, line 303. The attribute's comment: “for every cartesian square of algebraic spaces, in particular for the fibre product with its two projections (fiberProduct_upperRightCorner_homology), and every object E fitting into the upper right corner of the diagram of 09DK”.

Stacks 09DM, for a cartesian square. Let p : W ⟶ X, q : W ⟶ Y, f : X ⟶ Z, g : Y ⟶ Z be a cartesian square of algebraic spaces over S and let E be an object fitting into the upper right corner of the diagram of Stacks 09DK. Then H^0(E) = H^{-1}(E) = 0, and at every geometric point w̄ of W, with R = 𝒪_{Z, f(p(w̄))}, A = 𝒪_{X, p(w̄)}, B = 𝒪_{Y, q(w̄)} and C = 𝒪_{W, w̄} the étale local rings and the canonical maps between them, H^{-2}(E)_{w̄} ≅ Tor_1^R(A, B) ⊗_{A ⊗_R B} C as C-modules, χ : A ⊗_R B → C being the map induced by the canonical maps A → C and B → C. The stalk H^{-2}(E)_{w̄} is a module over the stalk of the structure sheaf, which is identified with C by AlgebraicGeometry.Space.smallEtaleStructureSheafULiftStalkEquiv.

theorem upperRightCorner_homology (hpb : IsPullback p q f g)
    (E : Triangulated.UpperRightCorner (transitivityUnit p f) (transitivityCounit p f)
      (fibreProductColumnUnit hpb.w) (fibreProductColumnCounit hpb.w)) :
    IsZero ((DerivedCategory.homologyFunctor (smallEtaleModulesULift B S hS W) 0).obj E.obj) ∧
    IsZero ((DerivedCategory.homologyFunctor (smallEtaleModulesULift B S hS W) (-1)).obj E.obj) ∧
    ∀ w : GeometricPoint B S hS W.1,
    letI : Algebra (etaleLocalRing B S hS Z.1 (geometricPointMap f.hom (geometricPointMap p.hom w)))
        (etaleLocalRing B S hS X.1 (geometricPointMap p.hom w)) :=
      (etaleLocalRingMap X.2 f.hom (geometricPointMap p.hom w)).toAlgebra
    letI : Algebra (etaleLocalRing B S hS Z.1 (geometricPointMap f.hom (geometricPointMap p.hom w)))
        (etaleLocalRing B S hS Y.1 (geometricPointMap q.hom w)) :=
      ((eqToHom (congrArg (etaleLocalRing B S hS Z.1)
          (congrArg (fun k : W ⟶ Z => geometricPointMap k.hom w) hpb.w)) ≫
        CommRingCat.ofHom (etaleLocalRingMap Y.2 g.hom (geometricPointMap q.hom w))).hom).toAlgebra
    ∃ χ : etaleLocalRing B S hS X.1 (geometricPointMap p.hom w) ⊗[etaleLocalRing B S hS Z.1
        (geometricPointMap f.hom (geometricPointMap p.hom w))]
        etaleLocalRing B S hS Y.1 (geometricPointMap q.hom w) →+* etaleLocalRing B S hS W.1 w,
      χ.comp Algebra.TensorProduct.includeLeftRingHom = etaleLocalRingMap W.2 p.hom w ∧
      χ.comp Algebra.TensorProduct.includeRight.toRingHom = etaleLocalRingMap W.2 q.hom w ∧
      Nonempty ((ModuleCat.extendScalars.{u + 1, u + 1, u + 1}
          (smallEtaleStructureSheafULiftStalkEquiv B S hS W w).toRingHom).obj
          ((Stacks.sheafModuleFiberOfCommRing (geometricSitePoint B S hS W w)
            (smallEtaleStructureSheafULift B S hS W)).obj
            ((DerivedCategory.homologyFunctor (smallEtaleModulesULift B S hS W) (-2)).obj E.obj)) ≅
        (ModuleCat.extendScalars.{u + 1, u + 1, u + 1} χ).obj
          (CommAlgCat.torOneTensorProductModule _ _ _))

AlgebraicGeometry.Space.fiberProduct_upperRightCorner_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Spaces/FibreProductCornerCohomology.lean, line 346. The attribute's comment: “for the fibre product X ×_Z Y with its two projections and every object E fitting into the upper right corner of the diagram of 09DK: H^0(E) = H^{-1}(E) = 0, and H^{-2}(E)_w ≅ Tor_1^R(A, B) ⊗_{A ⊗_R B} C as C-modules for the etale local rings R, A, B, C”.

Stacks 09DM. Let X ⟶ Z and Y ⟶ Z be morphisms of algebraic spaces over S, let W = X ×_Z Y with projections p and q, and let E be the object of Stacks 09DK, i.e. any object fitting into the upper right corner of its diagram. Then H^0(E) = H^{-1}(E) = 0, and for a geometric point w̄ of W, H^{-2}(E)_{w̄} ≅ Tor_1^R(A, B) ⊗_{A ⊗_R B} C as C-modules, where R = 𝒪_{Z, f(p(w̄))}, A = 𝒪_{X, p(w̄)}, B = 𝒪_{Y, q(w̄)} and C = 𝒪_{W, w̄} are the étale local rings, Tor_1^R(A, B) carries its canonical A ⊗_R B-module structure, and χ : A ⊗_R B → C is the map induced by the canonical maps of étale local rings.

theorem fiberProduct_upperRightCorner_homology (f : X ⟶ Z) (g : Y ⟶ Z) :
    ∀ E : Triangulated.UpperRightCorner (transitivityUnit (ObjectProperty.homMk (pullback.fst f.hom
        g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ X) f) (transitivityCounit
            (ObjectProperty.homMk (pullback.fst f.hom g.hom) : (AlgebraicSpaces.fiberProduct B S hS
                f g) ⟶ X) f)
      (fibreProductColumnUnit (AlgebraicSpaces.isPullback_fiberProduct B S hS f g).w)
      (fibreProductColumnCounit (AlgebraicSpaces.isPullback_fiberProduct B S hS f g).w),
      IsZero ((DerivedCategory.homologyFunctor (smallEtaleModulesULift B S hS
          (AlgebraicSpaces.fiberProduct B S hS f g)) 0).obj E.obj) ∧
      IsZero ((DerivedCategory.homologyFunctor (smallEtaleModulesULift B S hS
          (AlgebraicSpaces.fiberProduct B S hS f g)) (-1)).obj E.obj) ∧
      ∀ w : GeometricPoint B S hS (AlgebraicSpaces.fiberProduct B S hS f g).1,
      letI : Algebra (etaleLocalRing B S hS Z.1 (geometricPointMap f.hom (geometricPointMap
          (ObjectProperty.homMk (pullback.fst f.hom g.hom) : (AlgebraicSpaces.fiberProduct B S hS f
              g) ⟶ X).hom w)))
          (etaleLocalRing B S hS X.1 (geometricPointMap (ObjectProperty.homMk (pullback.fst f.hom
              g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ X).hom w)) :=
        (etaleLocalRingMap X.2 f.hom (geometricPointMap (ObjectProperty.homMk (pullback.fst f.hom
            g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ X).hom w)).toAlgebra
      letI : Algebra (etaleLocalRing B S hS Z.1 (geometricPointMap f.hom (geometricPointMap
          (ObjectProperty.homMk (pullback.fst f.hom g.hom) : (AlgebraicSpaces.fiberProduct B S hS f
              g) ⟶ X).hom w)))
          (etaleLocalRing B S hS Y.1 (geometricPointMap (ObjectProperty.homMk (pullback.snd f.hom
              g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ Y).hom w)) :=
        ((eqToHom (congrArg (etaleLocalRing B S hS Z.1)
            (congrArg (fun k : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ Z => geometricPointMap
                k.hom w) (AlgebraicSpaces.isPullback_fiberProduct B S hS f g).w)) ≫
          CommRingCat.ofHom (etaleLocalRingMap Y.2 g.hom (geometricPointMap (ObjectProperty.homMk
              (pullback.snd f.hom g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ Y).hom
                  w))).hom).toAlgebra
      ∃ χ : etaleLocalRing B S hS X.1 (geometricPointMap (ObjectProperty.homMk (pullback.fst f.hom
          g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ X).hom w) ⊗[etaleLocalRing B S hS Z.1
          (geometricPointMap f.hom (geometricPointMap (ObjectProperty.homMk (pullback.fst f.hom
              g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ X).hom w))]
          etaleLocalRing B S hS Y.1 (geometricPointMap (ObjectProperty.homMk (pullback.snd f.hom
              g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ Y).hom w) →+* etaleLocalRing B S
                  hS (AlgebraicSpaces.fiberProduct B S hS f g).1 w,
        χ.comp Algebra.TensorProduct.includeLeftRingHom = etaleLocalRingMap
            (AlgebraicSpaces.fiberProduct B S hS f g).2 (ObjectProperty.homMk (pullback.fst f.hom
                g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ X).hom w ∧
        χ.comp Algebra.TensorProduct.includeRight.toRingHom = etaleLocalRingMap
            (AlgebraicSpaces.fiberProduct B S hS f g).2 (ObjectProperty.homMk (pullback.snd f.hom
                g.hom) : (AlgebraicSpaces.fiberProduct B S hS f g) ⟶ Y).hom w ∧
        Nonempty ((ModuleCat.extendScalars.{u + 1, u + 1, u + 1}
            (smallEtaleStructureSheafULiftStalkEquiv B S hS (AlgebraicSpaces.fiberProduct B S hS f
                g) w).toRingHom).obj
            ((Stacks.sheafModuleFiberOfCommRing (geometricSitePoint B S hS
                (AlgebraicSpaces.fiberProduct B S hS f g) w)
              (smallEtaleStructureSheafULift B S hS (AlgebraicSpaces.fiberProduct B S hS f g))).obj
              ((DerivedCategory.homologyFunctor (smallEtaleModulesULift B S hS
                  (AlgebraicSpaces.fiberProduct B S hS f g)) (-2)).obj E.obj)) ≅
          (ModuleCat.extendScalars.{u + 1, u + 1, u + 1} χ).obj
            (CommAlgCat.torOneTensorProductModule _ _ _))

Sources

LeanCategoryTheory.Triangulated.nonempty_upperRightCorner · CategoryTheory.Triangulated.UpperRightCorner.ofBiprodCone · AlgebraicGeometry.Space.fibreProductCotangentCorner · AlgebraicGeometry.Space.fiberProductCotangentCorner · AlgebraicGeometry.Space.fiberProduct_cotangentComplex_of_torIndependent · AlgebraicGeometry.Space.upperRightCorner_homology · AlgebraicGeometry.Space.fiberProduct_upperRightCorner_homology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

92.18 The cotangent complex to 92.28 Fibre products of…

Section92.18 The cotangent complex#

Tag 08SR, a definition

Tag 08SS, a definition

Tag 08SV, a lemma

Tag 08SW, a lemma

Tag 08SX, a remark

Tag 08UR, a lemma

Tag 08SY, a lemma

Tag 08SZ, a lemma

Tag 08T0, a lemma

Tag 08US, a lemma

Sources

Section92.19 The Atiyah class of a sheaf of modules#

Tag 09DG, an equation

Tag 09DH, an equation

Tag 09DI, a definition

Sources

Section92.20 The cotangent complex of a morphism of ringed spaces#

Tag 08UU, a definition

Tag 08UV, a lemma

Tag 08T4, a lemma

Tag 08UW, a lemma

Sources

Section92.21 Deformations of ringed spaces and the cotangent complex#

Tag 08UY, an equation

Tag 08UZ, a lemma

Sources

Section92.22 The cotangent complex of a morphism of ringed topoi#

Tag 08SU, a definition

Tag 08V0, a lemma

Tag 08V1, a lemma

Tag 08V2, a lemma

Sources

Section92.23 Deformations of ringed topoi and the cotangent complex#

Tag 08V4, an equation

Tag 08V5, a lemma

Sources

Section92.24 The cotangent complex of a morphism of schemes#

Tag 08T2, a definition

Tag 08T3, a lemma

Tag 08V6, a lemma

Sources

Section92.25 The cotangent complex of a scheme over a ring#

Tag 08V8, an equation

Tag 08V9, a lemma

Tag 08VA, an equation

Tag 08VB, a remark

Tag 08T9, a lemma

Sources

Section92.26 The cotangent complex of a morphism of algebraic spaces#

Tag 08VD, a definition

Tag 08VE, a lemma

Tag 08VF, a lemma

Tag 08VG, a lemma

Sources

Section92.27 The cotangent complex of an algebraic space over a ring#

Tag 08VI, an equation

Tag 08VJ, a lemma

Tag 08VK, an equation

Tag 08VL, a remark

Tag 08VM, a lemma

Sources

Section92.28 Fibre products of algebraic spaces and the cotangent complex#

Tag 09DK, an equation

Tag 09DL, a lemma

Tag 09DM, a lemma

Sources

Section92.18 The cotangent complex #

Section92.19 The Atiyah class of a sheaf of modules #

Section92.20 The cotangent complex of a morphism of ringed spaces #

Section92.21 Deformations of ringed spaces and the cotangent complex #

Section92.22 The cotangent complex of a morphism of ringed topoi #

Section92.23 Deformations of ringed topoi and the cotangent complex #

Section92.24 The cotangent complex of a morphism of schemes #

Section92.25 The cotangent complex of a scheme over a ring #

Section92.26 The cotangent complex of a morphism of algebraic spaces #

Section92.27 The cotangent complex of an algebraic space over a ring #

Section92.28 Fibre products of algebraic spaces and the cotangent complex #