92.3 The cotangent complex of a… to 92.7 The fundamental triangle

Section92.3 The cotangent complex of a ring map#

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

Tag 08PM, a definition

Tag 08PM in the Stacks Project.

CommAlgCat.standardResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/StandardResolution.lean, line 177.

Stacks Project, Tag 08PM. The standard resolution of the commutative A-algebra B, augmented to B. Its degree n term is the (n + 1)-fold iteration of C ↦ A[C].

noncomputable def standardResolution (A : Type u) [CommRing A]
    (B : CommAlgCat.{max u v} A) : SimplicialObject.Augmented (CommAlgCat.{max u v} A)
Tag 08PN, a definition

Tag 08PN in the Stacks Project.

CommAlgCat.cotangentSimplicialModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Complex.lean, line 304. The attribute's comment: “the simplicial module”.

The canonical simplicial B-module Ω[P•⁄A] ⊗[P•] B.

noncomputable def cotangentSimplicialModule (A : Type u) [CommRing A]
    (B : CommAlgCat.{max u v} A) : CotangentSimplicialModuleData A B

CommAlgCat.cotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Complex.lean, line 335. The attribute's comment: “the associated complex”.

The cotangent complex L_{B/A} associated to the standard resolution.

noncomputable def cotangentComplex (A : Type u) [CommRing A]
    (B : CommAlgCat.{max u v} A) : CochainComplex (ModuleCat.{max u v} B) ℤ
Tag 08PP, a remark

Tag 08PP in the Stacks Project.

CommAlgCat.existsSliceStandardEndofunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SliceStandardResolution.lean, line 245. The attribute's comment: “the standard endofunctor in the slice”.

The comonad of the lifted adjunction has a standard augmented simplicial endofunctor in the category of algebras over B.

theorem existsSliceStandardEndofunctor :
    ∃ X : SimplicialObject.Augmented (Over B ⥤ Over B),
      IsSliceStandardEndofunctor A B X

CommAlgCat.sliceStandardResolution_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SliceStandardResolution.lean, line 320. The attribute's comment: “comparison of standard resolutions”.

Every standard simplicial endofunctor arising from the slice adjunction, evaluated on the identity of B, gives the ordinary augmented standard resolution of B.

theorem sliceStandardResolution_iso
    (X : SimplicialObject.Augmented (Over B ⥤ Over B))
    (hX : IsSliceStandardEndofunctor A B X) :
    Nonempty
      (((SimplicialObject.Augmented.whiskeringObj _ _ (Over.forget B)).obj
        ((SimplicialObject.Augmented.whiskeringObj _ _
        ((evaluation (Over B) (Over B)).obj (Over.mk (𝟙 B)))).obj X)) ≅
        standardResolution A B)

Declarations registered for the tag:

Tag 08S9, a lemma

Tag 08S9 in the Stacks Project.

CommAlgCat.isDirectedColimitOfTypes_cotangentComplexAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/DirectedColimit.lean, line 1057. The attribute's comment: “degreewise”.

Let A i → B i be a system of ring maps over a directed index set I, with Ainf the colimit of the A i and Binf the colimit of the B i. Then in every degree the canonical maps induced by the comparison squares exhibit L_{Binf⁄Ainf} as the directed colimit of the cotangent complexes L_{B i⁄A i}, the transition maps of the system being those induced by the squares of the system; that is, colim L_{B i⁄A i} = L_{colim B i⁄colim A i}.

theorem CommAlgCat.isDirectedColimitOfTypes_cotangentComplexAb
    (hA : IsDirectedColimitOfTypes (fun _ _ h a => (sq h).base a)
      (fun i a => (cocone i).base a))
    (hB : IsDirectedColimitOfTypes (fun _ _ h b => (sq h).map b)
      (fun i b => (cocone i).map b))
    (n : ℤ) :
    IsDirectedColimitOfTypes
      (fun _ _ h a => (CommAlgCat.cotangentComplexAbMap (sq h)).f n a)
      (fun i a => (CommAlgCat.cotangentComplexAbMap (cocone i)).f n a)

CommAlgCat.isColimit_cotangentComplexAbCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/DirectedColimit.lean, line 1270. The attribute's comment: “the colimit of complexes”.

Cotangent complexes commute with directed colimits of ring maps: the cocone of canonical maps L_{B i⁄A i} → L_{Binf⁄Ainf} on the system of canonical maps L_{B i⁄A i} → L_{B j⁄A j} is a colimit cocone.

noncomputable def CommAlgCat.isColimit_cotangentComplexAbCocone :
    IsColimit (CommAlgCat.cotangentComplexAbCocone sq cocone hA hB)
Sources
LeanCommAlgCat.standardResolution · CommAlgCat.cotangentSimplicialModule · CommAlgCat.cotangentComplex · CommAlgCat.existsSliceStandardEndofunctor · CommAlgCat.sliceStandardResolution_iso · CategoryTheory.Over.postAdjunctionRight · CategoryTheory.Over.post_forget_eq_forget_comp · CommAlgCat.isDirectedColimitOfTypes_cotangentComplexAb

Section92.4 Simplicial resolutions and derived lower shriek#

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

Tag 08PR, an equation

Tag 08PR in the Stacks Project.

CommAlgCat.polynomialSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 117. The attribute's comment: “the site C_{B/A}”.

Stacks 08PR. The site C_{B/A}: the opposite of the category of polynomial A-algebras augmented to B. Its topology is the chaotic one, recorded through the ringed point below.

abbrev polynomialSite

CommAlgCat.polynomialTopology_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 133. The attribute's comment: “the chaotic topology on C_{B/A}”.

Stacks 08PR. The topology of C_{B/A} is the chaotic topology: its only coverings are the maximal sieves, so every presheaf on C_{B/A} is a sheaf.

theorem polynomialTopology_eq_bot : polynomialTopology A B = ⊥

CommAlgCat.polynomialStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 155. The attribute's comment: “the structure sheaf 𝒪”.

Stacks 08PR. The tautological sheaf of rings 𝒪 on C_{B/A}, which sends the object (P, α) to P. It is a sheaf because the topology of C_{B/A} is chaotic.

def polynomialStructureSheaf : Sheaf (polynomialTopology A B) CommRingCat.{u + 1}

CommAlgCat.polynomialConstantSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 163. The attribute's comment: “the constant sheaf B”.

Stacks 08PR. The constant sheaf of rings B on C_{B/A}, written with an underline in the source. By Tag 08PF it is the inverse image along π of the ring on the point.

def polynomialConstantSheaf : Sheaf (polynomialTopology A B) CommRingCat.{u + 1}

CommAlgCat.polynomialConstantSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 188. The attribute's comment: “the constant sheaf B is constant”.

Stacks 08PR. The constant sheaf of rings B of Tag 08PF is the constant presheaf with value B.

def polynomialConstantSheafIso :
    (polynomialConstantSheaf A B).obj ≅ polynomialConstantPresheaf A B

CommAlgCat.polynomialAugmentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 219. The attribute's comment: “the augmentation 𝒪 ⟶ B”.

Stacks 08PR. The map of sheaves of rings 𝒪 → B given by the augmentations.

def polynomialAugmentation :
    polynomialStructureSheaf A B ⟶ polynomialConstantSheaf A B

CommAlgCat.polynomialAugmentation_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 228. The attribute's comment: “the augmentation is given by α”.

Stacks 08PR. On sections over the object (P, α) of C_{B/A}, the augmentation of sheaves of rings is α, read through the identification of the constant sheaf with the constant presheaf.

theorem polynomialAugmentation_app (X : polynomialSite A B) :
    (polynomialAugmentation A B).hom.app (Opposite.op X) ≫
        (polynomialConstantSheafIso A B).hom.app (Opposite.op X) =
      (polynomialAugmentationPresheaf A B).app (Opposite.op X)

CommAlgCat.polynomialInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 295. The attribute's comment: “the morphism i of ringed topoi”.

Stacks 08PR. The morphism of ringed topoi i : (Sh(C_{B/A}), B) ⟶ (Sh(C_{B/A}), 𝒪): the identity on underlying topoi, with i♯ : 𝒪 ⟶ i_*B the augmentation.

def polynomialInclusion :
    AlgebraicGeometry.RingedToposHom (polynomialConstantRingedTopos A B)
      (polynomialStructureRingedTopos A B)

CommAlgCat.polynomialInclusion_toToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 303. The attribute's comment: “i is the identity on topoi”.

Stacks 08PR. The geometric morphism underlying i is the identity.

theorem polynomialInclusion_toToposHom :
    (polynomialInclusion A B).toToposHom = polynomialIdentityTopos A B

CommAlgCat.polynomialProjection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSite.lean, line 319. The attribute's comment: “the morphism π of ringed topoi”.

Stacks 08PR. The morphism of ringed topoi π : (Sh(C_{B/A}), B) ⟶ (Sh(*), B), the projection of the chaotic site to its ringed point.

abbrev polynomialProjection

CommAlgCat.boundedPolynomialSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteSmall.lean, line 137. The attribute's comment: “the site C_{B/A} with the section's footnote in force, restricting the sets of variables to cardinality at most κ. The unrestricted version is CommAlgCat.polynomialSite; only this one is essentially small”.

The site C_{B/A} cut down to the polynomial algebras on at most κ variables: the opposite of CommAlgCat.BoundedPolynomialAugmentation. For κ = #B this is the site of the source, footnote included; CommAlgCat.polynomialSite is the same construction with the footnote omitted.

abbrev boundedPolynomialSite
Tag 08PS, a lemma

Tag 08PS in the Stacks Project.

CommAlgCat.exists_homotopyEquivalences_resolutionMor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterion.lean, line 377. The attribute's comment: “the hypothesis of the criterion of Tag 08Q9 for the cosimplicial object of a resolution: each Mor_C((P_•, ε), W) is homotopy equivalent to a singleton. The conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab), resp. D(B), functorially in ℱ, is not asserted: the criterion as formalized asks for a small site, and CommAlgCat.polynomialSite is large — see the first implementation note”.

Stacks 08PS. Let P_• be a simplicial A-algebra endowed with an augmentation ε : P_• ⟶ B, assume every P_n is a polynomial algebra over A and that ε is a trivial Kan fibration on underlying simplicial sets. Then for every object W = (Q, β) of the site C_{B/A} the simplicial set Mor_{C_{B/A}}((P_•, ε), W) is homotopy equivalent to the constant simplicial set on a singleton, which is the hypothesis the criterion of Tag 08Q9 asks of the cosimplicial object CommAlgCat.resolutionCosimplicialObject of the resolution.

theorem exists_homotopyEquivalences_resolutionMor
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A))))
    (W : polynomialSite A B) :
    ∃ f : (resolutionCosimplicialObject ε hP).op ⋙ yoneda.obj W ⟶
        (Functor.const SimplexCategoryᵒᵖ).obj PUnit.{u + 1},
      SimplicialObject.homotopyEquivalences (Type u) f

CommAlgCat.polynomialSiteResolutionDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterionPolynomialSite.lean, line 167. The attribute's comment: “the conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab) functorially in ℱ in Ab(C_{B/A}), at CommAlgCat.polynomialSite -- the site of Tag 08PR itself, not a restriction of it -- as an isomorphism in the derived category, with π_! in its colimit presentation of Tag 08PF and the coefficients at the universe u + 1 of the site's objects”.

Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab), functorially in ℱ, at the site C_{B/A}. Let ε : P_• ⟶ B be a simplicial A-algebra endowed with an augmentation to B, assume every P_n is a polynomial algebra over A and that ε is a trivial Kan fibration on underlying simplicial sets. Then the extended Moore complex of the simplicial abelian group ℱ(P_•, ε) is Lπ_!(ℱ) in D(Ab), as an isomorphism of functors of the abelian sheaf ℱ on the site C_{B/A} of Tag 08PR -- the abelian presheaves being its abelian sheaves, the topology being chaotic.

This is the abelian half of the conclusion of Tag 08PS. The hypothesis of the criterion of Tag 08Q9 is CommAlgCat.isPointResolution_resolutionCosimplicialObject, and Stacks.ChaoticSite.AbelianValued.mooreCochainNatIsoDerivedColimitOfLarge is that criterion in its derived form, natural in the coefficient presheaf and with no smallness hypothesis on the site.

def polynomialSiteResolutionDerivedColimitNatIso
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A)))) :
    Stacks.ChaoticSite.GeneralValued.mooreCochainComplex'
          (resolutionCosimplicialObject ε hP) AddCommGrpCat.{u + 1} ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single ((polynomialSite A B)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
          (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙
          totalDerivedColimit' (polynomialSite A B) AddCommGrpCat.{u + 1}

CommAlgCat.polynomialSiteResolutionModuleDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterionPolynomialSite.lean, line 195. The attribute's comment: “the conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(B) functorially in ℱ in Mod(B̲), at CommAlgCat.polynomialSite -- the site of Tag 08PR itself, not a restriction of it -- as an isomorphism in the derived category, with the coefficient ring read as ULift.{u+1} B exactly as the site's own ringed point CommAlgCat.polynomialRingedPoint reads it”.

Lπ_!(ℱ) = ℱ(P_•, ε) in D(B), functorially in ℱ, at the site C_{B/A}. Under the hypotheses of Tag 08PS, the extended Moore complex of the simplicial B-module ℱ(P_•, ε) is Lπ_!(ℱ) in D(B), as an isomorphism of functors of the sheaf of B-modules ℱ on the site C_{B/A} of Tag 08PR -- the diagrams of B-modules on the site being its B̲-modules, the topology being chaotic.

This is the module half of the conclusion of Tag 08PS, beside the abelian half CommAlgCat.polynomialSiteResolutionDerivedColimitNatIso: the same hypothesis CommAlgCat.isPointResolution_resolutionCosimplicialObject -- which does not mention the coefficients -- is fed to Stacks.ChaoticSite.ModuleValued.mooreCochainNatIsoDerivedColimitOfLarge. The coefficient ring is ULift.{u + 1} B, the ring of the site's ringed point CommAlgCat.polynomialRingedPoint.

def polynomialSiteResolutionModuleDerivedColimitNatIso
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A)))) :
    Stacks.ChaoticSite.GeneralValued.mooreCochainComplex'
          (resolutionCosimplicialObject ε hP)
          (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))) ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single
          ((polynomialSite A B)ᵒᵖ ⥤ ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u)))
          (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙
          totalDerivedColimit' (polynomialSite A B)
            (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u)))

CommAlgCat.smallResolutionModuleLeftDerivedLowerShriekNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterionSmallOfModules.lean, line 58. The attribute's comment: “the conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(B) functorially in ℱ in Mod(B̲), read at the small model of the footnote-restricted site, for the same reason as recorded for the abelian half in StacksFrontier/Cotangent/ResolutionPointCriterionSmall.lean”.

Let ε : P_• ⟶ B be a resolution of B over A whose terms are polynomial algebras on at most κ variables. For every sheaf of B-modules ℱ on the small model of the restricted site C_{B/A}, the sections at the point of L_nπ_!(ℱ) are the degree n homology of the Moore complex of the simplicial B-module ℱ(P_•, ε), naturally in ℱ; here π is the point morphism of the small model.

def smallResolutionModuleLeftDerivedLowerShriekNatIso
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A))))
    (n : ℕ) :
    (modulePointLowerShriek (smallBoundedPolynomialSite A B κ)
          (B : Type u)).leftDerived n ⋙
        Stacks.ChaoticSite.pointSections.{u, u + 1, u} (ModuleCat.{u} (B : Type u)) ≅
      sheafToPresheaf (GrothendieckTopology.trivial (smallBoundedPolynomialSite A B κ))
          (ModuleCat.{u} (B : Type u)) ⋙
        moduleCosimplicialMooreComplex (smallResolutionCosimplicialObject ε κ hPκ) ⋙
          HomologicalComplex.homologyFunctor (ModuleCat.{u} (B : Type u))
            (ComplexShape.down ℕ) n
Tag 08PT, a lemma

Tag 08PT in the Stacks Project.

Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitByPointResolution.lean, line 391. The attribute's comment: “derived form at module coefficients, for one module over the constant sheaf of rings: the extended Moore complex of the evaluation on a point resolution is derived lower shriek in D(B), derived lower shriek being the total left derived functor of the colimit over the index category. Not asserted natural in the coefficient module”.

The derived form of [Stacks, Tag 08PT] at module coefficients. Let C be a small category with the chaotic topology, B a ring, and U_• a cosimplicial object of C such that every simplicial set Mor_C(U_•, W) is homotopy equivalent to a singleton. Then for every diagram ℱ of B-modules on Cᵒᵖ — that is, every B̲-module on the chaotic site — the extended Moore complex of the simplicial B-module ℱ(U_•) computes derived lower shriek:

Q(ℱ(U_•)) ≅ Lπ_!(ℱ) in D(B).

Here Lπ_! is Stacks.CategoryHomology.totalDerivedColimit, the total left derived functor of the colimit over Cᵒᵖ, which is π_! on the chaotic site by [Stacks, Tag 08PF]. The proof compares the two filtrations of the double complex obtained by evaluating a projective resolution of ℱ on U_•.

The isomorphism depends on the chosen projective resolution and is not asserted to be natural in ℱ; see the implementation notes of this module.

def mooreCochainQIsoDerivedColimit (hU : IsPointResolution U) :
    DerivedCategory.Q.obj ((mooreCochainComplex U).obj F) ≅
      (totalDerivedColimit C (ModuleCat.{u} B)).obj
        (DerivedCategory.Q.obj
          ((HomologicalComplex.single (Cᵒᵖ ⥤ ModuleCat.{u} B) (ComplexShape.up ℤ) 0).obj F))

Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/DerivedColimitByPointResolutionNaturality.lean, line 398. The attribute's comment: “the derived form at module coefficients is natural in the point resolution: a morphism of cosimplicial objects between two point resolutions carries the comparison at one to the comparison at the other. Still not asserted natural in the coefficient module”.

The derived form of [Stacks, Tag 08PT] at module coefficients is independent of the point resolution, compatibly with morphisms of point resolutions. For a morphism v : U_• ⟶ V_• of cosimplicial objects of C, both point resolutions, and a diagram ℱ of B-modules on Cᵒᵖ, the triangle

Q(ℱ(V_•)) ⟶ Q(ℱ(U_•)) ⟶ Lπ_!(ℱ)

commutes, the second arrow being Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit at U_• and the composite being the same isomorphism at V_•. This is the totalized form of the canonical map of [Stacks, Tag 08Q6]: the comparison of the extended Moore complex of a point resolution with derived lower shriek does not depend on the point resolution.

The projective resolution of ℱ chosen by Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit is built from ℱ alone, so one and the same resolution serves both point resolutions and the statement is Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimitOfResolution_naturality.

theorem mooreCochainQIsoDerivedColimit_naturality (v : U ⟶ V) (hU : IsPointResolution U)
    (hV : IsPointResolution V) (F : Cᵒᵖ ⥤ ModuleCat.{u} B) :
    DerivedCategory.Q.map ((mooreCochainMap v).app F) ≫
        (mooreCochainQIsoDerivedColimit U F hU).hom =
      (mooreCochainQIsoDerivedColimit V F hV).hom

CommAlgCat.standardResolutionAbelianDerivedLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionDerivedLowerShriek.lean, line 343. The attribute's comment: “Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab) functorially in ℱ in Ab(C), on the site C_{B/A} of 08PR, with coefficients in the universe above that of A and B”.

Stacks 08PT, in D(Ab). Let A → B be a ring map and let ε : P_• → B be the standard resolution of B over A. Let π be as in Tag 08PR. Then

Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab), functorially in ℱ in Ab(C).

Here C = C_{B/A} is the site of Tag 08PR (CommAlgCat.polynomialSite), whose topology is chaotic so that Ab(C) is the category of abelian presheaves on it, with coefficients in Type (u + 1), the universe in which colimits over C exist; Lπ_! is CommAlgCat.polynomialDerivedLowerShriek; and ℱ(P_•, ε) is the extended Moore complex of the simplicial abelian group obtained by evaluating ℱ on the cosimplicial object of C given by the standard resolution. The standard resolution satisfies the hypotheses of Tag 08PS by Tag 08QI: its terms are polynomial algebras, and its augmentation is a homotopy equivalence of underlying simplicial sets (Tag 08ND), hence a quasi-isomorphism of associated complexes (Tag 08P2), hence a trivial Kan fibration (Tag 08P1).

def standardResolutionAbelianDerivedLowerShriekIso :
    polynomialMooreCochain A B
        (resolutionCosimplicialObject (standardResolution.{u, u} A B).hom
          (standardResolution_isResolution.{u, u} A B).isPolynomialAlgebra)
        AddCommGrpCat.{u + 1} ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single ((polynomialSite A B)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
          (ComplexShape.up ℤ) 0 ⋙ DerivedCategory.Q ⋙
        polynomialDerivedLowerShriek A B AddCommGrpCat.{u + 1}

CommAlgCat.standardResolutionModuleDerivedLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionDerivedLowerShriek.lean, line 369. The attribute's comment: “Lπ_!(ℱ) = ℱ(P_•, ε) in D(B) functorially in ℱ in Mod(B̲), on the site C_{B/A} of 08PR, with module sections in the universe above that of A and B”.

Stacks 08PT, in D(B). Let A → B be a ring map and let ε : P_• → B be the standard resolution of B over A. Let π be as in Tag 08PR. Then

Lπ_!(ℱ) = ℱ(P_•, ε) in D(B), functorially in ℱ in Mod(B̲).

Here C = C_{B/A} is the site of Tag 08PR (CommAlgCat.polynomialSite), whose topology is chaotic so that a B̲-module is a diagram of B-modules on it, with sections in Type (u + 1), the universe in which colimits over C exist, B being lifted to that universe as the ring on the point of π is; Lπ_! is CommAlgCat.polynomialDerivedLowerShriek; and ℱ(P_•, ε) is the extended Moore complex of the simplicial B-module obtained by evaluating ℱ on the cosimplicial object of C given by the standard resolution. The standard resolution satisfies the hypotheses of Tag 08PS by Tag 08QI, as recorded at CommAlgCat.standardResolutionAbelianDerivedLowerShriekIso.

def standardResolutionModuleDerivedLowerShriekIso :
    polynomialMooreCochain A B
        (resolutionCosimplicialObject (standardResolution.{u, u} A B).hom
          (standardResolution_isResolution.{u, u} A B).isPolynomialAlgebra)
        (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))) ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single
          ((polynomialSite A B)ᵒᵖ ⥤ ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u)))
          (ComplexShape.up ℤ) 0 ⋙ DerivedCategory.Q ⋙
        polynomialDerivedLowerShriek A B (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u)))

CommAlgCat.exists_homotopyEquivalences_standardResolutionMor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterion.lean, line 412. The attribute's comment: “the hypothesis of the criterion of Tag 08Q9 for the cosimplicial object of the standard resolution: each Mor_C((P_•, ε), W) is homotopy equivalent to a singleton. The conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab), resp. D(B), functorially in ℱ, is not asserted, for the reason recorded at Tag 08PS in this file”.

Stacks 08PT. Let A → B be a ring map and let ε : P_• ⟶ B be the standard resolution of B over A. Then for every object W of the site C_{B/A} the simplicial set Mor_{C_{B/A}}((P_•, ε), W) is homotopy equivalent to the constant simplicial set on a singleton, which is the hypothesis the criterion of Tag 08Q9 asks of the cosimplicial object of the standard resolution. The two hypotheses of Tag 08PS hold for it by Tag 08QI: its terms are polynomial algebras, and its augmentation is a trivial Kan fibration because it is a homotopy equivalence of underlying simplicial sets (Tag 08ND), hence a quasi-isomorphism of associated complexes (Tag 08P2), hence — being degreewise surjective — a trivial Kan fibration (Tag 08P1).

theorem exists_homotopyEquivalences_standardResolutionMor (A : Type u) [CommRing A]
    (B : CommAlgCat.{u} A) (W : polynomialSite A B) :
    ∃ f : (resolutionCosimplicialObject (standardResolution.{u, u} A B).hom
          (standardResolution_isResolution.{u, u} A B).isPolynomialAlgebra).op ⋙
        yoneda.obj W ⟶ (Functor.const SimplexCategoryᵒᵖ).obj PUnit.{u + 1},
      SimplicialObject.homotopyEquivalences (Type u) f

CommAlgCat.standardResolutionDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterionSmallDerived.lean, line 201. The attribute's comment: “the conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab) functorially in ℱ in Ab(C_{B/A}), for the standard resolution, as an isomorphism in the derived category rather than degreewise, read at the small model of the footnote-restricted site — for the reason recorded at Tag 08PS in this file”.

Lπ_!(ℱ) = ℱ(P_•, ε) in D(Ab) for the standard resolution, functorially in the abelian sheaf ℱ on the small model of the site restricted to polynomial algebras on at most CommAlgCat.standardResolutionVarCardinal A B variables.

This is the abelian half of the conclusion of Tag 08PT in the derived category. The two hypotheses of Tag 08PS hold for the standard resolution by Tag 08QI — its terms are polynomial algebras and its augmentation is a trivial Kan fibration — and its terms are boundedly many variables wide by CommAlgCat.standardResolution_isPolynomialAlgebraBelow, so nothing is assumed.

def standardResolutionDerivedColimitNatIso :
    Stacks.ChaoticSite.AbelianValued.mooreCochainComplex
          (smallResolutionCosimplicialObject (standardResolution.{u, u} A B).hom
            (standardResolutionVarCardinal A B)
            (standardResolution_isPolynomialAlgebraBelow A B)) ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single
          ((smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))ᵒᵖ ⥤
            AddCommGrpCat.{u})
          (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙
          totalDerivedColimit (smallBoundedPolynomialSite A B
            (standardResolutionVarCardinal A B)) AddCommGrpCat.{u}

CommAlgCat.standardResolutionModuleDerivedColimitNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterionSmallDerived.lean, line 228. The attribute's comment: “the conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(B) functorially in ℱ in Mod(B̲), for the standard resolution, as an isomorphism in the derived category rather than degreewise, read at the small model of the footnote-restricted site — for the reason recorded at Tag 08PS in this file”.

Lπ_!(ℱ) = ℱ(P_•, ε) in D(B) for the standard resolution, functorially in the sheaf of B-modules ℱ on the small model of the site restricted to polynomial algebras on at most CommAlgCat.standardResolutionVarCardinal A B variables.

This is the module half of the conclusion of Tag 08PT in the derived category, beside the abelian half CommAlgCat.standardResolutionDerivedColimitNatIso; as there, the hypotheses of Tag 08PS are discharged for the standard resolution by Tag 08QI.

def standardResolutionModuleDerivedColimitNatIso :
    Stacks.ChaoticSite.ModuleValued.mooreCochainComplex (B := (B : Type u))
          (smallResolutionCosimplicialObject (standardResolution.{u, u} A B).hom
            (standardResolutionVarCardinal A B)
            (standardResolution_isPolynomialAlgebraBelow A B)) ⋙ DerivedCategory.Q ≅
      HomologicalComplex.single
          ((smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))ᵒᵖ ⥤
            ModuleCat.{u} (B : Type u))
          (ComplexShape.up ℤ) 0 ⋙
        DerivedCategory.Q ⋙
          totalDerivedColimit (smallBoundedPolynomialSite A B
            (standardResolutionVarCardinal A B)) (ModuleCat.{u} (B : Type u))

CommAlgCat.standardResolutionModuleLeftDerivedLowerShriekNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionPointCriterionSmallOfModules.lean, line 84. The attribute's comment: “the conclusion Lπ_!(ℱ) = ℱ(P_•, ε) in D(B) functorially in ℱ in Mod(B̲), for the standard resolution, read at the small model of the footnote-restricted site, for the reason recorded at Tag 08PS in this file”.

For every sheaf of B-modules ℱ on the small model of the site C_{B/A} restricted to polynomial algebras on at most CommAlgCat.standardResolutionVarCardinal A B variables, the sections at the point of L_nπ_!(ℱ) are the degree n homology of the Moore complex of the simplicial B-module ℱ(P_•, ε) for P_• the standard resolution of B over A, naturally in ℱ.

def standardResolutionModuleLeftDerivedLowerShriekNatIso (n : ℕ) :
    (modulePointLowerShriek
          (smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))
          (B : Type u)).leftDerived n ⋙
        Stacks.ChaoticSite.pointSections.{u, u + 1, u} (ModuleCat.{u} (B : Type u)) ≅
      sheafToPresheaf (GrothendieckTopology.trivial
            (smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B)))
          (ModuleCat.{u} (B : Type u)) ⋙
        moduleCosimplicialMooreComplex
            (smallResolutionCosimplicialObject (standardResolution.{u, u} A B).hom
              (standardResolutionVarCardinal A B)
              (standardResolution_isPolynomialAlgebraBelow A B)) ⋙
          HomologicalComplex.homologyFunctor (ModuleCat.{u} (B : Type u))
            (ComplexShape.down ℕ) n
Tag 08PU, a lemma

Tag 08PU in the Stacks Project.

CommAlgCat.free_kaehlerDifferential_polynomialSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteCotangentComplex.lean, line 383. The attribute's comment: “the step Li^Ω_{𝒪/A} = i^Ω_{𝒪/A}: each Ω_{P/A} is a free P-module, hence Ω_{𝒪/A} is flat over 𝒪”.

The differentials of each object of C_{B/A} are free over it. Every object (P, α) of the site has P a polynomial algebra over A, so Ω[P⁄A] is free on the variables. This is the objectwise input that lets the argument of Tag 08PU replace Li^* by i^*; the sheaf-level statement is CommAlgCat.polynomialRelativeDifferentials_isFlat.

theorem free_kaehlerDifferential_polynomialSite (X : polynomialSite A B) :
    Module.Free (X.unop.obj.left : Type u) Ω[(X.unop.obj.left : Type u)⁄A]

CommAlgCat.standardResolutionCotangentMooreComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteCotangentComplex.lean, line 482. The attribute's comment: “the step Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) = (Ω_{𝒪/A} ⊗_𝒪 B̲)(P_•, ε): the evaluation of i^*Ω_{𝒪/A} on the standard resolution is the simplicial module whose complex is L_{B/A}, as an isomorphism of complexes”.

The Moore complex of (i^*Ω_{𝒪/A})(P_•, ε) is the complex of L_{B/A}. For the standard resolution of B over A, the Moore complex of the simplicial abelian group obtained by evaluating i^*Ω_{𝒪/A} on the cosimplicial object of the small model is the complex underlying the cotangent complex of Tag 08PN, namely the alternating face map complex of CommAlgCat.cotangentSimplicialModule with its B-module structures forgotten.

This is the heart of Tag 08PU: an isomorphism of complexes, not merely of their homology.

def standardResolutionCotangentMooreComplexIso :
    (Stacks.ChaoticSite.cosimplicialMooreComplex
          (standardResolutionSmallCosimplicialObject A B)).obj
        (smallPolynomialCotangentSheaf A B (standardResolutionVarCardinal A B)).obj ≅
      ((forget₂ (ModuleCat.{u} B) AddCommGrpCat.{u}).mapHomologicalComplex
          (ComplexShape.down ℕ)).obj
        ((alternatingFaceMapComplex (ModuleCat.{u} B)).obj
          (cotangentSimplicialModule.{u, u} A B).object)

CommAlgCat.standardResolutionLeftDerivedCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteCotangentComplex.lean, line 520. The attribute's comment: “the identification L_{B/A} = Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲), for the point morphism of the small model of the footnote-restricted site C_{B/A} and with Lπ_! read degreewise, as the left derived functors of the π_! of Tag 08PF at abelian coefficients: the sections at the point of L_nπ_! are the degree -n cohomology of the cotangent complex of Tag 08PN. The source's isomorphism in D(B) needs the module-level Lπ_!, which is absent from this library”.

Tag 08PU at the small model of the restricted site C_{B/A}. The sections at the point of L_nπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) are the degree -n cohomology of the cotangent complex L_{B/A} of Tag 08PN, with its B-module structure forgotten; here π is the point morphism of the small model of the footnote-restricted site and Lπ_! is read degreewise, as the left derived functors of the π_! of Tag 08PF.

The proof is the source's: Tag 08PT computes L_nπ_! on the standard resolution (CommAlgCat.standardResolutionLeftDerivedLowerShriekNatIso), the evaluation of Ω_{𝒪/A} ⊗_𝒪 B̲ there is the simplicial module defining L_{B/A} (CommAlgCat.standardResolutionCotangentMooreComplexIso), and the cotangent complex is the reindexing of that simplicial module's alternating face map complex. The step Li^*Ω_{𝒪/A} = i^*Ω_{𝒪/A} of the source is the flatness of Ω_{𝒪/A} over 𝒪, CommAlgCat.polynomialRelativeDifferentials_isFlat; see the implementation notes for what separates this statement from the source's isomorphism in D(B).

def standardResolutionLeftDerivedCotangentComplexIso (n : ℕ) :
    (Stacks.ChaoticSite.pointSections.{u, u + 1, u} AddCommGrpCat.{u}).obj
        (((Stacks.ChaoticSite.abelianPointLowerShriek
              (smallBoundedPolynomialSite A B
                (standardResolutionVarCardinal A B))).leftDerived n).obj
          (smallPolynomialCotangentSheaf A B (standardResolutionVarCardinal A B))) ≅
      (forget₂ (ModuleCat.{u} B) AddCommGrpCat.{u}).obj
        ((cotangentComplex.{u, u} A B).homology (-(n : ℤ)))

CommAlgCat.standardResolutionModuleLeftDerivedCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteModuleShriek.lean, line 162. The attribute's comment: “L_{B/A} = Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) at linear coefficients, for the point morphism of the small model of the footnote-restricted site C_{B/A} and with Lπ_! read degreewise, as the left derived functors of the π_! of Tag 08PF on sheaves of B-modules: the sections at the point of L_nπ_! are the degree -n cohomology of the cotangent complex of Tag 08PN, as B-modules. The source's isomorphism in D(B) needs the derived form of Tag 08PT”.

Tag 08PU at the small model of the restricted site C_{B/A}, with B-linear coefficients. The sections at the point of L_nπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) are the degree -n cohomology of the cotangent complex L_{B/A} of Tag 08PN, as B-modules; here π is the point morphism of the small model of the footnote-restricted site and Lπ_! is read degreewise, as the left derived functors of the π_! of Tag 08PF on sheaves of B-modules.

The proof is the source's: Tag 08PT at linear coefficients computes L_nπ_! on the standard resolution (CommAlgCat.standardResolutionModuleLeftDerivedLowerShriekNatIso), the evaluation of Ω_{𝒪/A} ⊗_𝒪 B̲ there is the simplicial B-module defining L_{B/A} (CommAlgCat.standardResolutionCotangentModuleMooreComplexIso), and the cotangent complex is the reindexing of that simplicial module's alternating face map complex.

def standardResolutionModuleLeftDerivedCotangentComplexIso (n : ℕ) :
    (Stacks.ChaoticSite.pointSections.{u, u + 1, u} (ModuleCat.{u} (B : Type u))).obj
        (((Stacks.ChaoticSite.ModuleValued.modulePointLowerShriek
              (smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))
              (B : Type u)).leftDerived n).obj
          (smallPolynomialCotangentModuleSheaf A B (standardResolutionVarCardinal A B))) ≅
      (cotangentComplex.{u, u} A B).homology (-(n : ℤ))

CommAlgCat.standardResolutionCotangentDerivedLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteModuleShriekDerived.lean, line 101. The attribute's comment: “in D(B), at module coefficients: Q(L_{B/A}) = L pi_!(Omega ⊗ B) for the point morphism of the small model of the footnote-restricted site C_{B/A}, with L pi_! the total left derived functor of the colimit on D(B-underline)”.

[Stacks, Tag 08PU] in D(B), at module coefficients and on the small model of the footnote-restricted site C_{B/A}. The cotangent complex L_{B/A} of [Stacks, Tag 08PN] is derived lower shriek of the sheaf of B̲-modules i^*Ω_{𝒪/A} = Ω_{𝒪/A} ⊗_𝒪 B̲, as an object of D(B):

Q(L_{B/A}) ≅ Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲).

Here Lπ_! is CommAlgCat.smallPolynomialModuleDerivedLowerShriek, the total left derived functor of the colimit over the index category of B̲-modules, which is the π_! of [Stacks, Tag 08PF].

The proof is the source's. The standard resolution is a point resolution of the small model (CommAlgCat.isPointResolution_standardResolutionSmallCosimplicialObject), so the derived form of [Stacks, Tag 08PT] at module coefficients (Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit) computes Lπ_! of i^*Ω_{𝒪/A} as the extended Moore complex of its evaluation on that resolution, and that complex is the cotangent complex. The step Li^*Ω_{𝒪/A} = i^*Ω_{𝒪/A} of the source is the flatness of Ω_{𝒪/A} over 𝒪, which is why i^*Ω_{𝒪/A} may be used underived.

def standardResolutionCotangentDerivedLowerShriekIso :
    DerivedCategory.Q.obj (cotangentComplex.{u, u} A B) ≅
      smallPolynomialCotangentDerivedLowerShriek A B (standardResolutionVarCardinal A B)

CommAlgCat.smallResolutionCotangentDerivedLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionCotangentDerived.lean, line 118. The attribute's comment: “in D(B), at module coefficients, for an arbitrary resolution whose terms have at most κ variables: Q of the complex of that resolution is L pi_!(Omega ⊗ B-underline) for the point morphism of the small model of the footnote-restricted site C_{B/A}. Combined with the same statement at the standard resolution this is Remark 08QI, that any resolution computes L_{B/A}”.

[Stacks, Tag 08PU] in D(B) for an arbitrary bounded resolution. Let ε : P_• ⟶ B be a resolution of B over A in the sense of [Stacks, Tag 08QI] whose terms are polynomial algebras on at most κ variables. Then the complex Ω[P_•⁄A] ⊗_{P_•} B of that resolution, read in cohomological degrees ≤ 0, is derived lower shriek of the sheaf of B̲-modules i^*Ω_{𝒪/A} = Ω_{𝒪/A} ⊗_𝒪 B̲, as an object of D(B):

Q(Ω[P_•⁄A] ⊗_{P_•} B) ≅ Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲).

Here Lπ_! is CommAlgCat.smallPolynomialModuleDerivedLowerShriek, the total left derived functor of the colimit over the index category of B̲-modules, which is the π_! of [Stacks, Tag 08PF].

The proof is the source's, with the standard resolution replaced by P_•: the resolution is a point resolution of the small model of the footnote-restricted site (CommAlgCat.isPointResolution_smallResolutionCosimplicialObject), so the derived form of [Stacks, Tag 08PT] at module coefficients (Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit) computes Lπ_! of i^*Ω_{𝒪/A} as the extended Moore complex of its evaluation on P_•, and that evaluation is Ω[P_•⁄A] ⊗_{P_•} B. Since the right-hand side does not mention the resolution, this is also the assertion of [Stacks, Remark 08QI] that any resolution computes L_{B/A}.

def smallResolutionCotangentDerivedLowerShriekIso
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A)))) :
    DerivedCategory.Q.obj
        (((alternatingFaceMapComplex (ModuleCat.{u} (B : Type u))).obj
            (resolutionOver ε ⋙ overDifferentialsFunctor)).extend
          (ComplexShape.embeddingUpIntLE (0 : ℤ))) ≅
      smallPolynomialCotangentDerivedLowerShriek A B κ

CommAlgCat.standardResolutionCotangentDerivedLowerShriekIsoOfLE, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionCotangentDerived.lean, line 162. The attribute's comment: “in D(B), at module coefficients, at an arbitrary cardinal bound κ containing the standard resolution: Q(L_{B/A}) = L pi_!(Omega ⊗ B-underline) for the point morphism of the small model of the site restricted to at most κ variables”.

[Stacks, Tag 08PU] in D(B) at an arbitrary cardinal bound. The cotangent complex L_{B/A} of [Stacks, Tag 08PN] is derived lower shriek of the sheaf of B̲-modules i^*Ω_{𝒪/A} = Ω_{𝒪/A} ⊗_𝒪 B̲ on the small model of the site restricted to polynomial algebras on at most κ variables, for any bound κ containing the standard resolution:

Q(L_{B/A}) ≅ Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲).

This is CommAlgCat.smallResolutionCotangentDerivedLowerShriekIso at the standard resolution, whose complex Ω[P_•⁄A] ⊗_{P_•} B is the cotangent complex by CommAlgCat.standardResolutionOverDifferentialsIso. At κ = CommAlgCat.standardResolutionVarCardinal A B it is CommAlgCat.standardResolutionCotangentDerivedLowerShriekIso; the point of the free bound is that a second resolution may need a larger one.

def standardResolutionCotangentDerivedLowerShriekIsoOfLE
    (hκ : standardResolutionVarCardinal A B ≤ κ) :
    DerivedCategory.Q.obj (cotangentComplex.{u, u} A B) ≅
      smallPolynomialCotangentDerivedLowerShriek A B κ

CommAlgCat.smallResolutionCotangentDerivedLowerShriekIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionCotangentDerivedNaturality.lean, line 312. The attribute's comment: “in D(B), at module coefficients: the identification of the complex of a resolution with L pi_!(Omega ⊗ B-underline) is functorial in the resolution, so the isomorphism it gives between the complexes of two resolutions is the map induced by a morphism between them. This is the arrow-level form of Remark 08QI”.

[Stacks, Tag 08PU] in D(B) is functorial in the resolution. Let ε : P_• ⟶ B and ε' : P'_• ⟶ B be resolutions of B over A in the sense of [Stacks, Tag 08QI] whose terms are polynomial algebras on at most κ variables, and let w : P_• ⟶ P'_• be a morphism of simplicial A-algebras over B. Then the triangle

Q(Ω[P_•⁄A] ⊗_{P_•} B) ⟶ Q(Ω[P'_•⁄A] ⊗_{P'_•} B) ⟶ Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲)

commutes: the comparison of CommAlgCat.smallResolutionCotangentDerivedLowerShriekIso at ε', precomposed with the map CommAlgCat.resolutionCotangentComplexMap induced by w, is the comparison at ε.

In particular the isomorphism between the complexes of two resolutions that the two instances of [Stacks, Tag 08PU] produce is the map induced by any morphism between the resolutions — which is the content of [Stacks, Remark 08QI] beyond the object-level statement, and what a comparison of two presentations consumes.

The proof is the naturality of the derived form of [Stacks, Tag 08PT] in the point resolution (Stacks.ChaoticSite.ModuleValued.mooreCochainQIsoDerivedColimit_naturality), applied at CommAlgCat.smallResolutionCosimplicialObjectMap, together with CommAlgCat.smallResolutionCotangentMooreCochainIso_naturality.

theorem smallResolutionCotangentDerivedLowerShriekIso_naturality (w : P ⟶ P') (hw : w ≫ ε' = ε)
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A))))
    (hε' : SSet.trivialKanFibrations (Functor.whiskerRight ε' (forget (CommAlgCat.{u} A)))) :
    DerivedCategory.Q.map (resolutionCotangentComplexMap ε ε' w hw) ≫
        (smallResolutionCotangentDerivedLowerShriekIso ε' κ hP'κ hε').hom =
      (smallResolutionCotangentDerivedLowerShriekIso ε κ hPκ hε).hom

CommAlgCat.leftDerivedColimPolynomialCotangentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSymmetricPowerVanishing.lean, line 119. The attribute's comment: “the identification L_{B/A} = Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) read degreewise at LINEAR coefficients: for every n, the nth left derived functor of the colimit over the opposite of the small model of the footnote-restricted site, applied to Ω, is the degree -n cohomology of the cotangent complex of Tag 08PN, as an isomorphism of B-modules. L_n colim is Tag 08PF's definition of H_n(C_{B/A}, -); the identification with the sections at the point of L_nπ_! is Stacks.ChaoticSite.ModuleValued.moduleLeftDerivedPointLowerShriekNatIso. Proved for every ring map A → B”.

Tag 08PU at the small model of the restricted site C_{B/A}, at linear coefficients. The nth homology of C_{B/A} with coefficients in Ω = Ω_{𝒪/A} ⊗_𝒪 B̲ — the nth left derived functor of the colimit over the opposite of the small model, which is Tag 08PF's definition — is the degree -n cohomology of the cotangent complex L_{B/A} of Tag 08PN, as B-modules.

This is the linear-coefficient refinement of CommAlgCat.standardResolutionLeftDerivedCotangentComplexIso, which is its image under the forgetful functor to abelian groups. The proof is the same: the module half of Tag 08Q9 computes L_n colim on the standard resolution, and the evaluation of Ω there is the simplicial module defining L_{B/A}.

def leftDerivedColimPolynomialCotangentIso (n : ℕ) :
    ((colim :
          ((smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))ᵒᵖ ⥤
            ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived n).obj
        (smallPolynomialCotangentModulePresheaf A B (standardResolutionVarCardinal A B)) ≅
      (cotangentComplex.{u, u} A B).homology (-(n : ℤ))
Tag 08QE, a lemma

Tag 08QE in the Stacks Project.

CommAlgCat.atiyahModuleDerivedInverseImageCompLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClassBigSiteResolution.lean, line 170. The attribute's comment: “in D(B), at module coefficients: Lπ_!(π^{-1}M) = M at CommAlgCat.polynomialSite -- the site of Tag 08PR itself, not a restriction of it, read on its AsSmall model -- with Lπ_! the total left derived functor of the colimit on D(B̲), π^{-1} the constant diagram, and the coefficient ring read as ULift.{u+1} B exactly as the site's own ringed point CommAlgCat.polynomialRingedPoint reads it”.

[Stacks, Tag 08QE] at the site C_{B/A} itself. Derived lower shriek of the inverse image of a B-module is that module: Lπ_!(π^{-1}M) = M in D(B), naturally in M. Here π^{-1} is the constant diagram and Lπ_! the total left derived functor of the colimit over the index category, which is the π_! of [Stacks, Tag 08PF]; the coefficient ring is ULift B, the ring of the site's own ringed point CommAlgCat.polynomialRingedPoint.

The proof is the source's: the augmentation A → B is a terminal object of the site (CommAlgCat.isTerminal_atiyahBaseObj), so π^{-1} has the exact right adjoint "sections over A → B" and Stacks.ChaoticSite.derivedConstCompColimitIso applies with no hypothesis on the existence of the derived functor. The statement at the footnote-restricted site is CommAlgCat.smallPolynomialModuleDerivedInverseImageCompLowerShriekIso; that is a statement about different coefficients, the restriction to a full subcategory changing both Mod(B̲) and Lπ_!.

def atiyahModuleDerivedInverseImageCompLowerShriekIso :
    (Functor.const (atiyahSite A B)ᵒᵖ :
          ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u)) ⥤ _).mapDerivedCategory ⋙
        totalDerivedColimit (atiyahSite A B)
          (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))) ≅ 𝟭 _

CommAlgCat.polynomialLeftDerivedZeroLowerShriekInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteCotangentComplex.lean, line 548. The attribute's comment: “Lπ_!(π^{-1}M) = M in degree zero, for the point morphism of the small model of the footnote-restricted site C_{B/A} at abelian coefficients”.

Tag 08QE at the small model of the restricted site C_{B/A}, in degree zero. The sections at the point of L_0π_!(π^{-1}M) are the sections of M, for every abelian sheaf M on the point; here π is the point morphism of the small model of the footnote-restricted site.

This is the source's proof: Tag 08PT computes Lπ_!(π^{-1}M) by (π^{-1}M)(P_•, ε) for the standard resolution, and that is the constant simplicial object on M.

def polynomialLeftDerivedZeroLowerShriekInverseImageIso
    (M : Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 1})) AddCommGrpCat.{u}) :
    (Stacks.ChaoticSite.pointSections.{u, u + 1, u} AddCommGrpCat.{u}).obj
        (((Stacks.ChaoticSite.abelianPointLowerShriek
              (smallBoundedPolynomialSite A B
                (standardResolutionVarCardinal A B))).leftDerived 0).obj
          ((Stacks.ChaoticSite.abelianPointInverseImage
            (smallBoundedPolynomialSite A B
              (standardResolutionVarCardinal A B))).obj M)) ≅
      (Stacks.ChaoticSite.pointSections.{u, u + 1, u} AddCommGrpCat.{u}).obj M

CommAlgCat.isZero_polynomialLeftDerivedSuccLowerShriekInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteCotangentComplex.lean, line 566. The attribute's comment: “Lπ_!(π^{-1}M) = M in positive degrees: L_nπ_!(π^{-1}M) = 0 for n > 0”.

Tag 08QE at the small model of the restricted site C_{B/A}, in positive degrees. The sections at the point of L_nπ_!(π^{-1}M) vanish for n > 0, so together with CommAlgCat.polynomialLeftDerivedZeroLowerShriekInverseImageIso this is the source's Lπ_!(π^{-1}M) = M, read degreewise.

theorem isZero_polynomialLeftDerivedSuccLowerShriekInverseImage
    (M : Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 1})) AddCommGrpCat.{u})
    (n : ℕ) :
    IsZero ((Stacks.ChaoticSite.pointSections.{u, u + 1, u} AddCommGrpCat.{u}).obj
      (((Stacks.ChaoticSite.abelianPointLowerShriek
            (smallBoundedPolynomialSite A B
              (standardResolutionVarCardinal A B))).leftDerived (n + 1)).obj
        ((Stacks.ChaoticSite.abelianPointInverseImage
          (smallBoundedPolynomialSite A B
            (standardResolutionVarCardinal A B))).obj M)))

CommAlgCat.smallPolynomialModuleDerivedInverseImageCompLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteModuleShriek.lean, line 271. The attribute's comment: “in D(B), at module coefficients: Lπ_!(π^{-1}M) = M for the point morphism of the small model of the footnote-restricted site C_{B/A}, with Lπ_! the total left derived functor of the colimit on D(B̲) and π^{-1} the constant diagram”.

Tag 08QE in D(B) at the small model of the restricted site C_{B/A}. Derived lower shriek of the inverse image of a B-module is that module: Lπ_!(π^{-1}M) = M in D(B), naturally in M. Here π^{-1} is the constant diagram and Lπ_! the total left derived functor of the colimit, and the proof is that the augmentation A → B is a terminal object of the site, so that π^{-1} has the exact right adjoint "sections over A → B".

def smallPolynomialModuleDerivedInverseImageCompLowerShriekIso :
    (Functor.const (smallBoundedPolynomialSite A B κ)ᵒᵖ :
          ModuleCat.{u} (B : Type u) ⥤ _).mapDerivedCategory ⋙
        Stacks.CategoryHomology.totalDerivedColimit (smallBoundedPolynomialSite A B κ)
          (ModuleCat.{u} (B : Type u)) ≅ 𝟭 _
Tag 08QF, a lemma

Tag 08QF in the Stacks Project.

CommAlgCat.cotangentComplex_homologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/HomologyZero.lean, line 345.

Stacks Project, Tag 08QF. The degree-zero homology of the cotangent complex L_{B/A} is the module of Kähler differentials Ω[B⁄A].

public noncomputable def cotangentComplex_homologyZeroIso :
    (cotangentComplex A B).homology 0 ≅ ModuleCat.of B (KaehlerDifferential A B)
Tag 08QG, a lemma

Tag 08QG in the Stacks Project.

CommAlgCat.polynomialEvaluationLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteShriek.lean, line 137. The attribute's comment: “evaluation at B → B is a lower shriek”.

Stacks 08QG. For B a polynomial algebra over A, evaluation at the identity augmentation B → B is left adjoint to π^{-1}: it is a lower shriek.

def polynomialEvaluationLowerShriekAdjunction (hB : IsPolynomialAlgebra A B) :
    Stacks.ChaoticSite.evaluationLowerShriek AddCommGrpCat.{max (u + 1) m}
        (polynomialIdentityObj A B hB) (polynomialTopology A B) ⊣
      polynomialAbelianInverseImage.{m} A B

CommAlgCat.polynomialAbelianLowerShriekEvaluationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteShriek.lean, line 147. The attribute's comment: “π_! is evaluation at B → B”.

Stacks 08QG. For B a polynomial algebra over A, the lower shriek π_! of Stacks 08PR is canonically evaluation at the identity augmentation B → B.

def polynomialAbelianLowerShriekEvaluationIso (hB : IsPolynomialAlgebra A B) :
    polynomialAbelianLowerShriek.{m} A B ≅
      Stacks.ChaoticSite.evaluationLowerShriek AddCommGrpCat.{max (u + 1) m}
        (polynomialIdentityObj A B hB) (polynomialTopology A B)

CommAlgCat.polynomialAbelianLowerShriek_pointSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteShriek.lean, line 157. The attribute's comment: “π_!F = F(B → B)”.

Stacks 08QG. π_!ℱ = ℱ(B → B): the sections of π_!ℱ at the point are the sections of ℱ over the identity augmentation, naturally in ℱ.

def polynomialAbelianLowerShriek_pointSectionsIso (hB : IsPolynomialAlgebra A B) :
    polynomialAbelianLowerShriek.{m} A B ⋙
        Stacks.ChaoticSite.pointSections AddCommGrpCat.{max (u + 1) m} ≅
      sheafToPresheaf (polynomialTopology A B) AddCommGrpCat.{max (u + 1) m} ⋙
        (evaluation (polynomialSite A B)ᵒᵖ AddCommGrpCat.{max (u + 1) m}).obj
          (polynomialIdentityObj A B hB)

CommAlgCat.polynomialAbelianLowerShriek_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteShriek.lean, line 170. The attribute's comment: “π_! is exact: finite limits”.

Stacks 08QG. For B a polynomial algebra over A, π_! preserves finite limits. With CommAlgCat.polynomialAbelianLowerShriek_preservesColimitsOfShape this is the exactness of π_! asserted by the source.

theorem polynomialAbelianLowerShriek_preservesFiniteLimits (hB : IsPolynomialAlgebra A B) :
    PreservesFiniteLimits (polynomialAbelianLowerShriek.{m} A B)

CommAlgCat.polynomialAbelianLowerShriek_preservesColimitsOfShape, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteShriek.lean, line 178. The attribute's comment: “π_! is exact: colimits”.

Stacks 08QG. π_! preserves all colimits, being a left adjoint; no hypothesis on B is needed for this half of exactness.

instance polynomialAbelianLowerShriek_preservesColimitsOfShape {K : Type*} [Category* K] :
    PreservesColimitsOfShape K (polynomialAbelianLowerShriek.{m} A B)
Tag 08QH, a lemma

Tag 08QH in the Stacks Project.

CommAlgCat.cotangentComplex_iso_kaehlerDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebra.lean, line 285.

Stacks Project, Tag 08QH. If B is a polynomial algebra over the ring A, then the cotangent complex L_{B/A} is quasi-isomorphic to Ω[B⁄A][0].

public theorem cotangentComplex_iso_kaehlerDifferential (hB : Algebra.IsPolynomialAlgebra A B) :
    Nonempty
      (DerivedCategory.Q.obj (cotangentComplex A B) ≅
        (DerivedCategory.singleFunctor (ModuleCat.{max u v} B) 0).obj
          (ModuleCat.of B (KaehlerDifferential A B)))
Sources
LeanCommAlgCat.polynomialSite · CommAlgCat.polynomialTopology_eq_bot · CommAlgCat.polynomialStructureSheaf · CommAlgCat.polynomialConstantSheaf · CommAlgCat.polynomialConstantSheafIso · CommAlgCat.polynomialAugmentation · CommAlgCat.polynomialAugmentation_app · CommAlgCat.polynomialInclusion

Section92.5 Constructing a resolution#

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

Tag 08PW, a lemma

Tag 08PW in the Stacks Project.

CommAlgCat.finiteType_succ_of_trivialKanFibration_of_isCoskeletal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/FiniteTypeCoskeletal.lean, line 154.

Stacks 08PW. For a finite type algebra B over a Noetherian ring A, an n-coskeletal simplicial A-algebra over B whose canonical augmentation is a trivial Kan fibration and whose terms through degree n are of finite type has a finite type term in degree n + 1.

theorem finiteType_succ_of_trivialKanFibration_of_isCoskeletal
    [IsNoetherianRing A] [Algebra.FiniteType A B]
    (P : SimplicialObject (Over (CommAlgCat.of A B))) (n : ℕ)
    (_hkan : SSet.trivialKanFibrations (underlyingAugmentation A B P))
    (hcosk : IsIso ((SimplicialObject.coskAdj n).unit.app P))
    (hfinite : ∀ k ≤ n,
      Algebra.FiniteType A (P.obj (op (SimplexCategory.mk k))).left) :
    Algebra.FiniteType A (P.obj (op (SimplexCategory.mk (n + 1)))).left
Tag 08PX, a proposition

Tag 08PX in the Stacks Project.

CommAlgCat.exists_trivialKanFibration_from_finiteType_polynomial_simplicialAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialResolution.lean, line 517.

Stacks 08PX. A finite type algebra over a Noetherian ring has a simplicial resolution by polynomial algebras of finite type whose augmentation is a trivial Kan fibration on underlying simplicial sets.

theorem exists_trivialKanFibration_from_finiteType_polynomial_simplicialAlgebra
    {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
    [IsNoetherianRing A] [Algebra.FiniteType A B] :
    ∃ (P : SimplicialObject (CommAlgCat.{u} A))
      (ε : P ⟶ (Functor.const _).obj (CommAlgCat.of A B)),
      (∀ n : ℕ, ∃ k : ℕ,
        Nonempty ((P.obj (op ⦋n⦌) : Type u) ≃ₐ[A] MvPolynomial (Fin k) A)) ∧
      SSet.trivialKanFibrations
        (Functor.whiskerRight ε (CategoryTheory.forget (CommAlgCat.{u} A)))
Tag 08PY, a lemma

Tag 08PY in the Stacks Project.

CommAlgCat.smallResolutionLeftDerivedMooreHomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/FiniteHomology.lean, line 289. The attribute's comment: “the half of the statement that says which modules the conclusion is about: the cohomology of Lπ_!(ℱ) for the point morphism of the small model of the footnote-restricted site, read degreewise at abelian coefficients, is the homology of the B-module Moore complex of ℱ(P_•, ε). The finiteness of those modules is CommAlgCat.finite_homology_smallResolutionMooreComplex”.

Lπ_!(ℱ) = ℱ(P_•, ε) for a presheaf of B-modules, with the module structure forgotten. The sections at the point of L_nπ_!(ℱ) are the degree n homology of the B-module Moore complex of ℱ(P_•, ε), read as an abelian group.

This is CommAlgCat.smallResolutionLeftDerivedLowerShriekNatIso — the conclusion of Tag 08PT at the small model of the restricted site — followed by the two identifications that move the computation from abelian groups to B-modules: the Moore complex of the underlying abelian presheaf is the image of the B-module Moore complex, and forget₂ preserves homology.

def smallResolutionLeftDerivedMooreHomologyIso (n : ℕ) :
    (Stacks.ChaoticSite.pointSections.{u, u + 1, u} AddCommGrpCat.{u}).obj
        (((Stacks.ChaoticSite.abelianPointLowerShriek
              (smallBoundedPolynomialSite A B κ)).leftDerived n).obj
          (smallPolynomialModuleSheaf A B κ ℱ)) ≅
      (forget₂ (ModuleCat.{u} B) AddCommGrpCat.{u}).obj
        ((smallResolutionMooreComplex ε κ hPκ ℱ).homology n)

CommAlgCat.finite_homology_smallResolutionMooreComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/FiniteHomology.lean, line 357. The attribute's comment: “the conclusion for a resolution satisfying the cardinality bound of the small model of the footnote-restricted site, and with the cohomology of Lπ_! read as the homology of the B-module Moore complex of ℱ(P_•, ε), which is what identifies it here (CommAlgCat.smallResolutionLeftDerivedMooreHomologyIso): the module-level Lπ_! is absent from this library. The finiteness hypothesis is carried for the terms of the resolution, not for every object of the site”.

Tag 08PY for a bounded resolution. Let B be Noetherian, let ε : P_• ⟶ B be a resolution of B over A whose terms are polynomial algebras on at most κ variables, and let ℱ be a presheaf of B-modules on the small model of the restricted site whose sections on the terms of the resolution are finite B-modules. Then the Moore homology of ℱ(P_•, ε) — which by CommAlgCat.smallResolutionLeftDerivedMooreHomologyIso is the sections at the point of L_nπ_!(ℱ) — is a finite B-module.

theorem finite_homology_smallResolutionMooreComplex [IsNoetherianRing (B : Type u)]
    (hfin : ∀ p : SimplexCategory,
      Module.Finite B (ℱ.obj (op ((smallResolutionCosimplicialObject ε κ hPκ).obj p))))
    (n : ℕ) : Module.Finite B ((smallResolutionMooreComplex ε κ hPκ ℱ).homology n)

CommAlgCat.finite_moduleLeftDerivedPointLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialResolutionFiniteCohomology.lean, line 133. The attribute's comment: “read at the small model of the footnote-restricted site, for the reason recorded for Tag 08PS in StacksFrontier/Cotangent/ResolutionPointCriterionSmallOfModules.lean; the cardinal bound κ of the footnote is a parameter, required only to be infinite so that the finite type resolution of Tag 08PX is an object of the site”.

Stacks 08PY. Let A be a Noetherian ring, let A → B be a finite type ring map and let π, B̲ be as in Tag 08PR. If ℱ is a B̲-module such that ℱ(P, α) is a finite B-module for every augmentation α : P → B whose P is of finite type over A, then every cohomology module of Lπ_!(ℱ) is a finite B-module.

By Tag 08PX there is a resolution ε : P_• ⟶ B of B over A all of whose terms are finite type polynomial algebras, and by the module half of Tag 08PS the sections at the point of L_nπ_!(ℱ) are the degree n homology of the Moore complex of ℱ(P_•, ε). Each term of that complex is ℱ evaluated at a finite type polynomial augmentation, hence a finite B-module, and B is Noetherian because it is of finite type over the Noetherian ring A; so each homology module is a subquotient of a finite module over a Noetherian ring.

theorem finite_moduleLeftDerivedPointLowerShriek (κ : Cardinal.{u})
    (hκ : Cardinal.aleph0.{u} ≤ κ)
    (ℱ : Sheaf (GrothendieckTopology.trivial (smallBoundedPolynomialSite A B κ))
      (ModuleCat.{u} (B : Type u)))
    (hℱ : ∀ W : smallBoundedPolynomialSite A B κ,
      Algebra.FiniteType A (smallBoundedPolynomialAlgebra A B κ W : Type u) →
        Module.Finite (B : Type u) (ℱ.obj.obj (op W)))
    (n : ℕ) :
    Module.Finite (B : Type u)
      (((modulePointLowerShriek (smallBoundedPolynomialSite A B κ)
            (B : Type u)).leftDerived n ⋙
          Stacks.ChaoticSite.pointSections.{u, u + 1, u}
            (ModuleCat.{u} (B : Type u))).obj ℱ)
Tag 08PZ, a lemma

Tag 08PZ in the Stacks Project.

CommAlgCat.finite_homology_cotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/FiniteHomology.lean, line 516.

Tag 08PZ. Let A be a Noetherian ring and let A → B be a finite type ring map. Then H^n(L_{B/A}) is a finite B-module for every n : ℤ.

In positive degrees the cotangent complex vanishes, so there is nothing to prove; the content is CommAlgCat.finite_homology_cotangentComplex_of_resolution fed with the finite type resolution of Tag 08PX.

theorem finite_homology_cotangentComplex (A : Type u) [CommRing A] [IsNoetherianRing A]
    (B : Type u) [CommRing B] [Algebra A B] [Algebra.FiniteType A B] (m : ℤ) :
    Module.Finite B ((cotangentComplex.{u, u} A (CommAlgCat.of A B)).homology m)
Tag 08QI, a remark

Tag 08QI in the Stacks Project.

CommAlgCat.IsResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Resolution.lean, line 71. The attribute's comment: “resolution”.

Stacks Project, Tag 08QI.

An augmentation ε : P• ⟶ B of a simplicial commutative A-algebra is a resolution of B over A if every Pₙ is a polynomial algebra over A and the underlying augmentation of simplicial sets is a trivial Kan fibration.

structure IsResolution (A : Type u) [CommRing A] (B : Type v) [CommRing B] [Algebra A B]
    (P : SimplicialObject (CommAlgCat.{v} A))
    (ε : P ⟶ (SimplicialObject.const _).obj (CommAlgCat.of A B)) : Prop

CommAlgCat.isResolution_quasiIso_homotopyEquivalence_tfae, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Resolution.lean, line 87. The attribute's comment: “resolution_criteria”.

Stacks Project, Tag 08QI.

For an augmentation ε : P• ⟶ B which is degreewise surjective and whose terms are polynomial A-algebras, the following are equivalent: ε is a resolution, the induced map of associated complexes is a quasi-isomorphism, and the underlying map of simplicial sets is a homotopy equivalence.

lemma isResolution_quasiIso_homotopyEquivalence_tfae
    (A : Type u) [CommRing A] (B : Type v) [CommRing B] [Algebra A B]
    (P : SimplicialObject (CommAlgCat.{v} A))
    (ε : P ⟶ (SimplicialObject.const _).obj (CommAlgCat.of A B))
    (hP : ∀ n : SimplexCategoryᵒᵖ, IsPolynomialAlgebra A (P.obj n))
    (hε : ∀ n : SimplexCategoryᵒᵖ, Function.Surjective (ε.app n).hom) :
    List.TFAE
      [IsResolution A B P ε,
       QuasiIso ((alternatingFaceMapComplex AddCommGrpCat.{v}).map
         (Functor.whiskerRight ε
           (forget₂ (CommAlgCat.{v} A) (AlgCat.{v} A) ⋙
            forget₂ (AlgCat.{v} A) (ModuleCat.{v} A) ⋙
            forget₂ (ModuleCat.{v} A) AddCommGrpCat.{v}))),
       SimplicialObject.homotopyEquivalences (Type v)
         (Functor.whiskerRight ε (forget (CommAlgCat.{v} A)))]

CommAlgCat.exists_isResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionCotangentAny.lean, line 85. The attribute's comment: “existence of resolutions: every A-algebra B admits a resolution, namely the standard resolution”.

[Stacks, Remark 08QI]: resolutions exist. Every commutative A-algebra B admits a resolution over A: the standard resolution of B over A is one, by CommAlgCat.standardResolution_isResolution.

theorem exists_isResolution (A : Type u) [CommRing A] (B : Type (max u v)) [CommRing B]
    [Algebra A B] :
    ∃ (P : SimplicialObject (CommAlgCat.{max u v} A))
      (ε : P ⟶ (SimplicialObject.const (CommAlgCat.{max u v} A)).obj (CommAlgCat.of A B)),
      IsResolution A B P ε

CommAlgCat.cotangentComplexIsoOfResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionCotangentAny.lean, line 156. The attribute's comment: “in D(B): for an arbitrary resolution of B over A, with no bound on the number of variables, Q(L_{B/A}) = Q(Omega[P_bullet/A] ⊗_{P_bullet} B); the cardinal bound of the two instances of Tag 08PU this composes is supplied by the resolution itself”.

[Stacks, Remark 08QI]: any resolution computes the cotangent complex. Let ε : P_• ⟶ B be a resolution of B over A — every P_n a polynomial algebra over A, ε a trivial Kan fibration of the underlying simplicial sets — with no bound on the number of variables. Then the cotangent complex L_{B/A} of [Stacks, Tag 08PN], which is built from the standard resolution, is the complex of base-changed differentials of P_•, as objects of D(B):

Q(L_{B/A}) ≅ Q(Ω[P_•⁄A] ⊗_{P_•, ε} B).

The proof is the source's. At the cardinal CommAlgCat.resolutionVarCardinal, which bounds the terms of P_• and those of the standard resolution at once, both resolutions lie on the small model of the footnote-restricted site, so the two instances of [Stacks, Tag 08PU] in D(B) — CommAlgCat.standardResolutionCotangentDerivedLowerShriekIsoOfLE and CommAlgCat.smallResolutionCotangentDerivedLowerShriekIso — identify both complexes with Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲), which mentions no resolution.

def cotangentComplexIsoOfResolution :
    DerivedCategory.Q.obj (cotangentComplex.{u, u} A B) ≅
      DerivedCategory.Q.obj (resolutionCotangentComplex.{u, u} A B P ε)

CommAlgCat.resolutionModuleLeftDerivedLowerShriekNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionCotangentAny.lean, line 182. The attribute's comment: “the cosimplicial object of a resolution and the conclusion Lpi_!(F) = F(P_bullet, ε) in D(B) functorially in F, for an arbitrary resolution with no bound on the number of variables, read at the small model of the footnote-restricted site for the reason recorded in StacksFrontier/Cotangent/ResolutionPointCriterionSmall.lean”.

Lπ_!(ℱ) = ℱ(P_•, ε) in D(B) for an arbitrary resolution. Let ε : P_• ⟶ B be a resolution of B over A, with no bound on the number of variables. For every sheaf of B-modules ℱ on the small model of the site C_{B/A} restricted to polynomial algebras on at most CommAlgCat.resolutionVarCardinal A B hε.isPolynomialAlgebra variables — a bound the resolution supplies — the sections at the point of L_nπ_!(ℱ) are the degree n homology of the Moore complex of the simplicial B-module ℱ(P_•, ε), naturally in ℱ.

This is CommAlgCat.smallResolutionModuleLeftDerivedLowerShriekNatIso at that cardinal. A bound cannot be dispensed with altogether here, as it can in CommAlgCat.cotangentComplexIsoOfResolution: the site, and with it π_!, is the one restricted by the bound.

def resolutionModuleLeftDerivedLowerShriekNatIso (n : ℕ) :
    (modulePointLowerShriek
          (smallBoundedPolynomialSite A B (resolutionVarCardinal A B hε.isPolynomialAlgebra))
          (B : Type u)).leftDerived n ⋙
        Stacks.ChaoticSite.pointSections.{u, u + 1, u} (ModuleCat.{u} (B : Type u)) ≅
      sheafToPresheaf (GrothendieckTopology.trivial
            (smallBoundedPolynomialSite A B (resolutionVarCardinal A B hε.isPolynomialAlgebra)))
          (ModuleCat.{u} (B : Type u)) ⋙
        moduleCosimplicialMooreComplex (smallResolutionCosimplicialObject ε
            (resolutionVarCardinal A B hε.isPolynomialAlgebra)
            (isPolynomialAlgebraBelow_resolutionVarCardinal A B hε.isPolynomialAlgebra)) ⋙
          HomologicalComplex.homologyFunctor (ModuleCat.{u} (B : Type u))
            (ComplexShape.down ℕ) n

CommAlgCat.quasiIso_alternatingFaceMapComplex_map_of_isResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionIndependence.lean, line 199. The attribute's comment: “the remark's payoff, at the arrow level: for any two resolutions of B over A and any morphism between them, the induced map of the complexes Omega[-/A] ⊗ B is a quasi-isomorphism, so any resolution computes L_{B/A} and the comparison is the induced map”.

Remark 08QI at the arrow level. Let ε : P_• ⟶ B and ε' : P'_• ⟶ B be resolutions of B over A in the sense of [Stacks, Tag 08QI]. Every morphism ψ of the attached simplicial objects of Over B — equivalently, every morphism P_• ⟶ P'_• of simplicial A-algebras compatible with the augmentations — induces a quasi-isomorphism

Ω[P_•⁄A] ⊗_{P_•} B ⟶ Ω[P'_•⁄A] ⊗_{P'_•} B.

So any resolution computes the cotangent complex, and the isomorphism is the one a morphism of resolutions induces; no cardinal bound appears, the terms of the two resolutions being bounded by a single cardinal.

theorem quasiIso_alternatingFaceMapComplex_map_of_isResolution
    (hres : IsResolution A (B : Type u) P ε) (hres' : IsResolution A (B : Type u) P' ε')
    (ψ : resolutionOver ε ⟶ resolutionOver ε') :
    QuasiIso ((alternatingFaceMapComplex (ModuleCat.{u} (B : Type u))).map
      (Functor.whiskerRight ψ (overDifferentialsFunctor (A := A) (B := B))))

CommAlgCat.resolutionCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ResolutionIndependence.lean, line 216. The attribute's comment: “the remark's payoff, at the object level: for any resolution of B over A the complex Omega[P_./A] ⊗_{P_.} B is L_{B/A} in D(B)”.

Remark 08QI at the object level. The complex Ω[P_•⁄A] ⊗_{P_•} B of an arbitrary resolution of B over A, read in cohomological degrees ≤ 0, is the cotangent complex L_{B/A} in D(B). Both are identified with Lπ_!(i^*Ω_{𝒪/A}) by [Stacks, Tag 08PU] in D(B), read at a bound containing both the given resolution and the standard one.

def resolutionCotangentComplexIso (hres : IsResolution A (B : Type u) P ε) :
    DerivedCategory.Q.obj
        (((alternatingFaceMapComplex (ModuleCat.{u} (B : Type u))).obj
            (resolutionOver ε ⋙ overDifferentialsFunctor)).extend
          (ComplexShape.embeddingUpIntLE (0 : ℤ))) ≅
      DerivedCategory.Q.obj (cotangentComplex.{u, u} A B)

CommAlgCat.standardResolution_isResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/StandardResolutionIsResolution.lean, line 120. The attribute's comment: “standard_qualifies”.

Stacks Project, Tag 08QI. The standard augmented simplicial algebra of a commutative A-algebra B is a resolution of B over A.

public theorem standardResolution_isResolution (A : Type u) [CommRing A]
    (B : CommAlgCat.{max u v} A) :
    IsResolution A B (standardResolution A B).left (standardResolution A B).hom
Tag 08QJ, a lemma

Tag 08QJ in the Stacks Project.

CommAlgCat.isIso_derivedColimitTensorComparison_smallPolynomialAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteCoefficientChange.lean, line 1276. The attribute's comment: “for an 𝒪-module in cohomological degree zero, on the small model of the site C_{B/A}; on a chaotic site Li^*ℱ and ℱ ⊗^L_𝒪 B̲ are the same object”.

The change of coefficients of [Stacks, Tag 08QJ]. Let A → B be a ring map and let 𝒪, B̲ and π be as in [Stacks, Tag 08PR], read on the small model of C_{B/A} at the cardinal CommAlgCat.standardResolutionVarCardinal A B bounding the standard resolution. Then for every 𝒪-module ℱ, placed in cohomological degree zero, the canonical comparison

Lπ_!(ℱ) ⟶ Lπ_!(ℱ ⊗^L_𝒪 B̲)

is an isomorphism in D(Ab).

The source states the right-hand side as Lπ_!(Li^*ℱ) for the morphism of topoi i attached to the ring map B ⟶ B; on a chaotic site that morphism is the identity on topoi, so Li^*ℱ and ℱ ⊗^L_𝒪 B̲ are one and the same object of D(Mod(B̲)) and the two readings of the statement coincide. The comparison itself is Stacks.ChaoticSite.derivedColimitTensorComparison: derived lower shriek applied to the unit of the derived change-of-coefficients adjunction, followed by the identification of Lπ_! on B̲-modules with Lπ_! on their underlying 𝒪-modules, which is an isomorphism because restriction of scalars does not change the underlying abelian presheaf.

Both hypotheses of [Stacks, Tag 08RX] are discharged, so nothing is assumed: CommAlgCat.isPointResolution_standardResolutionSmallCosimplicialObject is [Stacks, Tag 08PS] at this model, and CommAlgCat.isIso_leftDerivedColimit_map_smallPolynomialAugmentationAbelian is Lπ_!(𝒪) = Lπ_!(B̲) read degreewise. The dévissage from those two to an arbitrary 𝒪-module is Stacks.ChaoticSite.isIso_derivedColimitTensorComparison_app_single.

public theorem isIso_derivedColimitTensorComparison_smallPolynomialAugmentation
    (F : PresheafOfModules.{u}
      (smallPolynomialStructurePresheaf A B (standardResolutionVarCardinal A B))) :
    IsIso ((Stacks.ChaoticSite.derivedColimitTensorComparison
        (smallPolynomialAugmentation A B (standardResolutionVarCardinal A B))).app
      (DerivedCategory.Q.obj
        ((HomologicalComplex.single (PresheafOfModules.{u}
          (smallPolynomialStructurePresheaf A B (standardResolutionVarCardinal A B)))
            (ComplexShape.up ℤ) 0).obj F)))
Tag 08QK, a lemma

Tag 08QK in the Stacks Project.

CommAlgCat.polynomialSiteDerivedLowerShriekDifferentialsBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteDifferentialsBaseChangeLargeSite.lean, line 316. The attribute's comment: “Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) = Lπ_!(Ω_{𝒪/A}) in D(Ab), as the isomorphism induced by the base-change unit Ω_{𝒪/A} ⟶ Ω_{𝒪/A} ⊗_𝒪 B̲, for the point morphism of the site C_{B/A} of Tag 08PR itself -- not of the footnote-restricted site nor of a small model of it -- with Ω_{𝒪/A} the sheaf of relative differentials of that site and Ω_{𝒪/A} ⊗_𝒪 B̲ its base change along the augmentation 𝒪 ⟶ B̲ of Tag 08PR, under no hypothesis on A → B and no cardinal bound”.

Lπ_!(Ω_{𝒪/A}) = Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) in D(Ab) at the site C_{B/A} itself, the last identification of [Stacks, Tag 08QK], as the isomorphism induced by the base-change unit Ω_{𝒪/A} ⟶ Ω_{𝒪/A} ⊗_𝒪 B̲.

Here Ω_{𝒪/A} is the sheaf of relative differentials of [Stacks, Tag 08PR]'s site, read on its underlying abelian sheaf, Ω_{𝒪/A} ⊗_𝒪 B̲ is its base change along the augmentation 𝒪 ⟶ B̲ of that tag, π is the point morphism of the site C_{B/A} -- not of a restriction of it -- and Lπ_! is the total left derived functor of the colimit over the index category, which is the π_! of [Stacks, Tag 08PF]. There is no hypothesis on A → B beyond its being a ring map, and no cardinal bound on the sets of variables.

The two inputs are the criterion of [Stacks, Tag 08Q9] with no smallness hypothesis on the site, Stacks.ChaoticSite.AbelianValued.isIso_totalDerivedColimit_single_map_iff_of_large, and the quasi-isomorphism of Moore complexes CommAlgCat.quasiIso_mooreCochain_polynomialSiteDifferentialsBaseChangeUnit, which is the Δ-instance of [Stacks, Tag 08RX] rather than [Stacks, Tag 08QJ].

def polynomialSiteDerivedLowerShriekDifferentialsBaseChangeIso :
    polynomialSiteDerivedLowerShriekSingle A B
        (polynomialSiteAbelianRelativeDifferentials A B) ≅
      polynomialSiteDerivedLowerShriekSingle A B
        (polynomialSiteAbelianDifferentialsBaseChange A B)

CommAlgCat.polynomialSiteDerivedLowerShriekConstantIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSitePointValuesLargeSite.lean, line 259. The attribute's comment: “Lπ_!(B̲) = B in D(Ab), for the point morphism of the site C_{B/A} of Tag 08PR itself -- not of the footnote-restricted site nor of a small model of it -- with Lπ_! the total left derived functor of the colimit over the index category, which is the π_! of Tag 08PF, and with B read as the abelian group ULift.{u+1} B exactly as the site's own ringed point CommAlgCat.polynomialRingedPoint reads it”.

Lπ_!(B̲) = B in D(Ab) at the site C_{B/A} itself, the second identification of [Stacks, Tag 08QK]. Here B̲ is the constant sheaf of rings with value B of [Stacks, Tag 08PR] read on its underlying abelian sheaf, π is the point morphism of the site C_{B/A} of that tag -- not of a restriction of it -- and Lπ_! is the total left derived functor of the colimit over the index category, which is the π_! of [Stacks, Tag 08PF].

The proof is the source's: the polynomial algebra on no variables, augmented by A → B, is a terminal object of the site (CommAlgCat.isTerminal_polynomialBaseObj), so π^{-1} is the constant diagram and has an exact right adjoint, and [Stacks, Tag 08Q7] in the form Stacks.ChaoticSite.derivedConstCompColimitIso' gives Lπ_! ∘ π^{-1} = id.

def polynomialSiteDerivedLowerShriekConstantIso :
    polynomialSiteDerivedLowerShriekSingle A B (polynomialSiteAbelianConstantPresheaf A B) ≅
      polynomialSiteBaseInDerived A B

CommAlgCat.polynomialSiteDerivedLowerShriekStructureConstantIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSitePointValuesLargeSite.lean, line 430. The attribute's comment: “Lπ_!(𝒪) = Lπ_!(B̲) in D(Ab), as the isomorphism induced by the augmentation 𝒪 ⟶ B̲ of Tag 08PR, for the point morphism of the site C_{B/A} of Tag 08PR itself -- not of the footnote-restricted site nor of a small model of it”.

Lπ_!(𝒪) = Lπ_!(B̲) in D(Ab) at the site C_{B/A} itself, the first identification of [Stacks, Tag 08QK], as the isomorphism induced by the augmentation 𝒪 ⟶ B̲ of [Stacks, Tag 08PR].

The two inputs are the criterion of [Stacks, Tag 08Q9] with no smallness hypothesis on the site, Stacks.ChaoticSite.AbelianValued.isIso_totalDerivedColimit_single_map_iff_of_large, and the quasi-isomorphism of Moore complexes CommAlgCat.quasiIso_mooreCochain_polynomialSiteAbelianAugmentation, whose own input is [Stacks, Tag 08QI].

def polynomialSiteDerivedLowerShriekStructureConstantIso :
    polynomialSiteDerivedLowerShriekSingle A B (polynomialSiteAbelianStructurePresheaf A B) ≅
      polynomialSiteDerivedLowerShriekSingle A B (polynomialSiteAbelianConstantPresheaf A B)

CommAlgCat.polynomialSiteDerivedLowerShriekStructureIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSitePointValuesLargeSite.lean, line 448. The attribute's comment: “Lπ_!(𝒪) = B in D(Ab), for the point morphism of the site C_{B/A} of Tag 08PR itself -- not of the footnote-restricted site nor of a small model of it”.

Lπ_!(𝒪) = B in D(Ab) at the site C_{B/A} itself, the composite of the two identifications Lπ_!(𝒪) = Lπ_!(B̲) and Lπ_!(B̲) = B of [Stacks, Tag 08QK].

def polynomialSiteDerivedLowerShriekStructureIso :
    polynomialSiteDerivedLowerShriekSingle A B (polynomialSiteAbelianStructurePresheaf A B) ≅
      polynomialSiteBaseInDerived A B

CommAlgCat.polynomialSiteDerivedLowerShriekCotangentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSitePointValuesLargeSite.lean, line 520. The attribute's comment: “L_{B/A} = Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) in D(Ab), for the point morphism of the site C_{B/A} of Tag 08PR itself -- not of the footnote-restricted site nor of a small model of it: the cotangent complex of Tag 08PN, read in D(Ab) at the coefficient universe of the site, is Lπ_! of the sheaf i^*Ω_{𝒪/A}”.

L_{B/A} = Lπ_!(Ω_{𝒪/A} ⊗_𝒪 B̲) in D(Ab) at the site C_{B/A} itself, the third identification of [Stacks, Tag 08QK]. The left-hand side is the cotangent complex of [Stacks, Tag 08PN] with its B-module structures forgotten, read at the coefficient universe of the site; the right-hand side is Lπ_! of the abelian sheaf i^*Ω_{𝒪/A} = Ω_{𝒪/A} ⊗_𝒪 B̲.

The two inputs are [Stacks, Tag 08PS] at C_{B/A} itself, CommAlgCat.polynomialSiteResolutionDerivedColimitNatIso, which computes Lπ_! by the extended Moore complex of the evaluation on the standard resolution, and CommAlgCat.polynomialSiteCotangentMooreComplexIso, which is [Stacks, Tag 08PU] identifying that Moore complex with the complex of L_{B/A}.

def polynomialSiteDerivedLowerShriekCotangentIso :
    polynomialSiteDerivedLowerShriekSingle A B (polynomialSiteAbelianCotangentPresheaf A B) ≅
      polynomialSiteCotangentInDerived A B
Tag 08SA, a lemma

Tag 08SA in the Stacks Project.

CommAlgCat.exists_distTriang_derivedExtensionScalars_cotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/StandardResolutionOverPolynomialBase.lean, line 1089.

Stacks Project, Tag 08SA. Let A → B → C be ring maps. If B is a polynomial algebra over A, then there is a distinguished triangle

L_{B/A} ⊗^𝐋_B C → L_{C/A} → L_{C/B} → (L_{B/A} ⊗^𝐋_B C)[1]

in D(C). This is the lemma as stated.

The proof is the source's. The standard resolution P_• of C over B is, read over A, also a resolution of C over A (CommAlgCat.standardResolution_isResolution_restrictScalars); the differentials of the tower A → B → Pₙ form a split short exact sequence because Pₙ is a polynomial algebra over B, and base changing it to C gives a short exact sequence of complexes of C-modules Ω[B⁄A] ⊗[B] C → Ω[P_•⁄A] ⊗[P_•] C → Ω[P_•⁄B] ⊗[P_•] C (CommAlgCat.restrictedCotangentComplexShortComplex_shortExact) whose distinguished triangle is the one asserted. Its last term is L_{C/B} by definition; its first term is Ω[B⁄A] ⊗[B] C in degree 0, which is L_{B/A} ⊗^𝐋_B C by Tag 08QH and the projectivity of Ω[B⁄A] (CommAlgCat.nonempty_derivedExtensionScalars_cotangentComplex_iso_of_isPolynomialAlgebra); and its middle term is L_{C/A} because P_• and the standard resolution of C over A are two resolutions of C over A, so by Tag 08PU both compute derived lower shriek of i^*Ω_{𝒪/A} on the site C_{C/A} (CommAlgCat.nonempty_q_restrictedCotangentComplex_iso_cotangentComplex).

The triangle is stated existentially, as in the source: the identifications of the first and middle terms are isomorphisms of objects of D(C), which transport a distinguished triangle to one with the named objects. The three rings are taken in one universe, which is no restriction: three rings with maps between them always live in a common universe. The conditional form at two universes, with the identification of the middle term as a hypothesis, is CommAlgCat.exists_distTriang_derivedExtensionScalars_of_isPolynomialAlgebra.

public theorem exists_distTriang_derivedExtensionScalars_cotangentComplex
    (A : Type u) [CommRing A] (B : Type u) [CommRing B] [Algebra A B]
    (C : Type u) [CommRing C] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
    (hB : Algebra.IsPolynomialAlgebra A B) :
    ∃ (f : (CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral
            (algebraMap B C)).functor.obj
          (DerivedCategory.Q.obj (cotangentComplexOfAlgebra.{u, u} A B)) ⟶
        DerivedCategory.Q.obj (cotangentComplexOfAlgebra.{u, u} A C))
      (g : DerivedCategory.Q.obj (cotangentComplexOfAlgebra.{u, u} A C) ⟶
        DerivedCategory.Q.obj (cotangentComplexOfAlgebra.{u, u} B C))
      (h : DerivedCategory.Q.obj (cotangentComplexOfAlgebra.{u, u} B C) ⟶
        ((CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral
            (algebraMap B C)).functor.obj
          (DerivedCategory.Q.obj (cotangentComplexOfAlgebra.{u, u} A B)))⟦(1 : ℤ)⟧),
      Pretriangulated.Triangle.mk f g h ∈
        Pretriangulated.distinguishedTriangles (C := DerivedCategory (ModuleCat.{u} C))
Tag 09D4, an example

Tag 09D4 in the Stacks Project.

Algebra.PolynomialPresentationWithKernelGenerators.Degeneracies.degeneracyZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/Degeneracies.lean, line 81. The attribute's comment: “degeneracies”.

The first degeneracy fixes uᵢ and sends xₜ to yₜ.

noncomputable def degeneracyZero :
    DegreeOne.P1 p →ₐ[p.A] DegreeTwo.P2 p

Algebra.PolynomialPresentationWithKernelGenerators.Degeneracies.degeneracyOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/Degeneracies.lean, line 89. The attribute's comment: “degeneracies”.

The second degeneracy fixes uᵢ and sends xₜ to zₜ.

noncomputable def degeneracyOne :
    DegreeOne.P1 p →ₐ[p.A] DegreeTwo.P2 p

Algebra.PolynomialPresentationWithKernelGenerators.Degeneracies.degeneracyZero_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/Degeneracies.lean, line 98. The attribute's comment: “degeneracies”.

The first degeneracy is the unique algebra map with the displayed values on the old and relation variables.

theorem degeneracyZero_unique
    (f : DegreeOne.P1 p →ₐ[p.A] DegreeTwo.P2 p)
    (hu : ∀ i : p.variableIndex,
      f (MvPolynomial.X (Sum.inl i)) =
        MvPolynomial.X (DegreeTwo.DegreeTwoVariable.base i))
    (hx : ∀ t : p.relationIndex,
      f (MvPolynomial.X (Sum.inr t)) =
        MvPolynomial.X (DegreeTwo.DegreeTwoVariable.y t)) :
    f = degeneracyZero p

Algebra.PolynomialPresentationWithKernelGenerators.Degeneracies.degeneracyOne_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/Degeneracies.lean, line 116. The attribute's comment: “degeneracies”.

The second degeneracy is the unique algebra map with the displayed values on the old and relation variables.

theorem degeneracyOne_unique
    (f : DegreeOne.P1 p →ₐ[p.A] DegreeTwo.P2 p)
    (hu : ∀ i : p.variableIndex,
      f (MvPolynomial.X (Sum.inl i)) =
        MvPolynomial.X (DegreeTwo.DegreeTwoVariable.base i))
    (hx : ∀ t : p.relationIndex,
      f (MvPolynomial.X (Sum.inr t)) =
        MvPolynomial.X (DegreeTwo.DegreeTwoVariable.z t)) :
    f = degeneracyOne p

Algebra.PolynomialPresentationWithKernelGenerators.Degeneracies.degeneracyZero_lifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/Degeneracies.lean, line 330. The attribute's comment: “degeneracies”.

The displayed first degeneracy lifts the first degeneracy of the one-coskeleton.

theorem degeneracyZero_lifts :
    AlgCat.ofHom (degeneracyZeroLift p) ≫
        DegreeTwo.degreeTwoToCoskeleton p =
        (DegreeOne.degreeOneCoskeleton p).oneIso.inv ≫
        (DegreeOne.degreeOneCoskeleton p).simplicial.σ (0 : Fin 2)

Algebra.PolynomialPresentationWithKernelGenerators.Degeneracies.degeneracyOne_lifts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/Degeneracies.lean, line 344. The attribute's comment: “degeneracies”.

The displayed second degeneracy lifts the second degeneracy of the one-coskeleton.

theorem degeneracyOne_lifts :
    AlgCat.ofHom (degeneracyOneLift p) ≫
        DegreeTwo.degreeTwoToCoskeleton p =
      (DegreeOne.degreeOneCoskeleton p).oneIso.inv ≫
        (DegreeOne.degreeOneCoskeleton p).simplicial.σ (1 : Fin 2)

Algebra.PolynomialPresentationWithKernelGenerators.Degeneracies.explicitResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/Degeneracies.lean, line 1526. The attribute's comment: “degeneracies”.

The displayed first three degrees extend to a polynomial simplicial resolution of B over A.

noncomputable def explicitResolution : ExplicitResolution p

Algebra.PolynomialPresentationWithKernelGenerators.DegreeOne.degreeOneCoskeleton, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeOne.lean, line 377. The attribute's comment: “degree_one”.

The coskeleton of the explicit one-truncated polynomial simplicial algebra.

noncomputable def degreeOneCoskeleton : DegreeOneCoskeleton p

Algebra.PolynomialPresentationWithKernelGenerators.DegreeOne.range_faceZero_sub_faceOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeOne.lean, line 563. The attribute's comment: “degree_one”.

Exactness at P₀ of P₁ → P₀ → B.

theorem range_faceZero_sub_faceOne :
    Set.range (fun z : P1 p => faceZero p z - faceOne p z) =
      {z : p.P0 | augmentationZero p z = 0}

Algebra.PolynomialPresentationWithKernelGenerators.DegreeOne.facePair_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeOne.lean, line 606. The attribute's comment: “degree_one”.

Every compatible pair of degree-zero simplices lifts to degree one.

theorem facePair_surjective :
    ∀ a b : p.P0,
      augmentationZero p a = augmentationZero p b →
        ∃ z : P1 p, faceZero p z = a ∧ faceOne p z = b

Algebra.PolynomialPresentationWithKernelGenerators.DegreeOne.coskeleton_trivialKanFibration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeOne.lean, line 700. The attribute's comment: “degree_one”.

The augmentation of this degree-one coskeleton is a trivial Kan fibration.

theorem coskeleton_trivialKanFibration :
    SSet.trivialKanFibrations
      (Functor.whiskerRight (degreeOneCoskeleton p).augmentation
        (forget (AlgCat.{max u v w x} p.A)))

Algebra.PolynomialPresentationWithKernelGenerators.DegreeTwo.faces_matching, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeTwo.lean, line 191. The attribute's comment: “degree_two”.

The three displayed face maps define a map to the degree-two matching object.

theorem faces_matching (q : P2 p) :
    MatchingTriple p (faceZero p q) (faceOne p q) (faceTwo p q)

Algebra.PolynomialPresentationWithKernelGenerators.DegreeTwo.matchingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeTwo.lean, line 878. The attribute's comment: “degree_two”.

The actual second degree of the one-coskeleton is canonically the algebra of compatible triples of degree-one elements.

noncomputable def matchingEquiv :
    ((DegreeOne.degreeOneCoskeleton p).simplicial _⦋2⦌) ≃
      {g : (DegreeOne.P1 p ×
          DegreeOne.P1 p × DegreeOne.P1 p) //
        MatchingTriple p g.1 g.2.1 g.2.2}

Algebra.PolynomialPresentationWithKernelGenerators.DegreeTwo.matchingEquiv_faces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeTwo.lean, line 905. The attribute's comment: “degree_two”.

The canonical matching equivalence records exactly the three actual faces of a degree-two simplex.

theorem matchingEquiv_faces
    (a : (DegreeOne.degreeOneCoskeleton p).simplicial _⦋2⦌) :
    (matchingEquiv p a).val =
      (coskeletonFace p 0 a, coskeletonFace p 1 a, coskeletonFace p 2 a)

Algebra.PolynomialPresentationWithKernelGenerators.DegreeTwo.degreeTwoToCoskeleton, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeTwo.lean, line 1053. The attribute's comment: “degree_two”.

The algebra map from the displayed polynomial degree two to the actual degree-two object of the one-coskeleton.

noncomputable def degreeTwoToCoskeleton :
    algP2 p ⟶ (DegreeOne.degreeOneCoskeleton p).simplicial _⦋2⦌

Algebra.PolynomialPresentationWithKernelGenerators.DegreeTwo.matchingEquiv_degreeTwoToCoskeleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeTwo.lean, line 1136. The attribute's comment: “degree_two”.

Under the canonical matching equivalence, the algebra map has the three displayed face maps as its components.

theorem matchingEquiv_degreeTwoToCoskeleton (q : P2 p) :
    matchingEquiv p (degreeTwoToCoskeleton p (ULift.up q)) =
      ⟨(faceZero p q, faceOne p q, faceTwo p q), faces_matching p q⟩

Algebra.PolynomialPresentationWithKernelGenerators.DegreeTwo.degreeTwoToCoskeleton_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/Degeneracies/DegreeTwo.lean, line 1518. The attribute's comment: “degree_two”.

The displayed algebra map onto the actual second coskeleton degree is surjective.

theorem degreeTwoToCoskeleton_surjective :
    Function.Surjective (degreeTwoToCoskeleton p)
Sources
LeanCommAlgCat.finiteType_succ_of_trivialKanFibration_of_isCoskeletal · CommAlgCat.exists_trivialKanFibration_from_finiteType_polynomial_simplicialAlgebra · CommAlgCat.smallResolutionLeftDerivedMooreHomologyIso · CommAlgCat.finite_homology_smallResolutionMooreComplex · CommAlgCat.finite_moduleLeftDerivedPointLowerShriek · CommAlgCat.finite_homology_cotangentComplex · CommAlgCat.IsResolution · CommAlgCat.isResolution_quasiIso_homotopyEquivalence_tfae

Section92.6 Functoriality#

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

Tag 08QN, an equation

Tag 08QN in the Stacks Project.

Stacks.ChaoticSite.isTransport_coefficientSquareComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/ConstantRingedSquares.lean, line 396. The attribute's comment: “change-of-coefficients square: the comparison is the canonical one”.

The comparison is the canonical one. It is the identity of the restriction functor along C ⥤ *, not some other automorphism of it; this is what makes Stacks.ChaoticSite.coefficientSquare_commutes a statement about the square rather than about a choice.

theorem isTransport_coefficientSquareComparison :
    Stacks.IsTransport (coefficientSquareComparison.{w} C φ).hom

Stacks.ChaoticSite.coefficientSquare_commutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/ConstantRingedSquares.lean, line 475. The attribute's comment: “the change-of-coefficients square of constant-coefficient ringed topoi”.

The change-of-coefficients square commutes. The structure map of the one composite, transported along the adjoint mate of the canonical comparison, is the structure map of the other; see AlgebraicGeometry.RingedToposHom.SquareCommutes, which is that equation.

theorem coefficientSquare_commutes :
    SquareCommutes (X := constantRingedTopos C R')
      (Y := constantRingedTopos (Discrete PUnit.{u₁ + 1}) R)
      (coefficientSquareDownAcross.{w} C φ) (coefficientSquareAcrossDown.{w} C φ)
      (coefficientSquareComparison.{w} C φ)

Stacks.ChaoticSite.isTransport_functorialitySquareComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/ConstantRingedSquares.lean, line 552. The attribute's comment: “functoriality triangle: the comparison is the canonical one”.

The comparison is the canonical one, hence a transport: it is built from the identification u ⋙ star = star of the two functors to the point and nothing else.

theorem isTransport_functorialitySquareComparison :
    Stacks.IsTransport (functorialitySquareComparison.{w} C D u R).hom

Stacks.ChaoticSite.functorialitySquare_commutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/ConstantRingedSquares.lean, line 574. The attribute's comment: “the functoriality triangle of constant-coefficient ringed topoi”.

The functoriality triangle commutes. Every edge is a transport, so the structure map of π_C ∘ g transported along the adjoint mate of the canonical comparison is the structure map of π_D.

theorem functorialitySquare_commutes :
    (constantRingedTopos (Discrete PUnit.{u₁ + 1}) R).forgetRing.map
        (functorialitySquareAcrossDown.{w} C D u R).fSharp ≫
      (((functorialitySquareAcrossDown.{w} C D u R).toToposHom.adj.ofNatIsoLeft
            (functorialitySquareComparison.{w} C D u R)).rightAdjointUniq
          (constantProjection.{w} D R).toToposHom.adj).hom.app
        ((constantRingedTopos D R).forgetRing.obj (constantRingedTopos D R).O) =
      (constantRingedTopos (Discrete PUnit.{u₁ + 1}) R).forgetRing.map
        (constantProjection.{w} D R).fSharp

CommAlgCat.baseChangeAugmentation_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChange.lean, line 84. The attribute's comment: “base-change augmentation on a pure tensor”.

The augmentation of A' ⊗_A P sends a' ⊗ p to a' · b(α(p)).

theorem baseChangeAugmentation_tmul (X : Over B) (a' : A') (p : (X.left : Type u)) :
    baseChangeAugmentation b X (a' ⊗ₜ[A] p) =
      algebraMap A' (B' : Type u) a' * b (X.hom.hom p)

CommAlgCat.baseChangeMap_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChange.lean, line 96. The attribute's comment: “base change of a morphism on a pure tensor”.

Extension of scalars of a morphism f of augmented algebras sends a' ⊗ p to a' ⊗ f(p).

theorem baseChangeMap_tmul {X Y : Over B} (f : X ⟶ Y) (a' : A') (p : (X.left : Type u)) :
    baseChangeMap f (a' ⊗ₜ[A] p) = a' ⊗ₜ[A] f.left.hom p

CommAlgCat.isPolynomialAlgebra_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChange.lean, line 156. The attribute's comment: “base change preserves polynomial algebras”.

Extension of scalars takes a polynomial A-algebra to a polynomial A'-algebra: A' ⊗_A A[S] = A'[S].

theorem isPolynomialAlgebra_baseChange (P : CommAlgCat.{u} A)
    (hP : IsPolynomialAlgebra A P) :
    IsPolynomialAlgebra A' (baseChangeObj (A' := A') P)

CommAlgCat.polynomialBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChange.lean, line 180. The attribute's comment: “polynomial-site base change”.

The functor of sites C_{B/A} ⟶ C_{B'/A'} induced by a commutative square of rings, given by extension of scalars on polynomial algebras augmented to B.

def polynomialBaseChange : polynomialSite A B ⥤ polynomialSite A' B'

CommAlgCat.polynomialBaseChange_obj_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChange.lean, line 186. The attribute's comment: “polynomial-site base change on objects”.

The augmentation of the image of X under polynomialBaseChange b is baseChangeAugmentation b X.

theorem polynomialBaseChange_obj_hom (X : polynomialSite A B) :
    ((polynomialBaseChange b).obj X).unop.obj.hom =
      CommAlgCat.ofHom (baseChangeAugmentation b X.unop.obj)

CommAlgCat.polynomialBaseChange_map_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChange.lean, line 193. The attribute's comment: “polynomial-site base change on morphisms”.

The underlying algebra map of the image of f under polynomialBaseChange b is baseChangeMap f.

theorem polynomialBaseChange_map_left {X Y : polynomialSite A B} (f : X ⟶ Y) :
    ((polynomialBaseChange b).map f).unop.hom.left =
      CommAlgCat.ofHom (baseChangeMap f.unop.hom)

CommAlgCat.boundedPolynomialBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialSiteBaseChangeShriek.lean, line 92. The attribute's comment: “polynomial-site base change, with the section's footnote in force: the functor between the sites restricted to at most κ variables. The unrestricted version is CommAlgCat.polynomialBaseChange”.

The base-change functor of sites C_{B/A} ⟶ C_{B'/A'}, between the sites restricted to polynomial algebras on at most κ variables.

def boundedPolynomialBaseChange :
    boundedPolynomialSite A B κ ⥤ boundedPolynomialSite A' B' κ
Tag 08QP, a lemma

Tag 08QP in the Stacks Project.

CommAlgCat.leftDerivedPointLowerShriekPolynomialBaseChangeNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialSiteBaseChangeShriek.lean, line 210. The attribute's comment: “a GENERALIZATION of the lemma: the identification Lπ_!(g^{-1}ℱ') = Lπ'_!(ℱ') under the weaker hypothesis that the base change A' ⊗_A P_• ⟶ B' of the chosen resolution is again a resolution, which is what the source's proof derives from B ⊗_A^L A' = B'. The source's own statement is CommAlgCat.leftDerivedPointLowerShriekPolynomialBaseChangeNatIsoOfTorIndependent, proved from this one. Both are read at the small model of the footnote-restricted site C_{B/A} and through the sections at the point”.

Let 

A  --→  A'
|       |
B  --→  B'
be a commutative square of rings, let C_{B/A} and C_{B'/A'} be the sites of polynomial algebras augmented to B, resp. to B', of Tag 08PR, and let g be the morphism of topoi induced by the base-change functor of Tag 08QN, so that g^{-1} is restriction along it. Let ε : P_• ⟶ B be a resolution of B over A whose terms are polynomial algebras on at most κ variables, and assume that the base-changed augmentation A' ⊗_A P_• ⟶ B' is again a resolution of B' over A'. Then

Lπ_!(g^{-1}ℱ') = Lπ'_!(ℱ')

in every degree n and naturally in the abelian sheaf ℱ' on C_{B'/A'}, read through the sections at the point. Both sites are read at the small model of their restriction to at most κ variables.

def leftDerivedPointLowerShriekPolynomialBaseChangeNatIso
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A))))
    (hres : IsResolution A' (B' : Type u)
      (simplicialBaseChange b ε) (augmentationBaseChange b ε))
    (n : ℕ) :
    (smallPolynomialBaseChange b κ).sheafPushforwardContinuous AddCommGrpCat.{u}
          (GrothendieckTopology.trivial (smallBoundedPolynomialSite A B κ))
          (GrothendieckTopology.trivial (smallBoundedPolynomialSite A' B' κ)) ⋙
        (Stacks.ChaoticSite.abelianPointLowerShriek
            (smallBoundedPolynomialSite A B κ)).leftDerived n ⋙
          Stacks.ChaoticSite.pointSections AddCommGrpCat.{u} ≅
      (Stacks.ChaoticSite.abelianPointLowerShriek
          (smallBoundedPolynomialSite A' B' κ)).leftDerived n ⋙
        Stacks.ChaoticSite.pointSections AddCommGrpCat.{u}

CommAlgCat.leftDerivedPointLowerShriekPolynomialBaseChangeNatIsoOfTorIndependent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialSiteBaseChangeShriek.lean, line 254. The attribute's comment: “the lemma as stated: the identification Lπ_!(g^{-1}ℱ') = Lπ'_!(ℱ') from the source's own hypothesis that the square induce a quasi-isomorphism B ⊗_A^L A' = B', written out as vanishing of the positive Tor_i^A(A', B) together with bijectivity of A' ⊗_A B → B'. Read at the small model of the footnote-restricted site C_{B/A} and through the sections at the point; the generalization assuming only that the base-changed augmentation is a resolution is CommAlgCat.leftDerivedPointLowerShriekPolynomialBaseChangeNatIso”.

Let 

A  --→  A'
|       |
B  --→  B'
be a commutative square of rings which induces a quasi-isomorphism B ⊗_A^L A' = B' — that is, Tor_i^A(A', B) = 0 for i > 0 and the canonical map A' ⊗_A B → B' is bijective. Let C_{B/A} and C_{B'/A'} be the sites of polynomial algebras augmented to B, resp. to B', of Tag 08PR, and let g be the morphism of topoi induced by the base-change functor of Tag 08QN, so that g^{-1} is restriction along it. Then

Lπ_!(g^{-1}ℱ') = Lπ'_!(ℱ')

in every degree n and naturally in the abelian sheaf ℱ' on C_{B'/A'}, read through the sections at the point. Both sites are read at the small model of their restriction to at most κ variables, for any κ bounding the variables of a chosen resolution ε : P_• ⟶ B of B over A.

def leftDerivedPointLowerShriekPolynomialBaseChangeNatIsoOfTorIndependent
    (hres : IsResolution A (B : Type u) P ε)
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hφ : Function.Bijective (baseChangeUnit b))
    (n : ℕ) :
    (smallPolynomialBaseChange b κ).sheafPushforwardContinuous AddCommGrpCat.{u}
          (GrothendieckTopology.trivial (smallBoundedPolynomialSite A B κ))
          (GrothendieckTopology.trivial (smallBoundedPolynomialSite A' B' κ)) ⋙
        (Stacks.ChaoticSite.abelianPointLowerShriek
            (smallBoundedPolynomialSite A B κ)).leftDerived n ⋙
          Stacks.ChaoticSite.pointSections AddCommGrpCat.{u} ≅
      (Stacks.ChaoticSite.abelianPointLowerShriek
          (smallBoundedPolynomialSite A' B' κ)).leftDerived n ⋙
        Stacks.ChaoticSite.pointSections AddCommGrpCat.{u}
Tag 08QQ, a lemma

Tag 08QQ in the Stacks Project.

CommAlgCat.cotangentExtendScalarsComplexMap_eq_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeComplexCounit.lean, line 267. The attribute's comment: “the arrow of the lemma is the functoriality map of Tag 08PN: the adjoint map out of extension of scalars is extension of scalars of the B-linear map of Tag 08PN followed by the counit, as an equality of maps of cotangent complexes”.

The two shapes of the functoriality map agree, on the cotangent complexes. The adjoint map L_{B/A} ⊗_B B' ⟶ L_{B'/A'} of [Stacks, Tag 08QQ] is extension of scalars along B → B' of the B-linear map L_{B/A} ⟶ L_{B'/A'} of [Stacks, Tag 08PN], followed by the counit B' ⊗_B L_{B'/A'} ⟶ L_{B'/A'}.

This is CommAlgCat.cotangentExtendScalarsMooreMap_eq_counit transported through the reindexing which places simplicial degree n in cohomological degree -n, by ModuleCat.extendMap_comp_extendRestrictScalarsAdjCounitComplex.

theorem cotangentExtendScalarsComplexMap_eq_counit :
    cotangentExtendScalarsComplexMap b =
      ((ModuleCat.extendScalars b.toRingHom).mapHomologicalComplex (ComplexShape.up ℤ)).map
          (squareCotangentComplexMap.{u, u, u} (algebraSquareOfAlgHom b)) ≫
        ModuleCat.extendRestrictScalarsAdjCounitComplex b.toRingHom (ComplexShape.up ℤ)
          (cotangentComplex.{u, u} A' B')

CommAlgCat.overDifferentialsBaseChangeNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIso.lean, line 250. The attribute's comment: “the step of the proof the source performs by inspection: extension of scalars along B → B' of i^Ω_{𝒪/A} is the restriction of i^Ω_{𝒪'/A'} along the base-change functor of sites of Tag 08QN”.

i^*Ω_{𝒪/A} ⊗_B B' = g^{-1}(i^*Ω_{𝒪'/A'}), the step the source performs by inspection. Extension of scalars along B → B' of the B-module of differentials B ⊗_P Ω[P⁄A] is the B'-module of differentials of the base-changed algebra A' ⊗_A P, naturally in the A-algebra P augmented to B.

def overDifferentialsBaseChangeNatIso :
    overDifferentialsFunctor (A := A) (B := B) ⋙ ModuleCat.extendScalars b.toRingHom ≅
      baseChangeOver b ⋙ overDifferentialsFunctor (A := A') (B := B')

CommAlgCat.quasiIso_cotangentExtendScalarsMooreMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIso.lean, line 564. The attribute's comment: “on the alternating-face-map complexes, under ONE carried hypothesis: Remark 08QI as CommAlgCat.CotangentComputedByEveryResolution, which Tag 08QI discharges; the source's own hypothesis and its conclusion on THE functoriality map of Tag 08PN are kept”.

Stacks 08QQ, on the alternating-face-map complexes. If the commutative square A → B, A → A', B → B', A' → B' induces a quasi-isomorphism B ⊗_A^L A' = B' — that is, A' and B are Tor-independent over A and A' ⊗_A B → B' is bijective — then the functoriality map L_{B/A} ⊗_B B' ⟶ L_{B'/A'} of Tag 08PN is a quasi-isomorphism.

The hypothesis B ⊗_A^L A' = B' makes the base change A' ⊗_A P_• ⟶ B' of the standard resolution a resolution of B' over A', and the functoriality map is the map induced by A' ⊗_A P_• ⟶ P'_• read through the identification of L_{B/A} ⊗_B B' with the complex of A' ⊗_A P_•; Remark 08QI, carried as CommAlgCat.CotangentComputedByEveryResolution, inverts that map.

theorem quasiIso_cotangentExtendScalarsMooreMap
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b))
    (hQI : CotangentComputedByEveryResolution A' B') :
    QuasiIso (cotangentExtendScalarsMooreMap b)

CommAlgCat.quasiIso_cotangentExtendScalarsComplexMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIso.lean, line 607. The attribute's comment: “on the cotangent complexes, under ONE carried hypothesis: Remark 08QI as CommAlgCat.CotangentComputedByEveryResolution, which Tag 08QI discharges; the source's own hypothesis B ⊗_A^L A' = B' and its conclusion on THE functoriality map of 08PN are kept”.

Stacks 08QQ. If the commutative square A → B, A → A', B → B', A' → B' induces a quasi-isomorphism B ⊗_A^L A' = B', then the functoriality map L_{B/A} ⊗_B B' ⟶ L_{B'/A'} of Tag 08PN is a quasi-isomorphism of cotangent complexes. The terms of L_{B/A} are free B-modules, so the left-hand side computes L_{B/A} ⊗_B^L B'.

theorem quasiIso_cotangentExtendScalarsComplexMap
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b))
    (hQI : CotangentComputedByEveryResolution A' B') :
    QuasiIso (cotangentExtendScalarsComplexMap b)

CommAlgCat.isIso_Q_map_cotangentExtendScalarsComplexMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIso.lean, line 628. The attribute's comment: “the lemma as an isomorphism in D(B'): the image of the functoriality map of Tag 08PN under the localization D(B') is invertible. Carries the same single hypothesis, Remark 08QI as CommAlgCat.CotangentComputedByEveryResolution, discharged by Tag 08QI”.

Stacks 08QQ in the derived category. Under the hypothesis B ⊗_A^L A' = B' the functoriality map becomes an isomorphism L_{B/A} ⊗_B^L B' ⟶ L_{B'/A'} in D(B').

theorem isIso_Q_map_cotangentExtendScalarsComplexMap
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b))
    (hQI : CotangentComputedByEveryResolution A' B') :
    IsIso (DerivedCategory.Q.map (cotangentExtendScalarsComplexMap b))

CommAlgCat.cotangentBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIso.lean, line 643. The attribute's comment: “the base-change isomorphism itself, as data: an isomorphism in D(B') whose underlying morphism is the functoriality map of Tag 08PN. Carries the same single hypothesis, Remark 08QI as CommAlgCat.CotangentComputedByEveryResolution, discharged by Tag 08QI”.

Stacks 08QQ, the base-change isomorphism. The isomorphism L_{B/A} ⊗_B^L B' ≅ L_{B'/A'} in D(B') whose underlying morphism is the functoriality map of the square.

def cotangentBaseChangeIso
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b))
    (hQI : CotangentComputedByEveryResolution A' B') :
    DerivedCategory.Q.obj
        (((ModuleCat.extendScalars b.toRingHom).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj (cotangentComplex.{u, u} A B)) ≅
      DerivedCategory.Q.obj (cotangentComplex.{u, u} A' B')

CommAlgCat.quasiIso_cotangentExtendScalarsMooreMap_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIsoUnconditional.lean, line 57. The attribute's comment: “on the alternating-face-map complexes: under the source's own hypothesis and with no other, the functoriality map of Tag 08PN is a quasi-isomorphism”.

Stacks 08QQ on the Moore complexes. If the square induces B ⊗_A^L A' = B', the functoriality map of Tag 08PN is a quasi-isomorphism of the alternating face map complexes. This is CommAlgCat.quasiIso_cotangentExtendScalarsMooreMap with Remark 08QI supplied by CommAlgCat.cotangentComputedByEveryResolution.

theorem quasiIso_cotangentExtendScalarsMooreMap_unconditional
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b)) :
    QuasiIso (cotangentExtendScalarsMooreMap b)

CommAlgCat.quasiIso_cotangentExtendScalarsComplexMap_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIsoUnconditional.lean, line 70. The attribute's comment: “on the cotangent complexes, under the source's own hypothesis B ⊗_A^L A' = B' and no other: THE functoriality map of Tag 08PN is a quasi-isomorphism”.

Stacks 08QQ. If the commutative square A → B, A → A', B → B', A' → B' induces a quasi-isomorphism B ⊗_A^L A' = B', then the functoriality map L_{B/A} ⊗_B B' ⟶ L_{B'/A'} of Tag 08PN is a quasi-isomorphism of cotangent complexes. This is CommAlgCat.quasiIso_cotangentExtendScalarsComplexMap with Remark 08QI supplied by CommAlgCat.cotangentComputedByEveryResolution.

theorem quasiIso_cotangentExtendScalarsComplexMap_unconditional
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b)) :
    QuasiIso (cotangentExtendScalarsComplexMap b)

CommAlgCat.isIso_Q_map_cotangentExtendScalarsComplexMap_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIsoUnconditional.lean, line 82. The attribute's comment: “the lemma as an isomorphism in D(B'): the image of the functoriality map of Tag 08PN under the localization D(B') is invertible, under the source's own hypothesis and no other”.

Stacks 08QQ in the derived category. Under the hypothesis B ⊗_A^L A' = B' the functoriality map becomes an isomorphism L_{B/A} ⊗_B^L B' ⟶ L_{B'/A'} in D(B').

theorem isIso_Q_map_cotangentExtendScalarsComplexMap_unconditional
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b)) :
    IsIso (DerivedCategory.Q.map (cotangentExtendScalarsComplexMap b))

CommAlgCat.cotangentBaseChangeIsoUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/BaseChangeQuasiIsoUnconditional.lean, line 95. The attribute's comment: “the base-change isomorphism itself, as data: an isomorphism in D(B') whose underlying morphism is the functoriality map of Tag 08PN, under the source's own hypothesis and no other”.

Stacks 08QQ, the base-change isomorphism. The isomorphism L_{B/A} ⊗_B^L B' ≅ L_{B'/A'} in D(B') whose underlying morphism is the functoriality map of the square.

def cotangentBaseChangeIsoUnconditional
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hpush : Function.Bijective (baseChangeUnit b)) :
    DerivedCategory.Q.obj
        (((ModuleCat.extendScalars b.toRingHom).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj (cotangentComplex.{u, u} A B)) ≅
      DerivedCategory.Q.obj (cotangentComplex.{u, u} A' B')

CommAlgCat.derivedCotangentComplexBaseChangeFunctorialityIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/DerivedPushoutBaseChange.lean, line 395. The attribute's comment: “the lemma, with the arrow the source names: under the source's own hypothesis that the square induce a quasi-isomorphism B ⊗_A^L A' = B' — written out as vanishing of the positive Tor_i^A(A', B) together with bijectivity of A' ⊗_A B → B' — THE functoriality map of Tag 08PN induces an isomorphism L_{B/A} ⊗^L_B B' ≅ L_{B'/A'} in D(B'), the derived tensor product being the chapter's total derived extension-of-scalars functor. That the underlying morphism is that functoriality map is CommAlgCat.derivedCotangentComplexBaseChangeFunctorialityIso_hom below. No hypothesis beyond the source's is carried: Remark 08QI is proved, not assumed (CommAlgCat.cotangentComputedByEveryResolution)”.

[Stacks, Tag 08QQ]. Let 

A  --→  A'
|       |
B  --→  B'
be a commutative square of rings which induces a quasi-isomorphism B ⊗_A^𝐋 A' = B' — that is, Tor_i^A(A', B) = 0 for i > 0 and the canonical map A' ⊗_A B → B' is bijective. Then the functoriality map induces an isomorphism

L_{B/A} ⊗^𝐋_B B' ⟶ L_{B'/A'}

in D(B'), where - ⊗^𝐋_B B' is the total derived extension-of-scalars functor of StacksFrontier.Homology.Tor.DerivedExtensionScalars.

The arrow is the source's. The cotangent complex is a bounded above complex of free modules, so L_{B/A} ⊗^𝐋_B B' is the degreewise base change B' ⊗_B L_{B/A} (CommAlgCat.derivedExtensionScalarsCotangentComplexIso), and on that the functoriality map of [Stacks, Tag 08PN] after extension of scalars is CommAlgCat.cotangentExtendScalarsComplexMap, a quasi-isomorphism by CommAlgCat.quasiIso_cotangentExtendScalarsComplexMap. That the isomorphism built here is induced by the functoriality map and not merely some isomorphism between the two objects is CommAlgCat.derivedCotangentComplexBaseChangeFunctorialityIso_hom.

def derivedCotangentComplexBaseChangeFunctorialityIso
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hφ : Function.Bijective (baseChangeUnit b)) :
    (CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral
          b.toRingHom).functor.obj (DerivedCategory.Q.obj (cotangentComplex.{u, u} A B)) ≅
      DerivedCategory.Q.obj (cotangentComplex.{u, u} A' B')

CommAlgCat.derivedCotangentComplexBaseChangeFunctorialityIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/DerivedPushoutBaseChange.lean, line 412. The attribute's comment: “that the isomorphism is induced by THE functoriality map of Tag 08PN: its underlying morphism in D(B') is the image of the chain-level map CommAlgCat.cotangentExtendScalarsComplexMap, read after the canonical identification of L_{B/A} ⊗^L_B B' with the degreewise base change”.

The isomorphism of Tag 08QQ is the one the functoriality map induces. Its underlying morphism is the image in D(B') of CommAlgCat.cotangentExtendScalarsComplexMap — the B'-linear adjoint of the B-linear map L_{B/A} ⟶ L_{B'/A'} of [Stacks, Tag 08PN] — read after the identification of L_{B/A} ⊗^𝐋_B B' with the degreewise base change B' ⊗_B L_{B/A}.

theorem derivedCotangentComplexBaseChangeFunctorialityIso_hom
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hφ : Function.Bijective (baseChangeUnit b)) :
    (derivedCotangentComplexBaseChangeFunctorialityIso b hTor hφ).hom =
      (derivedExtensionScalarsCotangentComplexIso b).hom ≫
        DerivedCategory.Q.map (cotangentExtendScalarsComplexMap b)
Tag 08SB, a remark

Tag 08SB in the Stacks Project.

CommAlgCat.nonempty_homotopy_squareCotangentComplexMap_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SquareFactoringThroughBase.lean, line 180. The attribute's comment: “the conclusion of the remark: the induced map on cotangent complexes is homotopic to zero. The claim of the remark itself, that the functoriality map of standard resolutions is homotopic to the composition through κ, is CommAlgCat.eqvGen_homotopy_squareResolutionRingMap_baseMap of StacksFrontier.Cotangent.SquareResolutionBaseHomotopy; the proof here does not pass through it, factoring the square through the identity of A' instead.”.

Stacks Project, Tag 08SB. Let A → A', B → B' be a commutative square of ring maps compatible with the algebra structures A → B and A' → B'. If there is a ring map κ : B → A' which agrees with A → A' on the image of A and which recovers B → B' after A' → B', then the induced map of cotangent complexes L_{B/A} → L_{B'/A'} is homotopic to zero.

public theorem nonempty_homotopy_squareCotangentComplexMap_zero
    (sq : AlgebraSquare.{u, v, u} A A' B B') (κ : B →+* A')
    (hκ : ∀ a : A, κ (algebraMap A B a) = sq.base a)
    (hκ' : ∀ b : B, algebraMap A' B' (κ b) = sq.map b) :
    Nonempty (Homotopy (squareCotangentComplexMap.{u, v, u} sq) 0)

CommAlgCat.cotangentTermDifferential_squareResolutionRingBaseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SquareResolutionBaseHomotopy.lean, line 295. The attribute's comment: “the remark's observation that the composition through κ induces the zero map on differentials, read degreewise on the pure differentials 1 ⊗ d p which generate the terms of the cotangent complex.”.

The composition P_• → B → A' → P'_• lands in the image of A', so it kills differentials: the pure differential 1 ⊗ d of each of its values vanishes. This is the step by which the source passes from the homotopy below to the vanishing, up to homotopy, of the induced map on cotangent complexes.

public theorem cotangentTermDifferential_squareResolutionRingBaseMap
    (sq : AlgebraSquare.{u, v, u} A A' B B') (κ : B →+* A') (n : SimplexCategoryᵒᵖ)
    (p : (standardResolution.{u, max u v} A B).left.obj n) :
    cotangentTermDifferential.{u, max u v} A' B' n
      ((squareResolutionRingBaseMap.{u, v} sq κ).app n p) = 0

CommAlgCat.eqvGen_homotopy_squareResolutionRingMap_baseMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SquareResolutionBaseHomotopy.lean, line 376. The attribute's comment: “the claim of the remark: the functoriality map of standard resolutions is homotopic to the composition through κ. The consequence drawn from it, that the induced map of cotangent complexes is homotopic to zero, is CommAlgCat.nonempty_homotopy_squareCotangentComplexMap_zero.”.

Stacks Project, Tag 08SB. Let A → A', B → B' be a commutative square of ring maps compatible with the algebra structures A → B and A' → B', and let κ : B → A' be a ring map which agrees with A → A' on the image of A and which recovers B → B' after A' → B'. Then the functoriality map P_• → P'_• of the two standard resolutions is homotopic, as a map of simplicial commutative rings, to the composition P_• → B → A' → P'_•.

public theorem eqvGen_homotopy_squareResolutionRingMap_baseMap
    (sq : AlgebraSquare.{u, v, u} A A' B B') (κ : B →+* A')
    (hκ : ∀ a : A, κ (algebraMap A B a) = sq.base a)
    (hκ' : ∀ b : B, algebraMap A' B' (κ b) = sq.map b) :
    Relation.EqvGen
      (fun f g : resolutionRing.{u, v} A B ⟶ resolutionRing.{u, v} A' B' =>
        Nonempty (SimplicialObject.Homotopy f g))
      (squareResolutionRingMap.{u, v} sq) (squareResolutionRingBaseMap.{u, v} sq κ)
Tag 08SC, a lemma

Tag 08SC in the Stacks Project.

CommAlgCat.cotangentComplexProductMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ProductDecomposition.lean, line 460. The attribute's comment: “the canonical map L_{B×C/A} → L_{B/A} ⊕ L_{C/A} of the lemma, at chain level: the pair of the functoriality maps of the two projections, whose DerivedCategory.Q is the map in D(B × C) of the statement. That this map is an isomorphism in D(B × C) is CommAlgCat.isIso_Q_map_cotangentComplexProductMap of StacksFrontier/Cotangent/ProductDecompositionBase.lean, over an arbitrary base”.

The canonical map of [Stacks, Tag 08SC]. For ring maps A → B and A → C, the pair of the functoriality maps of the two projections B × C → B and B × C → C is a map of complexes of B × C-modules

L_{B×C/A} → L_{B/A} ⊕ L_{C/A},

the two summands being read over B × C along the projections. Tag 08SC asserts that DerivedCategory.Q of this map is an isomorphism in D(B × C); that is CommAlgCat.isIso_Q_map_cotangentComplexProductMap of StacksFrontier/Cotangent/ProductDecompositionBase.lean.

public noncomputable def cotangentComplexProductMap :
    cotangentComplex.{u, v} A (CommAlgCat.of A (B × C)) ⟶
      (((ModuleCat.restrictScalars (productFstSquare.{u, v} A B C).map).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj (cotangentComplex.{u, v} A B)) ⊞
        (((ModuleCat.restrictScalars (productSndSquare.{u, v} A B C).map).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj (cotangentComplex.{u, v} A C))

CommAlgCat.isIso_Q_map_cotangentComplexProductMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ProductDecompositionBase.lean, line 179. The attribute's comment: “the lemma: for ring maps A → B and A → C the canonical map L_{B×C/A} → L_{B/A} ⊕ L_{C/A} -- the pair of the functoriality maps of the two projections, CommAlgCat.cotangentComplexProductMap -- is an isomorphism in D(B × C), over an arbitrary base A. The chain-level form, that the map is a quasi-isomorphism, is CommAlgCat.quasiIso_cotangentComplexProductMap”.

Stacks Project, Tag 08SC. Let A → B and A → C be ring maps. Then the canonical map

L_{B×C/A} ⟶ L_{B/A} ⊕ L_{C/A}

is an isomorphism in D(B × C).

The map is CommAlgCat.cotangentComplexProductMap, the pair of the functoriality maps of [Stacks, Tag 08PN] for the two projections; it is a quasi-isomorphism by CommAlgCat.quasiIso_cotangentComplexProductMap, and the localization DerivedCategory.Q inverts exactly the quasi-isomorphisms.

theorem isIso_Q_map_cotangentComplexProductMap (A : Type u) [CommRing A]
    (B C : CommAlgCat.{u} A) :
    IsIso (DerivedCategory.Q.map (cotangentComplexProductMap.{u, u} A B C))
Sources
LeanStacks.ChaoticSite.isTransport_coefficientSquareComparison · Stacks.ChaoticSite.coefficientSquare_commutes · Stacks.ChaoticSite.isTransport_functorialitySquareComparison · Stacks.ChaoticSite.functorialitySquare_commutes · CommAlgCat.baseChangeAugmentation_tmul · CommAlgCat.baseChangeMap_tmul · CommAlgCat.isPolynomialAlgebra_baseChange · CommAlgCat.polynomialBaseChange

Section92.7 The fundamental triangle#

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

Tag 08QS, an equation

Tag 08QS in the Stacks Project.

CommAlgCat.fundamentalMor₁, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DisplayMorphisms.lean, line 143. The attribute's comment: “the first displayed morphism L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A}, canonical and with no hypothesis on the two ring maps: the functoriality map of Tag 08PN for the square (1_A, B → C) after extension of scalars. It is the first morphism of the distinguished triangle of Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished, whose third morphism is CommAlgCat.productFundamentalMor₃”.

Stacks Project, Tag 08QS.

The first displayed morphism L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A} of the triangle, for arbitrary ring maps A → B → C: the functoriality map of Tag 08PN for the square (𝟙_A, B → C) after extension of scalars along B → C, read through the identification of the derived base change L_{B/A} ⊗^𝐋_B C with the degreewise one C ⊗_B L_{B/A}.

def fundamentalMor₁ :
    fundamentalVertex₁.{u, u, u + 1, u + 1} A B C ⟶ fundamentalVertex₂.{u, u, u + 1} A C

CommAlgCat.fundamentalMor₂, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DisplayMorphisms.lean, line 167. The attribute's comment: “the second displayed morphism L_{C/A} ⟶ L_{C/B}, canonical and with no hypothesis on the two ring maps: the functoriality map of Tag 08PN for the square (A → B, 1_C). It is the second morphism of the distinguished triangle of Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished, whose third morphism is CommAlgCat.productFundamentalMor₃”.

Stacks Project, Tag 08QS.

The second displayed morphism L_{C/A} ⟶ L_{C/B} of the triangle, for arbitrary ring maps A → B → C: the functoriality map of Tag 08PN for the square (A → B, 𝟙_C), read in D(C).

def fundamentalMor₂ :
    fundamentalVertex₂.{u, u, u + 1} A C ⟶ fundamentalVertex₃.{u, u, u + 1} B C

CommAlgCat.fundamentalVertex₁, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/FundamentalDisplay.lean, line 77. The attribute's comment: “the first vertex of the displayed triangle, L_{B/A} ⊗^𝐋_B C. The display's three morphisms are CommAlgCat.fundamentalMor₁, CommAlgCat.fundamentalMor₂ and CommAlgCat.productFundamentalMor₃, and that the six form a distinguished triangle is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished”.

Stacks Project, Tag 08QS.

The first vertex L_{B/A} ⊗^𝐋_B C of the displayed triangle, as an object of D(C).

noncomputable abbrev fundamentalVertex₁ : DerivedCategory (ModuleCat.{max u v} C)

CommAlgCat.fundamentalVertex₂, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/FundamentalDisplay.lean, line 86. The attribute's comment: “the second vertex of the displayed triangle, L_{C/A}, the target of the first displayed morphism CommAlgCat.fundamentalMor₁ and the source of the second, CommAlgCat.fundamentalMor₂”.

Stacks Project, Tag 08QS.

The second vertex L_{C/A} of the displayed triangle, as an object of D(C).

noncomputable abbrev fundamentalVertex₂ : DerivedCategory (ModuleCat.{max u v} C)

CommAlgCat.fundamentalVertex₃, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/FundamentalDisplay.lean, line 95. The attribute's comment: “the third vertex of the displayed triangle, L_{C/B}, the target of the second displayed morphism CommAlgCat.fundamentalMor₂ and the source of the third, CommAlgCat.productFundamentalMor₃, which lands in (L_{B/A} ⊗^𝐋_B C)[1]”.

Stacks Project, Tag 08QS.

The third vertex L_{C/B} of the displayed triangle, as an object of D(C).

noncomputable abbrev fundamentalVertex₃ : DerivedCategory (ModuleCat.{max u v} C)

CommAlgCat.productFundamentalMor₃, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/ProductDescent.lean, line 317. The attribute's comment: “the third displayed morphism L_{C/B} → (L_{B/A} ⊗^𝐋_B C)[1], for arbitrary ring maps A → B → C: the connecting morphism of the fundamental triangle of A → B → B × C base changed along B × C → C, read between the display's own two vertices. The display is a distinguished triangle on these three morphisms by CommAlgCat.productFundamentalTriangle_distinguished”.

The third displayed morphism of [Stacks, Tag 08QS], for arbitrary ring maps A → B → C. It is the connecting morphism of the fundamental triangle of A → B → B × C, base changed along the flat ring map B × C → C and read between the display's own vertices L_{C/B} and (L_{B/A} ⊗^𝐋_B C)⟦1⟧.

def productFundamentalMor₃ :
    fundamentalVertex₃.{u, u, u + 1} B C ⟶
      (fundamentalVertex₁.{u, u, u + 1, u + 1} A B C)⟦(1 : ℤ)⟧

CommAlgCat.productFundamentalTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/ProductDescent.lean, line 357. The attribute's comment: “the distinguishedness asserted by the display: Equation 92.7.0.1 is written as a triangle, and that the display's three objects and three arrows form a DISTINGUISHED triangle in D(C) is the remaining clause of the display, for arbitrary ring maps A → B → C with no hypothesis on them. The display's three vertices are CommAlgCat.fundamentalVertex₁, CommAlgCat.fundamentalVertex₂ and CommAlgCat.fundamentalVertex₃ and its three morphisms are CommAlgCat.fundamentalMor₁, CommAlgCat.fundamentalMor₂ and CommAlgCat.productFundamentalMor₃, each of which carries the tag for its own constituent. That the triangle is distinguished is Proposition 08QX, which this declaration also carries”.

Stacks Project, Tag 08QX, and the distinguishedness asserted by the display of Tag 08QS. Let A → B → C be ring maps. Then

L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A} ⟶ L_{C/B} ⟶ (L_{B/A} ⊗^𝐋_B C)[1]

is a distinguished triangle in D(C), on the three vertices of the display of [Stacks, Tag 08QS], with the display's own first two morphisms CommAlgCat.fundamentalMor₁ and CommAlgCat.fundamentalMor₂ — the two functoriality maps of [Stacks, Tag 08PN] for the two commutative squares of the tower — and with CommAlgCat.productFundamentalMor₃ for its third.

The display of Tag 08QS is written as a triangle, and what makes it one is exactly this statement, so the display's distinguishedness clause is registered here as well: the three objects and the three arrows of the display are named by CommAlgCat.fundamentalVertex₁, CommAlgCat.fundamentalVertex₂, CommAlgCat.fundamentalVertex₃, CommAlgCat.fundamentalMor₁, CommAlgCat.fundamentalMor₂ and CommAlgCat.productFundamentalMor₃, and that they form a triangle at all is Proposition 08QX.

The proof is the one of [Stacks, Remark 08SD]: the triangle for A → B → B × C, where the map is the split injection b ↦ (b, f b), base changed along the flat projection B × C → C.

theorem productFundamentalTriangle_distinguished :
    Triangle.mk (fundamentalMor₁.{u} A B C) (fundamentalMor₂.{u} A B C)
        (productFundamentalMor₃ A B C) ∈ distTriang (DerivedCategory (ModuleCat.{u} C))
Tag 08QT, an equation

Tag 08QT in the Stacks Project.

CommAlgCat.polynomialTowerSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 247. The attribute's comment: “the site C_{C/B/A}”.

The site C_{C/B/A}: the opposite of the category of polynomial towers (P → B, Q → C), so that an object corresponds to the commutative diagram of spectra in which Spec C → Spec Q lies over Spec B → Spec P over Spec A.

abbrev polynomialTowerSite

CommAlgCat.polynomialTowerTopology_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 262. The attribute's comment: “the chaotic topology on C_{C/B/A}”.

The topology of C_{C/B/A} is the chaotic topology: its only coverings are the maximal sieves, so every presheaf on C_{C/B/A} is a sheaf.

theorem polynomialTowerTopology_eq_bot : polynomialTowerTopology A B C = ⊥

CommAlgCat.polynomialTowerFirst, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 275. The attribute's comment: “the functor u₁”.

u₁ : C_{C/B/A} ⥤ C_{B/A}, the functor (P → B, Q → C) ↦ (P → B).

def polynomialTowerFirst : polynomialTowerSite A B C ⥤ polynomialSite A (towerBaseAlgebra A B)

CommAlgCat.isPolynomialAlgebra_towerRightAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 284. The attribute's comment: “u₂ lands in C_{C/A}”.

The A-algebra Q of a polynomial tower is a polynomial algebra over A: it is a polynomial algebra over the polynomial A-algebra P, and P[κ] = A[ι][κ] = A[κ ⊕ ι]. This is what makes u₂ land in C_{C/A}.

theorem isPolynomialAlgebra_towerRightAlgebra (X : PolynomialTower A B C) :
    IsPolynomialAlgebra A (towerRightAlgebra X.obj)

CommAlgCat.polynomialTowerSecond, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 310. The attribute's comment: “the functor u₂”.

u₂ : C_{C/B/A} ⥤ C_{C/A}, the functor (P → B, Q → C) ↦ (Q → C).

def polynomialTowerSecond :
    polynomialTowerSite A B C ⥤ polynomialSite A (towerTotalAlgebra A C)

CommAlgCat.isPolynomialAlgebra_towerBaseChangeAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 442. The attribute's comment: “u₃ lands in C_{C/B}”.

Q ⊗_P B is a polynomial algebra over B: if Q = P[κ] then Q ⊗_P B = B[κ]. This is what makes u₃ land in C_{C/B}.

theorem isPolynomialAlgebra_towerBaseChangeAlgebra (X : PolynomialTower A B C) :
    IsPolynomialAlgebra B (towerBaseChangeAlgebra X.obj)

CommAlgCat.polynomialTowerThird, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 496. The attribute's comment: “the functor u₃”.

u₃ : C_{C/B/A} ⥤ C_{C/B}, the functor (P → B, Q → C) ↦ (Q ⊗_P B → C).

def polynomialTowerThird :
    polynomialTowerSite A B C ⥤ polynomialSite B (towerRelativeAlgebra B C)

CommAlgCat.polynomialTowerFirstStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 639. The attribute's comment: “the sheaf 𝒪₁ = g₁⁻¹𝒪”.

𝒪₁ = g₁⁻¹𝒪: the inverse image along g₁ of the tautological sheaf of rings on C_{B/A}.

def polynomialTowerFirstStructureSheaf :
    Sheaf (polynomialTowerTopology A B C) CommRingCat.{u + 1}

CommAlgCat.polynomialTowerSecondStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 647. The attribute's comment: “the sheaf 𝒪₂ = g₂⁻¹𝒪”.

𝒪₂ = g₂⁻¹𝒪: the inverse image along g₂ of the tautological sheaf of rings on C_{C/A}.

def polynomialTowerSecondStructureSheaf :
    Sheaf (polynomialTowerTopology A B C) CommRingCat.{u + 1}

CommAlgCat.polynomialTowerThirdStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 655. The attribute's comment: “the sheaf 𝒪₃ = g₃⁻¹𝒪”.

𝒪₃ = g₃⁻¹𝒪: the inverse image along g₃ of the tautological sheaf of rings on C_{C/B}.

def polynomialTowerThirdStructureSheaf :
    Sheaf (polynomialTowerTopology A B C) CommRingCat.{u + 1}

CommAlgCat.polynomialTowerFirstRinged, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 682. The attribute's comment: “the morphism g₁ of ringed topoi”.

g₁ : (Sh(C_{C/B/A}), 𝒪₁) ⟶ (Sh(C_{B/A}), 𝒪), the first morphism of ringed topoi of the fundamental triangle. Its structure map is the unit of g₁⁻¹ ⊣ g₁_* on sheaves of commutative rings at 𝒪, which is the structure map that 𝒪₁ = g₁⁻¹𝒪 forces.

def polynomialTowerFirstRinged :
    AlgebraicGeometry.RingedToposHom (polynomialTowerFirstRingedTopos A B C)
      (polynomialStructureRingedTopos A (towerBaseAlgebra A B))

CommAlgCat.polynomialTowerSecondRinged, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 692. The attribute's comment: “the morphism g₂ of ringed topoi”.

g₂ : (Sh(C_{C/B/A}), 𝒪₂) ⟶ (Sh(C_{C/A}), 𝒪), the second morphism of ringed topoi of the fundamental triangle.

def polynomialTowerSecondRinged :
    AlgebraicGeometry.RingedToposHom (polynomialTowerSecondRingedTopos A B C)
      (polynomialStructureRingedTopos A (towerTotalAlgebra A C))

CommAlgCat.polynomialTowerThirdRinged, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 702. The attribute's comment: “the morphism g₃ of ringed topoi”.

g₃ : (Sh(C_{C/B/A}), 𝒪₃) ⟶ (Sh(C_{C/B}), 𝒪), the third morphism of ringed topoi of the fundamental triangle.

def polynomialTowerThirdRinged :
    AlgebraicGeometry.RingedToposHom (polynomialTowerThirdRingedTopos A B C)
      (polynomialStructureRingedTopos B (towerRelativeAlgebra B C))

CommAlgCat.polynomialTowerProjection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 744. The attribute's comment: “the projection π”.

π : Sh(C_{C/B/A}) ⟶ Sh(*), the projection of the chaotic site C_{C/B/A} to the point.

abbrev polynomialTowerProjection

CommAlgCat.polynomialTowerFirstProjection_comp_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 762. The attribute's comment: “π = π₁ ∘ g₁, on inverse images”.

π = π₁ ∘ g₁, on inverse images: both are restriction along the unique functor to the point, because u₁ followed by C_{B/A} ⥤ * is C_{C/B/A} ⥤ *.

theorem polynomialTowerFirstProjection_comp_inverseImage :
    ((polynomialTowerFirstProjection A B).comp
        (polynomialTowerFirstTopos A B C)).inverseImage =
      (polynomialTowerProjection A B C).inverseImage

CommAlgCat.polynomialTowerSecondProjection_comp_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 769. The attribute's comment: “π = π₂ ∘ g₂, on inverse images”.

π = π₂ ∘ g₂, on inverse images.

theorem polynomialTowerSecondProjection_comp_inverseImage :
    ((polynomialTowerSecondProjection A C).comp
        (polynomialTowerSecondTopos A B C)).inverseImage =
      (polynomialTowerProjection A B C).inverseImage

CommAlgCat.polynomialTowerThirdProjection_comp_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 776. The attribute's comment: “π = π₃ ∘ g₃, on inverse images”.

π = π₃ ∘ g₃, on inverse images.

theorem polynomialTowerThirdProjection_comp_inverseImage :
    ((polynomialTowerThirdProjection B C).comp
        (polynomialTowerThirdTopos A B C)).inverseImage =
      (polynomialTowerProjection A B C).inverseImage

CommAlgCat.polynomialTowerFirstProjection_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 784. The attribute's comment: “π = π₁ ∘ g₁, on direct images”.

π = π₁ ∘ g₁, on direct images: the canonical isomorphism (π₁ ∘ g₁)_* ≅ π_* between the two right adjoints of the common inverse image.

def polynomialTowerFirstProjection_comp_pushforwardIso :
    ((polynomialTowerFirstProjection A B).comp (polynomialTowerFirstTopos A B C)).pushforward ≅
      (polynomialTowerProjection A B C).pushforward

CommAlgCat.polynomialTowerSecondProjection_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 794. The attribute's comment: “π = π₂ ∘ g₂, on direct images”.

π = π₂ ∘ g₂, on direct images.

def polynomialTowerSecondProjection_comp_pushforwardIso :
    ((polynomialTowerSecondProjection A C).comp (polynomialTowerSecondTopos A B C)).pushforward ≅
      (polynomialTowerProjection A B C).pushforward

CommAlgCat.polynomialTowerThirdProjection_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSite.lean, line 804. The attribute's comment: “π = π₃ ∘ g₃, on direct images”.

π = π₃ ∘ g₃, on direct images.

def polynomialTowerThirdProjection_comp_pushforwardIso :
    ((polynomialTowerThirdProjection B C).comp (polynomialTowerThirdTopos A B C)).pushforward ≅
      (polynomialTowerProjection A B C).pushforward

CommAlgCat.boundedPolynomialTowerSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 169. The attribute's comment: “the site C_{C/B/A} with the section's footnote in force, restricting the two layers of variables to cardinality at most κ, resp. μ. The unrestricted version is CommAlgCat.polynomialTowerSite; only this one is essentially small”.

Stacks 08QT with the footnote's restriction. The site C_{C/B/A} cut down to the towers whose two polynomial layers have at most κ, resp. μ, variables: the opposite of CommAlgCat.BoundedPolynomialTower. CommAlgCat.polynomialTowerSite is the same construction with the footnote omitted.

abbrev boundedPolynomialTowerSite

CommAlgCat.isPolynomialAlgebraBelow_towerRightAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 374. The attribute's comment: “u₂ lands in C_{C/A}, for the small model of the footnote-restricted tower site: the bound on the two layers gives the bound μ + κ on the variables of Q over A”.

The A-algebra Q of a restricted polynomial tower is a polynomial algebra over A on at most μ + κ variables: it is A[ι][τ] = A[τ ⊕ ι] with #ι ≤ κ and #τ ≤ μ. This is what makes u₂ land in the restricted site C_{C/A}.

theorem isPolynomialAlgebraBelow_towerRightAlgebra (Y : BoundedPolynomialTower A B C κ μ) :
    IsPolynomialAlgebraBelow A (μ + κ) (towerRightAlgebra Y.obj)

CommAlgCat.isPolynomialAlgebraBelow_towerBaseChangeAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 395. The attribute's comment: “u₃ lands in C_{C/B}, for the small model of the footnote-restricted tower site: the base change Q ⊗_P B has the same set of variables as Q over P, so the bound μ is kept”.

Q ⊗_P B is a polynomial algebra over B on at most μ variables: if Q = P[τ] then Q ⊗_P B = B[τ], with the same set of variables. This is what makes u₃ land in the restricted site C_{C/B}.

theorem isPolynomialAlgebraBelow_towerBaseChangeAlgebra (Y : BoundedPolynomialTower A B C κ μ) :
    IsPolynomialAlgebraBelow B μ (towerBaseChangeAlgebra Y.obj)

CommAlgCat.boundedPolynomialTowerFirst, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 440. The attribute's comment: “the functor u₁, for the footnote-restricted tower site”.

u₁ on the restricted sites.

def boundedPolynomialTowerFirst :
    boundedPolynomialTowerSite A B C κ μ ⥤ boundedPolynomialSite A (towerBaseAlgebra A B) κ

CommAlgCat.boundedPolynomialTowerSecond, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 446. The attribute's comment: “the functor u₂, for the footnote-restricted tower site”.

u₂ on the restricted sites.

def boundedPolynomialTowerSecond :
    boundedPolynomialTowerSite A B C κ μ ⥤
      boundedPolynomialSite A (towerTotalAlgebra A C) (μ + κ)

CommAlgCat.boundedPolynomialTowerThird, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 453. The attribute's comment: “the functor u₃, for the footnote-restricted tower site”.

u₃ on the restricted sites.

def boundedPolynomialTowerThird :
    boundedPolynomialTowerSite A B C κ μ ⥤ boundedPolynomialSite B (towerRelativeAlgebra B C) μ

CommAlgCat.boundedPolynomialTowerFirst_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 478. The attribute's comment: “the functor u₁ of the footnote-restricted tower site is u₁”.

Read in the unrestricted sites, u₁ on the restricted sites is u₁.

theorem boundedPolynomialTowerFirst_comp_ι :
    boundedPolynomialTowerFirst A B C κ μ ⋙ boundedPolynomialSiteι A (towerBaseAlgebra A B) κ =
      boundedPolynomialTowerSiteι A B C κ μ ⋙ polynomialTowerFirst A B C

CommAlgCat.boundedPolynomialTowerSecond_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 484. The attribute's comment: “the functor u₂ of the footnote-restricted tower site is u₂”.

Read in the unrestricted sites, u₂ on the restricted sites is u₂.

theorem boundedPolynomialTowerSecond_comp_ι :
    boundedPolynomialTowerSecond A B C κ μ ⋙
        boundedPolynomialSiteι A (towerTotalAlgebra A C) (μ + κ) =
      boundedPolynomialTowerSiteι A B C κ μ ⋙ polynomialTowerSecond A B C

CommAlgCat.boundedPolynomialTowerThird_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 491. The attribute's comment: “the functor u₃ of the footnote-restricted tower site is u₃”.

Read in the unrestricted sites, u₃ on the restricted sites is u₃.

theorem boundedPolynomialTowerThird_comp_ι :
    boundedPolynomialTowerThird A B C κ μ ⋙ boundedPolynomialSiteι B (towerRelativeAlgebra B C) μ =
      boundedPolynomialTowerSiteι A B C κ μ ⋙ polynomialTowerThird A B C

CommAlgCat.smallBoundedPolynomialTowerFirst, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 510. The attribute's comment: “the functor u₁, for the small model of the footnote-restricted tower site”.

u₁ : C_{C/B/A} ⥤ C_{B/A} on the small models of the restricted sites.

def smallBoundedPolynomialTowerFirst :
    smallBoundedPolynomialTowerSite A B C κ μ ⥤
      smallBoundedPolynomialSite A (towerBaseAlgebra A B) κ

CommAlgCat.smallBoundedPolynomialTowerSecond, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 518. The attribute's comment: “the functor u₂, for the small model of the footnote-restricted tower site”.

u₂ : C_{C/B/A} ⥤ C_{C/A} on the small models of the restricted sites: u₂ on the restricted sites, followed by the transport of its value into the small model of C_{C/A}.

def smallBoundedPolynomialTowerSecond :
    smallBoundedPolynomialTowerSite A B C κ μ ⥤
      smallBoundedPolynomialSite A (towerTotalAlgebra A C) (μ + κ)

CommAlgCat.smallBoundedPolynomialTowerThird, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 527. The attribute's comment: “the functor u₃, for the small model of the footnote-restricted tower site”.

u₃ : C_{C/B/A} ⥤ C_{C/B} on the small models of the restricted sites: u₃ on the restricted sites, followed by the transport of its value into the small model of C_{C/B}.

def smallBoundedPolynomialTowerThird :
    smallBoundedPolynomialTowerSite A B C κ μ ⥤
      smallBoundedPolynomialSite B (towerRelativeAlgebra B C) μ

CommAlgCat.smallBoundedPolynomialTowerFirst_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 536. The attribute's comment: “the functor u₁ of the small model of the footnote-restricted tower site is u₁”.

The square for u₁. Read in the unrestricted sites through the fully faithful comparisons, u₁ on the small models is u₁ on C_{C/B/A}.

theorem smallBoundedPolynomialTowerFirst_comp_ι :
    smallBoundedPolynomialTowerFirst A B C κ μ ⋙
        smallBoundedPolynomialSiteToPolynomialSite A (towerBaseAlgebra A B) κ =
      smallBoundedPolynomialTowerSiteToPolynomialTowerSite A B C κ μ ⋙
        polynomialTowerFirst A B C

CommAlgCat.smallBoundedPolynomialTowerSecondCompι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 546. The attribute's comment: “the functor u₂ of the small model of the footnote-restricted tower site is u₂”.

The square for u₂. Read in the unrestricted sites through the fully faithful comparisons, u₂ on the small models is u₂ on C_{C/B/A}, up to the canonical isomorphism coming from the transport into the small model of C_{C/A}.

def smallBoundedPolynomialTowerSecondCompι :
    smallBoundedPolynomialTowerSecond A B C κ μ ⋙
        smallBoundedPolynomialSiteToPolynomialSite A (towerTotalAlgebra A C) (μ + κ) ≅
      smallBoundedPolynomialTowerSiteToPolynomialTowerSite A B C κ μ ⋙
        polynomialTowerSecond A B C

CommAlgCat.smallBoundedPolynomialTowerThirdCompι, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 561. The attribute's comment: “the functor u₃ of the small model of the footnote-restricted tower site is u₃”.

The square for u₃. Read in the unrestricted sites through the fully faithful comparisons, u₃ on the small models is u₃ on C_{C/B/A}, up to the canonical isomorphism coming from the transport into the small model of C_{C/B}.

def smallBoundedPolynomialTowerThirdCompι :
    smallBoundedPolynomialTowerThird A B C κ μ ⋙
        smallBoundedPolynomialSiteToPolynomialSite B (towerRelativeAlgebra B C) μ ≅
      smallBoundedPolynomialTowerSiteToPolynomialTowerSite A B C κ μ ⋙
        polynomialTowerThird A B C

CommAlgCat.smallBoundedPolynomialTowerTopology_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 577. The attribute's comment: “the chaotic topology on C_{C/B/A}, for the small model of the footnote-restricted tower site”.

The topology of the small model of the restricted site C_{C/B/A} is the chaotic topology: its only coverings are the maximal sieves, so every presheaf on it is a sheaf.

theorem smallBoundedPolynomialTowerTopology_eq_bot :
    GrothendieckTopology.trivial (smallBoundedPolynomialTowerSite A B C κ μ) = ⊥

CommAlgCat.smallBoundedPolynomialTowerProjection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 683. The attribute's comment: “the projection π, for the small model of the footnote-restricted tower site”.

π : Sh(C_{C/B/A}) ⟶ Sh(*), the projection of the small model of the restricted site to the point, with coefficients in the site's own universe.

abbrev smallBoundedPolynomialTowerProjection :
    MorphismOfTopoi
      (Sheaf (GrothendieckTopology.trivial (smallBoundedPolynomialTowerSite A B C κ μ)) (Type u))
      (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 1})) (Type u))

CommAlgCat.smallBoundedPolynomialTowerFirstProjection_comp_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 719. The attribute's comment: “π = π₁ ∘ g₁ on inverse images, for the small model of the footnote-restricted tower site”.

π = π₁ ∘ g₁ on inverse images: both are restriction along the unique functor to the point, because u₁ followed by C_{B/A} ⥤ * is C_{C/B/A} ⥤ *.

theorem smallBoundedPolynomialTowerFirstProjection_comp_inverseImage :
    ((smallBoundedPolynomialTowerFirstProjection A B κ).comp
        (smallBoundedPolynomialTowerFirstTopos A B C κ μ)).inverseImage =
      (smallBoundedPolynomialTowerProjection A B C κ μ).inverseImage

CommAlgCat.smallBoundedPolynomialTowerSecondProjection_comp_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 727. The attribute's comment: “π = π₂ ∘ g₂ on inverse images, for the small model of the footnote-restricted tower site”.

π = π₂ ∘ g₂ on inverse images.

theorem smallBoundedPolynomialTowerSecondProjection_comp_inverseImage :
    ((smallBoundedPolynomialTowerSecondProjection A C κ μ).comp
        (smallBoundedPolynomialTowerSecondTopos A B C κ μ)).inverseImage =
      (smallBoundedPolynomialTowerProjection A B C κ μ).inverseImage

CommAlgCat.smallBoundedPolynomialTowerThirdProjection_comp_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 735. The attribute's comment: “π = π₃ ∘ g₃ on inverse images, for the small model of the footnote-restricted tower site”.

π = π₃ ∘ g₃ on inverse images.

theorem smallBoundedPolynomialTowerThirdProjection_comp_inverseImage :
    ((smallBoundedPolynomialTowerThirdProjection B C μ).comp
        (smallBoundedPolynomialTowerThirdTopos A B C κ μ)).inverseImage =
      (smallBoundedPolynomialTowerProjection A B C κ μ).inverseImage

CommAlgCat.smallBoundedPolynomialTowerFirstProjection_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 744. The attribute's comment: “π = π₁ ∘ g₁ on direct images, for the small model of the footnote-restricted tower site”.

π = π₁ ∘ g₁ on direct images: the canonical isomorphism (π₁ ∘ g₁)_* ≅ π_* between the two right adjoints of the common inverse image.

def smallBoundedPolynomialTowerFirstProjection_comp_pushforwardIso :
    ((smallBoundedPolynomialTowerFirstProjection A B κ).comp
        (smallBoundedPolynomialTowerFirstTopos A B C κ μ)).pushforward ≅
      (smallBoundedPolynomialTowerProjection A B C κ μ).pushforward

CommAlgCat.smallBoundedPolynomialTowerSecondProjection_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 757. The attribute's comment: “π = π₂ ∘ g₂ on direct images, for the small model of the footnote-restricted tower site”.

π = π₂ ∘ g₂ on direct images.

def smallBoundedPolynomialTowerSecondProjection_comp_pushforwardIso :
    ((smallBoundedPolynomialTowerSecondProjection A C κ μ).comp
        (smallBoundedPolynomialTowerSecondTopos A B C κ μ)).pushforward ≅
      (smallBoundedPolynomialTowerProjection A B C κ μ).pushforward

CommAlgCat.smallBoundedPolynomialTowerThirdProjection_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialSiteSmall.lean, line 770. The attribute's comment: “π = π₃ ∘ g₃ on direct images, for the small model of the footnote-restricted tower site”.

π = π₃ ∘ g₃ on direct images.

def smallBoundedPolynomialTowerThirdProjection_comp_pushforwardIso :
    ((smallBoundedPolynomialTowerThirdProjection B C μ).comp
        (smallBoundedPolynomialTowerThirdTopos A B C κ μ)).pushforward ≅
      (smallBoundedPolynomialTowerProjection A B C κ μ).pushforward
Tag 08QU, a lemma

Tag 08QU in the Stacks Project.

CommAlgCat.towerDifferential_shortExact_extendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 230. The attribute's comment: “the objectwise split differential sequence after base change: the exactness input of the lemma, at an object of the site”.

For a tower R → P → Q with Q formally smooth over P, the differential sequence 0 → Q ⊗_P Ω_{P/R} → Ω_{Q/R} → Ω_{Q/P} → 0 of Algebra, Lemma 10.138.9 is split, so it stays short exact after extending scalars along an arbitrary ring map ε : Q → S. This is the objectwise input to the exactness of the sequence of Tag 08QU.

theorem towerDifferential_shortExact_extendScalars
    (R P Q S : Type w) [CommRing R] [CommRing P] [CommRing Q] [CommRing S]
    [Algebra R P] [Algebra P Q] [Algebra R Q] [IsScalarTower R P Q]
    [Algebra.FormallySmooth P Q] (ε : Q →+* S) :
    ((ShortComplex.moduleCatMk (KaehlerDifferential.mapBaseChange R P Q)
        (KaehlerDifferential.map R P Q Q) (by
          apply LinearMap.ext
          intro x
          exact (KaehlerDifferential.exact_mapBaseChange_map R P Q).apply_apply_eq_zero x)).map
      (ModuleCat.extendScalars ε)).ShortExact

CommAlgCat.isSheaf_polynomialTowerTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 259. The attribute's comment: “exactness may be checked objectwise: every presheaf on the threefold site is a sheaf”.

Every presheaf on C_{C/B/A} is a sheaf, because the topology of the site is chaotic.

theorem isSheaf_polynomialTowerTopology {D : Type*} [Category D]
    (F : (polynomialTowerSite A B C)ᵒᵖ ⥤ D) :
    Presheaf.IsSheaf (polynomialTowerTopology A B C) F

CommAlgCat.towerFirstOmega, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 318. The attribute's comment: “the sheaf Ω₁ = Ω_{𝒪/A} ⊗_𝒪 B̲ on C_{B/A}”.

Ω₁ = Ω_{𝒪/A} ⊗_𝒪 B̲, the sheaf of B̲-modules on C_{B/A}.

abbrev towerFirstOmega : SheafOfModules.{u + 1} (polynomialConstantRingSheaf A
    (towerBaseAlgebra A B))

CommAlgCat.towerSecondOmega, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 324. The attribute's comment: “the sheaf Ω₂ = Ω_{𝒪/A} ⊗_𝒪 C̲ on C_{C/A}”.

Ω₂ = Ω_{𝒪/A} ⊗_𝒪 C̲, the sheaf of C̲-modules on C_{C/A}.

abbrev towerSecondOmega : SheafOfModules.{u + 1} (polynomialConstantRingSheaf A
    (towerTotalAlgebra A C))

CommAlgCat.towerThirdOmega, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 330. The attribute's comment: “the sheaf Ω₃ = Ω_{𝒪/B} ⊗_𝒪 C̲ on C_{C/B}”.

Ω₃ = Ω_{𝒪/B} ⊗_𝒪 C̲, the sheaf of C̲-modules on C_{C/B}.

abbrev towerThirdOmega : SheafOfModules.{u + 1} (polynomialConstantRingSheaf B
    (towerRelativeAlgebra B C))

CommAlgCat.towerSecondTerm, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 363. The attribute's comment: “the second term g₂⁻¹Ω₂ of the sequence”.

g₂⁻¹Ω₂, a presheaf of C̲-modules on C_{C/B/A}: the inverse image along g₂ is restriction along u₂, and the inverse image of C̲ is C̲.

def towerSecondTerm : PresheafOfModules.{u + 1} (towerConstantRingSheaf A B C).obj

CommAlgCat.towerThirdTerm, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 369. The attribute's comment: “the third term g₃⁻¹Ω₃ of the sequence”.

g₃⁻¹Ω₃, a presheaf of C̲-modules on C_{C/B/A}.

def towerThirdTerm : PresheafOfModules.{u + 1} (towerConstantRingSheaf A B C).obj

CommAlgCat.towerFirstTerm, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 382. The attribute's comment: “the first term g₁⁻¹Ω₁ ⊗_{B̲} C̲ of the sequence”.

g₁⁻¹Ω₁ ⊗_{B̲} C̲, a presheaf of C̲-modules on C_{C/B/A}.

def towerFirstTerm : PresheafOfModules.{u + 1} (towerConstantRingSheaf A B C).obj

CommAlgCat.towerSections_formallySmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 447. The attribute's comment: “the sections of 𝒪₂ are formally smooth over the sections of 𝒪₁: the formal smoothness input of the objectwise differential sequence”.

The sections of 𝒪₂ are formally smooth over the sections of 𝒪₁. Over the tower (P → B, Q → C) the map is the universe lift of P → Q, and Q is a polynomial algebra over P by the first condition on a polynomial tower, hence formally smooth over P; formal smoothness survives the universe lift by RingHom.FormallySmooth.ulift. This is the hypothesis Algebra.FormallySmooth that CommAlgCat.towerDifferential_shortExact_extendScalars needs at the object W of C_{C/B/A}.

theorem towerSections_formallySmooth (W : (polynomialTowerSite A B C)ᵒᵖ) :
    letI := ((towerLeftToRight A B C).app W).hom.toAlgebra
    Algebra.FormallySmooth ((towerLeftRingPresheaf A B C).obj W)
      ((towerRightRingPresheaf A B C).obj W)

CommAlgCat.towerSections_isPushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 466. The attribute's comment: “the pushout square of the tower on the universe-lifted sections: the input that identifies the third term of the objectwise sequence”.

The pushout square of a polynomial tower survives the universe lift. The sections of 𝒪₃ over the tower (P → B, Q → C) are Q ⊗_P B, so the square P → B, P → Q, B → Q ⊗_P B, Q → Q ⊗_P B of the tower is a pushout square of rings; Algebra.IsPushout.ulift_tensorProduct transports that to the universe lifts, which is the form in which the sections of the three structure sheaves carry it. This is the hypothesis Algebra.IsPushout that KaehlerDifferential.tensorKaehlerEquiv needs in order to identify Ω_{𝒪₃/B̲} with 𝒪₃ ⊗_{𝒪₂} Ω_{𝒪₂/𝒪₁} on sections.

theorem towerSections_isPushout (W : (polynomialTowerSite A B C)ᵒᵖ) :
    Algebra.IsPushout (ULift.{u + 1} ↑(towerLeftAlgebra W.unop.unop.obj)) (ULift.{u + 1} B)
      (ULift.{u + 1} ↑(towerRightAlgebra W.unop.unop.obj))
      (ULift.{u + 1} ↑(towerBaseChangeAlgebra W.unop.unop.obj))

CommAlgCat.towerFirstSequenceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 852. The attribute's comment: “the first map g₁⁻¹Ω₁ ⊗_{B̲} C̲ ⟶ g₂⁻¹Ω₂ of the sequence”.

The first map g₁⁻¹Ω₁ ⊗_{B̲} C̲ ⟶ g₂⁻¹Ω₂ of the sequence of Tag 08QU. Both source and target are base changes of presheaves of relative differentials, so by the change-of-rings adjunction of Tag 03CU and the universal property of the presheaf of differentials the map is the same datum as CommAlgCat.towerFirstDerivation, namely c ⊗ b ⊗ d p ↦ c·b ⊗ d p.

def towerFirstSequenceMap : towerFirstTerm A B C ⟶ towerSecondTerm A B C

CommAlgCat.towerSecondSequenceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 861. The attribute's comment: “the second map g₂⁻¹Ω₂ ⟶ g₃⁻¹Ω₃ of the sequence”.

The second map g₂⁻¹Ω₂ ⟶ g₃⁻¹Ω₃ of the sequence of Tag 08QU, the datum of CommAlgCat.towerSecondDerivation under the change-of-rings adjunction of Tag 03CU and the universal property of the presheaf of differentials: c ⊗ d q ↦ c ⊗ d(1 ⊗ q).

def towerSecondSequenceMap : towerSecondTerm A B C ⟶ towerThirdTerm A B C

CommAlgCat.towerSequenceMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 871. The attribute's comment: “the two maps of the sequence compose to zero”.

The composite of the two maps of the sequence of Tag 08QU vanishes. By the universal properties the composite is the map attached to the derivation p ↦ 1 ⊗ d(1 ⊗ image of p) of 𝒪₁ with values in g₃⁻¹Ω₃, and that derivation is zero: by the pushout square on sections (CommAlgCat.towerRightToPushout_app_towerLeftToRight) the image of p in 𝒪₃ comes from B̲, and d kills the image of the base sheaf of rings.

theorem towerSequenceMap_comp :
    towerFirstSequenceMap A B C ≫ towerSecondSequenceMap A B C = 0

CommAlgCat.towerShortComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 929. The attribute's comment: “the sequence 0 ⟶ g₁⁻¹Ω₁ ⊗_{B̲} C̲ ⟶ g₂⁻¹Ω₂ ⟶ g₃⁻¹Ω₃ ⟶ 0 of sheaves of C̲-modules on C_{C/B/A}; its short exactness is not asserted here”.

The sequence of Tag 08QU as a short complex of sheaves of C̲-modules on C_{C/B/A}, the image of CommAlgCat.towerShortComplexPresheaf under the equivalence CommAlgCat.towerPresheafToSheaf: every presheaf on the chaotic site is a sheaf.

def towerShortComplex : ShortComplex (SheafOfModules.{u + 1} (towerConstantRingSheaf A B C))

CommAlgCat.towerShortComplexPresheaf_shortExact_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 1026. The attribute's comment: “the sequence of sections over a polynomial tower is short exact: the objectwise form of the short exactness”.

The sequence of Tag 08QU is short exact over every object of C_{C/B/A}. Over the polynomial tower (P → B, Q → C), with T = Q ⊗_P B and every ring replaced by its universe lift, the three modules of sections are C̲(W) ⊗_{B̲(W)} (B̲(W) ⊗_P Ω_{P/A}), C̲(W) ⊗_Q Ω_{Q/A} and C̲(W) ⊗_T Ω_{T/B}, and the sequence they form is the split sequence of CommAlgCat.towerDifferential_shortExact_extendScalars for the tower A → P → Q base changed along the augmentation Q → C̲(W). The middle terms agree on the nose (CommAlgCat.towerSecondTerm_obj); the first terms are identified by cancelling the base change twice through C̲(W) ⊗_P Ω_{P/A}, and the third ones by KaehlerDifferential.tensorKaehlerEquiv, available because CommAlgCat.towerSections_isPushout makes T the pushout of B ← P → Q. Both squares are checked on the generators 1 ⊗ 1 ⊗ d p and 1 ⊗ d q, where the two maps of the sequence are computed by the change-of-rings adjunction of Tag 03CU.

theorem towerShortComplexPresheaf_shortExact_obj (W : (polynomialTowerSite A B C)ᵒᵖ) :
    ((towerShortComplexPresheaf A B C).map
      (PresheafOfModules.evaluation (towerConstantRingSheaf A B C).obj W)).ShortExact

CommAlgCat.towerShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldDifferentialSequence.lean, line 1345. The attribute's comment: “the sequence of sheaves of C-modules on C_{C/B/A} is short exact”.

Tag 08QU: the sequence of sheaves of C̲-modules on C_{C/B/A} 0 → g₁⁻¹Ω₁ ⊗_{B̲} C̲ → g₂⁻¹Ω₂ → g₃⁻¹Ω₃ → 0 is short exact. By CommAlgCat.towerShortComplex_shortExact_of_objectwise this is the objectwise statement CommAlgCat.towerShortComplexPresheaf_shortExact_obj: a short complex of presheaves of C̲-modules on the chaotic site C_{C/B/A} is short exact as soon as its sequence of sections over every polynomial tower is, and there the sequence is the split differential sequence of Algebra, Lemma 10.138.9 for A → P → Q base changed along the augmentation Q → C̲.

theorem towerShortComplex_shortExact : (towerShortComplex A B C).ShortExact
Tag 08QV, a lemma

Tag 08QV in the Stacks Project.

CommAlgCat.leftDerivedColimitThirdInverseImageZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialOnTop/SmallModel.lean, line 310. The attribute's comment: “the degree-zero half of Lπ_!(g₃^{-1}ℱ) = Lπ_{3,!}ℱ = π_{3,!}ℱ, read at the small models of the footnote-restricted sites of Tag 08QT, with π_! the colimit over the index category of Tag 08PF and κ, μ the bounds on the two layers of variables; the vanishing in positive degrees is CommAlgCat.isZero_leftDerivedColimitThirdInverseImage_succ”.

Stacks 08QV, in degree zero. With notation as in Tag 08QT, suppose C = B[E] is a polynomial algebra over B. Then π_!(g₃^{-1}ℱ) = π_{3,!}ℱ for every abelian presheaf ℱ on the small model of the restricted site C_{C/B}: both sides are the sections of ℱ at the identity augmentation C → C.

def leftDerivedColimitThirdInverseImageZeroIso
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A))))
    (F : (smallBoundedPolynomialSite B (towerRelativeAlgebra B C) μ)ᵒᵖ ⥤ AddCommGrpCat.{u}) :
    ((colim : ((smallBoundedPolynomialTowerSite A B C κ μ)ᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤
          AddCommGrpCat.{u}).leftDerived 0).obj
        ((smallTowerThirdInverseImage A B C κ μ).obj F) ≅
      colimit F

CommAlgCat.isZero_leftDerivedColimitThirdInverseImage_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialOnTop/SmallModel.lean, line 331. The attribute's comment: “the positive-degree half of Lπ_!(g₃^{-1}ℱ) = Lπ_{3,!}ℱ = π_{3,!}ℱ, read at the small models of the footnote-restricted sites of Tag 08QT: Lπ_!(g₃^{-1}ℱ) is concentrated in degree zero, where it is π_{3,!}ℱ by CommAlgCat.leftDerivedColimitThirdInverseImageZeroIso”.

Stacks 08QV, in positive degrees. With notation as in Tag 08QT, suppose C = B[E] is a polynomial algebra over B. Then L_nπ_!(g₃^{-1}ℱ) = 0 for n > 0: the simplicial abelian group (g₃^{-1}ℱ)(U_•) is constant.

theorem isZero_leftDerivedColimitThirdInverseImage_succ
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight ε (forget (CommAlgCat.{u} A))))
    (F : (smallBoundedPolynomialSite B (towerRelativeAlgebra B C) μ)ᵒᵖ ⥤ AddCommGrpCat.{u})
    (n : ℕ) :
    IsZero (((colim : ((smallBoundedPolynomialTowerSite A B C κ μ)ᵒᵖ ⥤ AddCommGrpCat.{u}) ⥤
        AddCommGrpCat.{u}).leftDerived (n + 1)).obj
      ((smallTowerThirdInverseImage A B C κ μ).obj F))

CommAlgCat.polynomialTowerDerivedColimitThirdInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialOnTopLargeSite.lean, line 268. The attribute's comment: “the first equality Lπ_!(g₃^{-1}ℱ) = Lπ_{3,!}ℱ in D(Ab), at the sites of Tag 08QT and Tag 08PR themselves -- CommAlgCat.polynomialTowerSite and CommAlgCat.polynomialSite B (towerRelativeAlgebra B C), not restrictions of them -- with Lπ_! and Lπ_{3,!} the total left derived functors of the colimits over the index categories of Tag 08PF and the coefficients at the universe u + 1 of the sites' objects. The second equality Lπ_{3,!}ℱ = π_{3,!}ℱ is CommAlgCat.polynomialSiteDerivedColimitThirdIso”.

Stacks 08QV, the first equality Lπ_!(g₃^{-1}ℱ) = Lπ_{3,!}ℱ, at the sites themselves. With notation as in Tag 08QT, suppose C = B[E] is a polynomial algebra over B. Then

Lπ_!(g₃^{-1}ℱ) = Lπ_{3,!}ℱ

in D(Ab), for every abelian sheaf ℱ on C_{C/B} -- the abelian presheaves being the abelian sheaves, the topology being chaotic.

Both sides are the extended Moore complex of ℱ(u₃(U_•)) for the cosimplicial object U_• of the towers (P_n → B, P_n[E] → C): on the left by the criterion of Tag 08Q9 applied to U_• on C_{C/B/A}, on the right by that criterion applied to the constant cosimplicial object at the identity augmentation C → C on C_{C/B}, which u₃(U_•) is. No hypothesis on a resolution survives: the resolution of B over A is the standard one of Tag 08PM, whose terms are polynomial algebras and whose augmentation is a trivial Kan fibration by Tag 08QI.

def polynomialTowerDerivedColimitThirdInverseImageIso
    (F : (polynomialSite B (towerRelativeAlgebra B C))ᵒᵖ ⥤ AddCommGrpCat.{u + 1}) :
    (totalDerivedColimit' (polynomialTowerSite A B C) AddCommGrpCat.{u + 1}).obj
        (DerivedCategory.Q.obj
          ((HomologicalComplex.single ((polynomialTowerSite A B C)ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
            (ComplexShape.up ℤ) 0).obj ((towerThirdInverseImage A B C).obj F))) ≅
      (totalDerivedColimit' (polynomialSite B (towerRelativeAlgebra B C))
          AddCommGrpCat.{u + 1}).obj
        (DerivedCategory.Q.obj
          ((HomologicalComplex.single
            ((polynomialSite B (towerRelativeAlgebra B C))ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
            (ComplexShape.up ℤ) 0).obj F))

CommAlgCat.polynomialSiteDerivedColimitThirdIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldPolynomialOnTopLargeSite.lean, line 304. The attribute's comment: “the second equality Lπ_{3,!}ℱ = π_{3,!}ℱ in D(Ab), at the site C_{C/B} of Tag 08PR itself -- CommAlgCat.polynomialSite B (towerRelativeAlgebra B C), not a restriction of it -- with Lπ_{3,!} the total left derived functor of the colimit over its index category and π_{3,!}ℱ that colimit, as in Tag 08PF. The first equality Lπ_!(g₃^{-1}ℱ) = Lπ_{3,!}ℱ is CommAlgCat.polynomialTowerDerivedColimitThirdInverseImageIso”.

Stacks 08QV, the second equality Lπ_{3,!}ℱ = π_{3,!}ℱ, at the site C_{C/B} itself. With notation as in Tag 08QT, suppose C = B[E] is a polynomial algebra over B. Then

Lπ_{3,!}ℱ = π_{3,!}ℱ

in D(Ab), for every abelian sheaf ℱ on C_{C/B}: the left side is the complex concentrated in degree zero on π_{3,!}ℱ, the colimit of ℱ over the index category of Tag 08PF.

This is where C = B[E] is used on C_{C/B} itself: it makes the identity augmentation C → C an object of that site, and that object is initial there, so π_{3,!} is an evaluation and hence exact.

def polynomialSiteDerivedColimitThirdIso
    (F : (polynomialSite B (towerRelativeAlgebra B C))ᵒᵖ ⥤ AddCommGrpCat.{u + 1}) :
    (totalDerivedColimit' (polynomialSite B (towerRelativeAlgebra B C))
          AddCommGrpCat.{u + 1}).obj
        (DerivedCategory.Q.obj
          ((HomologicalComplex.single
            ((polynomialSite B (towerRelativeAlgebra B C))ᵒᵖ ⥤ AddCommGrpCat.{u + 1})
            (ComplexShape.up ℤ) 0).obj F)) ≅
      DerivedCategory.Q.obj
        ((HomologicalComplex.single AddCommGrpCat.{u + 1} (ComplexShape.up ℤ) 0).obj
          (colimit F))
Tag 08QW, a lemma

Tag 08QW in the Stacks Project.

CommAlgCat.derivedLowerShriek_comp_inverseImage_polynomialTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ThreefoldLowerShriekComparison.lean, line 308.

Stacks Project, Tag 08QW. With notation as in Tag 08QT, Lg_{i,!} ∘ g_i⁻¹ = id for i = 1, 2, 3, and hence also Lπ_! ∘ g_i⁻¹ = Lπ_{i,!} for i = 1, 2, 3.

Here g₁, g₂, g₃ are the morphisms of topoi from C_{C/B/A} to C_{B/A}, C_{C/A} and C_{C/B} induced by u₁, u₂, u₃, and π, π₁, π₂, π₃ the projections of the four sites to the point; all four sites carry the chaotic topology. The statement is about abelian sheaves on the unbounded derived categories, for every left derived functor of each lower shriek and every derived functor of each inverse image, so it does not depend on choices. The six parts are CommAlgCat.derivedLowerShriekFirstInverseImageIso, CommAlgCat.derivedLowerShriekSecondInverseImageIso, CommAlgCat.derivedLowerShriekThirdInverseImageIso, CommAlgCat.derivedLowerShriekProjectionFirstIso, CommAlgCat.derivedLowerShriekProjectionSecondIso and CommAlgCat.derivedLowerShriekProjectionThirdIso.

theorem derivedLowerShriek_comp_inverseImage_polynomialTower :
    (∀ (L : DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (polynomialTopology A (towerBaseAlgebra A B)) AddCommGrpCat.{u + 1}))
      (α : DerivedCategory.Qh ⋙ L ⟶
        ((polynomialTowerFirst A B C).sheafPullback AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology A (towerBaseAlgebra A B))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso
        (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))]
      (G : DerivedCategory
          (Sheaf (polynomialTopology A (towerBaseAlgebra A B)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}))
      (_ : DerivedCategory.Qh ⋙ G ≅
        ((polynomialTowerFirst A B C).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology A (towerBaseAlgebra A B))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh),
      Nonempty (G ⋙ L ≅ 𝟭 _)) ∧
    (∀ (L : DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (polynomialTopology A (towerTotalAlgebra A C)) AddCommGrpCat.{u + 1}))
      (α : DerivedCategory.Qh ⋙ L ⟶
        ((polynomialTowerSecond A B C).sheafPullback AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology A (towerTotalAlgebra A C))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso
        (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))]
      (G : DerivedCategory
          (Sheaf (polynomialTopology A (towerTotalAlgebra A C)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}))
      (_ : DerivedCategory.Qh ⋙ G ≅
        ((polynomialTowerSecond A B C).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology A (towerTotalAlgebra A C))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh),
      Nonempty (G ⋙ L ≅ 𝟭 _)) ∧
    (∀ (L : DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (polynomialTopology B (towerRelativeAlgebra B C)) AddCommGrpCat.{u + 1}))
      (α : DerivedCategory.Qh ⋙ L ⟶
        ((polynomialTowerThird A B C).sheafPullback AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology B (towerRelativeAlgebra B C))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso
        (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))]
      (G : DerivedCategory
          (Sheaf (polynomialTopology B (towerRelativeAlgebra B C)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}))
      (_ : DerivedCategory.Qh ⋙ G ≅
        ((polynomialTowerThird A B C).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology B (towerRelativeAlgebra B C))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh),
      Nonempty (G ⋙ L ≅ 𝟭 _)) ∧
    (∀ (G : DerivedCategory
          (Sheaf (polynomialTopology A (towerBaseAlgebra A B)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}))
      (_ : DerivedCategory.Qh ⋙ G ≅
        ((polynomialTowerFirst A B C).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology A (towerBaseAlgebra A B))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      (L : DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 2})) AddCommGrpCat.{u + 1}))
      (α : DerivedCategory.Qh ⋙ L ⟶
        ((Functor.star (polynomialTowerSite A B C)).sheafPullback AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (GrothendieckTopology.trivial (Discrete PUnit.{u + 2}))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso
        (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))]
      (L' : DerivedCategory
          (Sheaf (polynomialTopology A (towerBaseAlgebra A B)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 2})) AddCommGrpCat.{u + 1}))
      (α' : DerivedCategory.Qh ⋙ L' ⟶
        ((Functor.star (polynomialSite A (towerBaseAlgebra A B))).sheafPullback
          AddCommGrpCat.{u + 1} (polynomialTopology A (towerBaseAlgebra A B))
          (GrothendieckTopology.trivial (Discrete PUnit.{u + 2}))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L'.IsLeftDerivedFunctor α' (HomotopyCategory.quasiIso
        (Sheaf (polynomialTopology A (towerBaseAlgebra A B)) AddCommGrpCat.{u + 1})
        (ComplexShape.up ℤ))],
      Nonempty (G ⋙ L ≅ L')) ∧
    (∀ (G : DerivedCategory
          (Sheaf (polynomialTopology A (towerTotalAlgebra A C)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}))
      (_ : DerivedCategory.Qh ⋙ G ≅
        ((polynomialTowerSecond A B C).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology A (towerTotalAlgebra A C))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      (L : DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 2})) AddCommGrpCat.{u + 1}))
      (α : DerivedCategory.Qh ⋙ L ⟶
        ((Functor.star (polynomialTowerSite A B C)).sheafPullback AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (GrothendieckTopology.trivial (Discrete PUnit.{u + 2}))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso
        (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))]
      (L' : DerivedCategory
          (Sheaf (polynomialTopology A (towerTotalAlgebra A C)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 2})) AddCommGrpCat.{u + 1}))
      (α' : DerivedCategory.Qh ⋙ L' ⟶
        ((Functor.star (polynomialSite A (towerTotalAlgebra A C))).sheafPullback
          AddCommGrpCat.{u + 1} (polynomialTopology A (towerTotalAlgebra A C))
          (GrothendieckTopology.trivial (Discrete PUnit.{u + 2}))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L'.IsLeftDerivedFunctor α' (HomotopyCategory.quasiIso
        (Sheaf (polynomialTopology A (towerTotalAlgebra A C)) AddCommGrpCat.{u + 1})
        (ComplexShape.up ℤ))],
      Nonempty (G ⋙ L ≅ L')) ∧
    (∀ (G : DerivedCategory
          (Sheaf (polynomialTopology B (towerRelativeAlgebra B C)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}))
      (_ : DerivedCategory.Qh ⋙ G ≅
        ((polynomialTowerThird A B C).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (polynomialTopology B (towerRelativeAlgebra B C))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      (L : DerivedCategory (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 2})) AddCommGrpCat.{u + 1}))
      (α : DerivedCategory.Qh ⋙ L ⟶
        ((Functor.star (polynomialTowerSite A B C)).sheafPullback AddCommGrpCat.{u + 1}
          (polynomialTowerTopology A B C)
          (GrothendieckTopology.trivial (Discrete PUnit.{u + 2}))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L.IsLeftDerivedFunctor α (HomotopyCategory.quasiIso
        (Sheaf (polynomialTowerTopology A B C) AddCommGrpCat.{u + 1}) (ComplexShape.up ℤ))]
      (L' : DerivedCategory
          (Sheaf (polynomialTopology B (towerRelativeAlgebra B C)) AddCommGrpCat.{u + 1}) ⥤
          DerivedCategory
            (Sheaf (GrothendieckTopology.trivial (Discrete PUnit.{u + 2})) AddCommGrpCat.{u + 1}))
      (α' : DerivedCategory.Qh ⋙ L' ⟶
        ((Functor.star (polynomialSite B (towerRelativeAlgebra B C))).sheafPullback
          AddCommGrpCat.{u + 1} (polynomialTopology B (towerRelativeAlgebra B C))
          (GrothendieckTopology.trivial (Discrete PUnit.{u + 2}))).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
      [L'.IsLeftDerivedFunctor α' (HomotopyCategory.quasiIso
        (Sheaf (polynomialTopology B (towerRelativeAlgebra B C)) AddCommGrpCat.{u + 1})
        (ComplexShape.up ℤ))],
      Nonempty (G ⋙ L ≅ L'))
Tag 08QX, a proposition

Tag 08QX in the Stacks Project.

CommAlgCat.exists_distTriang_fundamentalVertex_of_isResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/Fundamental.lean, line 159. The attribute's comment: “the triangle on the three vertices of the display of Tag 08QS, under TWO carried hypotheses the source lacks: B → C injective, as in Tag 08SD, whose removal needs the product decomposition of Tag 08SC; and the key fact of Tag 08SD, that the base-changed resolution Q_bullet ⊗_{P_bullet} B is a resolution of C over B, which rests on Tag 08RX. Neither tag is proved in this library”.

The fundamental triangle of the cotangent complex. Let A → B → C be ring maps. Then there is a distinguished triangle

L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A} ⟶ L_{C/B} ⟶ (L_{B/A} ⊗^𝐋_B C)[1]

in D(C), on the three vertices of the display of Tag 08QS.

Two hypotheses the source does not have are carried: B → C is injective, as in Tag 08SD, and the base-changed resolution Q̄_• = Q_• ⊗_{P_•} B of Tag 08SD is a resolution of C over B — its terms are polynomial algebras over B and its augmentation to C is a trivial Kan fibration on underlying simplicial sets.

theorem exists_distTriang_fundamentalVertex_of_isResolution
    (A : Type u) [CommRing A] (B : Type u) [CommRing B] [Algebra A B]
    (C : Type u) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C]
    (hf : Function.Injective (algebraMap B C))
    (hP : ∀ n, IsPolynomialAlgebra B
      ((baseChangedStandardResolution A (towerHom A B C)).left.obj n))
    (hε : SSet.trivialKanFibrations (Functor.whiskerRight
      (baseChangedStandardResolution A (towerHom A B C)).hom (forget (CommAlgCat.{u} B)))) :
    ∃ (α : fundamentalVertex₁.{u, u, u + 1, u + 1} A B C ⟶ fundamentalVertex₂.{u, u, u + 1} A C)
      (β : fundamentalVertex₂.{u, u, u + 1} A C ⟶ fundamentalVertex₃.{u, u, u + 1} B C)
      (δ : fundamentalVertex₃.{u, u, u + 1} B C ⟶
        (fundamentalVertex₁.{u, u, u + 1, u + 1} A B C)⟦(1 : ℤ)⟧),
      Triangle.mk α β δ ∈ distTriang (DerivedCategory (ModuleCat.{u} C))

CommAlgCat.productFundamentalTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/ProductDescent.lean, line 357. The attribute's comment: “the proposition: for ring maps A → B → C the display of Tag 08QS is a distinguished triangle in D(C), on the display's own three vertices and with the display's own three morphisms. The third of them is CommAlgCat.productFundamentalMor₃”.

Stacks Project, Tag 08QX, and the distinguishedness asserted by the display of Tag 08QS. Let A → B → C be ring maps. Then

L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A} ⟶ L_{C/B} ⟶ (L_{B/A} ⊗^𝐋_B C)[1]

is a distinguished triangle in D(C), on the three vertices of the display of [Stacks, Tag 08QS], with the display's own first two morphisms CommAlgCat.fundamentalMor₁ and CommAlgCat.fundamentalMor₂ — the two functoriality maps of [Stacks, Tag 08PN] for the two commutative squares of the tower — and with CommAlgCat.productFundamentalMor₃ for its third.

The display of Tag 08QS is written as a triangle, and what makes it one is exactly this statement, so the display's distinguishedness clause is registered here as well: the three objects and the three arrows of the display are named by CommAlgCat.fundamentalVertex₁, CommAlgCat.fundamentalVertex₂, CommAlgCat.fundamentalVertex₃, CommAlgCat.fundamentalMor₁, CommAlgCat.fundamentalMor₂ and CommAlgCat.productFundamentalMor₃, and that they form a triangle at all is Proposition 08QX.

The proof is the one of [Stacks, Remark 08SD]: the triangle for A → B → B × C, where the map is the split injection b ↦ (b, f b), base changed along the flat projection B × C → C.

theorem productFundamentalTriangle_distinguished :
    Triangle.mk (fundamentalMor₁.{u} A B C) (fundamentalMor₂.{u} A B C)
        (productFundamentalMor₃ A B C) ∈ distTriang (DerivedCategory (ModuleCat.{u} C))
Tag 08SD, a remark

Tag 08SD in the Stacks Project.

CommAlgCat.baseChangedStandardResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChange.lean, line 56. The attribute's comment: “base_changed_standard_resolution”.

The standard resolution of C over A, base changed along the standard resolution of B to give an augmented simplicial B-algebra.

noncomputable def baseChangedStandardResolution
    (A : Type u) [CommRing A]
    {B C : CommAlgCat.{max u v} A} (f : B ⟶ C) :
    SimplicialObject.Augmented (CommAlgCat.{max u v} B)

CommAlgCat.standardResolution_isPolynomialAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChange.lean, line 189. The attribute's comment: “polynomiality”.

Every term of the standard resolution of C is a polynomial algebra over the corresponding term of the standard resolution of B, when B → C is injective.

theorem standardResolution_isPolynomialAlgebra
    (A : Type u) [CommRing A]
    {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    (hf : Function.Injective f.hom) (n : SimplexCategoryᵒᵖ) :
    let P := (standardResolution A B).left.obj n
    let Q := (standardResolution A C).left.obj n
    letI : Algebra P Q :=
      (((standardResolutionFunctor A).map f).left.app n).hom.toAlgebra
    IsPolynomialAlgebra P (CommAlgCat.of P Q)

CommAlgCat.fundamentalTriangle_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangedResolutionTriangle.lean, line 132. The attribute's comment: “the first paragraph of the remark, for A → B → C with B → C injective: Q_n is polynomial over P_n; Q̄_• = Q_• ⊗_{P_•} B is a resolution of C over B; the sequence of differentials is short exact; and its triangle is the fundamental triangle, with the canonical first two morphisms, on the vertices L_{B/A} ⊗^𝐋_B C, L_{C/A}, L_{C/B}”.

Stacks Project, Remark 08SD, first paragraph. Let A → B → C be ring maps with B → C injective, let P_• → B be the standard resolution of B over A, Q_• → C that of C over A, and Q̄_• = Q_• ⊗_{P_•} B. Then

  1. every Q_n is a polynomial algebra over P_n;
  2. Q̄_• → C is a resolution of C over B (the key fact);
  3. the sequence of complexes of C-modules 0 → Ω_{P_•/A} ⊗_{P_•} C → Ω_{Q_•/A} ⊗_{Q_•} C → Ω_{Q̄_•/B} ⊗_{Q̄_•} C → 0 is short exact;
  4. the distinguished triangle associated to that short exact sequence is isomorphic to the fundamental triangle L_{B/A} ⊗^𝐋_B C → L_{C/A} → L_{C/B} → (L_{B/A} ⊗^𝐋_B C)[1] with its canonical first two morphisms, which is therefore distinguished in D(C).
theorem fundamentalTriangle_of_injective (hf : Function.Injective (algebraMap B C)) :
    (∀ n : SimplexCategoryᵒᵖ,
      letI : Algebra ((standardResolution A (CommAlgCat.of A B)).left.obj n)
          ((standardResolution A (CommAlgCat.of A C)).left.obj n) :=
        (((standardResolutionFunctor A).map (towerHom A B C)).left.app n).hom.toAlgebra
      IsPolynomialAlgebra ((standardResolution A (CommAlgCat.of A B)).left.obj n)
        (CommAlgCat.of ((standardResolution A (CommAlgCat.of A B)).left.obj n)
          ((standardResolution A (CommAlgCat.of A C)).left.obj n))) ∧
    @IsResolution ↥(CommAlgCat.of A B) (CommAlgCat.of A B).commRing
      ↥(algebraOver (towerHom A B C)) (algebraOver (towerHom A B C)).commRing
      (algebraOver (towerHom A B C)).algebra
      (baseChangedStandardResolution A (towerHom A B C)).left
      (baseChangedStandardResolution A (towerHom A B C)).hom ∧
    (cotangentDifferentialComplexes A (towerHom A B C)).ShortExact ∧
    Nonempty (cotangentTriangle A (towerHom A B C)
        (show Function.Injective (towerHom A B C).hom from hf) ≅
      Triangle.mk (fundamentalMor₁.{u} A B C) (fundamentalMor₂.{u} A B C)
        (fundamentalMor₃ A B C hf)) ∧
    Triangle.mk (fundamentalMor₁.{u} A B C) (fundamentalMor₂.{u} A B C)
        (fundamentalMor₃ A B C hf) ∈ distTriang (DerivedCategory (ModuleCat.{u} C))

CommAlgCat.fundamentalTriangle_of_productDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangedResolutionTriangle.lean, line 191. The attribute's comment: “the second paragraph of the remark, for arbitrary A → B → C: B → B × C is injective, the base change along the flat B × C → C of the fundamental triangle of A → B → B × C is distinguished in D(C) and, by Tag 08SC, isomorphic to the fundamental triangle of A → B → C with its canonical first two morphisms”.

Stacks Project, Remark 08SD, second paragraph. Let A → B → C be arbitrary ring maps. Then B → B × C, b ↦ (b, f b), is injective, so the first paragraph gives the fundamental triangle of A → B → B × C; its base change along the flat ring map B × C → C is a distinguished triangle in D(C), and by Tag 08SC it is isomorphic to the fundamental triangle L_{B/A} ⊗^𝐋_B C → L_{C/A} → L_{C/B} → (L_{B/A} ⊗^𝐋_B C)[1] with its canonical first two morphisms, which is therefore distinguished.

theorem fundamentalTriangle_of_productDescent :
    Function.Injective (algebraMap B (B × C)) ∧
    productDescentTriangle A B C ∈ distTriang (DerivedCategory (ModuleCat.{u} C)) ∧
    Nonempty (productDescentTriangle A B C ≅
      Triangle.mk (fundamentalMor₁.{u} A B C) (fundamentalMor₂.{u} A B C)
        (productFundamentalMor₃ A B C)) ∧
    Triangle.mk (fundamentalMor₁.{u} A B C) (fundamentalMor₂.{u} A B C)
        (productFundamentalMor₃ A B C) ∈ distTriang (DerivedCategory (ModuleCat.{u} C))

CommAlgCat.exists_distinguished_derivedBaseChange_cotangentTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DerivedFirstVertex.lean, line 167. The attribute's comment: “differential_sequence triangle, derived first vertex”.

Stacks Project, Tag 08SD, with the derived base change as first vertex.

For an injective map f : B ⟶ C of A-algebras there is a distinguished triangle in D(ModuleCat C) L_{B/A} ⊗ᴸ_B C → L_{C/A} → (third vertex of CommAlgCat.cotangentTriangle) → (L_{B/A} ⊗ᴸ_B C)[1] whose first vertex is literally the derived base change of L_{B/A} along f, whose second vertex is L_{C/A} and whose third vertex is the third vertex of CommAlgCat.cotangentTriangle, the complex of the base-changed relative differentials.

This statement leaves the third vertex as the complex of base-changed relative differentials. Its identification with L_{C/B}, and the passage to arbitrary A → B → C through B × C and Tag 08SC, are the two paragraphs of Remark 08SD stated whole in StacksFrontier/Cotangent/Triangle/BaseChangedResolutionTriangle.lean: CommAlgCat.fundamentalTriangle_of_injective and CommAlgCat.fundamentalTriangle_of_productDescent.

theorem exists_distinguished_derivedBaseChange_cotangentTriangle (A : Type u) [CommRing A]
    {B C : CommAlgCat.{max u v} A} [HasDerivedCategory.{wB} (ModuleCat.{max u v} B)]
    [HasDerivedCategory.{wC} (ModuleCat.{max u v} C)]
    (f : B ⟶ C) (hf : Function.Injective f.hom) :
    ∃ (α : (CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral
            f.hom.toRingHom).functor.obj
          (DerivedCategory.Q.obj (cotangentComplex.{u, v} A B)) ⟶
        DerivedCategory.Q.obj (cotangentComplex.{u, v} A C))
      (β : DerivedCategory.Q.obj (cotangentComplex.{u, v} A C) ⟶
        (cotangentTriangle A f hf).obj₃)
      (δ : (cotangentTriangle A f hf).obj₃ ⟶
        ((CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral
            f.hom.toRingHom).functor.obj
          (DerivedCategory.Q.obj (cotangentComplex.{u, v} A B)))⟦(1 : ℤ)⟧),
      Triangle.mk α β δ ∈ distTriang (DerivedCategory (ModuleCat.{max u v} C))

CommAlgCat.standardResolutionDifferentialSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 880. The attribute's comment: “differential_sequence construction”.

The specific canonical differential short complex for A → B → C.

noncomputable def standardResolutionDifferentialSequence
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C) :
    DifferentialSequenceData A f

CommAlgCat.standardResolution_differentials_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 926. The attribute's comment: “differential_sequence”.

The canonical differential complex is short exact.

theorem standardResolution_differentials_shortExact
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    (hf : Function.Injective f.hom) :
    (standardResolutionDifferentialSequence A f).complex.ShortExact

CommAlgCat.standardResolution_differentials_firstMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 1004. The attribute's comment: “differential_sequence first map”.

The first map sends a differential to the differential of its image.

theorem standardResolution_differentials_firstMap
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    (n : SimplexCategoryᵒᵖ) (p : (standardResolution A B).left.obj n) :
    let D := standardResolutionDifferentialSequence A f
    ((D.firstIso.inv.app n) ≫ (D.complex.f.app n) ≫ (D.secondIso.hom.app n))
      ((1 : C) ⊗ₜ[B] cotangentTermDifferential A B n p) =
      cotangentTermDifferential A C n
        (((standardResolutionFunctor A).map f).left.app n p)

CommAlgCat.standardResolution_differentials_secondMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 1016. The attribute's comment: “differential_sequence second map”.

The second map is the canonical map to base-changed relative differentials.

theorem standardResolution_differentials_secondMap
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    (n : SimplexCategoryᵒᵖ) (q : (standardResolution A C).left.obj n) :
    let D := standardResolutionDifferentialSequence A f
    let R := baseChangedStandardResolution A f
    let T := R.left.obj n
    letI : Algebra T C := ((R.hom.app n).hom.toRingHom).toAlgebra
    ((D.secondIso.inv.app n) ≫ (D.complex.g.app n) ≫ (D.thirdIso n).hom)
      (cotangentTermDifferential A C n q) =
      ((1 : C) ⊗ₜ[T] KaehlerDifferential.D B T (D.toBaseChange n q))

CommAlgCat.standardResolution_differentials_third_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 1030. The attribute's comment: “differential_sequence naturality”.

The identification of the third term respects every simplicial map.

theorem standardResolution_differentials_third_naturality
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    {i j : SimplexCategoryᵒᵖ} (h : i ⟶ j)
    (t : (baseChangedStandardResolution A f).left.obj
      i) :
    let D := standardResolutionDifferentialSequence A f
    let R := baseChangedStandardResolution A f
    let Ti := R.left.obj i
    let Tj := R.left.obj j
    letI : Algebra Ti C := ((R.hom.app i).hom.toRingHom).toAlgebra
    letI : Algebra Tj C := ((R.hom.app j).hom.toRingHom).toAlgebra
    ((D.thirdIso i).inv ≫ D.complex.X₃.map h ≫ (D.thirdIso j).hom)
      ((1 : C) ⊗ₜ[Ti] KaehlerDifferential.D B Ti t) =
      ((1 : C) ⊗ₜ[Tj] KaehlerDifferential.D B Tj (R.left.map h t))

CommAlgCat.standardResolution_differentials_pushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 1048. The attribute's comment: “differential_sequence base change”.

The map to the base-changed resolution is its canonical pushout leg.

theorem standardResolution_differentials_pushout
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    (n : SimplexCategoryᵒᵖ) :
    let D := standardResolutionDifferentialSequence A f
    let R := baseChangedStandardResolution A f
    CategoryTheory.IsPushout
      (CommRingCat.ofHom
        (((standardResolutionFunctor A).map f).left.app n).hom.toRingHom)
      (CommRingCat.ofHom (standardResolutionAugmentationHom A B n))
      (CommRingCat.ofHom (D.toBaseChange n))
      (CommRingCat.ofHom (algebraMap B (R.left.obj n)))

CommAlgCat.standardResolution_differentials_toBaseChange_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 1063. The attribute's comment: “differential_sequence base change naturality”.

The pushout leg is simplicially natural.

theorem standardResolution_differentials_toBaseChange_naturality
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    {i j : SimplexCategoryᵒᵖ} (h : i ⟶ j)
    (q : (standardResolution A C).left.obj i) :
    let D := standardResolutionDifferentialSequence A f
    let R := baseChangedStandardResolution A f
    R.left.map h (D.toBaseChange i q) =
      D.toBaseChange j ((standardResolution A C).left.map h q)

CommAlgCat.standardResolution_differentials_toBaseChange_augmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/DifferentialSequence.lean, line 1075. The attribute's comment: “differential_sequence augmentation”.

The pushout leg is compatible with augmentation to C.

theorem standardResolution_differentials_toBaseChange_augmentation
    (A : Type u) [CommRing A] {B C : CommAlgCat.{max u v} A} (f : B ⟶ C)
    (n : SimplexCategoryᵒᵖ) :
    let D := standardResolutionDifferentialSequence A f
    let R := baseChangedStandardResolution A f
    ((R.hom.app n).hom.toRingHom).comp (D.toBaseChange n) =
      standardResolutionAugmentationHom A C n

CommAlgCat.cotangentDifferentialComplexes_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/Distinguished.lean, line 142. The attribute's comment: “differential_sequence complexes”.

For an injective map f : B ⟶ C of A-algebras, the differential short complex of cochain complexes of C-modules is short exact.

theorem cotangentDifferentialComplexes_shortExact (A : Type u) [CommRing A]
    {B C : CommAlgCat.{max u v} A} (f : B ⟶ C) (hf : Function.Injective f.hom) :
    (cotangentDifferentialComplexes A f).ShortExact

CommAlgCat.cotangentTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/Distinguished.lean, line 151. The attribute's comment: “differential_sequence triangle”.

The triangle in D(ModuleCat C) attached to the differential short exact sequence of the standard resolutions of A → B → C, for f : B ⟶ C injective.

noncomputable def cotangentTriangle (A : Type u) [CommRing A]
    {B C : CommAlgCat.{max u v} A} [HasDerivedCategory.{t} (ModuleCat.{max u v} C)]
    (f : B ⟶ C) (hf : Function.Injective f.hom) :
    Triangle (DerivedCategory (ModuleCat.{max u v} C))

CommAlgCat.cotangentTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/Distinguished.lean, line 159. The attribute's comment: “differential_sequence triangle distinguished”.

The triangle attached to the differential sequence is distinguished.

theorem cotangentTriangle_distinguished (A : Type u) [CommRing A]
    {B C : CommAlgCat.{max u v} A} [HasDerivedCategory.{t} (ModuleCat.{max u v} C)]
    (f : B ⟶ C) (hf : Function.Injective f.hom) :
    cotangentTriangle A f hf ∈ distTriang (DerivedCategory (ModuleCat.{max u v} C))
Tag 08SE, a remark

Tag 08SE in the Stacks Project.

CommAlgCat.relativeBaseChangeLeg, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 209. The attribute's comment: “the first arrow of the comparison, R_bullet ⟶ R_bullet ⊗_{S_bullet} B”.

The canonical map R_• ⟶ R̄_• of Remark 08SE: degreewise the pushout leg out of the standard resolution of C over B.

noncomputable def relativeBaseChangeLeg (f : B ⟶ C) :
    (standardResolution ↥B (algebraOver f)).left ⟶ (relativeBaseChange f).left

CommAlgCat.standardResolutionSquareMap_baseRingSquare_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 315. The attribute's comment: “the commutative diagram of standard resolutions from which the canonical map Q_bullet ⊗_{P_bullet} B ⟶ R_bullet ⊗_{S_bullet} B is obtained”.

The commutative diagram of Remark 08SE. The square

Q_•  ⟶  R_•
 ↑        ↑
P_•  ⟶  S_•

commutes, the vertical maps being the functoriality of the standard resolution in the algebra and the horizontal ones the change of base ring from A to B.

theorem standardResolutionSquareMap_baseRingSquare_comm (f : B ⟶ C) (n : SimplexCategoryᵒᵖ) :
    (standardResolutionSquareMap.{u, u, u} (baseRingSquareTop f) n).comp
        ((((standardResolutionFunctor.{u, u} A).map f).left.app n).hom.toRingHom) =
      ((((standardResolutionFunctor.{u, u} ↥B).map (overBase f)).left.app n).hom.toRingHom).comp
        (standardResolutionSquareMap.{u, u, u} (baseRingSquareBot B) n)

CommAlgCat.baseChangedComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 415. The attribute's comment: “the canonical map Q_bullet ⊗_{P_bullet} B ⟶ R_bullet ⊗_{S_bullet} B obtained from the commutative diagram”.

The canonical map Q̄_• ⟶ R̄_• of Remark 08SE, obtained from the commutative diagram of standard resolutions by the pushout property of Q̄_•.

noncomputable def baseChangedComparison (f : B ⟶ C) :
    (baseChangedStandardResolution A f).left ⟶ (relativeBaseChange f).left

CommAlgCat.baseChangedStandardResolution_isPolynomialAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 588. The attribute's comment: “the degreewise polynomiality of a base-changed standard resolution, applied in the remark both to Q_bullet ⊗_{P_bullet} B and to R_bullet ⊗_{S_bullet} B; this is where the injectivity of B → C is used”.

Every term of the base-changed standard resolution Q̄_• = Q_• ⊗_{P_•} B is a polynomial algebra over B, when B → C is injective.

This is the elementary half of the "key fact" of Tag 08SD. Injectivity enters through the polynomiality of Tag 08SD, CommAlgCat.standardResolution_isPolynomialAlgebra, which presents Q_n as a polynomial algebra over P_n; the base change of that presentation along the augmentation P_n → B presents Q̄_n as a polynomial algebra over B on the same variables.

theorem baseChangedStandardResolution_isPolynomialAlgebra (f : B ⟶ C)
    (hf : Function.Injective f.hom) (n : SimplexCategoryᵒᵖ) :
    IsPolynomialAlgebra ↥B ((baseChangedStandardResolution A f).left.obj n)

CommAlgCat.relativeBaseChange_isPolynomialAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 603. The attribute's comment: “R_bullet ⊗_{S_bullet} B is a simplicial polynomial algebra over B, because B → C is injective”.

Every term of R̄_• = R_• ⊗_{S_•} B is a polynomial algebra over B, when B → C is injective: the functoriality map S_• → R_• presents R_n as a polynomial algebra over S_n, so this is CommAlgCat.baseChangedStandardResolution_isPolynomialAlgebra at the base ring B.

theorem relativeBaseChange_isPolynomialAlgebra (f : B ⟶ C) (hf : Function.Injective f.hom)
    (n : SimplexCategoryᵒᵖ) :
    IsPolynomialAlgebra ↥B ((relativeBaseChange f).left.obj n)

CommAlgCat.relativeBaseChangeCotangentLeg, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 649. The attribute's comment: “the induced map L_{C/B} = Omega[R_bullet/B] ⊗ C ⟶ Omega[R_bullet ⊗_{S_bullet} B / B] ⊗ C”.

The first arrow of the comparison of Remark 08SE, the map L_{C/B} = Ω[R_•⁄B] ⊗_{R_•} C ⟶ Ω[R̄_•⁄B] ⊗_{R̄_•} C induced by R_• ⟶ R̄_•.

noncomputable def relativeBaseChangeCotangentLeg (f : B ⟶ C) :
    cotangentComplex ↥B (algebraOver f) ⟶
      augmentedCotangentCochainComplex (relativeBaseChange f).hom

CommAlgCat.baseChangedCotangentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 660. The attribute's comment: “the induced map Omega[Q_bullet ⊗_{P_bullet} B / B] ⊗ C ⟶ Omega[R_bullet ⊗_{S_bullet} B / B] ⊗ C”.

The second arrow of the comparison of Remark 08SE, the map Ω[Q̄_•⁄B] ⊗_{Q̄_•} C ⟶ Ω[R̄_•⁄B] ⊗_{R̄_•} C induced by Q̄_• ⟶ R̄_•.

noncomputable def baseChangedCotangentComparison (f : B ⟶ C) :
    augmentedCotangentCochainComplex (baseChangedStandardResolution A f).hom ⟶
      augmentedCotangentCochainComplex (relativeBaseChange f).hom

CommAlgCat.isIso_q_relativeBaseChangeCotangentLeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 698. The attribute's comment: “the first of the two maps is a quasi-isomorphism. CARRIED as the hypothesis hεR: that the augmentation of R_bullet ⊗_{S_bullet} B to C is a trivial Kan fibration, the half of the source's appeal to Cohomology on Sites, Lemma 21.39.12 (Tag 08RX) that this library lacks. Degreewise polynomiality is NOT carried: it is proved from B → C injective”.

The first arrow of the comparison is a quasi-isomorphism.

Both R_• and R̄_• are resolutions of C over B, so by Tag 08PU each of their complexes is Lπ_!(i^*Ω_{𝒪/B}) in D(C), compatibly with the morphism R_• ⟶ R̄_• between them (CommAlgCat.smallResolutionCotangentDerivedLowerShriekIso_naturality).

That R̄_• is a resolution is used twice over: its degreewise polynomiality is CommAlgCat.relativeBaseChange_isPolynomialAlgebra, which consumes the injectivity of B → C, while the trivial Kan fibration condition hεR is carried.

theorem isIso_q_relativeBaseChangeCotangentLeg (f : B ⟶ C) (hf : Function.Injective f.hom)
    (hεR : SSet.trivialKanFibrations (Functor.whiskerRight (relativeBaseChange f).hom
      (forget (CommAlgCat.{u} ↥B)))) :
    IsIso (DerivedCategory.Q.map (relativeBaseChangeCotangentLeg f))

CommAlgCat.isIso_q_baseChangedCotangentComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 727. The attribute's comment: “the second of the two maps is a quasi-isomorphism. CARRIED as the hypotheses hεQ and hεR: that the augmentations of Q_bullet ⊗_{P_bullet} B and R_bullet ⊗_{S_bullet} B to C are trivial Kan fibrations, the half of Tag 08RX this library lacks. Degreewise polynomiality of both is NOT carried: it is proved from B → C injective”.

The second arrow of the comparison is a quasi-isomorphism, by Tag 08PU at the two resolutions Q̄_• and R̄_• of C over B and its functoriality in the resolution.

theorem isIso_q_baseChangedCotangentComparison (f : B ⟶ C) (hf : Function.Injective f.hom)
    (hεQ : SSet.trivialKanFibrations (Functor.whiskerRight
      (baseChangedStandardResolution A f).hom (forget (CommAlgCat.{u} ↥B))))
    (hεR : SSet.trivialKanFibrations (Functor.whiskerRight (relativeBaseChange f).hom
      (forget (CommAlgCat.{u} ↥B)))) :
    IsIso (DerivedCategory.Q.map (baseChangedCotangentComparison f))

CommAlgCat.baseChangedCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 757. The attribute's comment: “the canonical identification of Omega[Q_bullet ⊗_{P_bullet} B / B] ⊗ C with L_{C/B}: the second arrow of the comparison followed by the inverse of the first. CARRIED as the hypotheses hεQ and hεR, the trivial-Kan-fibration halves of Tag 08RX, which this library lacks. The remark's hypothesis that B → C be injective is NOT carried but consumed”.

Remark 08SE. The canonical identification of Ω[Q̄_•⁄B] ⊗_{Q̄_•} C with L_{C/B} = Ω[R_•⁄B] ⊗_{R_•} C in D(C): the second arrow of the comparison composed with the inverse of the first.

It is characterised by CommAlgCat.baseChangedCotangentComplexIso_hom_comp and CommAlgCat.eq_baseChangedCotangentComplexIso.

noncomputable def baseChangedCotangentComplexIso (f : B ⟶ C) (hf : Function.Injective f.hom)
    (hεQ : SSet.trivialKanFibrations (Functor.whiskerRight
      (baseChangedStandardResolution A f).hom (forget (CommAlgCat.{u} ↥B))))
    (hεR : SSet.trivialKanFibrations (Functor.whiskerRight (relativeBaseChange f).hom
      (forget (CommAlgCat.{u} ↥B)))) :
    DerivedCategory.Q.obj
        (augmentedCotangentCochainComplex (baseChangedStandardResolution A f).hom) ≅
      DerivedCategory.Q.obj (cotangentComplex ↥B (algebraOver f))

CommAlgCat.baseChangedCotangentComplexIso_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 779. The attribute's comment: “the characterising property of the identification: composed with the first arrow of the comparison it is the second, which is what 'composing one with the inverse of the other' means. Same two carried hypotheses as the identification itself”.

The identification of Remark 08SE commutes with the two arrows of the comparison.

theorem baseChangedCotangentComplexIso_hom_comp (f : B ⟶ C) (hf : Function.Injective f.hom)
    (hεQ : SSet.trivialKanFibrations (Functor.whiskerRight
      (baseChangedStandardResolution A f).hom (forget (CommAlgCat.{u} ↥B))))
    (hεR : SSet.trivialKanFibrations (Functor.whiskerRight (relativeBaseChange f).hom
      (forget (CommAlgCat.{u} ↥B)))) :
    (baseChangedCotangentComplexIso f hf hεQ hεR).hom ≫
        DerivedCategory.Q.map (relativeBaseChangeCotangentLeg f) =
      DerivedCategory.Q.map (baseChangedCotangentComparison f)

CommAlgCat.eq_baseChangedCotangentComplexIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparison.lean, line 802. The attribute's comment: “uniqueness of the identification: it is the ONLY isomorphism whose composite with the first arrow of the comparison is the second. Same two carried hypotheses as the identification itself”.

The identification of Remark 08SE is the unique isomorphism commuting with the two arrows of the comparison. This is what pins it down: the first arrow is an isomorphism in D(C), so the commutation determines the identification outright.

theorem eq_baseChangedCotangentComplexIso (f : B ⟶ C) (hf : Function.Injective f.hom)
    (hεQ : SSet.trivialKanFibrations (Functor.whiskerRight
      (baseChangedStandardResolution A f).hom (forget (CommAlgCat.{u} ↥B))))
    (hεR : SSet.trivialKanFibrations (Functor.whiskerRight (relativeBaseChange f).hom
      (forget (CommAlgCat.{u} ↥B))))
    (e : DerivedCategory.Q.obj
        (augmentedCotangentCochainComplex (baseChangedStandardResolution A f).hom) ≅
      DerivedCategory.Q.obj (cotangentComplex ↥B (algebraOver f)))
    (he : e.hom ≫ DerivedCategory.Q.map (relativeBaseChangeCotangentLeg f) =
      DerivedCategory.Q.map (baseChangedCotangentComparison f)) :
    e = baseChangedCotangentComplexIso f hf hεQ hεR

CommAlgCat.isResolution_relativeBaseChange_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparisonOfInjective.lean, line 71. The attribute's comment: “R_bullet ⊗_{S_bullet} B is a simplicial polynomial algebra over B and R_bullet ⊗_{S_bullet} B → C is a resolution, for B → C injective”.

R̄_• = R_• ⊗_{S_•} B is a resolution of C over B when B → C is injective: each R̄_n is a polynomial algebra over B and the augmentation R̄_• → C is a trivial Kan fibration. R̄_• is the base-changed standard resolution at the base ring B and the map CommAlgCat.overBase f, so this is CommAlgCat.isResolution_baseChangedStandardResolution_of_injective there.

theorem isResolution_relativeBaseChange_of_injective (f : B ⟶ C)
    (hf : Function.Injective f.hom) :
    @IsResolution ↥B B.commRing ↥(relativeBaseChange f).right
      (relativeBaseChange f).right.commRing (relativeBaseChange f).right.algebra
      (relativeBaseChange f).left (relativeBaseChange f).hom

CommAlgCat.isIso_q_relativeBaseChangeCotangentLeg_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparisonOfInjective.lean, line 83. The attribute's comment: “the map L_{C/B} = Omega[R_bullet/B] ⊗ C ⟶ Omega[R_bullet ⊗_{S_bullet} B / B] ⊗ C is a quasi-isomorphism, for B → C injective”.

The first map of Remark 08SE is a quasi-isomorphism: L_{C/B} = Ω[R_•⁄B] ⊗_{R_•} C ⟶ Ω[R̄_•⁄B] ⊗_{R̄_•} C becomes an isomorphism in D(C) for B → C injective.

theorem isIso_q_relativeBaseChangeCotangentLeg_of_injective (f : B ⟶ C)
    (hf : Function.Injective f.hom) :
    IsIso (DerivedCategory.Q.map (relativeBaseChangeCotangentLeg f))

CommAlgCat.isIso_q_baseChangedCotangentComparison_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparisonOfInjective.lean, line 94. The attribute's comment: “the map Omega[Q_bullet ⊗_{P_bullet} B / B] ⊗ C ⟶ Omega[R_bullet ⊗_{S_bullet} B / B] ⊗ C is a quasi-isomorphism, for B → C injective”.

The second map of Remark 08SE is a quasi-isomorphism: Ω[Q̄_•⁄B] ⊗_{Q̄_•} C ⟶ Ω[R̄_•⁄B] ⊗_{R̄_•} C becomes an isomorphism in D(C) for B → C injective.

theorem isIso_q_baseChangedCotangentComparison_of_injective (f : B ⟶ C)
    (hf : Function.Injective f.hom) :
    IsIso (DerivedCategory.Q.map (baseChangedCotangentComparison f))

CommAlgCat.baseChangedCotangentComplexIsoOfInjective_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparisonOfInjective.lean, line 110. The attribute's comment: “the identification composed with the first map of the comparison is the second, for B → C injective”.

The identification of Remark 08SE is the second map composed with the inverse of the first: followed by the first map it is the second.

theorem baseChangedCotangentComplexIsoOfInjective_hom_comp (f : B ⟶ C)
    (hf : Function.Injective f.hom) :
    (baseChangedCotangentComplexIsoOfInjective f hf).hom ≫
        DerivedCategory.Q.map (relativeBaseChangeCotangentLeg f) =
      DerivedCategory.Q.map (baseChangedCotangentComparison f)

CommAlgCat.eq_baseChangedCotangentComplexIsoOfInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/BaseChangeComparisonOfInjective.lean, line 122. The attribute's comment: “uniqueness of the identification: the only isomorphism whose composite with the first map of the comparison is the second, for B → C injective”.

The identification of Remark 08SE is canonical: it is the only isomorphism Ω[Q̄_•⁄B] ⊗_{Q̄_•} C ≅ L_{C/B} in D(C) whose composite with the first map of the comparison is the second.

theorem eq_baseChangedCotangentComplexIsoOfInjective (f : B ⟶ C)
    (hf : Function.Injective f.hom)
    (e : DerivedCategory.Q.obj
        (augmentedCotangentCochainComplex (baseChangedStandardResolution A f).hom) ≅
      DerivedCategory.Q.obj (cotangentComplex ↥B (algebraOver f)))
    (he : e.hom ≫ DerivedCategory.Q.map (relativeBaseChangeCotangentLeg f) =
      DerivedCategory.Q.map (baseChangedCotangentComparison f)) :
    e = baseChangedCotangentComplexIsoOfInjective f hf

Declarations registered for the tag:

Sources
LeanCommAlgCat.fundamentalMor₁ · CommAlgCat.fundamentalMor₂ · CommAlgCat.fundamentalVertex₁ · CommAlgCat.fundamentalVertex₂ · CommAlgCat.fundamentalVertex₃ · CommAlgCat.productFundamentalMor₃ · CommAlgCat.productFundamentalTriangle_distinguished · CommAlgCat.polynomialTowerSite

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.