92.8 Localization and étale… to 92.17 The Atiyah class of a…

Section92.8 Localization and étale ring maps#

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

Tag 08QZ, a lemma

Tag 08QZ in the Stacks Project.

CommAlgCat.quasiIso_midCotangentComplexMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChangeDerived.lean, line 221. The attribute's comment: “on the cotangent complexes: under the tag's own hypothesis B = B ⊗_A^𝐋 A' -- Tor independence of A' and B over A, and bijectivity of A' ⊗_A B → B -- the canonical map L_{B/A} ⟶ L_{B/A'} of Tag 08PN is a quasi-isomorphism”.

Stacks 08QZ. Let A → A' → B be ring maps such that B = B ⊗_A^𝐋 A', which is to say that Tor_i^A(A', B) vanishes for i > 0 and the canonical map A' ⊗_A B → B, a' ⊗ x ↦ a' · x, is bijective. Then the canonical map L_{B/A} ⟶ L_{B/A'} of Tag 08PN, CommAlgCat.midCotangentComplexMap, is a quasi-isomorphism.

This is the special case B' = B of Stacks 08QQ, CommAlgCat.quasiIso_cotangentExtendScalarsMooreMap: the square of the tower has the identity of B for its vertical map, so B ⊗_A^𝐋 A' = B' is the hypothesis of the tag, and the base-change map L_{B/A} ⊗_B B' ⟶ L_{B'/A'} of 08QQ is, under CommAlgCat.midCotangentMooreMap_eq, the functoriality map L_{B/A} ⟶ L_{B/A'}. Remark 08QI, which 08QQ carried as a hypothesis, is CommAlgCat.cotangentComputedByEveryResolution, so nothing beyond the tag's own hypothesis is assumed.

theorem quasiIso_midCotangentComplexMap
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hφ : Function.Bijective
      (baseChangeUnit (B' := midAlgebra A' B) (AlgHom.id A (B : Type u)))) :
    QuasiIso (midCotangentComplexMap A' B)

CommAlgCat.isIso_Q_map_midCotangentComplexMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChangeDerived.lean, line 241. The attribute's comment: “the lemma as the invertibility in D(B) of the canonical map of Tag 08PN: under the tag's own hypothesis B = B ⊗_A^𝐋 A', the image of L_{B/A} ⟶ L_{B/A'} under the localization D(B) is invertible”.

Stacks 08QZ in the derived category. Under the tag's hypothesis B = B ⊗_A^𝐋 A' the canonical map L_{B/A} ⟶ L_{B/A'} of Tag 08PN becomes an isomorphism in D(B).

theorem isIso_Q_map_midCotangentComplexMap
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hφ : Function.Bijective
      (baseChangeUnit (B' := midAlgebra A' B) (AlgHom.id A (B : Type u)))) :
    IsIso (DerivedCategory.Q.map (midCotangentComplexMap A' B))

CommAlgCat.midCotangentComplexDerivedIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChangeDerived.lean, line 262.

Stacks 08QZ: L_{B/A} = L_{B/A'} in D(B). Let A → A' → B be ring maps such that B = B ⊗_A^𝐋 A' — that is, Tor_i^A(A', B) = 0 for i > 0 and A' ⊗_A B → B is bijective. Then the cotangent complexes of B over A and over A' are isomorphic in D(B), by the canonical map CommAlgCat.midCotangentComplexMap of Tag 08PN.

This is the conclusion the source states. The degreewise form, CommAlgCat.midCotangentComplexHomologyIso, is a separate statement proved directly from the two resolutions; an isomorphism of cohomology in each degree does not by itself produce an isomorphism in D(B), and the comparison here is the canonical one.

This is the whole of the tag: the hypothesis is the source's, written out, and the conclusion is the source's, an isomorphism in D(B) along the canonical map.

def midCotangentComplexDerivedIso
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hφ : Function.Bijective
      (baseChangeUnit (B' := midAlgebra A' B) (AlgHom.id A (B : Type u)))) :
    DerivedCategory.Q.obj (cotangentComplex.{u, u} A B) ≅
      DerivedCategory.Q.obj (cotangentComplex.{u, u} A' (midAlgebra A' B))

CommAlgCat.midBaseChangeOverDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChangeDifferentials.lean, line 309. The attribute's comment: “the step the proof turns on: the sheaf (P → B) ↦ Ω_{P/A} ⊗_P B on C_{B/A} is the pullback along u : (P → B) ↦ (A' ⊗_A P → B) of the sheaf (Q → B) ↦ Ω_{Q/A'} ⊗_Q B on C_{B/A'}, stated on all augmented algebras rather than only the polynomial ones. The passage from here to L_{B/A} = L_{B/A'} is CommAlgCat.midCotangentComplexHomologyIso”.

i^*Ω_{𝒪/A} = u^{-1}(i^*Ω_{𝒪/A'}), the step of Stacks 08QZ that the proof turns on. For a tower of ring maps A → A' → B, the functor sending an A-algebra P augmented to B to Ω_{P/A} ⊗_P B is the composite of the base-change functor (P → B) ↦ (A' ⊗_A P → B) of Stacks 08QN with the functor sending an A'-algebra Q augmented to B to Ω_{Q/A'} ⊗_Q B:

Ω_{P/A} ⊗_P B = Ω_{(A' ⊗_A P)/A'} ⊗_{A' ⊗_A P} B ,

naturally in (P → B). Each component is Stacks 00RV base changed along the augmentation, Stacks.KaehlerDifferential.augmentationBaseChangeEquiv, and naturality holds because both composites send the pure differential 1 ⊗ d p to 1 ⊗ d(1 ⊗ p) — the pure differentials generate, by CommAlgCat.overDifferentials_hom_ext.

The source's C_{B/A} is the full subcategory of the polynomial algebras, so the comparison of abelian sheaves it asks for is the restriction of this isomorphism along that inclusion; nothing below uses that P is a polynomial algebra.

def midBaseChangeOverDifferentialsIso :
    overDifferentialsFunctor (B := B) ≅
      midBaseChangeOver A' B ⋙ overDifferentialsFunctor (A := A') (B := midAlgebra A' B)

CommAlgCat.midCotangentComplexHomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChangeDifferentials.lean, line 534. The attribute's comment: “the cohomology of L_{B/A} and of L_{B/A'} agrees in every degree, as B-modules, under the tag's own hypothesis B = B ⊗_A^𝐋 A' — Tor independence of A' and B over A, and bijectivity of A' ⊗_A B → B. Degreewise rather than in D(B), because the module half of Tag 08PS, which is what compares the two resolutions of B over A', is itself a statement about (Lπ_!)_n and H_n. The tag's own conclusion, an isomorphism in D(B) along the canonical map of Tag 08PN, is CommAlgCat.midCotangentComplexDerivedIso”.

Stacks 08QZ: L_{B/A} = L_{B/A'}. Let A → A' → B be ring maps such that B = B ⊗_A^𝐋 A', which is to say that Tor_i^A(A', B) vanishes for i > 0 and the canonical map A' ⊗_A B → B, a' ⊗ x ↦ a' · x, is bijective. Then the cotangent complexes of B over A and of B over A' have the same cohomology in every degree, as B-modules.

The proof is the source's. The cohomology of L_{B/A} in degree -n is the degree n homology of the complex of Ω_{P_•/A} ⊗_{P_•} B for the standard resolution P_• of B over A (Tag 08PN, CommAlgCat.cotangentComplexHomologyMooreIso); that simplicial module is Ω_{(A' ⊗_A P_•)/A'} ⊗_{A' ⊗_A P_•} B by the comparison of CommAlgCat.midBaseChangeOverDifferentialsIso, which is the step of Stacks 08QZ that the source's proof turns on; and A' ⊗_A P_• and the standard resolution of B over A' are two resolutions of B over A', so Tag 08PT computes the same L_nπ_!(Ω_{𝒪/A'} ⊗_𝒪 B̲) from both (CommAlgCat.resolutionModuleLeftDerivedCotangentHomologyIso).

The hypothesis enters exactly once, and only through the first half of the proof of Stacks 08QP: CommAlgCat.isResolution_augmentationBaseChange turns it into the statement that A' ⊗_A P_• ⟶ B is a resolution of B over A', which is what Tag 08PT needs of the base-changed resolution. Both halves are used there: Tor independence makes s(P_•) ⊗_A A' compute B ⊗_A^𝐋 A', and bijectivity of A' ⊗_A B → B identifies its degree-zero homology with B.

The conclusion here is degreewise, not an isomorphism in D(B): the module half of Tag 08PS, CommAlgCat.smallResolutionModuleLeftDerivedLowerShriekNatIso, identifies the degree n functor (Lπ_!)_n with the degree n homology of the Moore complex, so the two resolutions of B over A' are compared one degree at a time. The source's isomorphism in D(B) is CommAlgCat.midCotangentComplexDerivedIso of StacksFrontier/Cotangent/PolynomialAlgebraSiteBaseChangeDerived.lean, which carries the same hypotheses and is not deduced from this statement — degreewise isomorphisms do not give one in D(B).

def midCotangentComplexHomologyIso
    (hTor : RingTheory.TorIndependence.TorIndependent A A' (B : Type u))
    (hφ : Function.Bijective
      (baseChangeUnit (B' := midAlgebra A' B) (AlgHom.id A (B : Type u))))
    (n : ℕ) :
    (cotangentComplex.{u, u} A B).homology (-(n : ℤ)) ≅
      (cotangentComplex.{u, u} A' (midAlgebra A' B)).homology (-(n : ℤ))

Tag 08R0, a lemma

Tag 08R0 in the Stacks Project.

CommAlgCat.isZero_cotangentComplex_of_derivedTensor_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SelfDerivedTensorVanishing.lean, line 87.

Stacks Project, Tag 08R0. Let A → B be a ring map such that B = B ⊗_A^𝐋 B, that is, Tor_i^A(B, B) = 0 for i > 0 and the multiplication map B ⊗_A B → B is bijective. Then L_{B/A} = 0 in D(B).

By [Stacks, Tag 08QZ] for the tower A → B → B (CommAlgCat.midCotangentComplexHomologyIso), the cohomology of L_{B/A} in each degree ≤ 0 is that of L_{B/B}, which vanishes (CommAlgCat.isZero_cotangentComplex_self); in positive degrees L_{B/A} is itself zero.

theorem isZero_cotangentComplex_of_derivedTensor_self (A : Type u) [CommRing A]
    (B : CommAlgCat.{u} A)
    (hTor : RingTheory.TorIndependence.TorIndependent A B B)
    (hmul : Function.Bijective
      (Algebra.TensorProduct.lmul' (S := (B : Type u)) A)) :
    Limits.IsZero (DerivedCategory.Q.obj (cotangentComplex.{u, u} A B))

Tag 08R1, a lemma

Tag 08R1 in the Stacks Project.

CommAlgCat.isZero_cotangentComplexDerived_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/DiagonalVanishing.lean, line 193. The attribute's comment: “the lemma in full, with ONE carried hypothesis: the distinguished triangle of Proposition 08QX for the tower B → B ⊗_A B → B, carried as hT because Stacks 08QX is not formalized in this library and the triangle of Tag 08SD assumes an injective map whereas the multiplication B ⊗_A B → B is surjective. BOTH hypotheses of the source are used: the vanishing of the higher Tor^A_i(B, B) is hTor, consumed by Stacks 08QQ (CommAlgCat.derivedCotangentComplexBaseChangeIso) in identifying the first vertex of the triangle with L_{B/A}, and L_{B/(B ⊗_A B)} = 0 is hCot, the vanishing of the third vertex. The B ⊗_A B-algebra structure on B is the multiplication map, CommAlgCat.diagonalAlgebra”.

[Stacks, Tag 08R1]. Let A → B be a ring map such that Tor^A_i(B, B) = 0 for i > 0 and such that L_{B/(B ⊗_A B)} = 0. Then L_{B/A} = 0 in D(B).

The fundamental triangle of the tower B → B ⊗_A B → B, whose second map is the multiplication, is the carried hypothesis hT: Proposition 08QX is not formalized in this library and the triangle of Tag 08SD needs an injective map. Its middle vertex L_{B/B} vanishes by CommAlgCat.isZero_cotangentComplex_self, and its third vertex L_{B/(B ⊗_A B)} vanishes by hCot, so its first vertex vanishes; and that first vertex is L_{B/A} by CommAlgCat.cotangentComplexDerived_iso_fundamentalVertex₁_diagonal, which is where hTor is consumed.

theorem isZero_cotangentComplexDerived_of_torIndependent
    (hTor : RingTheory.TorIndependence.TorIndependent A B (B : Type u))
    {α : fundamentalVertex₁.{u, u} B (B ⊗[A] B) B ⟶ fundamentalVertex₂.{u, u} B B}
    {β : fundamentalVertex₂.{u, u} B B ⟶ fundamentalVertex₃.{u, u} (B ⊗[A] B) B}
    {γ : fundamentalVertex₃.{u, u} (B ⊗[A] B) B ⟶
      (fundamentalVertex₁.{u, u} B (B ⊗[A] B) B)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{u} B)))
    (hCot : IsZero (fundamentalVertex₃.{u, u} (B ⊗[A] B) B)) :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_torIndependent_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishingUnconditional.lean, line 75. The attribute's comment: “the lemma in full, with NOTHING carried: the distinguished triangle of the tower B → B ⊗_A B → B is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished, which holds for arbitrary ring maps and so covers the multiplication B ⊗_A B → B even though it is surjective rather than injective. BOTH hypotheses of the source are used: the vanishing of the higher Tor^A_i(B, B) is hTor, consumed by Stacks 08QQ (CommAlgCat.derivedCotangentComplexBaseChangeIso) in identifying the first vertex of the triangle with L_{B/A}, and L_{B/(B ⊗_A B)} = 0 is hCot, the vanishing of the third vertex. The B ⊗_A B-algebra structure on B is the multiplication map, CommAlgCat.diagonalAlgebra”.

[Stacks, Tag 08R1]. Let A → B be a ring map such that Tor^A_i(B, B) = 0 for i > 0 and such that L_{B/(B ⊗_A B)} = 0. Then L_{B/A} = 0 in D(B).

This is CommAlgCat.isZero_cotangentComplexDerived_of_torIndependent at the distinguished triangle of the tower B → B ⊗_A B → B that Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished, provides.

theorem isZero_cotangentComplexDerived_of_torIndependent_unconditional
    (hTor : RingTheory.TorIndependence.TorIndependent A B (B : Type u))
    (hCot : IsZero (fundamentalVertex₃.{u, u} (B ⊗[A] B) B)) :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

Tag 08R2, a lemma

Tag 08R2 in the Stacks Project.

CommAlgCat.isZero_cotangentComplexDerived_of_flat_of_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishing.lean, line 163. The attribute's comment: “item (2) of the lemma, a flat epimorphism of rings: Module.Flat A B together with bijectivity of b ↦ b ⊗ 1 : B → B ⊗_A B, which is item (3) of CommRingCat.epi_tfae (Stacks 04VN, proved in this library) and is therefore exactly the source's epimorphism condition. NOTHING is carried: no instance of Proposition 08QX is assumed. Both hypotheses are load-bearing — flatness gives the Tor independence that CommAlgCat.cotangentComplexDerived_iso_fundamentalVertex₁_diagonal consumes, and the epimorphism condition is what makes L_{(B ⊗_A B)/B} vanish”.

[Stacks, Tag 08R2] item (2). Let A → B be a flat epimorphism of rings. Then L_{B/A} = 0 in D(B).

The epimorphism condition is bijectivity of b ↦ b ⊗ 1 : B → B ⊗_A B, which is item (3) of CommRingCat.epi_tfae; see the module docstring. Flatness gives Tor^A_i(B, B) = 0 for i > 0, so CommAlgCat.cotangentComplexDerived_iso_fundamentalVertex₁_diagonal identifies L_{B/A} with L_{(B ⊗_A B)/B} ⊗^𝐋_{(B ⊗_A B)} B; and L_{(B ⊗_A B)/B} vanishes because the structure map B → B ⊗_A B is an isomorphism. No cotangent triangle is used.

theorem isZero_cotangentComplexDerived_of_flat_of_bijective [Module.Flat A B]
    (h : Function.Bijective (algebraMap B (B ⊗[A] B))) :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_weaklyEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishing.lean, line 201. The attribute's comment: “item (1) of the lemma, A → B weakly étale — Module.Flat A B together with flatness of the multiplication map B ⊗_A B → B, which is Mathlib's Algebra.WeaklyEtale. ONE carried hypothesis: the distinguished triangle of Proposition 08QX for the tower B → B ⊗_A B → B, carried as hT exactly as in CommAlgCat.isZero_cotangentComplexDerived_of_torIndependent (Stacks 08R1), because Stacks 08QX is not formalized in this library and the triangle of Tag 08SD assumes an injective map whereas the multiplication is surjective. Weak étaleness is NOT dead: Module.Flat A B supplies the Tor-independence hypothesis of Stacks 08R1, and flatness of the multiplication map supplies the vanishing of L_{B/(B ⊗_A B)} through item (2)”.

[Stacks, Tag 08R2] item (1). Let A → B be weakly étale, that is, let A → B and the multiplication map B ⊗_A B → B both be flat. Then L_{B/A} = 0 in D(B).

The multiplication map is surjective, so item (2) applies to it and gives L_{B/(B ⊗_A B)} = 0; flatness of A → B gives Tor^A_i(B, B) = 0 for i > 0; and [Stacks, Tag 08R1] concludes. The distinguished triangle of Proposition 08QX for the tower B → B ⊗_A B → B is the carried hypothesis hT of CommAlgCat.isZero_cotangentComplexDerived_of_torIndependent and is passed through.

theorem isZero_cotangentComplexDerived_of_weaklyEtale [Algebra.WeaklyEtale A B]
    {α : fundamentalVertex₁.{u, u} B (B ⊗[A] B) B ⟶ fundamentalVertex₂.{u, u} B B}
    {β : fundamentalVertex₂.{u, u} B B ⟶ fundamentalVertex₃.{u, u} (B ⊗[A] B) B}
    {γ : fundamentalVertex₃.{u, u} (B ⊗[A] B) B ⟶
      (fundamentalVertex₁.{u, u} B (B ⊗[A] B) B)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{u} B))) :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishing.lean, line 221. The attribute's comment: “item (5) of the lemma, A → B étale, obtained as the instance of item (1) along Mathlib's instance Algebra.Etale → Algebra.WeaklyEtale. The SAME one carried hypothesis hT: the distinguished triangle of Proposition 08QX for the tower B → B ⊗_A B → B. Étaleness is load-bearing, being the only source of the two flatness facts item (1) consumes”.

[Stacks, Tag 08R2] item (5). If A → B is étale then L_{B/A} = 0 in D(B).

An étale algebra is weakly étale, so this is the instance of item (1). The distinguished triangle of Proposition 08QX for the tower B → B ⊗_A B → B is carried as hT, as there.

theorem isZero_cotangentComplexDerived_of_etale [Algebra.Etale A B]
    {α : fundamentalVertex₁.{u, u} B (B ⊗[A] B) B ⟶ fundamentalVertex₂.{u, u} B B}
    {β : fundamentalVertex₂.{u, u} B B ⟶ fundamentalVertex₃.{u, u} (B ⊗[A] B) B}
    {γ : fundamentalVertex₃.{u, u} (B ⊗[A] B) B ⟶
      (fundamentalVertex₁.{u, u} B (B ⊗[A] B) B)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{u} B))) :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishingFurtherCases.lean, line 99. The attribute's comment: “item (3) of the lemma, B = S⁻¹A for a multiplicative subset S ⊂ A, read as IsLocalization S B. NOTHING is carried: the source derives it from item (2), and so does this proof, through CommAlgCat.isZero_cotangentComplexDerived_localization, a localization being flat and an epimorphism. The localization hypothesis is load-bearing, being the only source of both”.

[Stacks, Tag 08R2] item (3). Let S ⊂ A be a multiplicative subset and let B = S⁻¹A. Then L_{B/A} = 0 in D(B).

A localization is flat and an epimorphism, so this is item (2), CommAlgCat.isZero_cotangentComplexDerived_of_flat_of_bijective, through CommAlgCat.isZero_cotangentComplexDerived_localization.

theorem isZero_cotangentComplexDerived_of_isLocalization (S : Submonoid A) [IsLocalization S B] :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_unramified_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishingFurtherCases.lean, line 116. The attribute's comment: “item (4) of the lemma, A → B unramified and flat: Algebra.Unramified A B (formally unramified and of finite type, which is Stacks 00UT by Stacks 00UU) together with Module.Flat A B. NOTHING is carried: the source derives it from item (1), and so does this proof — flatness and unramifiedness make the multiplication B ⊗_A B → B a localization at an idempotent, hence flat (Algebra.WeaklyEtale.of_formallyUnramified_of_flat), and item (1) is CommAlgCat.isZero_cotangentComplexDerived_of_weaklyEtale_unconditional, whose triangle is Proposition 08QX. Both hypotheses are load-bearing”.

[Stacks, Tag 08R2] item (4). Let A → B be unramified and flat. Then L_{B/A} = 0 in D(B).

Unramified is Mathlib's Algebra.Unramified, formally unramified and of finite type, which is the source's definition (Stacks 00UT, through 00UU). A flat unramified algebra is weakly étale, Algebra.WeaklyEtale.of_formallyUnramified_of_flat, so this is item (1).

theorem isZero_cotangentComplexDerived_of_unramified_of_flat [Algebra.Unramified A B]
    [Module.Flat A B] :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_isHenselization_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishingFurtherCases.lean, line 140. The attribute's comment: “items (7) and (8) of the lemma, at once, for an ARBITRARY ring A: B a henselization (L = κ(𝔭), item (7)) or a strict henselization (L = κ(𝔭)^sep, item (8)) of the local ring A_𝔭 = Localization.AtPrime 𝔭 of A, read as IsLocalRing.IsHenselization (Stacks 04GQ) with the A-algebra structure on B the composite A → A_𝔭 → B. NOTHING is carried: the triangle of A → A_𝔭 → B is Proposition 08QX, CommAlgCat.exists_distTriang_fundamentalVertex; its first vertex vanishes by item (3) and its third by IsLocalRing.IsHenselization.isZero_cotangentComplexDerived_unconditional, which is the source's route through items (5) and (6) over the local ring”.

[Stacks, Tag 08R2] items (7) and (8). Let A be a ring, 𝔭 ⊂ A a prime, and let A_𝔭 → B be a henselization of the local ring A_𝔭 of A with residue field a prescribed extension κ(𝔭) ⊆ L. Then L_{B/A} = 0 in D(B).

At L = κ(𝔭) this is item (7), a henselization of a local ring of A, and at L = κ(𝔭)^sep it is item (8), a strict henselization. The fundamental triangle of A → A_𝔭 → B (Proposition 08QX) has first vertex L_{A_𝔭/A} ⊗^𝐋 B = 0 by item (3) and third vertex L_{B/A_𝔭} = 0 by the local case IsLocalRing.IsHenselization.isZero_cotangentComplexDerived_unconditional, so its middle vertex L_{B/A} vanishes.

theorem isZero_cotangentComplexDerived_of_isHenselization_atPrime (p : Ideal A) [p.IsPrime]
    (L : Type v) [Field L] [Algebra (IsLocalRing.ResidueField (Localization.AtPrime p)) L]
    [IsLocalRing B] [Algebra (Localization.AtPrime p) B]
    [IsScalarTower A (Localization.AtPrime p) B]
    [IsLocalRing.IsHenselization (Localization.AtPrime p) L B] :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_weaklyEtale_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishingUnconditional.lean, line 94. The attribute's comment: “item (1) of the lemma, A → B weakly étale — Module.Flat A B together with flatness of the multiplication map B ⊗_A B → B, which is Mathlib's Algebra.WeaklyEtale. NOTHING is carried: the distinguished triangle of the tower B → B ⊗_A B → B is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished. Weak étaleness is NOT dead: Module.Flat A B supplies the Tor-independence hypothesis of Stacks 08R1, and flatness of the multiplication map supplies the vanishing of L_{B/(B ⊗_A B)} through item (2)”.

[Stacks, Tag 08R2] item (1). Let A → B be weakly étale: A → B flat and the multiplication map B ⊗_A B → B flat. Then L_{B/A} = 0 in D(B).

This is CommAlgCat.isZero_cotangentComplexDerived_of_weaklyEtale at the distinguished triangle of the tower B → B ⊗_A B → B that Proposition 08QX provides.

theorem isZero_cotangentComplexDerived_of_weaklyEtale_unconditional [Algebra.WeaklyEtale A B] :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.isZero_cotangentComplexDerived_of_etale_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/EtaleVanishingUnconditional.lean, line 106. The attribute's comment: “item (5) of the lemma, A → B étale, obtained as the instance of item (1) along Mathlib's instance Algebra.Etale → Algebra.WeaklyEtale. NOTHING is carried, as in item (1). Étaleness is load-bearing, being the only source of the two flatness facts item (1) consumes”.

[Stacks, Tag 08R2] item (5). If A → B is étale then L_{B/A} = 0 in D(B).

An étale algebra is weakly étale, so this is the instance of item (1).

theorem isZero_cotangentComplexDerived_of_etale_unconditional [Algebra.Etale A B] :
    IsZero (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B))

CommAlgCat.cotangentComplex_isZero_of_filtered_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/FilteredColimitVanishing.lean, line 180. The attribute's comment: “filtered colimit”.

Stacks Project, Tag 08R2, filtered colimits. If every map of a filtered system of ring maps has vanishing relative cotangent complex, so has the map induced on the colimits.

theorem cotangentComplex_isZero_of_filtered_colimit
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (A B : J ⥤ CommRingCat.{u}) (f : A ⟶ B)
    (h : ∀ i : J,
      letI : Algebra (A.obj i) (B.obj i) := (f.app i).hom.toAlgebra
      IsZero (DerivedCategory.Q.obj
        (cotangentComplex (A.obj i) (CommAlgCat.of (A.obj i) (B.obj i))))) :
    letI : Algebra (colimit A : CommRingCat.{u}) (colimit B : CommRingCat.{u}) :=
      (colim.map f).hom.toAlgebra
    IsZero (DerivedCategory.Q.obj
      (cotangentComplex (colimit A : CommRingCat.{u})
        (CommAlgCat.of (colimit A : CommRingCat.{u})
          (colimit B : CommRingCat.{u}))))

IsLocalRing.IsHenselization.isZero_cotangentComplexDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Henselization.lean, line 283. The attribute's comment: “items (7) and (8) of the lemma, at once: L_{R^h/R} = 0 and L_{R^{sh}/R} = 0 for R → Rh a henselization of the local ring R with residue field the prescribed extension κ ⊆ L (IsLocalRing.IsHenselization, Stacks 04GQ), item (7) being the case L = κ and item (8) the case L = κ^sep. ONE carried hypothesis, hQX: the distinguished triangle of Proposition 08QX for the diagonal tower P → P ⊗_R P → P of EVERY étale R-algebra P, which is the hypothesis hT of item (5) (CommAlgCat.isZero_cotangentComplexDerived_of_etale) quantified over the étale stages, since the index category of the colimit presentation is produced inside the proof. Proposition 08QX is not formalized in this library. The source's own route is followed: items (5) and (6), the latter being CommAlgCat.cotangentComplex_isZero_of_filtered_colimit. The henselization hypothesis is load-bearing through IsLocalRing.IsHenselization.ind_etale, which supplies the presentation of Rh as a filtered colimit of étale R-algebras”.

[Stacks, Tag 08R2] items (7) and (8). Let (R, 𝔪, κ) be a local ring and let R → Rh be a henselization of R with residue field a prescribed extension κ ⊆ L of its residue field. Then L_{Rh/R} = 0 in D(Rh).

At L = κ this is item (7), the henselization R → R^h, and at L = κ^sep a separable algebraic closure it is item (8), a strict henselization R → R^{sh}; the two are the two instances of IsLocalRing.IsHenselization, so one statement covers both.

The henselization hypothesis enters through IsLocalRing.IsHenselization.ind_etale: a henselization is a filtered colimit of étale R-algebras, and CommAlgCat.isZero_cotangentComplexDerived_of_ind_etale concludes.

theorem isZero_cotangentComplexDerived {R : Type u} [CommRing R] [IsLocalRing R] (L : Type v)
    [Field L] [Algebra (ResidueField R) L] {Rh : Type u} [CommRing Rh] [IsLocalRing Rh]
    [Algebra R Rh] [IsHenselization R L Rh] (hQX : HasEtaleDiagonalTriangle.{u} R) :
    IsZero (cotangentComplexDerived.{u, u} R (CommAlgCat.of R Rh))

IsLocalRing.IsHenselization.isZero_cotangentComplexDerived_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/HenselizationUnconditional.lean, line 84. The attribute's comment: “items (7) and (8) of the lemma, at once: L_{R^h/R} = 0 and L_{R^{sh}/R} = 0 for R → Rh a henselization of the local ring R with residue field the prescribed extension κ ⊆ L (IsLocalRing.IsHenselization, Stacks 04GQ), item (7) being the case L = κ and item (8) the case L = κ^sep. NOTHING is carried: item (5) needs the distinguished triangle of the diagonal tower P → P ⊗_R P → P of every étale stage, and that is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished, through CommAlgCat.hasEtaleDiagonalTriangle, so it applies at every étale stage of the colimit presentation even though the index category is produced inside the proof. The source's own route is followed: items (5) and (6), the latter being CommAlgCat.cotangentComplex_isZero_of_filtered_colimit. The henselization hypothesis is load-bearing through IsLocalRing.IsHenselization.ind_etale, which supplies the presentation of Rh as a filtered colimit of étale R-algebras”.

[Stacks, Tag 08R2] items (7) and (8). Let (R, 𝔪, κ) be a local ring and let R → Rh be a henselization of R with residue field a prescribed extension κ ⊆ L of its residue field. Then L_{Rh/R} = 0 in D(Rh).

At L = κ this is item (7), the henselization R → R^h, and at L = κ^sep a separable algebraic closure it is item (8), a strict henselization R → R^{sh}. This is IsLocalRing.IsHenselization.isZero_cotangentComplexDerived with its family of diagonal triangles supplied by CommAlgCat.hasEtaleDiagonalTriangle.

theorem isZero_cotangentComplexDerived_unconditional {R : Type u} [CommRing R] [IsLocalRing R]
    (L : Type v) [Field L] [Algebra (ResidueField R) L] {Rh : Type u} [CommRing Rh]
    [IsLocalRing Rh] [Algebra R Rh] [IsHenselization R L Rh] :
    IsZero (cotangentComplexDerived.{u, u} R (CommAlgCat.of R Rh))

Tag 08R3, a lemma

Tag 08R3 in the Stacks Project.

CommAlgCat.isIso_fundamentalMor₁_of_isZero_fundamentalVertex₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/ProductDescent.lean, line 390. The attribute's comment: “the lemma for arbitrary ring maps A → B → C. The source's hypothesis L_{C/B} = 0 is the vanishing of CommAlgCat.fundamentalVertex₃, which IS L_{C/B} as an object of D(C), and the conclusion is that the display's own first morphism CommAlgCat.fundamentalMor₁ is an isomorphism, i.e. L_{C/A} = L_{B/A} ⊗^𝐋_B C. The distinguished triangle the source reads this off is CommAlgCat.productFundamentalTriangle_distinguished, Proposition 08QX”.

Stacks Project, Tag 08R3. Let A → B → C be ring maps with L_{C/B} = 0. Then the display's own first morphism L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A} is an isomorphism, so that L_{C/A} = L_{B/A} ⊗^𝐋_B C in D(C).

The source's proof is that a distinguished triangle whose third vertex vanishes has invertible first morphism, which is CommAlgCat.isIso_of_isZero_fundamentalVertex₃; the triangle it is applied to is the display's own, CommAlgCat.productFundamentalTriangle_distinguished.

theorem isIso_fundamentalMor₁_of_isZero_fundamentalVertex₃
    (h : IsZero (fundamentalVertex₃.{u, u, u + 1} B C)) :
    IsIso (fundamentalMor₁.{u} A B C)

CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_of_isZero_fundamentalVertex₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/ProductDescent.lean, line 400. The attribute's comment: “the equality L_{C/A} = L_{B/A} ⊗^𝐋_B C of the lemma, read as an isomorphism of the display's first and second vertices in D(C), for arbitrary ring maps A → B → C”.

Stacks Project, Tag 08R3, as the identification of the source. Let A → B → C be ring maps with L_{C/B} = 0. Then L_{C/A} = L_{B/A} ⊗^𝐋_B C in D(C).

theorem nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_of_isZero_fundamentalVertex₃
    (h : IsZero (fundamentalVertex₃.{u, u, u + 1} B C)) :
    Nonempty (fundamentalVertex₁.{u, u, u + 1, u + 1} A B C ≅
      fundamentalVertex₂.{u, u, u + 1} A C)

CommAlgCat.isIso_of_isZero_fundamentalVertex₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/VanishingVertex.lean, line 96. The attribute's comment: “the lemma in the spelling of the display 92.7.0.1, with the distinguished triangle of Proposition 08QX carried as the hypothesis hT because Stacks 08QX is not formalized in this library (see the No @[stacks 08QX] section of StacksFrontier.Cotangent.Triangle.Distinguished). The source's hypothesis L_{C/B} = 0 is the vanishing of CommAlgCat.fundamentalVertex₃, which is L_{C/B} as an object of D(C), and the conclusion is that the first arrow L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A} of the given triangle is an isomorphism”.

Stacks Project, Tag 08R3.

Let A → B → C be ring maps with L_{C/B} = 0. Then the first arrow L_{B/A} ⊗^𝐋_B C ⟶ L_{C/A} of the fundamental triangle of Equation 92.7.0.1 is an isomorphism, so that L_{C/A} = L_{B/A} ⊗^𝐋_B C in D(C).

The distinguished triangle itself is the hypothesis hT, since Proposition 08QX is not formalized in this library; see the module docstring. The source's proof is the remaining step: a distinguished triangle whose third vertex vanishes has invertible first arrow.

theorem isIso_of_isZero_fundamentalVertex₃
    {α : fundamentalVertex₁.{u, v, wB, wC} A B C ⟶ fundamentalVertex₂.{u, v, wC} A C}
    {β : fundamentalVertex₂.{u, v, wC} A C ⟶ fundamentalVertex₃.{u, v, wC} B C}
    {γ : fundamentalVertex₃.{u, v, wC} B C ⟶ (fundamentalVertex₁.{u, v, wB, wC} A B C)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{max u v} C)))
    (h : IsZero (fundamentalVertex₃.{u, v, wC} B C)) : IsIso α

CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_of_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/VanishingVertex.lean, line 109. The attribute's comment: “the equality of the lemma read as an isomorphism L_{B/A} ⊗^𝐋_B C ≅ L_{C/A} in D(C), under the same carried hypothesis hT as CommAlgCat.isIso_of_isZero_fundamentalVertex₃”.

Stacks Project, Tag 08R3, as an isomorphism. Let A → B → C be ring maps with L_{C/B} = 0. Then L_{C/A} = L_{B/A} ⊗^𝐋_B C in D(C).

theorem nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_of_isZero
    {α : fundamentalVertex₁.{u, v, wB, wC} A B C ⟶ fundamentalVertex₂.{u, v, wC} A C}
    {β : fundamentalVertex₂.{u, v, wC} A C ⟶ fundamentalVertex₃.{u, v, wC} B C}
    {γ : fundamentalVertex₃.{u, v, wC} B C ⟶ (fundamentalVertex₁.{u, v, wB, wC} A B C)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{max u v} C)))
    (h : IsZero (fundamentalVertex₃.{u, v, wC} B C)) :
    Nonempty (fundamentalVertex₁.{u, v, wB, wC} A B C ≅ fundamentalVertex₂.{u, v, wC} A C)

CommAlgCat.nonempty_derivedBaseChange_iso_cotangentComplexDerived_of_isZero_obj₃, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Triangle/VanishingVertex.lean, line 145. The attribute's comment: “the lemma for an INJECTIVE map f : B ⟶ C of A-algebras, with L_{C/B} read as the third vertex of the triangle of Tag 08SD — the complex of the base-changed relative differentials, which Tag 08RX (not formalized in this library) would identify with L_{C/B}. NO triangle is carried: it is CommAlgCat.exists_distinguished_derivedBaseChange_cotangentTriangle, proved in this library. The conclusion is the source's, L_{C/A} = L_{B/A} ⊗^𝐋_B C in D(C), with the derived base change taken along f”.

Stacks Project, Tag 08R3, from the triangle of Tag 08SD.

Let f : B ⟶ C be an injective map of A-algebras and suppose the third vertex of CommAlgCat.cotangentTriangle vanishes. Then L_{C/A} = L_{B/A} ⊗^𝐋_B C in D(C), the derived base change being taken along f.

The third vertex of the triangle of Tag 08SD is the complex of the base-changed relative differentials; identifying it with L_{C/B} is the "key fact" of Tag 08SD, which rests on Tag 08RX and is not available in this library, so the source's hypothesis L_{C/B} = 0 is read as the vanishing of that vertex. Nothing else is assumed: the triangle is the one the library proves.

theorem nonempty_derivedBaseChange_iso_cotangentComplexDerived_of_isZero_obj₃
    (f : B ⟶ C) (hf : Function.Injective f.hom)
    (h : IsZero ((cotangentTriangle A f hf).obj₃)) :
    Nonempty
      ((CochainComplex.DerivedExtensionScalars.derivedExtensionScalarsGeneral
            f.hom.toRingHom).functor.obj
          (DerivedCategory.Q.obj (cotangentComplex.{u, v} A B)) ≅
        DerivedCategory.Q.obj (cotangentComplex.{u, v} A C))

Tag 08SF, a lemma

Tag 08SF in the Stacks Project.

CommAlgCat.nonempty_cotangentComplexDerivedBaseChange_iso_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Localization.lean, line 206. The attribute's comment: “granted the distinguished fundamental triangle of Proposition 08QX as the hypothesis hT, carried unchanged from Tag 08R3 CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_of_isZero, which carries it for the same reason because Stacks 08QX is not formalized in this library. Everything else is proved outright and carries nothing: L_{T⁻¹B/B} = 0 is isZero_cotangentComplexDerived_localization from Tag 08R2 item (2), and L_{T⁻¹B/A} ≅ L_{T⁻¹B/S⁻¹A} is nonempty_cotangentComplexDerived_iso_localizationBase from Tag 08QQ at the identity base change — the D(T⁻¹B)-level upgrade of the library's Tag 08QZ, which is only degreewise. The source's equality is read as an isomorphism in D(T⁻¹B) without naming the arrow, as the library's Tag 08R3 and Tag 08QQ do, no canonical arrow being available to pin. All four rings are in a single universe, which is the generality of the library's Tag 08QQ”.

[Stacks, Tag 08SF]. Let A → B be a ring map and let S ⊆ A and T ⊆ B be multiplicative subsets such that S maps into T. Then

L_{T⁻¹B/S⁻¹A} = L_{B/A} ⊗^𝐋_B T⁻¹B

in D(T⁻¹B).

The distinguished triangle of Proposition 08QX for the tower A → B → T⁻¹B is the hypothesis hT, as Proposition 08QX is not formalized in this library; it is the hypothesis that [Stacks, Tag 08R3] carries in this library. The two remaining steps are proved outright: L_{T⁻¹B/B} = 0, which is the vanishing third vertex Tag 08R3 asks for, and L_{T⁻¹B/A} = L_{T⁻¹B/S⁻¹A}.

theorem nonempty_cotangentComplexDerivedBaseChange_iso_localization
    (hST : ∀ s ∈ S, algebraMap A B s ∈ T)
    {α : fundamentalVertex₁.{u, u} A B B' ⟶ fundamentalVertex₂.{u, u} A B'}
    {β : fundamentalVertex₂.{u, u} A B' ⟶ fundamentalVertex₃.{u, u} B B'}
    {γ : fundamentalVertex₃.{u, u} B B' ⟶ (fundamentalVertex₁.{u, u} A B B')⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{u} B'))) :
    Nonempty (cotangentComplexDerivedBaseChange.{u, u} A (CommAlgCat.of A B) B' ≅
      cotangentComplexDerived.{u, u} A' (CommAlgCat.of A' B'))

CommAlgCat.nonempty_cotangentComplexDerivedBaseChange_iso_localization_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LocalizationUnconditional.lean, line 71. The attribute's comment: “the lemma in full, with NOTHING carried. The distinguished fundamental triangle of the tower A → B → T⁻¹B is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished. Everything else is proved outright too: L_{T⁻¹B/B} = 0 is isZero_cotangentComplexDerived_localization from Tag 08R2 item (2), and L_{T⁻¹B/A} ≅ L_{T⁻¹B/S⁻¹A} is nonempty_cotangentComplexDerived_iso_localizationBase from Tag 08QQ at the identity base change, at the localization square. The source's equality is read as an isomorphism in D(T⁻¹B) without naming the arrow, as Tag 08R3 and Tag 08QQ do, no canonical arrow being available to pin. All four rings are in a single universe, which is the generality of Tag 08QQ”.

[Stacks, Tag 08SF]. Let A → B be a ring map and let S ⊆ A and T ⊆ B be multiplicative subsets such that S maps into T. Then

L_{T⁻¹B/S⁻¹A} = L_{B/A} ⊗^𝐋_B T⁻¹B

in D(T⁻¹B).

This is CommAlgCat.nonempty_cotangentComplexDerivedBaseChange_iso_localization at the distinguished triangle of the tower A → B → T⁻¹B that Proposition 08QX provides.

theorem nonempty_cotangentComplexDerivedBaseChange_iso_localization_unconditional
    (hST : ∀ s ∈ S, algebraMap A B s ∈ T) :
    Nonempty (cotangentComplexDerivedBaseChange.{u, u} A (CommAlgCat.of A B) B' ≅
      cotangentComplexDerived.{u, u} A' (CommAlgCat.of A' B'))

CommAlgCat.nonempty_extendScalars_cotangentComplex_iso_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LocalizationUnconditional.lean, line 101. The attribute's comment: “the lemma in full, with NOTHING carried, reading the source's ⊗_B T⁻¹B as the DEGREEWISE extension of scalars along B → T⁻¹B — which is the tensor product the source writes, the derived reading being nonempty_cotangentComplexDerivedBaseChange_iso_localization_unconditional. The two differ only by nonempty_derivedExtensionScalars_cotangentComplex_iso, which identifies the derived base change of L_{B/A} with the degreewise one and assumes nothing of B → T⁻¹B, L_{B/A} being a complex of free B-modules vanishing in positive degrees. The source's equality is read as an isomorphism in D(T⁻¹B) without naming the arrow, as Tag 08R3 and Tag 08QQ do, no canonical arrow being available to pin. All four rings are in a single universe, which is the generality of Tag 08QQ”.

[Stacks, Tag 08SF], with the base change read degreewise. Let A → B be a ring map and let S ⊆ A and T ⊆ B be multiplicative subsets such that S maps into T. Then

L_{T⁻¹B/S⁻¹A} = L_{B/A} ⊗_B T⁻¹B

in D(T⁻¹B), where the right-hand side is the degreewise extension of scalars along B → T⁻¹B — which is the tensor product the source writes.

This is CommAlgCat.nonempty_cotangentComplexDerivedBaseChange_iso_localization_unconditional composed with the identification of the derived base change of L_{B/A} with the degreewise one, CommAlgCat.nonempty_derivedExtensionScalars_cotangentComplex_iso. That identification needs no hypothesis on B → T⁻¹B: L_{B/A} is a complex of free B-modules vanishing in positive degrees, so it already computes its own derived base change.

theorem nonempty_extendScalars_cotangentComplex_iso_localization
    (hST : ∀ s ∈ S, algebraMap A B s ∈ T) :
    Nonempty (DerivedCategory.Q.obj (cotangentComplex A' (CommAlgCat.of A' B')) ≅
      DerivedCategory.Q.obj ((CochainComplex.extendScalarsLarge.{0, u, u}
        (algebraMap B B')).obj (cotangentComplex A (CommAlgCat.of A B))))

Tag 08UN, a lemma

Tag 08UN in the Stacks Project.

CommAlgCat.nonempty_fundamentalVertex₂_iso_fundamentalVertex₃_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Henselization.lean, line 322. The attribute's comment: “the FIRST of the lemma's two equalities, L_{B^h/A^h} = L_{B^h/A}, and its resp. strict variant L_{B^{sh}/A^{sh}} = L_{B^{sh}/A} — one statement for both, because the henselization and a strict henselization are the two instances L = κ and L = κ^sep of IsLocalRing.IsHenselization (Stacks 04GQ). It is proved for an ARBITRARY A^h-algebra C in place of B^h, which is a generalization of the lemma and not a weakening of it. TWO carried hypotheses: hT, the distinguished triangle of Proposition 08QX for the tower A → A^h → C, which is not formalized in this library (see the No @[stacks 08QX] section of StacksFrontier.Cotangent.Triangle.Distinguished), and hQX, the family of instances of Proposition 08QX that items (7) and (8) of Stacks 08R2 consume. The source's input L_{A^h/A} = 0 is NOT carried: it is proved here, as IsLocalRing.IsHenselization.isZero_cotangentComplexDerived, which is what makes the henselization hypothesis on A^h load-bearing. The lemma's SECOND equality, L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h, is CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_henselization”.

[Stacks, Tag 08UN], the identification over the henselized source. Let A → A^h be a henselization of the local ring A and let C be an A^h-algebra. Then L_{C/A} = L_{C/A^h} in D(C).

This is the first equality of the lemma, at C = B^h: the fundamental triangle of the tower A → A^h → C has first vertex L_{A^h/A} ⊗^𝐋_{A^h} C, which vanishes because L_{A^h/A} = 0, so its second arrow L_{C/A} ⟶ L_{C/A^h} is an isomorphism. Both the henselization A^h and a strict henselization A^{sh} are instances of IsLocalRing.IsHenselization, so the statement covers the lemma's resp. variant as well.

theorem nonempty_fundamentalVertex₂_iso_fundamentalVertex₃_henselization [IsLocalRing A]
    (L : Type v) [Field L] [Algebra (ResidueField A) L]
    (Ah : Type u) [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah] [IsHenselization A L Ah]
    (C : Type u) [CommRing C] [Algebra A C] [Algebra Ah C] [IsScalarTower A Ah C]
    (hQX : HasEtaleDiagonalTriangle.{u} A)
    {α : fundamentalVertex₁.{u, u} A Ah C ⟶ fundamentalVertex₂.{u, u} A C}
    {β : fundamentalVertex₂.{u, u} A C ⟶ fundamentalVertex₃.{u, u} Ah C}
    {γ : fundamentalVertex₃.{u, u} Ah C ⟶ (fundamentalVertex₁.{u, u} A Ah C)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{u} C))) :
    Nonempty (fundamentalVertex₂.{u, u} A C ≅ fundamentalVertex₃.{u, u} Ah C)

CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Henselization.lean, line 356. The attribute's comment: “the SECOND of the lemma's two equalities, L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h, and its resp. strict variant L_{B^{sh}/A} = L_{B/A} ⊗^𝐋_B B^{sh} — one statement for both, the henselization and a strict henselization being the two instances L = κ and L = κ^sep of IsLocalRing.IsHenselization (Stacks 04GQ). TWO carried hypotheses: hT, the distinguished triangle of Proposition 08QX for the tower A → B → B^h, not formalized in this library, and hQX, the family of instances of Proposition 08QX that items (7) and (8) of Stacks 08R2 consume. The source's input L_{B^h/B} = 0 is NOT carried: it is proved here, as IsLocalRing.IsHenselization.isZero_cotangentComplexDerived, so the henselization hypothesis on B^h is load-bearing. The lemma's FIRST equality, L_{B^h/A^h} = L_{B^h/A}, is CommAlgCat.nonempty_fundamentalVertex₂_iso_fundamentalVertex₃_henselization. NOTE that the local ring homomorphism A → B of the source is not assumed: the conclusion holds for any ring map A → B whose target is local, which is a generalization”.

[Stacks, Tag 08UN], the derived scalar-extension identification. Let A → B be a ring map, let B → B^h be a henselization of the local ring B, and let A → B → B^h be a tower. Then L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h in D(B^h).

This is the second equality of the lemma: the fundamental triangle of the tower A → B → B^h has third vertex L_{B^h/B}, which vanishes because B → B^h is a henselization, so its first arrow is an isomorphism. As above, one statement covers the lemma's resp. variant.

theorem nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_henselization
    (B : Type u) [CommRing B] [IsLocalRing B] [Algebra A B] (L : Type v) [Field L]
    [Algebra (ResidueField B) L]
    (Bh : Type u) [CommRing Bh] [IsLocalRing Bh] [Algebra B Bh] [IsHenselization B L Bh]
    [Algebra A Bh] [IsScalarTower A B Bh] (hQX : HasEtaleDiagonalTriangle.{u} B)
    {α : fundamentalVertex₁.{u, u} A B Bh ⟶ fundamentalVertex₂.{u, u} A Bh}
    {β : fundamentalVertex₂.{u, u} A Bh ⟶ fundamentalVertex₃.{u, u} B Bh}
    {γ : fundamentalVertex₃.{u, u} B Bh ⟶ (fundamentalVertex₁.{u, u} A B Bh)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{u} Bh))) :
    Nonempty (fundamentalVertex₁.{u, u} A B Bh ≅ fundamentalVertex₂.{u, u} A Bh)

CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₃_henselization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Henselization.lean, line 389. The attribute's comment: “the lemma's full chain L_{B^h/A^h} = L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h, read as the isomorphism L_{B/A} ⊗^𝐋_B B^h ≅ L_{B^h/A^h} in D(B^h) obtained by composing the two equalities, together with its resp. strict variant — one statement for both, the henselization and a strict henselization being the instances L = κ and L = κ^sep of IsLocalRing.IsHenselization (Stacks 04GQ). The induced map A^h → B^h is taken as given data (an A^h-algebra structure on B^h with IsScalarTower A A^h B^h) rather than constructed. FOUR carried hypotheses: the two distinguished triangles hT₁ and hT₂ of Proposition 08QX, for the towers A → B → B^h and A → A^h → B^h, Proposition 08QX not being formalized in this library; and hQXA, hQXB, the families of instances of Proposition 08QX that items (7) and (8) of Stacks 08R2 consume over A and over B. The source's inputs L_{A^h/A} = 0 and L_{B^h/B} = 0 are NOT carried: both are proved, by IsLocalRing.IsHenselization.isZero_cotangentComplexDerived, so both henselization hypotheses are load-bearing”.

[Stacks, Tag 08UN], the full chain. Let A → B be a ring map of local rings, let A → A^h and B → B^h be henselizations, and let A^h → B^h be compatible with them. Then L_{B^h/A^h} = L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h in D(B^h), read as an isomorphism L_{B/A} ⊗^𝐋_B B^h ≅ L_{B^h/A^h}.

This composes the two identifications above. The resp. strict variant is the same statement at L_A = κ_A^sep and L_B = κ_B^sep.

theorem nonempty_fundamentalVertex₁_iso_fundamentalVertex₃_henselization [IsLocalRing A]
    (B : Type u) [CommRing B] [IsLocalRing B] [Algebra A B]
    (LA : Type v) [Field LA] [Algebra (ResidueField A) LA]
    (LB : Type w) [Field LB] [Algebra (ResidueField B) LB]
    (Ah : Type u) [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah] [IsHenselization A LA Ah]
    (Bh : Type u) [CommRing Bh] [IsLocalRing Bh] [Algebra B Bh] [IsHenselization B LB Bh]
    [Algebra A Bh] [IsScalarTower A B Bh] [Algebra Ah Bh] [IsScalarTower A Ah Bh]
    (hQXA : HasEtaleDiagonalTriangle.{u} A) (hQXB : HasEtaleDiagonalTriangle.{u} B)
    {α₁ : fundamentalVertex₁.{u, u} A B Bh ⟶ fundamentalVertex₂.{u, u} A Bh}
    {β₁ : fundamentalVertex₂.{u, u} A Bh ⟶ fundamentalVertex₃.{u, u} B Bh}
    {γ₁ : fundamentalVertex₃.{u, u} B Bh ⟶ (fundamentalVertex₁.{u, u} A B Bh)⟦(1 : ℤ)⟧}
    (hT₁ : Triangle.mk α₁ β₁ γ₁ ∈ distTriang (DerivedCategory (ModuleCat.{u} Bh)))
    {α₂ : fundamentalVertex₁.{u, u} A Ah Bh ⟶ fundamentalVertex₂.{u, u} A Bh}
    {β₂ : fundamentalVertex₂.{u, u} A Bh ⟶ fundamentalVertex₃.{u, u} Ah Bh}
    {γ₂ : fundamentalVertex₃.{u, u} Ah Bh ⟶ (fundamentalVertex₁.{u, u} A Ah Bh)⟦(1 : ℤ)⟧}
    (hT₂ : Triangle.mk α₂ β₂ γ₂ ∈ distTriang (DerivedCategory (ModuleCat.{u} Bh))) :
    Nonempty (fundamentalVertex₁.{u, u} A B Bh ≅ fundamentalVertex₃.{u, u} Ah Bh)

CommAlgCat.nonempty_fundamentalVertex₂_iso_fundamentalVertex₃_henselization_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/HenselizationUnconditional.lean, line 118. The attribute's comment: “the FIRST of the lemma's two equalities, L_{B^h/A^h} = L_{B^h/A}, and its resp. strict variant L_{B^{sh}/A^{sh}} = L_{B^{sh}/A} — one statement for both, because the henselization and a strict henselization are the two instances L = κ and L = κ^sep of IsLocalRing.IsHenselization (Stacks 04GQ). It is proved for an ARBITRARY A^h-algebra C in place of B^h, which is a generalization of the lemma and not a weakening of it. NOTHING is carried: the distinguished triangle of the tower A → A^h → C is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished. The source's input L_{A^h/A} = 0 is not carried either: it is proved, as IsLocalRing.IsHenselization.isZero_cotangentComplexDerived_unconditional, which is what makes the henselization hypothesis on A^h load-bearing. The lemma's SECOND equality, L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h, is CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_henselization_unconditional”.

[Stacks, Tag 08UN], the identification over the henselized source. Let A → A^h be a henselization of the local ring A and let C be an A^h-algebra. Then L_{C/A} = L_{C/A^h} in D(C).

This is CommAlgCat.nonempty_fundamentalVertex₂_iso_fundamentalVertex₃_henselization at the triangle of the tower A → A^h → C that Proposition 08QX provides.

theorem nonempty_fundamentalVertex₂_iso_fundamentalVertex₃_henselization_unconditional
    [IsLocalRing A] (L : Type v) [Field L] [Algebra (ResidueField A) L]
    (Ah : Type u) [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah] [IsHenselization A L Ah]
    (C : Type u) [CommRing C] [Algebra A C] [Algebra Ah C] [IsScalarTower A Ah C] :
    Nonempty (fundamentalVertex₂.{u, u} A C ≅ fundamentalVertex₃.{u, u} Ah C)

CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_henselization_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/HenselizationUnconditional.lean, line 146. The attribute's comment: “the SECOND of the lemma's two equalities, L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h, and its resp. strict variant L_{B^{sh}/A} = L_{B/A} ⊗^𝐋_B B^{sh} — one statement for both, the henselization and a strict henselization being the two instances L = κ and L = κ^sep of IsLocalRing.IsHenselization (Stacks 04GQ). NOTHING is carried: the distinguished triangle of the tower A → B → B^h is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished. The source's input L_{B^h/B} = 0 is not carried either: it is proved, as IsLocalRing.IsHenselization.isZero_cotangentComplexDerived_unconditional, so the henselization hypothesis on B^h is load-bearing. The lemma's FIRST equality, L_{B^h/A^h} = L_{B^h/A}, is CommAlgCat.nonempty_fundamentalVertex₂_iso_fundamentalVertex₃_henselization_unconditional. NOTE that the local ring homomorphism A → B of the source is not assumed: the conclusion holds for any ring map A → B whose target is local, which is a generalization”.

[Stacks, Tag 08UN], the derived scalar-extension identification. Let A → B be a ring map, let B → B^h be a henselization of the local ring B, and let A → B → B^h be a tower. Then L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h in D(B^h).

This is CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_henselization at the triangle of the tower A → B → B^h that Proposition 08QX provides.

theorem nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_henselization_unconditional
    (B : Type u) [CommRing B] [IsLocalRing B] [Algebra A B] (L : Type v) [Field L]
    [Algebra (ResidueField B) L]
    (Bh : Type u) [CommRing Bh] [IsLocalRing Bh] [Algebra B Bh] [IsHenselization B L Bh]
    [Algebra A Bh] [IsScalarTower A B Bh] :
    Nonempty (fundamentalVertex₁.{u, u} A B Bh ≅ fundamentalVertex₂.{u, u} A Bh)

CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₃_henselization_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/HenselizationUnconditional.lean, line 175. The attribute's comment: “the lemma's full chain L_{B^h/A^h} = L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h, read as the isomorphism L_{B/A} ⊗^𝐋_B B^h ≅ L_{B^h/A^h} in D(B^h) obtained by composing the two equalities, together with its resp. strict variant — one statement for both, the henselization and a strict henselization being the instances L = κ and L = κ^sep of IsLocalRing.IsHenselization (Stacks 04GQ). The induced map A^h → B^h is taken as given data (an A^h-algebra structure on B^h with IsScalarTower A A^h B^h) rather than constructed. NOTHING is carried: the distinguished triangles of the towers A → B → B^h and A → A^h → B^h are both Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished. The source's inputs L_{A^h/A} = 0 and L_{B^h/B} = 0 are not carried either: both are proved, by IsLocalRing.IsHenselization.isZero_cotangentComplexDerived_unconditional, so both henselization hypotheses are load-bearing”.

[Stacks, Tag 08UN], the full chain. Let A → B be a ring map of local rings, let A → A^h and B → B^h be henselizations, and let A^h → B^h be compatible with them. Then L_{B^h/A^h} = L_{B^h/A} = L_{B/A} ⊗^𝐋_B B^h in D(B^h), read as an isomorphism L_{B/A} ⊗^𝐋_B B^h ≅ L_{B^h/A^h}.

This is CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₃_henselization at the triangles of the towers A → B → B^h and A → A^h → B^h that Proposition 08QX provides.

theorem nonempty_fundamentalVertex₁_iso_fundamentalVertex₃_henselization_unconditional
    [IsLocalRing A] (B : Type u) [CommRing B] [IsLocalRing B] [Algebra A B]
    (LA : Type v) [Field LA] [Algebra (ResidueField A) LA]
    (LB : Type w) [Field LB] [Algebra (ResidueField B) LB]
    (Ah : Type u) [CommRing Ah] [IsLocalRing Ah] [Algebra A Ah] [IsHenselization A LA Ah]
    (Bh : Type u) [CommRing Bh] [IsLocalRing Bh] [Algebra B Bh] [IsHenselization B LB Bh]
    [Algebra A Bh] [IsScalarTower A B Bh] [Algebra Ah Bh] [IsScalarTower A Ah Bh] :
    Nonempty (fundamentalVertex₁.{u, u} A B Bh ≅ fundamentalVertex₃.{u, u} Ah Bh)

Sources

• Section 92.8, Tag 08QY
• AxiomMath/Stacks at 5ed82d14

LeanCommAlgCat.quasiIso_midCotangentComplexMap · CommAlgCat.isIso_Q_map_midCotangentComplexMap · CommAlgCat.midCotangentComplexDerivedIso · CommAlgCat.midBaseChangeOverDifferentialsIso · CommAlgCat.midCotangentComplexHomologyIso · CommAlgCat.isZero_cotangentComplex_of_derivedTensor_self · CommAlgCat.isZero_cotangentComplexDerived_of_torIndependent · CommAlgCat.isZero_cotangentComplexDerived_of_torIndependent_unconditional

Section92.9 Smooth ring maps#

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

Tag 08R4, the section

Tag 08R4 in the Stacks Project.

CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothRingMap.lean, line 331. The attribute's comment: “the SECTION tag \section{Smooth ring maps}; its lemma is 08R5”.

Stacks Project, Tag 08R5 for a standard smooth ring map, and the covering declaration for the section tag 08R4.

Let A → B be standard smooth. Then L_{B/A} = Ω[B⁄A][0] in D(B).

The chart A → A[x_1, …, x_n] → B with étale second map is built, not assumed: it is Mathlib's RingHom.IsStandardSmooth.exists_etale_mvPolynomial, which is the content of the source's appeal to Algebra, Lemma 00TA. The conclusion is then CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale.

One hypothesis is carried, hQX : CommAlgCat.HasFundamentalTriangles, which is Proposition 08QX — the display of Equation 92.7.0.1 is a distinguished triangle for every tower of ring maps. Proposition 08QX is not formalized in this library (see the No @[stacks 08QX] section of StacksFrontier.Cotangent.Triangle.Distinguished) and no @[stacks 08QX] attribute is claimed for it here. It is carried as the whole proposition rather than as named instances because the two towers it is needed for — A → A[x_1, …, x_n] → B and B → B ⊗_{A[x_1, …, x_n]} B → B — are built inside the proof and so cannot be referred to in the statement.

This is not the full smooth case of Lemma 08R5. Lemma 00TA is available, and gives a standard open cover of Spec(B) on which a smooth A → B is standard smooth, so this result applies to each B_g; what is missing is L_{B_g/A} = (L_{B/A})_g, which needs Lemma 08R2 item (3), and descent along the cover in D(B). See the module docstring.

theorem nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth
    [Algebra.IsStandardSmooth A B] (hQX : HasFundamentalTriangles.{u}) :
    Nonempty
      (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
        (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
          (ModuleCat.of B (KaehlerDifferential A B)))

CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothUnconditional.lean, line 122. The attribute's comment: “the SECTION tag \section{Smooth ring maps}; its lemma is 08R5”.

Stacks Project, Tag 08R5 for a standard smooth ring map, and the covering declaration for the section tag 08R4. This is CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth with Proposition 08QX supplied by CommAlgCat.hasFundamentalTriangles.

theorem nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth_unconditional
    [Algebra.IsStandardSmooth A B] :
    Nonempty
      (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
        (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
          (ModuleCat.of B (KaehlerDifferential A B)))

Tag 08R5, a lemma

Tag 08R5 in the Stacks Project.

CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothRingMap.lean, line 228. The attribute's comment: “the lemma for a ring map A → B presented by a CHART: a factorization A → P → B with P a polynomial algebra over A and P → B étale. This is the lemma from which the standard-smooth case is deduced in CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth, which carries the 08R4 tag as well; neither is the FULL SMOOTH case, the localization step of the source's proof being unavailable (it needs Lemma 08R2 item (3), which StacksFrontier.Cotangent.EtaleVanishing records as not claimed, and a Zariski-descent statement in D(B)). TWO carried hypotheses, both instances of Proposition 08QX (NOT formalized here, and no @[stacks 08QX] is claimed): hT, the fundamental triangle of A → P → B, which Lemma 08R3 consumes, and hT', the fundamental triangle of B → B ⊗_P B → B, which CommAlgCat.isZero_cotangentComplexDerived_of_etale (Lemma 08R2 item (5)) already carries and which is passed through. The conclusion is the source's, L_{B/A} = Ω_{B/A}[0], read as an isomorphism in D(B) in the same spelling as Tag 08QH”.

Stacks Project, Tag 08R5, for a ring map presented by a chart.

Let A → P → B be ring maps with P a polynomial algebra over A and P → B étale. Then L_{B/A} = Ω[B⁄A][0] in D(B).

This is the lemma the standard smooth case is deduced from in CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth, where the chart is built rather than assumed. It is kept separate because its carried hypotheses are two named instances of Proposition 08QX rather than the whole proposition, and because Algebra.IsPolynomialAlgebra allows an arbitrary type of variables, so the hypothesis here is not merely the standard smooth case.

Two hypotheses are carried, and both are instances of Proposition 08QX, which is not formalized in this library (see the No @[stacks 08QX] section of StacksFrontier.Cotangent.Triangle.Distinguished); no @[stacks 08QX] is claimed anywhere here.

• hT is the distinguished triangle of the display of Equation 92.7.0.1 for the tower A → P → B. It is what Lemma 08R3 consumes, in the form CommAlgCat.nonempty_fundamentalVertex₁_iso_fundamentalVertex₂_of_isZero, to turn L_{B/P} = 0 into L_{B/A} = L_{P/A} ⊗^𝐋_P B. Proposition 08QX would discharge it.
• hT' is the distinguished triangle of the same display for the tower B → B ⊗_P B → B. It is the hypothesis that CommAlgCat.isZero_cotangentComplexDerived_of_etale — Lemma 08R2 item (5) — already carries, on its way through Lemma 08R1, and it is passed straight through. Proposition 08QX would discharge it too.

The hypothesis hP and the instance Algebra.Etale P B are both load-bearing: hP is the input to Lemma 08QH and the source of the projectivity of Ω[P⁄A] that makes the termwise extension of scalars compute the derived one, and étaleness supplies both the vanishing of L_{B/P} through Lemma 08R2 item (5) and, through KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale, the identification of B ⊗_P Ω[P⁄A] with Ω[B⁄A].

theorem nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale
    (hP : Algebra.IsPolynomialAlgebra A P) [Algebra.Etale P B]
    {α : fundamentalVertex₁.{u, u} A P B ⟶ fundamentalVertex₂.{u, u} A B}
    {β : fundamentalVertex₂.{u, u} A B ⟶ fundamentalVertex₃.{u, u} P B}
    {γ : fundamentalVertex₃.{u, u} P B ⟶ (fundamentalVertex₁.{u, u} A P B)⟦(1 : ℤ)⟧}
    (hT : Triangle.mk α β γ ∈ distTriang (DerivedCategory (ModuleCat.{u} B)))
    {α' : fundamentalVertex₁.{u, u} B (B ⊗[P] B) B ⟶ fundamentalVertex₂.{u, u} B B}
    {β' : fundamentalVertex₂.{u, u} B B ⟶ fundamentalVertex₃.{u, u} (B ⊗[P] B) B}
    {γ' : fundamentalVertex₃.{u, u} (B ⊗[P] B) B ⟶
      (fundamentalVertex₁.{u, u} B (B ⊗[P] B) B)⟦(1 : ℤ)⟧}
    (hT' : Triangle.mk α' β' γ' ∈ distTriang (DerivedCategory (ModuleCat.{u} B))) :
    Nonempty
      (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
        (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
          (ModuleCat.of B (KaehlerDifferential A B)))

CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothRingMap.lean, line 331. The attribute's comment: “the lemma for a STANDARD SMOOTH ring map, Algebra.IsStandardSmooth A B. The chart A → A[x_1, …, x_n] → B with étale second map is BUILT, not assumed — it is Mathlib's RingHom.IsStandardSmooth.exists_etale_mvPolynomial, which is the content of the source's appeal to Algebra, Lemma 00TA — and the conclusion then comes from CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale, which carries the 08R5 tag too. This is NOT the full smooth case: Lemma 00TA gives a cover of Spec(B) on which a smooth map is standard smooth, so this applies to each B_g, but L_{B_g/A} = (L_{B/A})_g needs Lemma 08R2 item (3) (which StacksFrontier.Cotangent.EtaleVanishing records as not claimed) and descent along the cover in D(B) is absent. ONE carried hypothesis, hQX : CommAlgCat.HasFundamentalTriangles, which is Proposition 08QX itself, carried whole rather than as instances because the towers it is needed for are built inside the proof; 08QX is NOT formalized in this library and no @[stacks 08QX] is claimed here. The conclusion is the source's, L_{B/A} = Ω_{B/A}[0], read as an isomorphism in D(B) in the same spelling as Tag 08QH. As for 08R4: the section's only mathematical content is Lemma 08R5, so this declaration covers it; the definitional remark opening the section introduces weakly quasi-regular ring maps only to say what a generalization of Lemma 08R2 would look at, and the source then says For the moment we just stick to smooth ring maps, so it states no result and nothing is defined for it”.

Stacks Project, Tag 08R5 for a standard smooth ring map, and the covering declaration for the section tag 08R4.

Let A → B be standard smooth. Then L_{B/A} = Ω[B⁄A][0] in D(B).

The chart A → A[x_1, …, x_n] → B with étale second map is built, not assumed: it is Mathlib's RingHom.IsStandardSmooth.exists_etale_mvPolynomial, which is the content of the source's appeal to Algebra, Lemma 00TA. The conclusion is then CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale.

One hypothesis is carried, hQX : CommAlgCat.HasFundamentalTriangles, which is Proposition 08QX — the display of Equation 92.7.0.1 is a distinguished triangle for every tower of ring maps. Proposition 08QX is not formalized in this library (see the No @[stacks 08QX] section of StacksFrontier.Cotangent.Triangle.Distinguished) and no @[stacks 08QX] attribute is claimed for it here. It is carried as the whole proposition rather than as named instances because the two towers it is needed for — A → A[x_1, …, x_n] → B and B → B ⊗_{A[x_1, …, x_n]} B → B — are built inside the proof and so cannot be referred to in the statement.

This is not the full smooth case of Lemma 08R5. Lemma 00TA is available, and gives a standard open cover of Spec(B) on which a smooth A → B is standard smooth, so this result applies to each B_g; what is missing is L_{B_g/A} = (L_{B/A})_g, which needs Lemma 08R2 item (3), and descent along the cover in D(B). See the module docstring.

theorem nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth
    [Algebra.IsStandardSmooth A B] (hQX : HasFundamentalTriangles.{u}) :
    Nonempty
      (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
        (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
          (ModuleCat.of B (KaehlerDifferential A B)))

CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothUnconditional.lean, line 87. The attribute's comment: “the lemma for a ring map A → B presented by a CHART: a factorization A → P → B with P a polynomial algebra over A and P → B étale. NOTHING is carried: the fundamental triangles of A → P → B and of B → B ⊗_P B → B are both Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished. The conclusion is the source's, L_{B/A} = Ω_{B/A}[0], read as an isomorphism in D(B) in the same spelling as Tag 08QH; the full smooth case is CommAlgCat.cotangentComplexDerivedIsoKaehlerDifferentialOfSmoothUnconditional”.

Stacks Project, Tag 08R5, for a chart. Let A → P → B be ring maps with P a polynomial algebra over A and P → B étale. Then L_{B/A} = Ω[B⁄A][0] in D(B).

This is CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale at the fundamental triangles of the towers A → P → B and B → B ⊗_P B → B that Proposition 08QX provides.

theorem nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale_unconditional
    (hP : Algebra.IsPolynomialAlgebra A P) [Algebra.Etale P B] :
    Nonempty
      (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
        (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
          (ModuleCat.of B (KaehlerDifferential A B)))

CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothUnconditional.lean, line 122. The attribute's comment: “the lemma for a STANDARD SMOOTH ring map, Algebra.IsStandardSmooth A B. The chart A → A[x_1, …, x_n] → B with étale second map is BUILT, not assumed — it is Mathlib's RingHom.IsStandardSmooth.exists_etale_mvPolynomial, which is the content of the source's appeal to Algebra, Lemma 00TA. NOTHING is carried: the towers the fundamental triangle is needed for are built inside the proof and Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished, holds at each of them. The full smooth case is CommAlgCat.cotangentComplexDerivedIsoKaehlerDifferentialOfSmoothUnconditional. The conclusion is the source's, L_{B/A} = Ω_{B/A}[0], read as an isomorphism in D(B) in the same spelling as Tag 08QH. As for 08R4: the section's only mathematical content is Lemma 08R5, so this declaration covers it; the definitional remark opening the section introduces weakly quasi-regular ring maps only to say what a generalization of Lemma 08R2 would look at, and the source then says For the moment we just stick to smooth ring maps, so it states no result and nothing is defined for it”.

Stacks Project, Tag 08R5 for a standard smooth ring map, and the covering declaration for the section tag 08R4. This is CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth with Proposition 08QX supplied by CommAlgCat.hasFundamentalTriangles.

theorem nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth_unconditional
    [Algebra.IsStandardSmooth A B] :
    Nonempty
      (cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
        (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
          (ModuleCat.of B (KaehlerDifferential A B)))

CommAlgCat.isZero_homology_cotangentComplex_of_smooth_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothUnconditional.lean, line 142. The attribute's comment: “the vanishing: Hⁱ(L_{B/A}) = 0 for every i ≠ 0, which together with Tag 08QF in degree 0 is the lemma. NOTHING is carried: the fundamental triangle is Tag 08QX, CommAlgCat.productFundamentalTriangle_distinguished, applied at each of the towers the proof produces”.

[Stacks, Tag 08R5], the vanishing. For a smooth ring map A → B, Hⁱ(L_{B/A}) = 0 for i ≠ 0. This is CommAlgCat.isZero_homology_cotangentComplex_of_smooth with Proposition 08QX supplied by CommAlgCat.hasFundamentalTriangle.

theorem isZero_homology_cotangentComplex_of_smooth_unconditional
    (A : Type u) [CommRing A] (B : Type u) [CommRing B] [Algebra A B] [Algebra.Smooth A B]
    (i : ℤ) (hi : i ≠ 0) :
    IsZero ((cotangentComplex A (CommAlgCat.of A B)).homology i)

CommAlgCat.cotangentComplexDerivedIsoKaehlerDifferentialOfSmoothUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothUnconditional.lean, line 157. The attribute's comment: “the lemma in full and as data: the isomorphism L_{B/A} ≅ Ω[B⁄A][0] in D(B), for a SMOOTH ring map and with NOTHING carried — the fundamental triangle is Tag 08QX, CommAlgCat.productFundamentalTriangle_distinguished. Nothing beyond smoothness is assumed, and the conclusion is the source's whole equality rather than only its degree 0 part”.

[Stacks, Tag 08R5]. For a smooth ring map A → B, the identification L_{B/A} ≅ Ω[B⁄A][0] in D(B) of the cotangent complex with the module of Kähler differentials placed in cohomological degree 0. This is CommAlgCat.cotangentComplexDerivedIsoKaehlerDifferentialOfSmooth with Proposition 08QX supplied by CommAlgCat.hasFundamentalTriangle.

noncomputable def cotangentComplexDerivedIsoKaehlerDifferentialOfSmoothUnconditional
    (A : Type u) [CommRing A] (B : Type u) [CommRing B] [Algebra A B] [Algebra.Smooth A B] :
    cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
        (ModuleCat.of B (KaehlerDifferential A B))

CommAlgCat.isZero_homology_cotangentComplex_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothVanishing.lean, line 258. The attribute's comment: “the vanishing: Hⁱ(L_{B/A}) = 0 for every i ≠ 0, which together with Tag 08QF in degree 0 is the lemma. One carried hypothesis h08QX: Tag 08QX, that the fundamental triangle is distinguished, which is not formalized in this library; it is quantified over towers because the towers are produced by the proof itself and cannot be enumerated”.

[Stacks, Tag 08R5], the vanishing. For a smooth ring map A → B the cotangent complex L_{B/A} has no cohomology outside degree 0.

A smooth ring map is standard smooth on a cover of Spec B by basic opens, [Stacks, Tag 00TA], and the cohomology of L_{B/A} is a B-module whose localizations along that cover vanish.

theorem isZero_homology_cotangentComplex_of_smooth (h08QX : HasFundamentalTriangle.{u})
    (A : Type u) [CommRing A] (B : Type u) [CommRing B] [Algebra A B] [Algebra.Smooth A B]
    (i : ℤ) (hi : i ≠ 0) :
    IsZero ((cotangentComplex A (CommAlgCat.of A B)).homology i)

CommAlgCat.cotangentComplexDerivedIsoKaehlerDifferentialOfSmooth, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SmoothVanishing.lean, line 277. The attribute's comment: “the lemma in full and as data: the isomorphism L_{B/A} ≅ Ω[B⁄A][0] in D(B). One carried hypothesis h08QX: Tag 08QX, not formalized in this library. Nothing else is assumed, and the conclusion is the source's whole equality rather than only its degree 0 part”.

[Stacks, Tag 08R5]. For a smooth ring map A → B, the identification L_{B/A} ≅ Ω[B⁄A][0] in D(B) of the cotangent complex with the module of Kähler differentials placed in cohomological degree 0.

The cohomology vanishes outside degree 0 and is Ω[B⁄A] in degree 0 by [Stacks, Tag 08QF], so the t-structure on D(B) exhibits L_{B/A} as a single module in degree 0.

noncomputable def cotangentComplexDerivedIsoKaehlerDifferentialOfSmooth
    (h08QX : HasFundamentalTriangle.{u}) (A : Type u) [CommRing A] (B : Type u) [CommRing B]
    [Algebra A B] [Algebra.Smooth A B] :
    cotangentComplexDerived.{u, u} A (CommAlgCat.of A B) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj
        (ModuleCat.of B (KaehlerDifferential A B))

Sources

• Section 92.9, Tag 08R4
• AxiomMath/Stacks at 5ed82d14

LeanCommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth · CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_isStandardSmooth_unconditional · CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale · CommAlgCat.nonempty_cotangentComplexDerived_iso_kaehlerDifferential_of_etale_unconditional · CommAlgCat.isZero_homology_cotangentComplex_of_smooth_unconditional · CommAlgCat.cotangentComplexDerivedIsoKaehlerDifferentialOfSmoothUnconditional · CommAlgCat.isZero_homology_cotangentComplex_of_smooth · CommAlgCat.cotangentComplexDerivedIsoKaehlerDifferentialOfSmooth

Section92.10 Positive characteristic#

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

Tag 0G5Y, a lemma

Tag 0G5Y in the Stacks Project.

CommAlgCat.nonempty_homotopy_frobeniusEndo_squareEndo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/StandardResolutionFrobeniusHomotopy.lean, line 1236.

Stacks Project, Tag 0G5Y. Let A → B be a ring map with p = 0 in A for a prime p, and let P_• be the standard resolution of B over A. The endomorphism of P_• induced by the commutative square of Frobenius maps F_A and F_B is homotopic to the endomorphism given by Frobenius on each term P_n. The homotopy produced here runs from the termwise Frobenius to the square-induced map; the source states the relation without an orientation.

public theorem nonempty_homotopy_frobeniusEndo_squareEndo (hp : p.Prime) (A : Type u)
    [CommRing A] (B : CommAlgCat.{max u v} A) (hA : (p : A) = 0) :
    Nonempty (SimplicialObject.Homotopy
      (frobeniusEndo.{u, v} p hp A B hA) (squareEndo.{u, v} p hp A B hA))

Tag 0G5Z, a lemma

Tag 0G5Z in the Stacks Project.

CommAlgCat.nonempty_homotopy_squareCotangentComplexMap_frobeniusSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/FrobeniusNullHomotopy.lean, line 281.

Let p be a prime, let A → B be a ring map with p = 0 in A, and let F_A and F_B be the Frobenius endomorphisms. The endomorphism of the cotangent complex L_{B/A} induced by the commutative square (F_A, F_B) — the map of Section 08QL, namely the complexMap field of CommAlgCat.squareFunctoriality at CommAlgCat.frobeniusSquare — is homotopic to zero.

The target is the cotangent complex read over B along F_B: the induced map is semilinear over F_B, not B-linear. Restriction of scalars leaves the underlying complex of abelian groups and its differentials unchanged, so a null homotopy of this map is a null homotopy of the endomorphism L_{B/A} → L_{B/A}.

public theorem nonempty_homotopy_squareCotangentComplexMap_frobeniusSquare :
    Nonempty (Homotopy
      (squareCotangentComplexMap.{u, v, u} (frobeniusSquare.{u, v} p hp A B hA)) 0)

Tag 0G60, a lemma

Tag 0G60 in the Stacks Project.

CommAlgCat.isZero_cotangentComplexDerived_of_perfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PerfectVanishing.lean, line 100.

Let p be a prime number, let A → B be a ring homomorphism with p = 0 in A, and assume that A and B are perfect. Then L_{B/A} is zero in D(B).

theorem isZero_cotangentComplexDerived_of_perfect [PerfectRing A p]
    [PerfectRing (B : Type u) p] :
    IsZero (cotangentComplexDerived.{u, u} A B)

Sources

• Section 92.10, Tag 0G5X
• AxiomMath/Stacks at 5ed82d14

LeanCommAlgCat.nonempty_homotopy_frobeniusEndo_squareEndo · CommAlgCat.nonempty_homotopy_squareCotangentComplexMap_frobeniusSquare · CommAlgCat.isZero_cotangentComplexDerived_of_perfect

Section92.11 Comparison with the naive cotangent complex#

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

Tag 08R7, a remark

Tag 08R7 in the Stacks Project.

CommAlgCat.polynomialAugmentationModuleHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteAugmentationIdeal.lean, line 66. The attribute's comment: “the augmentation O → B of sheaves of O-modules”.

The augmentation 𝒪 → B̲, read as a map of sheaves of 𝒪-modules: the target is B̲ with its 𝒪-module structure obtained by restriction of scalars along the augmentation, and the map is the one sending the unit section of 𝒪 to the unit section of B̲.

def polynomialAugmentationModuleHom :
    SheafOfModules.unit (polynomialStructureRingSheaf A B) ⟶
      (SheafOfModules.restrictScalars (polynomialAugmentationRingHom A B)).obj
        (SheafOfModules.unit (polynomialConstantRingSheaf A B))

CommAlgCat.polynomialAugmentationIdeal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteAugmentationIdeal.lean, line 80. The attribute's comment: “the defining ideal J = ker(O → B)”.

The augmentation ideal 𝒥 = ker(𝒪 → B̲) on the site C_{B/A}, a sheaf of 𝒪-modules. Its inclusion 𝒥 ⊂ 𝒪 is CategoryTheory.Limits.kernel.ι.

abbrev polynomialAugmentationIdeal :
    SheafOfModules.{u + 1} (polynomialStructureRingSheaf A B)

CommAlgCat.isZero_polynomialSiteDerivedLowerShriek_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparison.lean, line 429. The attribute's comment: “Lπ_!(𝒥) = 0 for 𝒥 = ker(𝒪 → B̲), in D(A), at the site C_{B/A} of Tag 08PR itself, with Lπ_! the total left derived functor of the colimit over the site (the π_! of Tag 08PF) and the coefficients at the universe of the site's objects”.

Lπ_!(𝒥) = 0 in D(A), the first assertion of Remark 08R7, at the site C_{B/A} itself, for the augmentation ideal 𝒥 = ker(𝒪 → B̲) read as a sheaf of A-modules.

theorem isZero_polynomialSiteDerivedLowerShriek_ideal :
    IsZero ((polynomialSiteModuleDerivedLowerShriek A B (ULift.{u + 1} A)).obj
      (DerivedCategory.Q.obj ((HomologicalComplex.single _ (ComplexShape.up ℤ) 0).obj
        (polynomialSiteIdealSheaf A B))))

CommAlgCat.polynomialSiteDerivedLowerShriekCotangentIdealComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparison.lean, line 468. The attribute's comment: “Lπ_!(𝒥 → Ω) = Lπ_!(Ω) in D(A), at the site C_{B/A} of Tag 08PR itself, as the isomorphism induced by the inclusion Ω → (𝒥 → Ω) of the degree-zero term”.

Lπ_!(Ω) = Lπ_!(𝒥 → Ω) in D(A), induced by the inclusion Ω → (𝒥 → Ω).

def polynomialSiteDerivedLowerShriekCotangentIdealComplexIso :
    (polynomialSiteModuleDerivedLowerShriek A B (ULift.{u + 1} A)).obj
        (DerivedCategory.Q.obj ((HomologicalComplex.single _ (ComplexShape.up ℤ) 0).obj
          (polynomialSiteCotangentSheafOverBase A B))) ≅
      (polynomialSiteModuleDerivedLowerShriek A B (ULift.{u + 1} A)).obj
        (DerivedCategory.Q.obj (polynomialSiteIdealComplex A B))

CommAlgCat.polynomialSiteDerivedLowerShriekIdealComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparison.lean, line 487. The attribute's comment: “Lπ_!(𝒥 → Ω) = Lπ_!(Ω) = L_{B/A} in D(A), at the site C_{B/A} of Tag 08PR itself, for the two-term complex 𝒥 → Ω in degrees -1, 0, Ω = Ω_{𝒪/A} ⊗_𝒪 B̲, the identification being the inverse of the one induced by Ω → (𝒥 → Ω) followed by Tag 08PU”.

Lπ_!(𝒥 → Ω) = L_{B/A} in D(A), Remark 08R7, at the site C_{B/A} itself: the two-term complex 𝒥 → Ω of sheaves of A-modules, in degrees -1, 0, has Lπ_! the cotangent complex of Tag 08PN.

def polynomialSiteDerivedLowerShriekIdealComplexIso :
    (polynomialSiteModuleDerivedLowerShriek A B (ULift.{u + 1} A)).obj
        (DerivedCategory.Q.obj (polynomialSiteIdealComplex A B)) ≅
      cotangentComplexOverBase A B

CommAlgCat.idealComplexToCotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparison.lean, line 502. The attribute's comment: “the map (08R8): (J → Ω_{P/A} ⊗_P B) → L_{B/A} in D(A) for every object U = (P → B) of C_{B/A}, J = ker(P → B), as the canonical map of Tag 08Q6 followed by Lπ_!(𝒥 → Ω) = L_{B/A}”.

The map (08R8) of Remark 08R7: for an object U = (P → B) of C_{B/A}, with J = ker(P → B), the map (J → Ω_{P/A} ⊗_P B) ⟶ L_{B/A} in D(A). It is the canonical map K(U) ⟶ Lπ_!(K) of Tag 08Q6 for the two-term complex K = (𝒥 → Ω), followed by Lπ_!(𝒥 → Ω) = L_{B/A}; the two-term complex J → Ω_{P/A} ⊗_P B of A-modules is the value of 𝒥 → Ω at U.

def idealComplexToCotangentComplex (U : polynomialSite A B) :
    DerivedCategory.Q.obj (CochainComplex.doubleNegOneZero
        ((liftModuleFunctor A).map ((polynomialSiteIdealToCotangent A B).app (op U)))) ⟶
      cotangentComplexOverBase A B

CommAlgCat.isZero_polynomialSiteConormalHomology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparisonTruncated.lean, line 212. The attribute's comment: “H_0(C_{B/A}, 𝒥/𝒥²) = 0, read as H⁰(Lπ_!(𝒥/𝒥²)) = 0 in D(B) at the site C_{B/A} of Tag 08PR itself, for the B̲-module 𝒥/𝒥² = Tor₀^𝒪(𝒥, B̲) = 𝒥 ⊗_𝒪 B̲”.

H₀(C_{B/A}, 𝒥/𝒥²) = 0, Remark 08R7, at the site C_{B/A} itself: H⁰(Lπ_!(𝒥/𝒥²)) = 0 for 𝒥/𝒥² = 𝒥 ⊗_𝒪 B̲ = Tor₀^𝒪(𝒥, B̲).

theorem isZero_polynomialSiteConormalHomology_zero :
    IsZero ((DerivedCategory.homologyFunctor _ 0).obj
      (polynomialSiteDerivedLowerShriekConormal A B))

CommAlgCat.isZero_polynomialSiteConormalHomology_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparisonTruncated.lean, line 222. The attribute's comment: “H_1(C_{B/A}, 𝒥/𝒥²) = 0, read as H⁻¹(Lπ_!(𝒥/𝒥²)) = 0 in D(B) at the site C_{B/A} of Tag 08PR itself, for the B̲-module 𝒥/𝒥² = Tor₀^𝒪(𝒥, B̲) = 𝒥 ⊗_𝒪 B̲”.

H₁(C_{B/A}, 𝒥/𝒥²) = 0, Remark 08R7, at the site C_{B/A} itself: H⁻¹(Lπ_!(𝒥/𝒥²)) = 0 for 𝒥/𝒥² = 𝒥 ⊗_𝒪 B̲ = Tor₀^𝒪(𝒥, B̲).

theorem isZero_polynomialSiteConormalHomology_one :
    IsZero ((DerivedCategory.homologyFunctor _ (-1)).obj
      (polynomialSiteDerivedLowerShriekConormal A B))

CommAlgCat.polynomialSiteTruncGEConormalComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparisonTruncated.lean, line 284. The attribute's comment: “τ_{≥-1} Lπ_!(𝒥/𝒥² → Ω) = τ_{≥-1} L_{B/A} in D(B), at the site C_{B/A} of Tag 08PR itself, for the two-term complex 𝒥/𝒥² → Ω of B̲-modules in degrees -1, 0, 𝒥/𝒥² = Tor₀^𝒪(𝒥, B̲) = 𝒥 ⊗_𝒪 B̲, the identification being induced by Ω → (𝒥/𝒥² → Ω) and Tag 08PU”.

τ_{≥ -1} Lπ_!(𝒥/𝒥² → Ω) = τ_{≥ -1} L_{B/A} in D(B), Remark 08R7, at the site C_{B/A} itself, for the two-term complex 𝒥/𝒥² → Ω in degrees -1, 0.

def polynomialSiteTruncGEConormalComplexIso :
    (DerivedCategory.TStructure.t.truncGE (-1)).obj
        ((polynomialSiteModuleDerivedLowerShriek A B (ULift.{u + 1} (B : Type u))).obj
          (DerivedCategory.Q.obj (polynomialSiteConormalComplex A B))) ≅
      (DerivedCategory.TStructure.t.truncGE (-1)).obj (cotangentComplexLift A B)

CommAlgCat.conormalComplexToTruncGECotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialAlgebraSiteNaiveComparisonTruncated.lean, line 310. The attribute's comment: “the map (08R9): (J/J² → Ω_{P/A} ⊗_P B) → τ_{≥-1} L_{B/A} in D(B) for every object U = (P → B) of C_{B/A}, the degree -1 term being the sections B ⊗_P J of 𝒥/𝒥² = 𝒥 ⊗_𝒪 B̲, which are J/J² for surjective P → B, as the canonical map of Tag 08Q6 followed by τ_{≥-1} Lπ_!(𝒥/𝒥² → Ω) = τ_{≥-1} L_{B/A}”.

The map (08R9) of Remark 08R7: for an object U = (P → B) of C_{B/A}, with J = ker(P → B), the map (J/J² → Ω_{P/A} ⊗_P B) ⟶ τ_{≥ -1} L_{B/A} in D(B). Its domain is the value at U of the two-term complex 𝒥/𝒥² → Ω, whose degree -1 term is B ⊗_P J, which is J/J² whenever P → B is surjective (Algebra.Extension.tensorKerEquivCotangent). The map is the canonical map K(U) ⟶ Lπ_!(K) of Tag 08Q6 for K = (𝒥/𝒥² → Ω), followed by the truncation and by τ_{≥ -1} Lπ_!(𝒥/𝒥² → Ω) = τ_{≥ -1} L_{B/A}.

def conormalComplexToTruncGECotangentComplex (U : polynomialSite A B) :
    DerivedCategory.Q.obj (CochainComplex.doubleNegOneZero
        ((liftModuleFunctor (B : Type u)).map
          ((polynomialSiteConormalToCotangent A B).app (op U)))) ⟶
      (DerivedCategory.TStructure.t.truncGE (-1)).obj (cotangentComplexLift A B)

Tag 08R9, an equation

Tag 08R9 in the Stacks Project.

Algebra.Extension.naiveComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparison.lean, line 142. The attribute's comment: “the source complex (J/J² → Ω_{P/A} ⊗_P B) of the displayed map, for a presentation P → B, in cohomological degrees -1 and 0”.

Stacks Project, Tag 08R9 (the source of the displayed map).

The naive cotangent complex NL(P → B) : J/J² ⟶ Ω[P⁄A] ⊗[P] B of a presentation, in cohomological degrees -1 and 0.

public noncomputable def naiveComplex : CochainComplex (ModuleCat.{v} S) ℤ

Stacks.Cotangent.comparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonMap.lean, line 301. The attribute's comment: “the displayed map (J/J² → Ω_{P/A} ⊗_P B) → τ_{≥ -1} L_{B/A} in D(B), at an object (P → B) of C_{B/A}, with the source the two-term complex Algebra.Extension.naiveComplex of that object and the target the degree ≥ -1 truncation of the cotangent complex of Tag 08PN”.

Stacks Project, Tag 08R9. The comparison map

(J/J² → Ω_{P/A} ⊗_P B) ⟶ τ_{≥ -1} L_{B/A}

in D(B), at an object U = (P → B) of C_{B/A} with kernel J. It is the evaluation at U of the two-term complex 𝒥/𝒥² → Ω of Remark 08R7, followed by the identification τ_{≥ -1} Lπ_!(𝒥/𝒥² → Ω) = τ_{≥ -1} L_{B/A} of that remark, both read on the standard resolution.

def comparison (E : Algebra.Extension.{max u v} A ↥B)
    (hP : Algebra.IsPolynomialAlgebra A E.Ring) :
    DerivedCategory.Q.obj (Algebra.Extension.naiveComplex E) ⟶
      (DerivedCategory.TStructure.t.truncGE (-1)).obj
        (DerivedCategory.Q.obj (cotangentComplex A B))

Tag 08RA, a lemma

Tag 08RA in the Stacks Project.

CommAlgCat.cotangentComplex_isZero_homology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Surjection.lean, line 102. The attribute's comment: “the degree-zero conclusion H⁰(L_{B/A}) = 0”.

Stacks Project, Tag 08RA. The degree-zero homology of the cotangent complex of a surjective ring map vanishes: it is the module of Kähler differentials, which is zero.

public theorem cotangentComplex_isZero_homology_zero (A : Type u) [CommRing A]
    (B : CommAlgCat.{max u v} A) (h : Function.Surjective (algebraMap A B)) :
    IsZero ((cotangentComplex A B).homology 0)

CommAlgCat.cotangentComplex_homologyNegOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Surjection.lean, line 729. The attribute's comment: “the degree-minus-one conclusion H⁻¹(L_{B/A}) = I/I², with I/I² the conormal module of the presentation A → B, the isomorphism being the connecting homomorphism of the short exact sequence 0 → I/I² → J•/J•² → Ω[P•⁄A] ⊗[P•] B → 0 of the Stacks proof”.

Stacks Project, Tag 08RA. For a surjective ring map A → B with kernel I, the degree -1 homology of the cotangent complex L_{B/A} is the conormal module I/I². The isomorphism is the connecting homomorphism of the short exact sequence 0 → I/I² → J•/J•² → Ω[P•⁄A] ⊗[P•] B → 0 of simplicial modules, which is the sequence used in the Stacks proof.

public noncomputable def cotangentComplex_homologyNegOneIso :
    (cotangentComplex A B).homology (-1) ≅
      ModuleCat.of B (surjectionExtension A B h).Cotangent

CommAlgCat.cotangentComplexHomologyNegOneIsoComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionComparisonMap.lean, line 501. The attribute's comment: “the degree-minus-one conclusion H⁻¹(L_{B/A}) = I/I², with the isomorphism the one induced by the comparison map of Tag 08R9 at the object (A → B) of C_{B/A}, which is the identification the source's statement names”.

Stacks Project, Tag 08RA. For a surjective ring map A → B with kernel I, the identification H^{-1}(L_{B/A}) ≅ I/I² induced by the comparison map of Tag 08R9 at the object (A → B) of C_{B/A} — which is the identification the source's statement names.

Read from right to left it is: the conormal module I/I² is the degree -1 cohomology of the two-term complex NL(A → B), that cohomology is carried into H^{-1}(τ_{≥ -1} L_{B/A}) by the comparison map, and τ_{≥ -1} changes no cohomology in degree -1.

def cotangentComplexHomologyNegOneIsoComparison :
    (cotangentComplex A B).homology (-1) ≅
      ModuleCat.of B (surjectionExtension A B h).Cotangent

Tag 08RB, a lemma

Tag 08RB in the Stacks Project.

CommAlgCat.cotangentComplexHomologyZeroIsoNaive, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparison.lean, line 125. The attribute's comment: “degree zero: H⁰(L_{B/A}) = H⁰(NL_{B/A})”.

Stacks 08RB, degree zero. The degree-zero cohomology of the cotangent complex L_{B/A} agrees with the degree-zero cohomology of the naive cotangent complex NL_{B/A}; both are Ω[B⁄A], by the augmentation of the standard resolution on one side and by Algebra.Extension.toKaehler on the other.

noncomputable def cotangentComplexHomologyZeroIsoNaive :
    (cotangentComplex A B).homology 0 ≅ ModuleCat.of ↥B (naiveHomologyZero A B)

Stacks.Cotangent.isIso_comparisonAtNaive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonIsIso.lean, line 166. The attribute's comment: “the canonical map c : NL_{B/A} → τ_{≥ -1} L_{B/A} of Tag 08R9, at the canonical presentation A[B] → B, is an isomorphism in D(B)”.

Stacks 08RB. For a ring map A → B, the canonical map c : NL_{B/A} → τ_{≥ -1} L_{B/A} of Tag 08R9 at the canonical presentation A[B] → B is an isomorphism in D(B): the truncation τ_{≥ -1} L_{B/A} is canonically quasi-isomorphic to the naive cotangent complex.

theorem isIso_comparisonAtNaive : IsIso (comparisonAtNaive A B)

Stacks.Cotangent.naiveComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonIsIso.lean, line 199. The attribute's comment: “the isomorphism NL_{B/A} ≅ τ_{≥ -1} L_{B/A} in D(B) whose underlying map is the canonical map c of Tag 08R9”.

Stacks 08RB. The isomorphism NL_{B/A} ≅ τ_{≥ -1} L_{B/A} in D(B), with the naive cotangent complex the two-term complex I/I² → Ω_{A[B]/A} ⊗_{A[B]} B of the canonical presentation; its underlying map is the canonical map c of Tag 08R9.

def naiveComparisonIso :
    DerivedCategory.Q.obj (Algebra.Extension.naiveComplex (conormalExtension A B (op ⦋0⦌))) ≅
      (DerivedCategory.TStructure.t.truncGE (-1)).obj
        (DerivedCategory.Q.obj (cotangentComplex A B))

Tag 08UP, a remark

Tag 08UP in the Stacks Project.

Stacks.Cotangent.explicitNaiveComparison_comp_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonAgreement.lean, line 801. The attribute's comment: “the chain map of the remark induces the comparison map of Lemma 08RB: composed with the map of Tag 08R9 at the object A[B] → B it is the truncation map L_{B/A} → τ_{≥ -1} L_{B/A} in D(B)”.

Stacks Project, Tag 08UP. The explicit chain map L_{B/A} ⟶ NL_{B/A} of the remark induces, in D(B), a map inverse to the comparison map c of Lemma 08RB: composed with c it is the truncation map L_{B/A} ⟶ τ_{≥ -1} L_{B/A}. This is the verification the source omits ("We omit the verification that this is the same as the map of Lemma 92.11.3"), with c the tagged map Stacks.Cotangent.comparison of Tag 08R9 at the object A[B] → B of C_{B/A}.

The proof reduces the equation, by the naturality of truncGEπ and the definition of Stacks.Cotangent.truncGEConeIso, to the vanishing of the difference f ≫ e - ι in D(B) after τ_{≥ -1}; see the module docstring for the route.

theorem explicitNaiveComparison_comp_comparison :
    DerivedCategory.Q.map (explicitNaiveComparison A B) ≫
        comparison A B (standardResolutionExtension A B 0)
          (isPolynomialAlgebra_standardResolutionExtension_ring A B 0) =
      (DerivedCategory.TStructure.t.truncGEπ (-1)).app
        (DerivedCategory.Q.obj (cotangentComplex A B))

Stacks.Cotangent.explicitNaiveComparison_comp_comparisonAtNaive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonAgreement.lean, line 822. The attribute's comment: “the chain map of the remark induces the comparison map of Lemma 08RB: composed with comparisonAtNaive it is the truncation map L_{B/A} → τ_{≥ -1} L_{B/A} in D(B), after the isomorphism naiveSpellingIso identifying the two spellings of NL_{B/A}”.

Stacks Project, Tag 08UP. The same equation with Stacks.Cotangent.comparisonAtNaive, the comparison map of Lemma 08RB at the spelling Stacks.Cotangent.conormalExtension A B (op ⦋0⦌) of the presentation A[B] → B: the two spellings of NL_{B/A} differ only by the section of the augmentation they carry, and Stacks.Cotangent.naiveSpellingIso is the isomorphism between them induced by the identity of A[B].

theorem explicitNaiveComparison_comp_comparisonAtNaive :
    DerivedCategory.Q.map (explicitNaiveComparison A B ≫ (naiveSpellingIso A B 0).hom) ≫
        comparisonAtNaive A B =
      (DerivedCategory.TStructure.t.truncGEπ (-1)).app
        (DerivedCategory.Q.obj (cotangentComplex A B))

CommAlgCat.comparisonComponent_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonChainMap.lean, line 315. The attribute's comment: “the comparison vanishes outside degrees 0 and -1, the bottom row being zero there”.

Stacks Project, Tag 08UP. Outside cohomological degrees 0 and -1 the comparison is zero: the bottom row of the diagram vanishes there, so every downward arrow from Ω[Pₙ⁄A] ⊗[Pₙ] B with n ≥ 2 is zero.

theorem comparisonComponent_eq_zero (i : ℤ) (h : i ≠ 0) (h' : i ≠ -1) :
    comparisonComponent A B i = 0

CommAlgCat.explicitNaiveComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonChainMap.lean, line 332. The attribute's comment: “the map of complexes L_{B/A} → NL_{B/A} itself, assembled from the two squares (the source's Hence a map of complexes): the identity in degree 0, the explicit arrow d f ⊗ b ↦ (d₀ f - d₁ f) b in degree -1, and zero in every other degree”.

Stacks Project, Tag 08UP. The map of complexes L_{B/A} ⟶ NL_{B/A} displayed by the remark: the identity in degree zero, the explicit arrow d f ⊗ b ↦ (d₀ f - d₁ f) b in degree -1, and zero above. This is the source's "Hence a map of complexes": the two commuting squares are CommAlgCat.core_lower and CommAlgCat.core_upper, and in every other pair of adjacent degrees the bottom row vanishes.

The agreement of this map with the comparison map c of Tag 08RB — the verification the source omits — is not claimed by this definition; it is Stacks.Cotangent.explicitNaiveComparison_comp_comparison of StacksFrontier/Cotangent/NaiveComparisonAgreement.lean.

noncomputable def explicitNaiveComparison :
    cotangentComplex A B ⟶
      Algebra.Extension.naiveComplex (standardResolutionExtension A B 0)

CommAlgCat.isIso_comparisonDegreeZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonChainMap.lean, line 370. The attribute's comment: “degree zero: the downward arrow is the identity, hence an isomorphism, the two rows having the same term there”.

Stacks Project, Tag 08UP. In degree zero the comparison is an isomorphism: the two rows of the diagram have the same term Ω[P₀⁄A] ⊗[P₀] B there and the downward arrow is the identity between the two presentations of it.

theorem isIso_comparisonDegreeZero : IsIso (comparisonDegreeZero A B)

CommAlgCat.naiveCotangentComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonExplicitArrow.lean, line 232. The attribute's comment: “the explicit downward arrow of the diagram, d f ⊗ b ↦ (d₀ f - d₁ f) b, with no hypothesis beyond the remark's own standard resolution of B over A; well defined by construction, as the remark's two omitted verifications are discussed in this module's implementation notes”.

Stacks Project, Tag 08UP. The downward arrow of the comparison diagram in degree one: the difference of the two faces P₁ → P₀, which lands in the kernel I of the augmentation, read as a map Ω[P₁⁄A] ⊗[P₁] B → I/I².

noncomputable def naiveCotangentComparison :
    (standardResolutionExtension A B 1).CotangentSpace →ₗ[B]
      (standardResolutionExtension A B 0).Cotangent

CommAlgCat.naiveCotangentComparison_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonExplicitArrow.lean, line 239. The attribute's comment: “the value of the arrow on a pure differential”.

The arrow sends d f ⊗ b to b times the class of d₀ f - d₁ f in I/I².

theorem naiveCotangentComparison_tmul (b : B)
    (f : (standardResolutionExtension A B 1).Ring) :
    naiveCotangentComparison A B
        (b ⊗ₜ KaehlerDifferential.D A (standardResolutionExtension A B 1).Ring f) =
      b • Algebra.Extension.Cotangent.mk
        ((standardResolutionExtensionFace A B 0 0).subToKer
          (standardResolutionExtensionFace A B 0 1) f)

CommAlgCat.naiveCotangentComparison_subToKer_coe, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonExplicitArrow.lean, line 250. The attribute's comment: “the difference of the two faces, which is the element of I the arrow uses”.

The element of I whose class the arrow takes: the difference of the two faces.

theorem naiveCotangentComparison_subToKer_coe
    (f : (standardResolutionExtension A B 1).Ring) :
    ((standardResolutionExtensionFace A B 0 0).subToKer
        (standardResolutionExtensionFace A B 0 1) f).val =
      (standardResolution A B).left.δ (0 : Fin 2) f -
        (standardResolution A B).left.δ (1 : Fin 2) f

CommAlgCat.naiveCotangentComparison_cotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonExplicitArrow.lean, line 262. The attribute's comment: “the lower square: compatibility with the differential out of degree one”.

The lower commuting square of the diagram: following the arrow by the differential I/I² → Ω[P₀⁄A] ⊗[P₀] B of the naive cotangent complex is the differential Ω[P₁⁄A] ⊗[P₁] B → Ω[P₀⁄A] ⊗[P₀] B, the difference of the two faces.

theorem naiveCotangentComparison_cotangentComplex :
    (standardResolutionExtension A B 0).cotangentComplex ∘ₗ naiveCotangentComparison A B =
      Algebra.Extension.CotangentSpace.map (standardResolutionExtensionFace A B 0 0) -
        Algebra.Extension.CotangentSpace.map (standardResolutionExtensionFace A B 0 1)

CommAlgCat.naiveCotangentComparison_faceSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/NaiveComparisonExplicitArrow.lean, line 272. The attribute's comment: “the upper square: the arrow annihilates the differential into degree one”.

The upper commuting square of the diagram: the arrow annihilates the alternating sum of the three faces P₂ → P₁, which is the differential of the cotangent complex out of degree two.

theorem naiveCotangentComparison_faceSum :
    naiveCotangentComparison A B ∘ₗ
        (Algebra.Extension.CotangentSpace.map (standardResolutionExtensionFace A B 1 0) -
          Algebra.Extension.CotangentSpace.map (standardResolutionExtensionFace A B 1 1) +
          Algebra.Extension.CotangentSpace.map (standardResolutionExtensionFace A B 1 2)) = 0

Tag 09D5, a remark

Tag 09D5 in the Stacks Project.

Stacks.Cotangent.isIso_conormalTorOneDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ConormalTorDifferential.lean, line 743. The attribute's comment: “the differential H₂(C_{B/A}, 𝒥/𝒥²) → H₀(C_{B/A}, Tor₁^𝒪(𝒥, B̲)) of the spectral sequence of Remark 08R7 is an isomorphism, read on the standard resolution”.

Stacks 09D5: the differential H₂(C_{B/A}, 𝒥/𝒥²) → H₀(C_{B/A}, Tor₁^𝒪(𝒥, B̲)) of the spectral sequence of Remark 08R7 is an isomorphism. The differential is the composite of the two connecting maps, which is d₂ of that spectral sequence (see the module docstring); each is an isomorphism because H₁ and H₂ of 𝒥, and H₀ and H₁ of 𝒥 ⊗_𝒪 𝒥, vanish.

theorem isIso_conormalTorOneDifferential : IsIso (conormalTorOneDifferential.{u, v} A B)

Stacks.Cotangent.cotangentComplexHomologyTwoLinearIsoTorOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/ConormalTorDifferentialLinear.lean, line 455. The attribute's comment: “H₂(L_{B/A}) = H₀(C_{B/A}, Tor₁^𝒪(𝒥, B̲)), an isomorphism of B-modules”.

Stacks 09D5: H₂(L_{B/A}) = H₀(C_{B/A}, Tor₁^𝒪(𝒥, B̲)), as B-modules. H₂(L_{B/A}) is the homology in cohomological degree -2 of the cotangent complex of Tag 08PN, and the right-hand side is H₀ of the Moore complex of the simplicial B-module n ↦ Tor₁^{Pₙ}(Jₙ, B) on the standard resolution. The isomorphism is H₂(L_{B/A}) ≅ H₂(C_{B/A}, 𝒥/𝒥²) followed by the differential, made B-linear by Stacks.Cotangent.isoOfRestrictScalarsIso.

def cotangentComplexHomologyTwoLinearIsoTorOne :
    (cotangentComplex A B).homology (-2) ≅ (torOneMooreComplexB.{u, v} A B).homology 0

Stacks.Cotangent.isZero_homology_kernel_conormalToCotangentMoore, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectivePresentationHigherHomology.lean, line 532. The attribute's comment: “Ker(d) has vanishing higher homology on C_{B/A}”.

Stacks 09D5, the kernel of d has no higher homology on C_{B/A}. By Tag 08PS the homology of a sheaf on C_{B/A} is the homology of the simplicial module it gives on the standard resolution, and Ker(d) is there the constant simplicial module on Algebra.H1Cotangent A B (Stacks.Cotangent.kernelConormalToCotangentMooreIso, which is the constancy of Stacks.Cotangent.outerTerms_constant combined with the exactness of Stacks.Cotangent.surjectivePresentation_exact); the Moore complex of a constant simplicial module has no homology in positive degrees.

theorem isZero_homology_kernel_conormalToCotangentMoore (n : ℕ) (hn : 0 < n) :
    IsZero ((kernel (conormalToCotangentMoore A B)).homology n)

Stacks.Cotangent.isZero_homology_cokernel_conormalToCotangentMoore, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectivePresentationHigherHomology.lean, line 542. The attribute's comment: “Coker(d) has vanishing higher homology on C_{B/A}”.

Stacks 09D5, the cokernel of d has no higher homology on C_{B/A}: on the standard resolution Coker(d) is the constant simplicial module on Ω[B⁄A] (Stacks.Cotangent.cokernelConormalToCotangentMooreIso), and the Moore complex of a constant simplicial module has no homology in positive degrees.

theorem isZero_homology_cokernel_conormalToCotangentMoore (n : ℕ) (hn : 0 < n) :
    IsZero ((cokernel (conormalToCotangentMoore A B)).homology n)

Stacks.Cotangent.isIso_homologyMap_conormalToCotangentComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectivePresentationHigherHomology.lean, line 578. The attribute's comment: “H_n(C_{B/A}, 𝒥/𝒥²) → H_n(L_{B/A}) is an isomorphism for n ≥ 2, at the cotangent complex of Tag 08PN”.

Stacks 09D5, the map H_n(C_{B/A}, 𝒥/𝒥²) → H_n(L_{B/A}) is an isomorphism for every n ≥ 2, stated at the cotangent complex CommAlgCat.cotangentComplex of Tag 08PN, whose homology in cohomological degree -n is H_n(L_{B/A}). This is Stacks.Cotangent.isIso_homologyMap_conormalToCotangentMoore transported along the reindexing, which changes no homology.

theorem isIso_homologyMap_conormalToCotangentComplex (n : ℕ) (hn : 2 ≤ n) :
    IsIso (HomologicalComplex.homologyMap (conormalToCotangentComplex A B) (-(n : ℤ)))

Stacks.Cotangent.surjectivePresentation_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectivePresentationSequence.lean, line 148. The attribute's comment: “the exact sequence 0 → H₁(L_{B/A}) → J/J² → Ω → Ω_{B/A} → 0 at an object of C'_{B/A}”.

Stacks 09D5, the exact sequence of sheaves on C'_{B/A}, read at an object: for a surjection α : P → B with P a polynomial algebra over A and J = ker α, the sequence

0 ⟶ H₁(L_{B/A}) ⟶ J/J² --d--> Ω_{P/A} ⊗_P B ⟶ Ω[B⁄A] ⟶ 0

is exact. The source writes the right-hand term as H₂(L_{B/A}), which is a slip for H₀(L_{B/A}); that term is Ω[B⁄A], and Stacks.Cotangent.cokerCotangentComplexIsoHomologyZero identifies it with the degree-zero homology of the cotangent complex of Tag 08PN.

theorem surjectivePresentation_exact (P : Algebra.Extension.{w} A B)
    (hP : Algebra.IsPolynomialAlgebra A P.Ring) :
    Function.Injective (h1CotangentIncl P) ∧
      Function.Exact (h1CotangentIncl P) P.cotangentComplex ∧
        Function.Exact P.cotangentComplex P.toKaehler ∧
          Function.Surjective P.toKaehler

Stacks.Cotangent.outerTerms_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectivePresentationSequence.lean, line 166. The attribute's comment: “Ker(d) and Coker(d) are the constant sheaves on C'_{B/A}”.

Stacks 09D5, the outer terms of the sequence are the constant sheaves on C'_{B/A}: for any morphism f : P ⟶ P' of extensions of B over A, the left-hand map H₁(L_{B/A}) ⟶ J/J² is carried to the one of P' by f, and the right-hand map Ω_{P/A} ⊗_P B ⟶ Ω[B⁄A] is the composite of f with the one of P'. Hence the identifications Ker(d) = H₁(L_{B/A}) and Coker(d) = Ω[B⁄A] of Stacks.Cotangent.surjectivePresentation_exact do not depend on the object.

theorem outerTerms_constant {P P' : Algebra.Extension.{w} A B} (f : P.Hom P') :
    Algebra.Extension.Cotangent.map f ∘ₗ h1CotangentIncl P = h1CotangentIncl P' ∧
      P'.toKaehler ∘ₗ Algebra.Extension.CotangentSpace.map f = P.toKaehler

Stacks.Cotangent.cokerCotangentComplexIsoHomologyZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectivePresentationSequence.lean, line 202. The attribute's comment: “Coker(d) = H₀(L_{B/A})”.

Stacks 09D5, the right-hand term of the sequence is H₀(L_{B/A}): at an object α : P → B of C'_{B/A} the cokernel of d : J/J² → Ω_{P/A} ⊗_P B is the degree-zero homology of the cotangent complex of Tag 08PN, by Tag 08QF.

def cokerCotangentComplexIsoHomologyZero (P : Algebra.Extension.{max u v} A B) :
    ModuleCat.of (B : Type (max u v))
        (P.CotangentSpace ⧸ LinearMap.range P.cotangentComplex) ≅
      (CommAlgCat.cotangentComplex A B).homology 0

Sources

• Section 92.11, Tag 08R6
• AxiomMath/Stacks at 5ed82d14

LeanCommAlgCat.polynomialAugmentationModuleHom · CommAlgCat.polynomialAugmentationIdeal · CommAlgCat.isZero_polynomialSiteDerivedLowerShriek_ideal · CommAlgCat.polynomialSiteDerivedLowerShriekCotangentIdealComplexIso · CommAlgCat.polynomialSiteDerivedLowerShriekIdealComplexIso · CommAlgCat.idealComplexToCotangentComplex · CommAlgCat.isZero_polynomialSiteConormalHomology_zero · CommAlgCat.isZero_polynomialSiteConormalHomology_one

Section92.12 A spectral sequence of Quillen#

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

Tag 08RD, a lemma

Tag 08RD in the Stacks Project.

Stacks.ChaoticSite.isZero_leftDerivedColim_symmetricPowerDiagram_of_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SymmetricPowerVanishing/HomologyVanishing.lean, line 717. The attribute's comment: “No hypothesis beyond the source statement: C is any small category, H_l(C, -) is L_l of the colimit over Cᵒᵖ at linear coefficients, which is Tag 08PF's definition of the homology of a category, the B-module F on the chaotic site is the diagram F, flat means that every module of sections is flat, Sym^k is the sectionwise symmetric power, U is a point resolution as in Tag 08Q9, and the induction on k over the Koszul resolution is carried out in full for every k. The Künneth input of the source proof, the Eilenberg-Zilber comparison of Tag 08QD, is replaced by the weaker vanishing statement StacksDraft.SimplicialTensor.isZero_homology_tensor_of_lt, which is proved here.”.

Let C be a small category with the chaotic topology, let B be a commutative ring and let F be a B̲-module on C — that is, a diagram F : Cᵒᵖ ⥤ ModuleCat B, every presheaf being a sheaf for the chaotic topology — which is flat, meaning that every module of sections is flat. Assume C carries a cosimplicial object U_• which is a point resolution, as in Tag 08Q9, and that H_0(C, F) = 0. Then H_l(C, Sym^k_{B̲}(F)) = 0 for every l < k.

Here H_l(C, -) = L_lπ_! is the lth left derived functor of the colimit over Cᵒᵖ, as in Tag 08PF, read at linear coefficients.

theorem isZero_leftDerivedColim_symmetricPowerDiagram_of_lt
    (C : Type u) [SmallCategory C] (B : Type u) [CommRing B]
    (U : CosimplicialObject C) (hU : IsPointResolution U)
    (F : Cᵒᵖ ⥤ ModuleCat.{u} B) (hF : ∀ X, Module.Flat B (F.obj X))
    (h₀ : IsZero (((colim : (Cᵒᵖ ⥤ ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived 0).obj F))
    (k l : ℕ) (hl : l < k) :
    IsZero (((colim : (Cᵒᵖ ⥤ ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived l).obj
      (symmetricPowerDiagram C B F k))

Tag 08SG, a remark

Tag 08SG in the Stacks Project.

Stacks.ChaoticSite.nonempty_linearEquiv_leftDerivedColim_symmetricPowerDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/ChaoticSite/SymmetricPowerDecalage.lean, line 100. The attribute's comment: “H_k(C, Sym^k_{B̲}(F)) = ∧^k_B(H_1(C, F)) over an arbitrary commutative ring B, with no invertibility hypothesis on 2: C is any small category with the chaotic topology, H_l(C, -) is L_l of the colimit over Cᵒᵖ at linear coefficients, which is Tag 08PF's definition of the homology of a category, the flat B-module F on the chaotic site is the diagram F, flat meaning that every module of sections is flat, Sym^k is the sectionwise symmetric power, and U is a point resolution as in Tag 08Q9. The remark's own route through the sign-twisted S_k-coinvariants of H_1(C, F)^{⊗ k} is a proof erratum: that intermediate step is FALSE for the coefficient ring ℤ, which is the theorem Stacks.ChaoticSite.not_quillenSignedCoinvariants_int, refuted at the polynomial site of the surjection ℤ[x] → ℤ with k = 2. The proof here is Illusie's and Quillen's décalage, run at the Moore complex of F(U_•) over the relative Koszul resolution of Sym^k by the acyclic terms ∧^p W ⊗ Sym^{k-p} D attached to the reduced décalage D and W = ker(D → F(U_•)).”.

Let C be a small category with the chaotic topology, let B be a commutative ring and let F be a flat B̲-module on C — a diagram F : Cᵒᵖ ⥤ ModuleCat B, every presheaf being a sheaf for the chaotic topology, flat meaning that every module of sections is flat — with H_0(C, F) = 0, and let U_• be a cosimplicial object of C which is a point resolution as in Tag 08Q9. Then

H_k(C, Sym^k_{B̲}(F)) ≅ ∧^k_B(H_1(C, F))

for every k, where H_l(C, -) = L_lπ_! is the lth left derived functor of the colimit over Cᵒᵖ read at linear coefficients, which is the definition of the homology of a category in Tag 08PF.

No hypothesis is placed on B: in particular 2 need not be invertible.

public theorem nonempty_linearEquiv_leftDerivedColim_symmetricPowerDiagram
    (C : Type u) [SmallCategory C] (B : Type u) [CommRing B]
    (U : CosimplicialObject C) (hU : IsPointResolution U)
    (F : Cᵒᵖ ⥤ ModuleCat.{u} B) (hF : ∀ X, Module.Flat B (F.obj X))
    (h₀ : IsZero (((colim : (Cᵒᵖ ⥤ ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived 0).obj F))
    (k : ℕ) :
    Nonempty (↥(((colim : (Cᵒᵖ ⥤ ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived k).obj
        (symmetricPowerDiagram C B F k)) ≃ₗ[B]
      ⋀[B]^k ↥(((colim : (Cᵒᵖ ⥤ ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived 1).obj F))

Tag 08RE, a lemma

Tag 08RE in the Stacks Project.

MvPolynomial.tor_map_variableIdeal_pow_succ_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/QuillenTorVanishing.lean, line 56.

Tag 08RE. Let P = A[E] be a polynomial ring and let I be the ideal generated by its variables. For any P-module on which I acts as zero -- equivalently, for any module over the coefficient ring, pulled back along the augmentation -- the inclusion I ^ (n + 1) ⊆ I ^ n induces the zero map on Tor_i^P in every degree.

theorem tor_map_variableIdeal_pow_succ_eq_zero
    (A : Type u) [CommRing A] (E : Type v) (i n : ℕ)
    (M : ModuleCat.{max u v} (MvPolynomial E A))
    (hM : ∀ r ∈ (Ideal.span (Set.range (MvPolynomial.X : E → MvPolynomial E A)) :
        Ideal (MvPolynomial E A)), ∀ m : M, r • m = 0) :
    ((Tor (ModuleCat.{max u v} (MvPolynomial E A)) i).obj M).map
        (ModuleCat.ofHom
          (Submodule.inclusion
            (Ideal.pow_le_pow_right (Nat.le_succ n) :
              (Ideal.span (Set.range (MvPolynomial.X : E → MvPolynomial E A)) ^ (n + 1) :
                  Ideal (MvPolynomial E A)) ≤
                Ideal.span (Set.range (MvPolynomial.X : E → MvPolynomial E A)) ^ n))) = 0

Tag 08RF, a theorem

Tag 08RF in the Stacks Project.

CommAlgCat.quillenSpectralSequence_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/QuillenSpectralSequenceSurjective.lean, line 136. The attribute's comment: “whole theorem, for a surjective A → B: the spectral sequence exists as a CohomologicalSpectralSequence of B-modules starting at page 1, so d_r has bidegree (r, -r + 1) by definition of that type; its first page is identified with E₁^{p,q} = H_{-p-q}(C_{B/A}, Sym^p_{B̲}(Ω)) (pageOneIso, zero for p < 0 by pageOne_isZero); it converges to Tor^A_{-p-q}(B, B) in the sense of SpectralSequence.AbutsTo: an infinity page at every bidegree and, on each Tor^A_{-n}(B, B), a finite decreasing filtration whose graded pieces are the infinity-page terms. The second conjunct is the final vanishing H_i(C_{B/A}, Sym^k_{B̲}(Ω)) = 0 for i < k. H_i(C_{B/A}, -) is L_i colim over the opposite of the small model of the polynomial site (Tag 08PF), extended by zero to i < 0; Tor^A_i(B, B) is the i-th left derived functor of B ⊗_A - at B. The sequence is that of the filtered complex C = Ō(U_•) on the standard point resolution, filtered by τ^{≤ -p}(𝒦^p(U_•)), whose cohomology is Lπ_!(Ō) = B ⊗^L_A B; every input (𝒦ⁿ/𝒦ⁿ⁺¹ = Sym^n(Ω), the footnote vanishing H_i(C_{B/A}, 𝒦ⁿ) = 0 for i < n via Tags 08RE, 068F, 08QJ, 08Q2) is proved.”.

Stacks 08RF (Quillen spectral sequence). Let A → B be a surjective ring map and Ω = Ω_{𝒪/A} ⊗_𝒪 B̲ on the polynomial site C_{B/A}. Then

• there is a cohomological spectral sequence of B-modules (E_r)_{r ≥ 1}, with d_r of bidegree (r, -r + 1), first page E₁^{p,q} ≅ H_{-p-q}(C_{B/A}, Sym^p_{B̲}(Ω)) (and 0 for p < 0), converging to Tor^A_{-p-q}(B, B): it has an infinity page at every bidegree, and each Tor^A_{-n}(B, B) carries a finite decreasing filtration with E_∞^{p, n - p} ≅ F^p/F^{p+1}; and
• H_i(C_{B/A}, Sym^k_{B̲}(Ω)) = 0 for i < k.

The first conjunct is CommAlgCat.QuillenSpectralSequenceData A B inhabited, the datum being CommAlgCat.quillenSpectralSequenceDataOfSurjective; the second is stated on the same entries CommAlgCat.symmetricPowerSiteHomology the first page is identified with.

theorem quillenSpectralSequence_of_surjective
    (h : Function.Surjective (algebraMap A (B : Type u))) :
    Nonempty (QuillenSpectralSequenceData A B) ∧
      ∀ (k : ℕ) (i : ℤ), i < k → IsZero (symmetricPowerSiteHomology A B k i)

CommAlgCat.isZero_lowerShriekZero_polynomialCotangentSheaf_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionDifferentialsVanishing.lean, line 71. The attribute's comment: “the final vanishing H_i(C_{B/A}, Symᵏ(Ω)) = 0 for i < k, in the case k = 1, where Sym¹(Ω) = Ω: for a surjective A → B the sections at the point of L₀π_!(Ω_{𝒪/A} ⊗_𝒪 B̲) vanish. As in Tag 08PU, Lπ_! is read degreewise at abelian coefficients on the small model of the footnote-restricted site. The same vanishing for every k, at linear coefficients, is CommAlgCat.isZero_leftDerivedColim_symmetricPower_polynomialCotangent_of_surjective”.

Stacks 08RF, the final vanishing in the case k = 1. For a surjective ring map A → B the zeroth homology of the sheaf of base-changed differentials on the polynomial site vanishes, because it is H⁰(L_{B/A}) = Ω[B⁄A] and Ω[B⁄A] = 0 for a surjection.

theorem isZero_lowerShriekZero_polynomialCotangentSheaf_of_surjective
    (hsurj : Function.Surjective (algebraMap A ↥B)) :
    IsZero ((Stacks.ChaoticSite.pointSections.{u, u + 1, u} AddCommGrpCat.{u}).obj
      (((Stacks.ChaoticSite.abelianPointLowerShriek
            (smallBoundedPolynomialSite A B
              (standardResolutionVarCardinal A B))).leftDerived 0).obj
        (smallPolynomialCotangentSheaf A B (standardResolutionVarCardinal A B))))

CommAlgCat.isZero_leftDerivedColim_symmetricPower_polynomialCotangent_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSymmetricPowerVanishing.lean, line 168. The attribute's comment: “the final vanishing H_i(C_{B/A}, Symᵏ_{B̲}(Ω)) = 0 for i < k, for EVERY k, where Symᵏ is the sectionwise symmetric power, which is the sheaf symmetric power because the topology of C_{B/A} is chaotic. H_i(C_{B/A}, -) is L_i of the colimit over the opposite of the small model of the footnote-restricted site at linear coefficients, which is Tag 08PF's definition of the homology of a category. The proof is the source's: Ω is a flat B̲-module because each Ω[P⁄A] is free over P, π_!(Ω) = Ω_{B/A} = 0 for a surjective A → B, and Tag 08RD turns those into the vanishing. No hypothesis beyond the source's surjectivity of A → B”.

Stacks 08RF, the final vanishing, for every k. For a surjective ring map A → B and the sheaf Ω = Ω_{𝒪/A} ⊗_𝒪 B̲ on the polynomial site C_{B/A},

H_i(C_{B/A}, Symᵏ_{B̲}(Ω)) = 0 for i < k.

The source's proof: Ω is flat and H₀(C_{B/A}, Ω) = π_!(Ω) = Ω_{B/A} = 0 because A → B is surjective, and Tag 08RD gives the vanishing from those two facts.

theorem isZero_leftDerivedColim_symmetricPower_polynomialCotangent_of_surjective
    (hsurj : Function.Surjective (algebraMap A (B : Type u))) (k l : ℕ) (hl : l < k) :
    IsZero (((colim :
          ((smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))ᵒᵖ ⥤
            ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived l).obj
      (Stacks.ChaoticSite.symmetricPowerDiagram
        (smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B)) (B : Type u)
        (smallPolynomialCotangentModulePresheaf A B (standardResolutionVarCardinal A B)) k))

Tag 08RG, a remark

Tag 08RG in the Stacks Project.

CommAlgCat.pageOneDisplay_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/QuillenSpectralSequence.lean, line 353. The attribute's comment: “the E₁-page display, for a surjective A → B with I = ker(A → B): every entry of the displayed array is identified. The array is E₁^{p,q} = H_{-p-q}(C_{B/A}, Sym^p_{B̲}(Ω)), which is Theorem 08RF's own identification of the first page, read here as the ℕ × ℤ-indexed family CommAlgCat.pageOneDisplayEntry with p along the columns and q down the rows from q = 0; H_i(C_{B/A}, -) = L_i colim over the opposite of the small model of the footnote-restricted site at linear coefficients is Tag 08PF's definition of the homology of a category, and Sym^p_{B̲} is the sectionwise symmetric power, which is the sheaf symmetric power because the topology of C_{B/A} is chaotic. The six conjuncts are the array's six regions: zero strictly below the antidiagonal p + q = 0 (negative homological degree); zero strictly above the diagonal -p - q = p, by the final clause of Theorem 08RF; B at the top of the column p = 0; zero down the rest of that column, which Theorem 08RF's vanishing does not give since it is vacuous at p = 0; H^{-i}(L_{B/A}) down the column p = 1, by Tag 08PU together with Sym¹(Ω) = Ω, which at the position (1, -2) is the I/I² of the display's third row by the remark's opening clause; and ∧^p_B(I/I²) at the diagonal position (p, -2p), by the remark's second clause. The entries strictly inside the triangle with p ≥ 2, which the display writes as H_3(C_{B/A}, Sym²(Ω)) and H_4(C_{B/A}, Sym²(Ω)), the remark leaves unidentified and so does this statement. The display's parenthetical with horizontal differential is Theorem 08RF's clause that d_r has bidegree (r, -r + 1), at r = 1, which holds by definition of the type CohomologicalSpectralSequence _ 1 carried by CommAlgCat.QuillenSpectralSequenceData.sequence. I/I² is (CommAlgCat.surjectionExtension A B h).Cotangent, the conormal module of the presentation of B by A itself, which CommAlgCat.surjectionConormalAddEquiv identifies with Ideal.Cotangent (RingHom.ker (algebraMap A B)). No hypothesis beyond the remark's own surjectivity of A → B”.

Stacks 08RG, the E₁-page display, for a surjective ring map A → B with kernel I: every entry of the displayed array

B
0
0   I/I²
0   H^{-2}(L_{B/A})
0   H^{-3}(L_{B/A})   ∧²(I/I²)
0   H^{-4}(L_{B/A})   H_3(C_{B/A}, Sym²(Ω))
0   H^{-5}(L_{B/A})   H_4(C_{B/A}, Sym²(Ω))   ∧³(I/I²)

is the module the remark displays there. The array is E₁^{p,q} = H_{-p-q}(C_{B/A}, Sym^p(Ω)) of Theorem 08RF, p along the columns and q down the rows from q = 0, so the six conjuncts below are, in order:

• the entries strictly below the antidiagonal p + q = 0 vanish — those are the positions the display leaves blank beyond the triangle, where the homological degree -p - q is negative;
• the entries strictly above the diagonal -p - q = p vanish — the blanks inside the triangle, by the final clause of Theorem 08RF;
• the top entry of the column p = 0 is B;
• the rest of the column p = 0 vanishes — together with the previous two conjuncts this is the column B, 0, 0, … the display opens with;
• the column p = 1 is H^{-i}(L_{B/A}) in homological degree i, which at i = 1, the position (1, -2), is the I/I² of the third row by the remark's opening clause;
• the diagonal entry at (p, -2p) is ∧^p_B(I/I²), by the remark's second clause.

The entries strictly inside the triangle with p ≥ 2 — H_3(C_{B/A}, Sym²(Ω)) and H_4(C_{B/A}, Sym²(Ω)) in the display — are left as they stand, exactly as the remark leaves them.

"With horizontal differential" is Theorem 08RF's own clause that d_r has bidegree (r, -r + 1), at r = 1; it holds by definition of CohomologicalSpectralSequence _ 1, which is the type of CommAlgCat.QuillenSpectralSequenceData.sequence.

theorem pageOneDisplay_of_surjective (h : Function.Surjective (algebraMap A (B : Type u))) :
    (∀ (p : ℕ) (q : ℤ), 0 < (p : ℤ) + q → IsZero (pageOneDisplayEntry A B p q)) ∧
      (∀ (p : ℕ) (q : ℤ), -(p : ℤ) - q < p → IsZero (pageOneDisplayEntry A B p q)) ∧
      Nonempty (pageOneDisplayEntry A B 0 0 ≅ ModuleCat.of (B : Type u) (B : Type u)) ∧
      (∀ q : ℤ, q < 0 → IsZero (pageOneDisplayEntry A B 0 q)) ∧
      (∀ i : ℕ, Nonempty (pageOneDisplayEntry A B 1 (-1 - (i : ℤ)) ≅
          (cotangentComplex.{u, u} A B).homology (-(i : ℤ)))) ∧
      (∀ p : ℕ, Nonempty (pageOneDisplayEntry A B p (-2 * (p : ℤ)) ≅
          ModuleCat.of (B : Type u)
            (⋀[(B : Type u)]^p (surjectionExtension.{u, u} A B h).Cotangent)))

CommAlgCat.polynomialSiteHomologyOneCotangentNegOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteConormal.lean, line 174. The attribute's comment: “the first equality of the opening clause, H^{-1}(L_{B/A}) = H_1(C_{B/A}, Ω), as the degree n = 1 case of Tag 08PU: the sections at the point of L₁π_!(Ω_{𝒪/A} ⊗_𝒪 B̲) are the degree -1 cohomology of the cotangent complex of Tag 08PN. As in Tag 08PU, Lπ_! is read degreewise at abelian coefficients, as the left derived functors of the π_! of Tag 08PF, on the small model of the footnote-restricted site, so this is an isomorphism of abelian groups; the B-module statement H^{-1}(L_{B/A}) = I/I² is Tag 08RA, CommAlgCat.cotangentComplex_homologyNegOneIso. Proved for every ring map A → B, hence in particular for the surjective one of the remark”.

Stacks 08RG, the first equality of the remark's opening clause, which is Tag 08PU in degree n = 1: the sections at the point of L₁π_!(Ω_{𝒪/A} ⊗_𝒪 B̲) are the degree -1 cohomology of the cotangent complex L_{B/A}. The remark states it for a surjective A → B; it holds for every ring map.

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

CommAlgCat.polynomialSiteHomologyOneConormalIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteConormal.lean, line 212. The attribute's comment: “the second equality of the opening clause, H_1(C_{B/A}, Ω) = I/I² for I = ker(A → B), as the composite of the first equality with Tag 08RA: for a surjective A → B the sections at the point of L₁π_!(Ω_{𝒪/A} ⊗_𝒪 B̲) are Ideal.Cotangent (RingHom.ker (algebraMap A B)), by way of H^{-1}(L_{B/A}), so the whole opening clause is covered by this declaration together with CommAlgCat.polynomialSiteHomologyOneCotangentNegOneIso. As in Tag 08PU, Lπ_! is read degreewise at abelian coefficients, so this is an isomorphism of abelian groups; the B-module statement H^{-1}(L_{B/A}) = I/I² is Tag 08RA itself. This declaration carries no hypothesis beyond the remark's own surjectivity of A → B. It states the opening clause and that clause alone; the section Where the rest of 08RG stands of this module's docstring says where each of the remark's other clauses stands”.

Stacks 08RG, the opening clause H^{-1}(L_{B/A}) = H_1(C_{B/A}, Ω) = I/I² for a surjective ring map A → B with kernel I: the sections at the point of L₁π_!(Ω_{𝒪/A} ⊗_𝒪 B̲) are the conormal module I/I². The isomorphism is the composite of CommAlgCat.polynomialSiteHomologyOneCotangentNegOneIso with Tag 08RA's CommAlgCat.cotangentComplex_homologyNegOneIso, so it factors through H^{-1}(L_{B/A}) exactly as the remark says.

def polynomialSiteHomologyOneConormalIso :
    (Stacks.ChaoticSite.pointSections.{u, u + 1, u} AddCommGrpCat.{u}).obj
        (((Stacks.ChaoticSite.abelianPointLowerShriek
              (smallBoundedPolynomialSite A B
                (standardResolutionVarCardinal A B))).leftDerived 1).obj
          (smallPolynomialCotangentSheaf A B (standardResolutionVarCardinal A B))) ≅
      AddCommGrpCat.of (RingHom.ker (algebraMap A ↥B)).Cotangent

CommAlgCat.torToCotangentEdge, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteEdgeMaps.lean, line 201. The attribute's comment: “the first family of edge maps, Tor_i^A(B, B) → H^{-i}(L_{B/A}) for every i > 0, for a surjective A → B with I = ker(A → B). These are the remark's own edge maps, read -- as the remark reads them -- off the filtration … ⊆ 𝒦² ⊆ 𝒦 ⊆ Ō of the abutment, where Ō = 𝒪 ⊗_A B̲ and 𝒦 = ker(Ō → B̲) are presheaves on C_{B/A}: the composite Tor^A_i(B,B) ≅ H_i(C_{B/A}, Ō) ≅ H_i(C_{B/A}, 𝒦) ⟶ H_i(C_{B/A}, 𝒦/𝒦²) ≅ H^{-i}(L_{B/A}). Tor^A_i(B, B) is RingTheory.TorProducts.torBaseChange, the i-th left derived functor of extension of scalars along A → B, which is the spelling in which this development identifies the abutment H_i(C_{B/A}, Ō) of Theorem 08RF; H^{-i}(L_{B/A}) is the degree -i cohomology of the cotangent complex of Tag 08PN, reached by Tag 08PU at linear coefficients; and H_i(C_{B/A}, -) = L_i colim over the opposite of the small model of the footnote-restricted site is Tag 08PF's definition of the homology of a category. No spectral sequence is involved, and no hypothesis is carried: the construction holds for every ring map A → B, hence in particular for the surjective one of the remark. The remark's SECOND family, ∧^i_B(I/I²) → Tor_i^A(B, B), is not this declaration; it needs the footnote vanishing of Theorem 08RF and is recorded separately”.

The first family of edge maps of Stacks Remark 08RG: for every i > 0 a map

Tor_i^A(B, B) ⟶ H^{-i}(L_{B/A}).

It is the remark's own map, read off the filtration … ⊆ 𝒦² ⊆ 𝒦 ⊆ Ō of the abutment: the composite

Tor^A_i(B, B) ≅ H_i(C_{B/A}, Ō) ≅ H_i(C_{B/A}, 𝒦) ⟶ H_i(C_{B/A}, 𝒦/𝒦²) ≅ H^{-i}(L_{B/A})

of CommAlgCat.torToCotangentHomologyEdge with CommAlgCat.siteHomologyGradedOneCotangentIso. The first identification is CommAlgCat.leftDerivedColimQuotientTorIso, the second CommAlgCat.leftDerivedColimAugmentationIdealIsoOfPos — available because H_j(C_{B/A}, B̲) vanishes for j > 0 — the arrow is induced by the projection onto the first graded piece, and the last identification is Ω ≅ 𝒦/𝒦² followed by Tag 08PU.

The remark states these maps for a surjective A → B; they exist for every ring map.

def torToCotangentEdge (i : ℕ) (hi : 0 < i) :
    (RingTheory.TorProducts.torBaseChange.{u, u, u} A (B : Type u) i).obj
        (ModuleCat.of A (B : Type u)) ⟶
      (cotangentComplex.{u, u} A B).homology (-(i : ℤ))

CommAlgCat.symmetricPowerToTorEdge_of_surjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteEdgeMapsUnconditional.lean, line 118. The attribute's comment: “the second family of edge maps, ∧^i_B(I/I²) → Tor_i^A(B, B) for every i > 0, for a surjective A → B with I = ker(A → B). It is the remark's own map, read -- as the remark reads it -- off the filtration … ⊆ 𝒦² ⊆ 𝒦 ⊆ Ō of the abutment, where Ō = 𝒪 ⊗_A B̲ and 𝒦 = ker(Ō → B̲) are presheaves on C_{B/A}: the composite H_i(C_{B/A}, Sym^i(Ω)) ≅ H_i(C_{B/A}, 𝒦ⁱ/𝒦ⁱ⁺¹) ≅ H_i(C_{B/A}, 𝒦ⁱ) ⟶ H_i(C_{B/A}, 𝒦) ≅ H_i(C_{B/A}, Ō) ≅ Tor_i^A(B, B), whose middle isomorphism is the diagonal identification H_i(C_{B/A}, 𝒦ⁱ) ≅ H_i(C_{B/A}, 𝒦ⁱ/𝒦ⁱ⁺¹) and whose arrow is induced by the inclusion 𝒦ⁱ ⊆ 𝒦. Tor_i^A(B, B) is RingTheory.TorProducts.torBaseChange, the i-th left derived functor of extension of scalars along A → B, in which this development identifies the abutment H_i(C_{B/A}, Ō) of Theorem 08RF; and H_i(C_{B/A}, -) = L_i colim over the opposite of the small model of the footnote-restricted site is Tag 08PF's definition of the homology of a category. The source is written ∧^i_B(I/I²) by the remark and H_i(C_{B/A}, Sym^i_{B̲}(Ω)) here; they are the same object by the remark's own second clause, which this library has unconditionally as CommAlgCat.exteriorPower_conormal_leftDerivedColim_symmetricPower_of_surjective, and that clause is the other declaration of this part's covering set. It is stated at the symmetric power because the clause produces its linear equivalence inside a Nonempty -- Remark 08SG is reached by décalage, which chooses an isomorphism rather than constructing a canonical one -- so there is no canonical map out of ∧^i_B(I/I²) to be had. The construction needs the footnote vanishing H_j(C_{B/A}, 𝒦ⁿ) = 0 for j < n of the proof of Theorem 08RF, which is a theorem here for every surjective A → B, so no hypothesis beyond the remark's own surjectivity is carried”.

The second family of edge maps of Stacks Remark 08RG, for a surjective A → B and on no other hypothesis: for every i > 0 a map

∧^i_B(I/I²) = H_i(C_{B/A}, Sym^i_{B̲}(Ω)) ⟶ Tor_i^A(B, B).

This is CommAlgCat.symmetricPowerToTorEdge with its hypothesis hvan discharged by isZero_leftDerivedColim_smallPolynomialAugmentationIdealPow_of_surjective_unconditional, the footnote vanishing of [Stacks, Tag 08RF]. The map itself is the remark's own, read off the filtration … ⊆ 𝒦² ⊆ 𝒦 ⊆ Ō of the abutment.

def symmetricPowerToTorEdge_of_surjective
    (hsurj : Function.Surjective (algebraMap A (B : Type u))) (i : ℕ) (hi : 0 < i) :
    (siteHomologyFunctor A B (standardResolutionVarCardinal A B) i).obj
        (Stacks.ChaoticSite.symmetricPowerDiagram
          (smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B)) (B : Type u)
          (smallPolynomialCotangentModulePresheaf A B
            (standardResolutionVarCardinal A B)) i) ⟶
      (RingTheory.TorProducts.torBaseChange.{u, u, u} A (B : Type u) i).obj
        (ModuleCat.of A (B : Type u))

CommAlgCat.exact_fiveTerm_cotangentNegThree_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteEdgeMapsUnconditional.lean, line 177. The attribute's comment: “the five term exact sequence of low degree terms, Tor_3^A(B, B) → H^{-3}(L_{B/A}) → ∧²_B(I/I²) → Tor_2^A(B, B) → H^{-2}(L_{B/A}) → 0, for a surjective A → B with I = ker(A → B) -- exactness at H^{-3}(L_{B/A}). The sequence is the five term segment of the long exact sequence of 0 → 𝒦² → 𝒦 → 𝒦/𝒦² → 0 on C_{B/A} read through the remark's identifications H_i(C_{B/A}, 𝒦) = Tor_i^A(B, B) for i ≥ 1, H_i(C_{B/A}, 𝒦/𝒦²) = H^{-i}(L_{B/A}) and H_2(C_{B/A}, 𝒦²) = H_2(C_{B/A}, Sym²(Ω)) = ∧²_B(I/I²), the last of these being the remark's second clause (CommAlgCat.exteriorPower_conormal_leftDerivedColim_symmetricPower_of_surjective); its first and fourth maps are the first family of edge maps, CommAlgCat.torToCotangentEdge, its third is the second family, CommAlgCat.symmetricPowerToTorEdge_of_surjective, and its second is CommAlgCat.fiveTermConnecting_of_surjective. The covering set of this part is this declaration together with CommAlgCat.exact_fiveTerm_exteriorSquare_of_surjective, CommAlgCat.exact_fiveTerm_torTwo_of_surjective and CommAlgCat.epi_fiveTerm_torToCotangentEdge_two_of_surjective, which state exactness at the other two interior terms and the final → 0. No spectral sequence is involved. The footnote vanishing H_j(C_{B/A}, 𝒦ⁿ) = 0 for j < n of the proof of Theorem 08RF, which the sequence needs, is a theorem here for every surjective A → B, so no hypothesis beyond the remark's own surjectivity is carried”.

The five term exact sequence of Stacks Remark 08RG, exactness at H^{-3}(L_{B/A}), for a surjective A → B and on no other hypothesis: the image of the edge map Tor_3^A(B, B) → H^{-3}(L_{B/A}) is the kernel of the middle map H^{-3}(L_{B/A}) → ∧²_B(I/I²).

This is CommAlgCat.exact_fiveTerm_cotangentNegThree with its hypothesis hvan discharged.

theorem exact_fiveTerm_cotangentNegThree_of_surjective
    (hsurj : Function.Surjective (algebraMap A (B : Type u))) :
    (ShortComplex.mk (torToCotangentEdge A B 3 (by norm_num))
      (fiveTermConnecting_of_surjective A B hsurj)
      (torToCotangentEdge_comp_fiveTermConnecting A B
        (isZero_leftDerivedColim_smallPolynomialAugmentationIdealPow_of_surjective_unconditional
          A B hsurj))).Exact

CommAlgCat.exact_fiveTerm_exteriorSquare_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteEdgeMapsUnconditional.lean, line 206. The attribute's comment: “the five term exact sequence of low degree terms, Tor_3^A(B, B) → H^{-3}(L_{B/A}) → ∧²_B(I/I²) → Tor_2^A(B, B) → H^{-2}(L_{B/A}) → 0, for a surjective A → B with I = ker(A → B) -- exactness at ∧²_B(I/I²), the term the remark writes ∧²_B(I/I²) and this development spells H_2(C_{B/A}, Sym²_{B̲}(Ω)), the two being the same object by the remark's second clause (CommAlgCat.exteriorPower_conormal_leftDerivedColim_symmetricPower_of_surjective). The sequence is the five term segment of the long exact sequence of 0 → 𝒦² → 𝒦 → 𝒦/𝒦² → 0 on C_{B/A} read through the remark's identifications H_i(C_{B/A}, 𝒦) = Tor_i^A(B, B) for i ≥ 1 and H_i(C_{B/A}, 𝒦/𝒦²) = H^{-i}(L_{B/A}). The covering set of this part is this declaration together with CommAlgCat.exact_fiveTerm_cotangentNegThree_of_surjective, CommAlgCat.exact_fiveTerm_torTwo_of_surjective and CommAlgCat.epi_fiveTerm_torToCotangentEdge_two_of_surjective. The footnote vanishing H_j(C_{B/A}, 𝒦ⁿ) = 0 for j < n of the proof of Theorem 08RF, which the sequence needs, is a theorem here for every surjective A → B, so no hypothesis beyond the remark's own surjectivity is carried”.

The five term exact sequence of Stacks Remark 08RG, exactness at ∧²_B(I/I²), for a surjective A → B and on no other hypothesis: the image of the middle map H^{-3}(L_{B/A}) → ∧²_B(I/I²) is the kernel of the second edge map ∧²_B(I/I²) → Tor_2^A(B, B).

This is CommAlgCat.exact_fiveTerm_exteriorSquare with its hypothesis hvan discharged.

theorem exact_fiveTerm_exteriorSquare_of_surjective
    (hsurj : Function.Surjective (algebraMap A (B : Type u))) :
    (ShortComplex.mk (fiveTermConnecting_of_surjective A B hsurj)
      (symmetricPowerToTorEdge_of_surjective A B hsurj 2 (by norm_num))
      (fiveTermConnecting_comp_symmetricPowerToTorEdge A B
        (isZero_leftDerivedColim_smallPolynomialAugmentationIdealPow_of_surjective_unconditional
          A B hsurj))).Exact

CommAlgCat.exact_fiveTerm_torTwo_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteEdgeMapsUnconditional.lean, line 237. The attribute's comment: “the five term exact sequence of low degree terms, Tor_3^A(B, B) → H^{-3}(L_{B/A}) → ∧²_B(I/I²) → Tor_2^A(B, B) → H^{-2}(L_{B/A}) → 0, for a surjective A → B with I = ker(A → B) -- exactness at Tor_2^A(B, B), which is RingTheory.TorProducts.torBaseChange in degree 2, the second left derived functor of extension of scalars along A → B applied to B, in which this development identifies the abutment H_2(C_{B/A}, Ō) of Theorem 08RF. The sequence is the five term segment of the long exact sequence of 0 → 𝒦² → 𝒦 → 𝒦/𝒦² → 0 on C_{B/A} read through the remark's identifications H_i(C_{B/A}, 𝒦) = Tor_i^A(B, B) for i ≥ 1, H_i(C_{B/A}, 𝒦/𝒦²) = H^{-i}(L_{B/A}) and H_2(C_{B/A}, 𝒦²) = ∧²_B(I/I²). The covering set of this part is this declaration together with CommAlgCat.exact_fiveTerm_cotangentNegThree_of_surjective, CommAlgCat.exact_fiveTerm_exteriorSquare_of_surjective and CommAlgCat.epi_fiveTerm_torToCotangentEdge_two_of_surjective. The footnote vanishing H_j(C_{B/A}, 𝒦ⁿ) = 0 for j < n of the proof of Theorem 08RF, which the sequence needs, is a theorem here for every surjective A → B, so no hypothesis beyond the remark's own surjectivity is carried”.

The five term exact sequence of Stacks Remark 08RG, exactness at Tor_2^A(B, B), for a surjective A → B and on no other hypothesis: the image of the second edge map ∧²_B(I/I²) → Tor_2^A(B, B) is the kernel of the first edge map Tor_2^A(B, B) → H^{-2}(L_{B/A}).

This is CommAlgCat.exact_fiveTerm_torTwo with its hypothesis hvan discharged.

theorem exact_fiveTerm_torTwo_of_surjective
    (hsurj : Function.Surjective (algebraMap A (B : Type u))) :
    (ShortComplex.mk (symmetricPowerToTorEdge_of_surjective A B hsurj 2 (by norm_num))
      (torToCotangentEdge A B 2 (by norm_num))
      (symmetricPowerToTorEdge_comp_torToCotangentEdge A B
        (isZero_leftDerivedColim_smallPolynomialAugmentationIdealPow_of_surjective_unconditional
          A B hsurj))).Exact

CommAlgCat.epi_fiveTerm_torToCotangentEdge_two_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteEdgeMapsUnconditional.lean, line 264. The attribute's comment: “the five term exact sequence of low degree terms, Tor_3^A(B, B) → H^{-3}(L_{B/A}) → ∧²_B(I/I²) → Tor_2^A(B, B) → H^{-2}(L_{B/A}) → 0, for a surjective A → B with I = ker(A → B) -- the final → 0, i.e. surjectivity of the last map Tor_2^A(B, B) → H^{-2}(L_{B/A}), which is the first family of edge maps (CommAlgCat.torToCotangentEdge) in degree 2. It holds because H_1(C_{B/A}, 𝒦²) = 0, the footnote vanishing of the proof of Theorem 08RF at j = 1 < 2 = n, which is a theorem here for every surjective A → B; so no hypothesis beyond the remark's own surjectivity is carried. The covering set of this part is this declaration together with CommAlgCat.exact_fiveTerm_cotangentNegThree_of_surjective, CommAlgCat.exact_fiveTerm_exteriorSquare_of_surjective and CommAlgCat.exact_fiveTerm_torTwo_of_surjective, which state exactness at the sequence's three interior terms”.

The five term exact sequence of Stacks Remark 08RG ends in zero, for a surjective A → B and on no other hypothesis: the first edge map Tor_2^A(B, B) → H^{-2}(L_{B/A}) is surjective.

This is CommAlgCat.epi_fiveTerm_torToCotangentEdge_two with its hypothesis hvan discharged.

theorem epi_fiveTerm_torToCotangentEdge_two_of_surjective
    (hsurj : Function.Surjective (algebraMap A (B : Type u))) :
    Epi (torToCotangentEdge A B 2 (by norm_num))

CommAlgCat.leftDerivedColimOneConormalLinearEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteExteriorConormal.lean, line 116. The attribute's comment: “the opening clause H^{-1}(L_{B/A}) = H_1(C_{B/A}, Ω) = I/I² for a surjective A → B with I = ker(A → B), as an isomorphism of B-MODULES: the first left derived functor of the colimit over the opposite of the small model of the footnote-restricted site, applied to Ω = Ω_{𝒪/A} ⊗_𝒪 B̲, is the conormal module I/I² of the presentation of B by A itself. H_1(C_{B/A}, -) = L_1 colim at linear coefficients is Tag 08PF's definition; the first equality is Tag 08PU in degree 1 and the second is Tag 08RA. I/I² is (CommAlgCat.surjectionExtension A B h).Cotangent, which CommAlgCat.surjectionConormalAddEquiv identifies with Ideal.Cotangent (RingHom.ker (algebraMap A B)). No hypothesis beyond the remark's own surjectivity of A → B”.

Stacks 08RG, the opening clause H^{-1}(L_{B/A}) = H_1(C_{B/A}, Ω) = I/I² for a surjective ring map A → B with kernel I, as an isomorphism of B-modules: the first homology of C_{B/A} with coefficients in Ω = Ω_{𝒪/A} ⊗_𝒪 B̲ is the conormal module I/I² of the presentation of B by A itself.

The first equality is Tag 08PU in degree n = 1, at linear coefficients (CommAlgCat.leftDerivedColimPolynomialCotangentIso); the second is Tag 08RA (CommAlgCat.cotangentComplex_homologyNegOneIso). The abelian-group form of the same clause is CommAlgCat.polynomialSiteHomologyOneConormalIso, which reads H_1 as the sections at the point of L₁π_!.

def leftDerivedColimOneConormalLinearEquiv :
    ↥(((colim :
            ((smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))ᵒᵖ ⥤
              ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived 1).obj
        (smallPolynomialCotangentModulePresheaf A B (standardResolutionVarCardinal A B))) ≃ₗ[B]
      (surjectionExtension.{u, u} A B h).Cotangent

CommAlgCat.exteriorPower_conormal_leftDerivedColim_symmetricPower_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SurjectionSiteExteriorConormal.lean, line 164. The attribute's comment: “the second clause H_k(C_{B/A}, Sym^k_{B̲}(Ω)) = ∧^k_B(I/I²) for a surjective A → B with I = ker(A → B), as an isomorphism of B-modules, for every k, over an arbitrary commutative ring B and with no hypothesis beyond the remark's own surjectivity of A → B; in particular 2 need not be invertible. H_k(C_{B/A}, -) = L_k colim over the opposite of the small model of the footnote-restricted site at linear coefficients is Tag 08PF's definition of the homology of a category, Sym^k_{B̲} is the sectionwise symmetric power, which is the sheaf symmetric power because the topology of C_{B/A} is chaotic, and I/I² is (CommAlgCat.surjectionExtension A B h).Cotangent, the conormal module of the presentation of B by A itself, which CommAlgCat.surjectionConormalAddEquiv identifies with Ideal.Cotangent (RingHom.ker (algebraMap A B)). The deduction is the remark's own: Remark 08SG applied to ℱ = Ω, which is a flat B̲-module with H_0(C_{B/A}, Ω) = 0 on a site with a point resolution, composed with the remark's opening clause H_1(C_{B/A}, Ω) = I/I². Remark 08SG enters in the form Stacks.ChaoticSite.nonempty_linearEquiv_leftDerivedColim_symmetricPowerDiagram, which holds over every commutative ring by Illusie's and Quillen's décalage; 08SG's own sign-twisted S_k-coinvariants step is a proof erratum, refuted over ℤ by Stacks.ChaoticSite.not_quillenSignedCoinvariants_int, and plays no role here”.

Stacks 08RG, the second clause H_k(C_{B/A}, Sym^k(Ω)) = ∧^k_B(I/I²), which the remark gets from Remark 08SG applied to Ω.

Let A → B be surjective with kernel I and let Ω = Ω_{𝒪/A} ⊗_𝒪 B̲ on C_{B/A}. Then the k-th homology of C_{B/A} with coefficients in the k-th sectionwise symmetric power of Ω is the k-th exterior power of I/I² over B, for every k.

The deduction is the remark's own: Ω is a flat B̲-module (CommAlgCat.flat_smallPolynomialCotangentModulePresheaf_obj) with H_0(C_{B/A}, Ω) = 0 (CommAlgCat.isZero_leftDerivedColimZero_polynomialCotangentModulePresheaf_of_surjective) on a site with a point resolution (CommAlgCat.isPointResolution_standardResolutionSmallCosimplicialObject), so Remark 08SG applies and gives H_k(C_{B/A}, Sym^k(Ω)) = ∧^k_B(H_1(C_{B/A}, Ω)); the remark's opening clause leftDerivedColimOneConormalLinearEquiv then replaces H_1(C_{B/A}, Ω) by I/I².

No hypothesis is placed on B; in particular 2 need not be invertible. Remark 08SG is used in the form Stacks.ChaoticSite.nonempty_linearEquiv_leftDerivedColim_symmetricPowerDiagram, which holds over every commutative ring by décalage, and not through 08SG's own sign-twisted coinvariants step, which Stacks.ChaoticSite.not_quillenSignedCoinvariants_int refutes over ℤ; see the module docstring.

theorem exteriorPower_conormal_leftDerivedColim_symmetricPower_of_surjective (k : ℕ) :
    Nonempty (↥(((colim :
              ((smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B))ᵒᵖ ⥤
                ModuleCat.{u} B) ⥤ ModuleCat.{u} B).leftDerived k).obj
            (Stacks.ChaoticSite.symmetricPowerDiagram
              (smallBoundedPolynomialSite A B (standardResolutionVarCardinal A B)) (B : Type u)
              (smallPolynomialCotangentModulePresheaf A B
                (standardResolutionVarCardinal A B)) k)) ≃ₗ[B]
        ⋀[(B : Type u)]^k (surjectionExtension.{u, u} A B h).Cotangent)

RingHom.torOneSelfIsoCotangent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorQuotientSelf.lean, line 112. The attribute's comment: “the clause Tor_1^A(B, B) = I/I² for a surjective ring map f : A → B with I = ker f: the first Tor of B with itself over A is Ideal.Cotangent I, which is Mathlib's I/I². Tor is Mathlib's monoidal Tor on ModuleCat A, the left derived functor of the tensor product, so both sides are read as A-modules; each is annihilated by I and hence a B-module. The route is the vanishing of Tor_1^A(B, A), the long exact sequence of 0 → I → A → B → 0 tensored with B, and B ⊗_A I = I/I². No hypothesis beyond the remark's own surjectivity of A → B”.

Stacks 08RG, the clause Tor_1^A(B, B) = I/I²: for a surjective ring map f : A → B with kernel I, the first Tor of B with itself over A is the conormal module I/I².

The route is the vanishing of Tor_1^A(B, A), the long exact sequence of 0 → I → A → B → 0 tensored with B, and the identification B ⊗_A I = I/I².

noncomputable def torOneSelfIsoCotangent
    {A B : Type u} [CommRing A] [CommRing B]
    (f : A →+* B) (hf : Function.Surjective f) :
    letI : Algebra A B := f.toAlgebra
    ((Tor (ModuleCat.{u} A) 1).obj
      (ModuleCat.of A B)).obj (ModuleCat.of A B) ≅
        ModuleCat.of A (RingHom.ker f).Cotangent

Tag 09D6, a remark

Tag 09D6 in the Stacks Project.

Stacks.Cotangent.TorTwo.cotangentHomologyTwoIsoTorTwoCoker, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/CotangentHomologyTwoTorCoker.lean, line 224. The attribute's comment: “H₂(L_{B/A}) is canonically Coker(Tor₂^{P₁}(B, B) → Tor₂^{P₀}(B, B)), the map being d₀ - d₁, for an arbitrary resolution P_• of B over A (Remark 08QI), as B-modules, with Tor₂^{P_n}(B, B) read as Ker(J_n ⊗_{P_n} J_n → J_n²); obtained from Remark 09D5, Stacks.Cotangent.cotangentComplexHomologyTwoLinearIsoTorOne, as the source obtains it”.

H₂(L_{B/A}) = Coker(Tor₂^{P₁}(B, B) → Tor₂^{P₀}(B, B)) for an arbitrary resolution P_• of B over A, as B-modules, where Tor₂^{P_n}(B, B) = Ker(J_n ⊗_{P_n} J_n → J_n²) and the map is d₀ - d₁. The isomorphism is Remark 09D5's H₂(L_{B/A}) = H₀(C_{B/A}, Tor₁^𝒪(𝒥, B̲)), followed by H₀ = Coker(d₀ - d₁) on the standard resolution and the canonical comparison of the cokernels of two resolutions.

def cotangentHomologyTwoIsoTorTwoCoker (hP : CommAlgCat.IsResolution A B P ε) :
    (cotangentComplex A B).homology (-2) ≅ torTwoCoker hP

Stacks.Cotangent.TorTwo.toHomologyTwo_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/CotangentHomologyTwoTorCoker.lean, line 264. The attribute's comment: “the exact sequence ∧²_B(J₀/J₀²) → Tor₂^{P₀}(B, B) → H^{-2}(L_{B/A}) → 0 for the resolution of Example 09D4: the last map is surjective”.

The map Tor₂^{P₀}(B, B) → H^{-2}(L_{B/A}) is surjective.

theorem toHomologyTwo_surjective : Function.Surjective (toHomologyTwo p)

Stacks.Cotangent.TorTwo.exact_wedgeAntisymm_toHomologyTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/CotangentHomologyTwoTorCoker.lean, line 274. The attribute's comment: “the exact sequence ∧²_B(J₀/J₀²) → Tor₂^{P₀}(B, B) → H^{-2}(L_{B/A}) → 0 for the resolution of Example 09D4: exactness at Tor₂^{P₀}(B, B), the first map being ā ∧ b̄ ↦ a ⊗ b - b ⊗ a”.

The exact sequence ∧²_B(J₀/J₀²) → Tor₂^{P₀}(B, B) → H^{-2}(L_{B/A}) → 0 for the resolution of Example 09D4: exactness at Tor₂^{P₀}(B, B), the first map being ā ∧ b̄ ↦ a ⊗ b - b ⊗ a; the second map is surjective by toHomologyTwo_surjective. Both maps are B-linear.

theorem exact_wedgeAntisymm_toHomologyTwo :
    Function.Exact (wedgeAntisymm (φ := aug p 0)) (toHomologyTwo p)

Stacks.Cotangent.TorTwo.Explicit.decomposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 486. The attribute's comment: “the decomposition Tor₂^{P₁}(B, B) = ∧²(⨁_{t ∈ T} B) ⊕ ⨁_{t ∈ T} J₀/J₀² ⊕ Tor₂^{P₀}(B, B) for the resolution P_• of Example 09D4, as B-modules, with Tor₂^{P_n}(B, B) read as Ker(J_n ⊗_{P_n} J_n → J_n²) (the remark's own identification, Stacks.Cotangent.torTwoSelfIsoMulKernel); the correspondences are decomposition_wedge, decomposition_mixed and decomposition_degen”.

The decomposition of Tor₂^{P₁}(B, B) for the explicit resolution:

Tor₂^{P₁}(B, B) = ∧²_B(⨁_{t ∈ T} B) ⊕ ⨁_{t ∈ T} J₀/J₀² ⊕ Tor₂^{P₀}(B, B)

as B-modules, Tor₂ read in the tensor-kernel model. The correspondences are decomposition_wedge, decomposition_mixed and decomposition_degen.

def decomposition :
    (⋀[target p]^2 (p.relationIndex →₀ target p) ×
        (p.relationIndex →₀ (RingHom.ker (aug p 0)).Cotangent) × mulKernel (aug p 0)) ≃ₗ[target p]
      mulKernel (aug p 1)

Stacks.Cotangent.TorTwo.Explicit.decomposition_wedge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 504. The attribute's comment: “the basis element x_t ∧ x_{t'} of the first summand corresponds to x_t ⊗ x_{t'} - x_{t'} ⊗ x_t in J₁ ⊗_{P₁} J₁”.

The basis element x_t ∧ x_{t'} of ∧²(⨁_T B) corresponds to x_t ⊗ x_{t'} - x_{t'} ⊗ x_t.

theorem decomposition_wedge (t t' : p.relationIndex) :
    decomposition p (wedgeBilin (Finsupp.single t 1) (Finsupp.single t' 1), 0, 0) =
      antisymm (xJ p t) (xJ p t')

Stacks.Cotangent.TorTwo.Explicit.decomposition_mixed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 514. The attribute's comment: “for f ∈ J₀ the element x_t ⊗ f̄ of the second summand corresponds to x_t ⊗ s₀(f) - s₀(f) ⊗ x_t in J₁ ⊗_{P₁} J₁”.

For f ∈ J₀, the element x_t ⊗ f̄ of ⨁_T J₀/J₀² corresponds to x_t ⊗ s₀(f) - s₀(f) ⊗ x_t.

theorem decomposition_mixed (t : p.relationIndex) (f : RingHom.ker (aug p 0)) :
    decomposition p (0, Finsupp.single t ((RingHom.ker (aug p 0)).toCotangent f), 0) =
      antisymm (xJ p t) (degenJ p f)

Stacks.Cotangent.TorTwo.Explicit.decomposition_degen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 522. The attribute's comment: “the map Tor₂^{P₀}(B, B) → Tor₂^{P₁}(B, B) onto the last summand is given by s₀”.

The map Tor₂^{P₀}(B, B) → Tor₂^{P₁}(B, B) onto the last summand is given by s₀.

theorem decomposition_degen (k : mulKernel (aug p 0)) :
    decomposition p (0, 0, k) = mulKernelMap (degenMap p) (aug_comp_degenMap p) k

Stacks.Cotangent.TorTwo.Explicit.face_degen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 545. The attribute's comment: “d₀ - d₁ : Tor₂^{P₁}(B, B) → Tor₂^{P₀}(B, B) is zero on the last summand”.

d₀ - d₁ vanishes on the summand Tor₂^{P₀}(B, B).

theorem face_degen (k : mulKernel (aug p 0)) :
    face p (mulKernelMap (degenMap p) (aug_comp_degenMap p) k) = 0

Stacks.Cotangent.TorTwo.Explicit.face_mixed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 552. The attribute's comment: “d₀ - d₁ maps x_t ⊗ f̄ to f ⊗ f_t - f_t ⊗ f”.

d₀ - d₁ sends x_t ⊗ f̄ to f ⊗ f_t - f_t ⊗ f.

theorem face_mixed (t : p.relationIndex) (f : RingHom.ker (aug p 0)) :
    face p (antisymm (xJ p t) (degenJ p f)) = antisymm f (relJ p t)

Stacks.Cotangent.TorTwo.Explicit.face_wedge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 560. The attribute's comment: “d₀ - d₁ maps x_t ∧ x_{t'} to f_{t'} ⊗ f_t - f_t ⊗ f_{t'}”.

d₀ - d₁ sends x_t ∧ x_{t'} to f_{t'} ⊗ f_t - f_t ⊗ f_{t'}.

theorem face_wedge (t t' : p.relationIndex) :
    face p (antisymm (xJ p t) (xJ p t')) = antisymm (relJ p t') (relJ p t)

Stacks.Cotangent.TorTwo.Explicit.torTwoDecomposition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoExplicitResolution.lean, line 592. The attribute's comment: “the decomposition of Tor₂^{P₁}(B, B) read on Mathlib's Tor' itself”.

The decomposition of Tor₂^{P₁}(B, B), on Mathlib's Tor': for the P₁-algebra B (through the augmentation),

Tor₂^{P₁}(B, B) ≅ ∧²_B(⨁_T B) ⊕ ⨁_T J₀/J₀² ⊕ Tor₂^{P₀}(B, B),

an additive isomorphism which is P₁-linear for P₁ acting on the right through P₁ → B (torTwoDecomposition_smul). It is Stacks.Cotangent.torTwoSelfIsoMulKernel followed by the inverse of decomposition.

def torTwoDecomposition :
    letI : Algebra (term p 1) (target p) := (aug p 1).toAlgebra
    ((CategoryTheory.Tor' (ModuleCat.{max u v w x} (term p 1)) 2).obj
        (ModuleCat.of (term p 1) (target p))).obj (ModuleCat.of (term p 1) (target p)) ≃+
      (⋀[target p]^2 (p.relationIndex →₀ target p) ×
        (p.relationIndex →₀ (RingHom.ker (aug p 0)).Cotangent) × mulKernel (aug p 0))

Stacks.Cotangent.torTwoSelfIsoTorOneIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoQuotientSelf.lean, line 110. The attribute's comment: “Tor₂^P(B, B) = Tor₁^P(J, B)”.

Stacks 09D6, first identification. For a surjection P → B with kernel J, the connecting homomorphism of 0 → J → P → B → 0 for the functor - ⊗ B is an isomorphism Tor₂^P(B, B) ≅ Tor₁^P(J, B): the two flanking terms are Tor_i^P(P, B) for i = 1, 2, which vanish because P is projective over itself.

noncomputable def torTwoSelfIsoTorOneIdeal (hf : Function.Surjective (algebraMap P B)) :
    ((Tor' (ModuleCat.{u} P) 2).obj (ModuleCat.of P B)).obj (ModuleCat.of P B) ≅
      ((Tor' (ModuleCat.{u} P) 1).obj
          (ModuleCat.of P (RingHom.ker (algebraMap P B)))).obj (ModuleCat.of P B)

Stacks.Cotangent.torOneIdealIsoMulKernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoQuotientSelf.lean, line 159. The attribute's comment: “Tor₁^P(J, B) = Ker(J ⊗_P J → J²)”.

Stacks 09D6, second identification. For a surjection P → B with kernel J, the connecting homomorphism of 0 → J → P → B → 0 for the functor J ⊗ - identifies Tor₁^P(J, B) with the kernel of the multiplication map J ⊗_P J → J².

noncomputable def torOneIdealIsoMulKernel (hf : Function.Surjective (algebraMap P B)) :
    ((Tor' (ModuleCat.{u} P) 1).obj
          (ModuleCat.of P (RingHom.ker (algebraMap P B)))).obj (ModuleCat.of P B) ≅
      ModuleCat.of P ↥(LinearMap.ker (Submodule.mulMap' (RingHom.ker (algebraMap P B))
        (RingHom.ker (algebraMap P B))))

Stacks.Cotangent.torTwoSelfIsoMulKernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TorTwoQuotientSelf.lean, line 218. The attribute's comment: “Tor₂^P(B, B) = Tor₁^P(J, B) = Ker(J ⊗_P J → J²)”.

Stacks 09D6, the composite identification Tor₂^P(B, B) = Ker(J ⊗_P J → J²) for a surjection P → B with kernel J.

noncomputable def torTwoSelfIsoMulKernel (hf : Function.Surjective (algebraMap P B)) :
    ((Tor' (ModuleCat.{u} P) 2).obj (ModuleCat.of P B)).obj (ModuleCat.of P B) ≅
      ModuleCat.of P ↥(LinearMap.ker (Submodule.mulMap' (RingHom.ker (algebraMap P B))
        (RingHom.ker (algebraMap P B))))

Sources

• Section 92.12, Tag 08RC
• AxiomMath/Stacks at 5ed82d14

LeanStacks.ChaoticSite.isZero_leftDerivedColim_symmetricPowerDiagram_of_lt · Stacks.ChaoticSite.nonempty_linearEquiv_leftDerivedColim_symmetricPowerDiagram · MvPolynomial.tor_map_variableIdeal_pow_succ_eq_zero · CommAlgCat.quillenSpectralSequence_of_surjective · CommAlgCat.isZero_lowerShriekZero_polynomialCotangentSheaf_of_surjective · CommAlgCat.isZero_leftDerivedColim_symmetricPower_polynomialCotangent_of_surjective · CommAlgCat.pageOneDisplay_of_surjective · CommAlgCat.polynomialSiteHomologyOneCotangentNegOneIso

Section92.13 Comparison with Lichtenbaum-Schlessinger#

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

Tag 09CD, an equation

Tag 09CD in the Stacks Project.

Algebra.Presentation.lichtenbaumSchlessingerComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessinger.lean, line 392.

The Lichtenbaum–Schlessinger complex associated to a polynomial presentation and chosen generators of its defining ideal.

noncomputable def lichtenbaumSchlessingerComplex
    (P : Algebra.Presentation A B X T) : LichtenbaumSchlessingerComplex P

Tag 09CE, a definition

Tag 09CE in the Stacks Project.

Biderivation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Biderivation.lean, line 77. References: EGA 0 (20.1.2); EGA 0 (20.1.1).

An A-biderivation from an A-algebra B to a (B, B)-bimodule M is an A-linear map satisfying the Leibniz rule for the left and right actions.

structure Biderivation (A : Type u) (B : Type v) (M : Type w)
    [CommSemiring A] [Semiring B] [AddCommMonoid M] [Algebra A B]
    [Module A M] [Module B M] [Module Bᵐᵒᵖ M]
    [IsScalarTower A B M] [IsScalarTower A Bᵐᵒᵖ M]
    [SMulCommClass B Bᵐᵒᵖ M]
    extends B →ₗ[A] M

Tag 09CF, a lemma

Tag 09CF in the Stacks Project.

Biderivation.IsCompatibleOnVars, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Biderivation.lean, line 130. The attribute's comment: “the compatibility equations the values on the variables must satisfy”.

Stacks 09CF. The equations that commutativity of the polynomial variables forces on the values of a biderivation of A[S]: the Leibniz rule applied to the two readings of X s * X t = X t * X s. For a bimodule whose two actions agree they hold automatically.

The source imposes no such condition; that omission is a Stacks erratum, and these equations really can fail, as Biderivation.not_isCompatibleOnVars_erratumValues shows for the counterexample of StacksFrontier.Cotangent.BiderivationErratum.

def IsCompatibleOnVars (A : Type u) {S : Type v} {M : Type w} [CommSemiring A]
    [AddCommGroup M] [Module (MvPolynomial S A) M] [Module (MvPolynomial S A)ᵐᵒᵖ M]
    (m : S → M) : Prop

Biderivation.existsUnique_mvPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Biderivation.lean, line 358. The attribute's comment: “existence and uniqueness of the biderivation with prescribed values”.

Stacks 09CF. Let P = A[S] be a polynomial ring over A and let M be a (P, P) bimodule over A. Given m s ∈ M for s ∈ S satisfying the compatibility equations that commutativity of the variables forces, there is a unique A-biderivation P → M sending X s to m s.

This is the corrected form of the tag. The source prescribes the values m s with no condition at all, and the existence half of that unrestricted claim is false: it is a Stacks erratum, refuted by Biderivation.not_exists_biderivation_erratum in StacksFrontier.Cotangent.BiderivationErratum, which exhibits k[x, y] acting on k by evaluation at (1, 0) on the left and at (0, 0) on the right and prescribed values 0 and 1 admitting no biderivation. Uniqueness is unaffected, and by Biderivation.existsUnique_mvPolynomial_iff the compatibility hypothesis below is not merely sufficient but exactly the obstruction.

theorem existsUnique_mvPolynomial (m : S → M) (hcomm : IsCompatibleOnVars A m) :
    ∃! D : Biderivation A (MvPolynomial S A) M, ∀ s, D (X s) = m s

Biderivation.existsUnique_mvPolynomial_of_op_smul_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/Biderivation.lean, line 391. The attribute's comment: “the unrestricted assertion of the source, for a bimodule whose two actions agree”.

Stacks 09CF, in the case the source applies it: when the two actions of the polynomial ring on M agree, the compatibility equations hold for every family of prescribed values, and the source's unrestricted assertion is recovered.

This hypothesis cannot be dropped: stated for an arbitrary bimodule the source's assertion is a Stacks erratum, refuted by Biderivation.not_forall_existsUnique_mvPolynomial_erratumModule in StacksFrontier.Cotangent.BiderivationErratum, whose bimodule is a copy of k carrying the two different actions evaluation at (1, 0) and evaluation at (0, 0).

theorem existsUnique_mvPolynomial_of_op_smul_eq
    (h : ∀ (q : MvPolynomial S A) (x : M), MulOpposite.op q • x = q • x) (m : S → M) :
    ∃! D : Biderivation A (MvPolynomial S A) M, ∀ s, D (X s) = m s

Tag 09CG, a lemma

Tag 09CG in the Stacks Project.

Algebra.Presentation.cotangentToLichtenbaumSchlessinger, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparison.lean, line 154. The attribute's comment: “the canonical map L_{B/A} → L in D(B), attached to a chain-level comparison carried as the explicit datum Algebra.Presentation.LichtenbaumSchlessingerComparison”.

Stacks 09CG. The canonical map L_{B/A} → L in D(B) attached to a chain-level comparison: its image under the localization functor.

public def cotangentToLichtenbaumSchlessinger (c : LichtenbaumSchlessingerComparison P) :
    DerivedCategory.Q.obj (cotangentComplexULift.{u, v, w} A B) ⟶
      DerivedCategory.Q.obj (lichtenbaumSchlessingerComplex P).complex

Algebra.Presentation.truncGECotangentIsoLichtenbaumSchlessinger, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparison.lean, line 190. The attribute's comment: “the induced map τ_{≥ -2} L_{B/A} → L is an isomorphism in D(B)”.

Stacks 09CG. The isomorphism τ_{≥ -2} L_{B/A} ≅ L induced by the canonical map.

public def truncGECotangentIsoLichtenbaumSchlessinger
    (c : LichtenbaumSchlessingerComparison P) :
    (DerivedCategory.TStructure.t.truncGE (-2)).obj
        (DerivedCategory.Q.obj (cotangentComplexULift.{u, v, w} A B)) ≅
      DerivedCategory.Q.obj (lichtenbaumSchlessingerComplex P).complex

Algebra.Presentation.truncGECotangentIsoLichtenbaumSchlessinger_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparison.lean, line 202. The attribute's comment: “the isomorphism τ_{≥ -2} L_{B/A} → L is induced by the canonical map L_{B/A} → L”.

Stacks 09CG. The isomorphism τ_{≥ -2} L_{B/A} ≅ L is the one induced by the canonical map L_{B/A} → L: composing it with the projection to the truncation returns that map.

public theorem truncGECotangentIsoLichtenbaumSchlessinger_fac
    (c : LichtenbaumSchlessingerComparison P) :
    (DerivedCategory.TStructure.t.truncGEπ (-2)).app
        (DerivedCategory.Q.obj (cotangentComplexULift.{u, v, w} A B)) ≫
      (truncGECotangentIsoLichtenbaumSchlessinger c).hom =
        cotangentToLichtenbaumSchlessinger c

Algebra.Presentation.LichtenbaumSchlessingerComparison.canonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparisonCanonical/Canonical.lean, line 37. The attribute's comment: “the map of complexes L_{B/A} → L built from the choices ψ and λ of the source, with its isomorphisms on H^0 (Remark 08UP, Lemma 08RB), H^{-1} (idem) and H^{-2} (Remark 09D6)”.

The chain-level comparison of a presentation constructed in the source: the map of complexes Algebra.Presentation.lsChainMap, which is dψ ⊗ 1, λ̄ and q in degrees 0, -1 and -2, together with its isomorphisms on H⁰, H^{-1} and H^{-2}.

public def LichtenbaumSchlessingerComparison.canonical : LichtenbaumSchlessingerComparison P

Algebra.Presentation.canonicalCotangentToLichtenbaumSchlessinger, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparisonCanonical/Canonical.lean, line 53. The attribute's comment: “the canonical map L_{B/A} → L in D(B), the class of the map of complexes dψ ⊗ 1, λ̄, q built from the choices ψ : P₀ → P and the biderivation λ of the source”.

The canonical map L_{B/A} → L in D(B): the image under the localization functor of the map of complexes Algebra.Presentation.lsChainMap. It does not depend on the choices ψ and λ: Algebra.Presentation.Q_map_eq_canonicalCotangentToLichtenbaumSchlessinger.

public def canonicalCotangentToLichtenbaumSchlessinger :
    DerivedCategory.Q.obj (cotangentComplexULift.{u, v, w} A B) ⟶
      DerivedCategory.Q.obj (lichtenbaumSchlessingerComplex P).complex

Algebra.Presentation.isIso_descTruncGE_canonicalCotangentToLichtenbaumSchlessinger, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparisonCanonical/Canonical.lean, line 71. The attribute's comment: “the canonical map L_{B/A} → L induces an isomorphism τ_{≥ -2} L_{B/A} → L in D(B)”.

The canonical map L_{B/A} → L factors through the truncation τ_{≥ -2} L_{B/A}, and the factorization is an isomorphism.

public theorem isIso_descTruncGE_canonicalCotangentToLichtenbaumSchlessinger :
    IsIso (DerivedCategory.TStructure.t.descTruncGE
      (canonicalCotangentToLichtenbaumSchlessinger P) (-2))

Algebra.Presentation.canonicalTruncGECotangentIsoLichtenbaumSchlessinger, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparisonCanonical/Canonical.lean, line 79. The attribute's comment: “the induced map τ_{≥ -2} L_{B/A} → L is an isomorphism in D(B)”.

The isomorphism τ_{≥ -2} L_{B/A} ≅ L induced by the canonical map.

public def canonicalTruncGECotangentIsoLichtenbaumSchlessinger :
    (DerivedCategory.TStructure.t.truncGE (-2)).obj
        (DerivedCategory.Q.obj (cotangentComplexULift.{u, v, w} A B)) ≅
      DerivedCategory.Q.obj (lichtenbaumSchlessingerComplex P).complex

Algebra.Presentation.canonicalTruncGECotangentIsoLichtenbaumSchlessinger_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparisonCanonical/Canonical.lean, line 90. The attribute's comment: “the isomorphism τ_{≥ -2} L_{B/A} → L is induced by the canonical map L_{B/A} → L”.

The isomorphism τ_{≥ -2} L_{B/A} ≅ L is the one induced by the canonical map L_{B/A} → L: composing it with the projection to the truncation returns that map.

public theorem canonicalTruncGECotangentIsoLichtenbaumSchlessinger_fac :
    (DerivedCategory.TStructure.t.truncGEπ (-2)).app
        (DerivedCategory.Q.obj (cotangentComplexULift.{u, v, w} A B)) ≫
      (canonicalTruncGECotangentIsoLichtenbaumSchlessinger P).hom =
        canonicalCotangentToLichtenbaumSchlessinger P

Algebra.Presentation.Q_map_eq_canonicalCotangentToLichtenbaumSchlessinger, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparisonIndependence.lean, line 630. The attribute's comment: “the formulas dψ ⊗ 1, λ̄, q specify the comparison for every permissible choice of ψ and λ, and changing these choices gives the same morphism in D(B)”.

Independence of the choices. Every map of complexes L_{B/A} → L given by the formulas dψ ⊗ 1, λ̄, q of the source, for any permissible choice of ψ : P₀ → P and of the biderivation λ : P₁ → F/TrivRel, represents the canonical map Algebra.Presentation.canonicalCotangentToLichtenbaumSchlessinger in D(B).

theorem Q_map_eq_canonicalCotangentToLichtenbaumSchlessinger (c : LichtenbaumSchlessingerChoice P)
    (f : cotangentComplexULift.{u, v, w} A B ⟶ (lichtenbaumSchlessingerComplex P).complex)
    (hf : IsLichtenbaumSchlessingerComparison P c f) :
    DerivedCategory.Q.map f = canonicalCotangentToLichtenbaumSchlessinger P

Tag 09D7, a remark

Tag 09D7 in the Stacks Project.

Algebra.Presentation.LichtenbaumSchlessingerHom.canonicalCotangentToLichtenbaumSchlessinger_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerComparisonNatural.lean, line 411. The attribute's comment: “the second commutative diagram: L_{B/A} → L, L → L' equals L_{B/A} → L_{B'/A'}, L_{B'/A'} → L' in D(B)”.

For a commutative square of rings A → A', B → B' and compatible presentations P → P' with f'_t the image of f_t, the canonical maps L_{B/A} → L and L_{B'/A'} → L' commute in D(B) with the map L_{B/A} → L_{B'/A'} of cotangent complexes and the map L → L' of Lichtenbaum–Schlessinger complexes, the objects over B' being read over B along B → B'.

theorem canonicalCotangentToLichtenbaumSchlessinger_naturality :
    DerivedCategory.Q.map (cotangentComplexULiftSquareMap.{u, u', v, w} A A' B B') ≫
        (ModuleCat.restrictScalars (algebraMap B B')).mapDerivedCategoryFactors.inv.app
          (cotangentComplexULift.{u', max u v, w} A' B') ≫
        (ModuleCat.restrictScalars (algebraMap B B')).mapDerivedCategory.map
          (canonicalCotangentToLichtenbaumSchlessinger.{u', max u v, w} P') ≫
        (ModuleCat.restrictScalars (algebraMap B B')).mapDerivedCategoryFactors.hom.app
          (lichtenbaumSchlessingerComplex P').complex =
      canonicalCotangentToLichtenbaumSchlessinger.{u, max u' v, w} P ≫
        DerivedCategory.Q.map f.complexMap

Algebra.Presentation.LichtenbaumSchlessingerHom.relationQuotientMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerFunctoriality.lean, line 206. The attribute's comment: “the vertical arrow Rel/TrivRel → Rel'/TrivRel' of the displayed diagram”.

The map Rel/TrivRel → Rel'/TrivRel' induced by Rel → Rel', in degree -2.

def relationQuotientMap : relationQuotient P →ₛₗ[f.ringHom] relationQuotient P'

Algebra.Presentation.LichtenbaumSchlessingerHom.freeTensorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerFunctoriality.lean, line 246. The attribute's comment: “the vertical arrow F ⊗_P B → F' ⊗_{P'} B' of the displayed diagram”.

Stacks 09D7. The arrow F ⊗_P B → F' ⊗_{P'} B' of the diagram, in degree -1.

def freeTensorMap :
    (B ⊗[P.Ring] (T →₀ P.Ring)) →ₗ[B] B' ⊗[P'.Ring] ((T ⊕ S) →₀ P'.Ring)

Algebra.Presentation.LichtenbaumSchlessingerHom.differentialTensorMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerFunctoriality.lean, line 270. The attribute's comment: “the vertical arrow Ω_{P/A} ⊗_P B → Ω_{P'/A'} ⊗_{P'} B' of the displayed diagram”.

Stacks 09D7. The arrow Ω_{P/A} ⊗_P B → Ω_{P'/A'} ⊗_{P'} B' of the diagram, in degree 0.

def differentialTensorMap :
    (B ⊗[P.Ring] Ω[P.Ring⁄A]) →ₗ[B] B' ⊗[P'.Ring] Ω[P'.Ring⁄A']

Algebra.Presentation.LichtenbaumSchlessingerHom.freeTensorMap_relationBoundaryR, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerFunctoriality.lean, line 308. The attribute's comment: “commutativity of the left-hand square of the displayed diagram”.

Stacks 09D7. The left-hand square of the displayed diagram commutes: the arrow Rel/TrivRel → F ⊗_P B followed by the vertical arrow in degree -1 agrees with the vertical arrow in degree -2 followed by Rel'/TrivRel' → F' ⊗_{P'} B'.

lemma freeTensorMap_relationBoundaryR (q : relationQuotient P) :
    f.freeTensorMap (relationBoundaryR P q) =
      relationBoundaryR P' (f.relationQuotientMap q)

Algebra.Presentation.LichtenbaumSchlessingerHom.differentialTensorMap_relationDifferentialB, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerFunctoriality.lean, line 331. The attribute's comment: “commutativity of the right-hand square of the displayed diagram”.

Stacks 09D7. The right-hand square of the displayed diagram commutes: the arrow F ⊗_P B → Ω_{P/A} ⊗_P B followed by the vertical arrow in degree 0 agrees with the vertical arrow in degree -1 followed by F' ⊗_{P'} B' → Ω_{P'/A'} ⊗_{P'} B'.

lemma differentialTensorMap_relationDifferentialB (z : B ⊗[P.Ring] (T →₀ P.Ring)) :
    f.differentialTensorMap (relationDifferentialB P z) =
      relationDifferentialB P' (f.freeTensorMap z)

Algebra.Presentation.LichtenbaumSchlessingerHom.complexMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LichtenbaumSchlessingerFunctorialityComplex.lean, line 272. The attribute's comment: “the first commutative diagram: the canonical map of Lichtenbaum–Schlessinger complexes L → L' with vertical arrows Rel/TrivRel → Rel'/TrivRel', F ⊗_P B → F' ⊗_{P'} B', Ω_{P/A} ⊗_P B → Ω_{P'/A'} ⊗_{P'} B'”.

The canonical map of Lichtenbaum–Schlessinger complexes L → L' attached to compatible presentations of a commutative square of rings: the arrows Rel/TrivRel → Rel'/TrivRel', F ⊗_P B → F' ⊗_{P'} B', Ω_{P/A} ⊗_P B → Ω_{P'/A'} ⊗_{P'} B' (tensored up to B'), which commute with the differentials. It is B-linear, L' being read over B along B → B'.

def complexMap : (lichtenbaumSchlessingerComplex P).complex ⟶
    ((𝓡).mapHomologicalComplex (ComplexShape.up ℤ)).obj
      (lichtenbaumSchlessingerComplex P').complex

Sources

• Section 92.13, Tag 09AM
• AxiomMath/Stacks at 5ed82d14

LeanAlgebra.Presentation.lichtenbaumSchlessingerComplex · Biderivation · Biderivation.IsCompatibleOnVars · Biderivation.existsUnique_mvPolynomial · Biderivation.existsUnique_mvPolynomial_of_op_smul_eq · Algebra.Presentation.cotangentToLichtenbaumSchlessinger · Algebra.Presentation.truncGECotangentIsoLichtenbaumSchlessinger · Algebra.Presentation.truncGECotangentIsoLichtenbaumSchlessinger_fac

Section92.14 The cotangent complex of a local complete intersection#

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

Tag 08SI, a lemma

Tag 08SI in the Stacks Project.

CommAlgCat.nonempty_cotangentComplex_retraction_iso_single, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialRetraction.lean, line 267. The attribute's comment: “the lemma for a general base ring A and a general polynomial algebra B over it with an augmentation B → A, of which the source's A = Z[x_1,...,x_n] -> B = Z sending every x_i to 0 is the case A = Z; the source's ideal I = (x_1,...,x_n) is the kernel of the augmentation, and I/I^2 is its conormal module. ONE carried hypothesis: h08QX, Proposition 08QX for the tower A -> B -> A, which is the triangle the source's proof invokes and which is not proved in this library — the triangle the library carries, Tag 08SD, needs the middle map injective, whereas the augmentation B → A is surjective. The hypothesis is 08QX itself, for a general not-necessarily-injective map, and not the conclusion proved here”.

Stacks Project, Tag 08SI. Let A be a commutative ring, let B be a polynomial algebra over A, and let B → A be a retraction of A → B — an augmentation. Let I = ker(B → A). Then L_{A/B} is quasi-isomorphic to I/I²[1], that is, isomorphic in D(A) to the conormal module I/I² placed in cohomological degree -1.

The source states this for A = ℤ, B = ℤ[x₁, …, xₙ] and the augmentation sending every variable to 0, whose kernel is the ideal I = (x₁, …, xₙ); the statement here is that case with the base ring and the set of variables left general.

theorem nonempty_cotangentComplex_retraction_iso_single
    (hB : Algebra.IsPolynomialAlgebra A B) (h08QX : HasFundamentalTriangleAt A B A) :
    Nonempty (DerivedCategory.Q.obj (cotangentComplex B (CommAlgCat.of B A)) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} ↥(CommAlgCat.of B A)) (-1)).obj
        (ModuleCat.of ↥(CommAlgCat.of B A)
          (surjectionExtension B (CommAlgCat.of B A)
            (surjective_algebraMap_of_isScalarTower_self A B)).Cotangent))

CommAlgCat.nonempty_cotangentComplex_retraction_iso_single_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/PolynomialRetractionUnconditional.lean, line 69. The attribute's comment: “the lemma for a general base ring A and a general polynomial algebra B over it with an augmentation B → A, of which the source's A = Z[x_1,...,x_n] -> B = Z sending every x_i to 0 is the case A = Z; the source's ideal I = (x_1,...,x_n) is the kernel of the augmentation, and I/I^2 is its conormal module. NOTHING is carried: the triangle the source's proof invokes is Proposition 08QX for the tower A -> B -> A, CommAlgCat.productFundamentalTriangle_distinguished, which holds for arbitrary ring maps — the triangle of Tag 08SD needs the middle map injective, whereas the augmentation B → A is surjective, so it is the proposition and not Tag 08SD that applies”.

Stacks Project, Tag 08SI. Let B be a polynomial algebra over A with an augmentation B → A, and let I be its kernel. Then L_{A/B} is isomorphic in D(A) to I/I² placed in cohomological degree -1.

This is CommAlgCat.nonempty_cotangentComplex_retraction_iso_single with the fundamental triangle of the tower A → B → A supplied by CommAlgCat.hasFundamentalTriangleAt.

theorem nonempty_cotangentComplex_retraction_iso_single_unconditional
    (hB : Algebra.IsPolynomialAlgebra A B) :
    Nonempty (DerivedCategory.Q.obj (cotangentComplex B (CommAlgCat.of B A)) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} ↥(CommAlgCat.of B A)) (-1)).obj
        (ModuleCat.of ↥(CommAlgCat.of B A)
          (surjectionExtension B (CommAlgCat.of B A)
            (surjective_algebraMap_of_isScalarTower_self A B)).Cotangent))

Tag 08SJ, a lemma

Tag 08SJ in the Stacks Project.

CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/KoszulRegularQuotient.lean, line 338. The attribute's comment: “the lemma for a kernel generated by a Koszul-regular SEQUENCE f_1,...,f_r (the case Tag 08SK generalizes to a Koszul-regular ideal, which this does not prove: see the No @[stacks 08SK] section of the module docstring). I/I^2 is the conormal module of the surjection, as the cotangent module of the corresponding algebra extension. ONE carried hypothesis: h08QX, Proposition 08QX for the towers R -> P -> R with P a polynomial algebra over R carrying a retraction — exactly the hypothesis that Tag 08SI (CommAlgCat.nonempty_cotangentComplex_retraction_iso_single) carries, 08QX not being proved in this library because the triangle the library has, Tag 08SD, needs the middle map injective, whereas an augmentation is surjective. The hypothesis is 08QX itself and not the conclusion proved here”.

Stacks Project, Tag 08SJ. Let R → S be a surjective map of commutative rings whose kernel I is generated by a Koszul-regular sequence f₁, …, f_r ∈ R. Then L_{S/R} is quasi-isomorphic to I/I²[1], that is, isomorphic in D(S) to the conormal module I/I² placed in cohomological degree -1.

The source's proof: the square of P = R[x₁, …, x_r] → R, x_i ↦ f_i over the augmentation P → R, x_i ↦ 0 induces a quasi-isomorphism R ⊗_P^𝐋 R = S, so [Stacks, Tag 08QQ] reduces the computation to L_{R/P}, which [Stacks, Tag 08SI] gives as a projective module in degree -1. Hence L_{S/R} has no cohomology in the degrees ≤ -2, and CommAlgCat.nonempty_cotangentComplex_iso_single_of_isZero_homology_le_negTwo concludes.

theorem nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence
    (h : Function.Surjective (algebraMap R (S : Type u)))
    {r : ℕ} (f : Fin r → R) (hf : Koszul.IsKoszulRegular f)
    (hI : RingHom.ker (algebraMap R (S : Type u)) = Ideal.span (Set.range f))
    (h08QX : ∀ (P : Type u) [CommRing P] [Algebra R P] [Algebra P R] [IsScalarTower R P R],
      Algebra.IsPolynomialAlgebra R P → HasFundamentalTriangleAt R P R) :
    Nonempty (DerivedCategory.Q.obj (cotangentComplex R S) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} (S : Type u)) (-1)).obj
        (ModuleCat.of (S : Type u) (surjectionExtension R S h).Cotangent))

CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/KoszulRegularQuotientUnconditional.lean, line 56. The attribute's comment: “the lemma for a kernel generated by a Koszul-regular SEQUENCE f_1,...,f_r. I/I^2 is the conormal module of the surjection, as the cotangent module of the corresponding algebra extension. NOTHING is carried: the fundamental triangle of the towers R -> P -> R with P a polynomial algebra over R carrying a retraction is Proposition 08QX, CommAlgCat.productFundamentalTriangle_distinguished. The triangle of Tag 08SD does not apply, needing the middle map injective whereas an augmentation is surjective; the proposition does, assuming nothing”.

Stacks Project, Tag 08SJ. Let R → S be a surjective map of commutative rings whose kernel I is generated by a Koszul-regular sequence f₁, …, f_r ∈ R. Then L_{S/R} is isomorphic in D(S) to the conormal module I/I² placed in cohomological degree -1.

This is CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence with the fundamental triangles of the towers R → P → R supplied by CommAlgCat.hasFundamentalTriangleAt.

theorem nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence_unconditional
    (h : Function.Surjective (algebraMap R (S : Type u)))
    {r : ℕ} (f : Fin r → R) (hf : Koszul.IsKoszulRegular f)
    (hI : RingHom.ker (algebraMap R (S : Type u)) = Ideal.span (Set.range f)) :
    Nonempty (DerivedCategory.Q.obj (cotangentComplex R S) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} (S : Type u)) (-1)).obj
        (ModuleCat.of (S : Type u) (surjectionExtension R S h).Cotangent))

Tag 08SK, a lemma

Tag 08SK in the Stacks Project.

CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/KoszulRegularIdealQuotient.lean, line 381. The attribute's comment: “the lemma for a Koszul-regular IDEAL (Tag 07CV (2), Ideal.IsKoszulRegular), generalizing the sequence case Tag 08SJ (CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence). I/I^2 is the conormal module of the surjection, as the cotangent module of the corresponding algebra extension. TWO carried hypotheses, neither of them the conclusion. (1) h08SF: the localization lemma of Tag 08SF, cotangent-lemma-localize, which is not proved in this library and which no declaration here carries — it says L_{B_g/A_g} is isomorphic in D(B_g) to the degreewise extension of scalars of L_{B/A} along the flat map B -> B_g, an isomorphism of whole complexes for a DIFFERENT ring map A_g -> B_g, mentioning no homology in any degree, no single module and no conormal module; it is carried pointwise, only at the g at which the Koszul-regularity of the kernel produces a generating sequence. (2) h08QX: Proposition 08QX for the towers A_g -> P -> A_g with P a polynomial algebra over A_g carrying a retraction — verbatim the hypothesis that Tag 08SJ carries, inherited because Tag 08SJ is applied to the localized maps, 08QX not being proved in this library because the triangle the library has, Tag 08SD, needs the middle map injective whereas an augmentation is surjective. Everything else is proved outright: the Koszul cover generates the unit ideal, the localized map is surjective with kernel the localized ideal, Tag 08SJ at it, the flatness of B -> B_g, and the Zariski descent of the vanishing”.

Stacks Project, Tag 08SK. Let A → B be a surjective map of commutative rings whose kernel I is a Koszul-regular ideal, Tag 07CV (2). Then L_{B/A} is quasi-isomorphic to I/I²[1], that is, isomorphic in D(B) to the conormal module I/I² placed in cohomological degree -1.

The source's proof: locally on Spec(A) the ideal I is generated by a Koszul-regular sequence, so [Stacks, Tag 08SJ] gives the vanishing of H^i(L_{B_g/A_g}) for i ≤ -2 over a cover, and [Stacks, Tag 08SF] turns that into the vanishing of the localizations of H^i(L_{B/A}), hence of H^i(L_{B/A}) itself; then CommAlgCat.nonempty_cotangentComplex_iso_single_of_isZero_homology_le_negTwo concludes.

See the module docstring for the two carried hypotheses.

theorem nonempty_cotangentComplex_iso_single_of_isKoszulRegular
    (h : Function.Surjective (algebraMap A (B : Type u)))
    (hI : Ideal.IsKoszulRegular (RingHom.ker (algebraMap A (B : Type u))))
    (h08SF : ∀ g : A, KernelKoszulRegularAway A B g → HasLocalizedCotangentComplexAt A B g)
    (h08QX : ∀ g : A, KernelKoszulRegularAway A B g →
      HasFundamentalTriangleAtPolynomialRetractions (Localization.Away g)) :
    Nonempty (DerivedCategory.Q.obj (cotangentComplex A B) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} (B : Type u)) (-1)).obj
        (ModuleCat.of (B : Type u) (surjectionExtension A B h).Cotangent))

CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/KoszulRegularIdealQuotientUnconditional.lean, line 122. The attribute's comment: “the lemma for a Koszul-regular IDEAL (Tag 07CV (2), Ideal.IsKoszulRegular), generalizing the sequence case Tag 08SJ. I/I^2 is the conormal module of the surjection, as the cotangent module of the corresponding algebra extension. NOTHING is carried: the hypotheses are the source's two, that A -> B is surjective and that its kernel is a Koszul-regular ideal. Tag 08SF, cotangent-lemma-localize, is PROVED, not assumed: CommAlgCat.hasLocalizedCotangentComplexAt supplies it at every principal localization A_g -> B_g, from CommAlgCat.nonempty_extendScalars_cotangentComplex_iso_localization, the degreewise reading of Tag 08SF, whose S maps into T hypothesis is automatic for S the powers of g. Proposition 08QX is likewise NOT carried: the fundamental triangle of the towers A_g -> P -> A_g that Tag 08SJ consumes is CommAlgCat.productFundamentalTriangle_distinguished, through CommAlgCat.hasFundamentalTriangleAt. Everything else is proved outright: the Koszul cover generates the unit ideal, the localized map is surjective with kernel the localized ideal, Tag 08SJ at it, the flatness of B -> B_g, and the Zariski descent of the vanishing”.

Stacks Project, Tag 08SK. Let A → B be a surjective map of commutative rings whose kernel I is a Koszul-regular ideal, Tag 07CV (2). Then L_{B/A} is quasi-isomorphic to I/I²[1], that is, isomorphic in D(B) to the conormal module I/I² placed in cohomological degree -1.

This is CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular with its two inputs supplied by CommAlgCat.hasLocalizedCotangentComplexAt and CommAlgCat.hasFundamentalTriangleAt, so that the only hypotheses left are the source's own two.

theorem nonempty_cotangentComplex_iso_single_of_isKoszulRegular_unconditional
    (h : Function.Surjective (algebraMap A (B : Type u)))
    (hI : Ideal.IsKoszulRegular (RingHom.ker (algebraMap A (B : Type u)))) :
    Nonempty (DerivedCategory.Q.obj (cotangentComplex A B) ≅
      (DerivedCategory.singleFunctor (ModuleCat.{u} (B : Type u)) (-1)).obj
        (ModuleCat.of (B : Type u) (surjectionExtension A B h).Cotangent))

Tag 08SL, a proposition

Tag 08SL in the Stacks Project.

CommAlgCat.isPerfect_and_hasTorAmplitude_cotangentComplexDerived_of_isLocalCompleteIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LocalCompleteIntersectionPerfect.lean, line 208. The attribute's comment: “perfectness and Tor amplitude in [-1, 0] are both proved, conditionally on the hypothesis e that L_{B/A} is isomorphic in D(B) to the naive complex of the given finite polynomial presentation; that isomorphism is Tag 08RB (only its degree-zero clause is in this library) together with Tag 08SK (absent from this library). All the local complete intersection hypothesis is used for, finite projectivity of the two terms, is proved”.

Stacks 08SL. Let A → B be a local complete intersection map. Then the cotangent complex L_{B/A} is a perfect object of D(B) with Tor amplitude in [-1, 0].

The quasi-isomorphism L_{B/A} ≅ NL(P → B) with the naive complex of a finite polynomial presentation P is taken as the hypothesis e: it is the conjunction of Tag 08RB and Tag 08SK, neither of which is available in this library (see the module documentation). What the local complete intersection hypothesis supplies, and what is proved here, is that the two terms of NL(P → B) are finite projective B-modules — the conormal module J/J² by Tag 08RK through Tags 07CZ and 062I, and ⨁ B dxᵢ by the canonical basis of the cotangent space. Perfectness is then immediate from the definition and the Tor-amplitude bound follows by Tag 0654, a projective module being flat.

theorem isPerfect_and_hasTorAmplitude_cotangentComplexDerived_of_isLocalCompleteIntersection
    (A : Type u) [CommRing A] (B : CommAlgCat.{u} A) {ι : Type u} [Finite ι]
    (P : Algebra.Generators A ↥B ι)
    (hlci : RingHom.IsLocalCompleteIntersection (algebraMap A ↥B))
    (e : cotangentComplexDerived.{u, u} A B ≅
      DerivedCategory.Q.obj (Algebra.Extension.naiveComplex P.toExtension)) :
    StacksDraft.Perfect.IsPerfect (cotangentComplexDerived.{u, u} A B) ∧
      StacksDraft.TorAmplitude.HasTorAmplitudeCanonical ↥B
        (cotangentComplexDerived.{u, u} A B) (-1) 0

CommAlgCat.isPerfect_and_hasTorAmplitude_cotangentComplexDerived_of_isLCI, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/LocalCompleteIntersectionPerfectUnconditional.lean, line 311. The attribute's comment: “the proposition, under the source's single hypothesis that A → B is a local complete intersection (RingHom.IsLocalCompleteIntersection, Tag 07D0). Perfect is Tag 0657 (1) and Tor amplitude is Tag 0652 (1) at the canonical derived tensor product. The isomorphism of L_{B/A} with the naive complex of a finite polynomial presentation is constructed here from Tag 08RB (Stacks.Cotangent.naiveComparisonIso), the fundamental triangle of A → P → B (Proposition 08QX), Tag 08QH and Tag 08SK”. References: SGA 6 0 (4.3), “special case”; SGA 6 VIII (2.4), “special case”; SGA 6 XIV (2.1), “special case”.

If A → B is a local complete intersection map, then the cotangent complex L_{B/A} is a perfect object of D(B) with Tor amplitude in [-1, 0].

Choose a finite polynomial presentation P = A[x₁, …, x_n] → B. The naive complex NL(P → B) = (J/J² → ⨁ B dxᵢ) consists of finite projective modules, by Tag 08RK, CommAlgCat.isPerfect_and_hasTorAmplitude_cotangentComplexDerived_of_isLocalCompleteIntersection; and L_{B/A} is isomorphic to it in D(B) (CommAlgCat.cotangentComplexDerivedIsoNaiveComplexOfIsLocalCompleteIntersection): by Tag 08RB NL(P → B) ≅ τ_{≥ -1} L_{B/A}, and by the fundamental triangle 08QS of A → P → B together with Tags 08QH and 08SK, H^i(L_{B/A}) = 0 for i ≤ -2.

theorem isPerfect_and_hasTorAmplitude_cotangentComplexDerived_of_isLCI
    (A : Type u) [CommRing A] (B : CommAlgCat.{u} A)
    (hlci : RingHom.IsLocalCompleteIntersection (algebraMap A ↥B)) :
    StacksDraft.Perfect.IsPerfect (cotangentComplexDerived.{u, u} A B) ∧
      StacksDraft.TorAmplitude.HasTorAmplitudeCanonical ↥B
        (cotangentComplexDerived.{u, u} A B) (-1) 0

Sources

• Section 92.14, Tag 08SH
• AxiomMath/Stacks at 5ed82d14

LeanCommAlgCat.nonempty_cotangentComplex_retraction_iso_single · CommAlgCat.nonempty_cotangentComplex_retraction_iso_single_unconditional · CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence · CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_sequence_unconditional · CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular · CommAlgCat.nonempty_cotangentComplex_iso_single_of_isKoszulRegular_unconditional · CommAlgCat.isPerfect_and_hasTorAmplitude_cotangentComplexDerived_of_isLocalCompleteIntersection · CommAlgCat.isPerfect_and_hasTorAmplitude_cotangentComplexDerived_of_isLCI

Section92.15 Tensor products and the cotangent complex#

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

Tag 09D9, an equation

Tag 09D9 in the Stacks Project.

CommAlgCat.exists_tensorProduct_nine_diagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TensorProduct.lean, line 134.

Stacks 09D9, Equation 92.15.0.1. Let A and B be algebras over a ring R. Given the fundamental triangle L_{A/R} ⊗^L_A (A ⊗_R B) ⟶ L_{A ⊗_R B/R} ⟶ L_{A ⊗_R B/A} of R → A → A ⊗_R B and the fundamental triangle L_{B/R} ⊗^L_B (A ⊗_R B) ⟶ L_{A ⊗_R B/R} ⟶ L_{A ⊗_R B/B} of R → B → A ⊗_R B, there is an object E of D(A ⊗_R B) fitting into the upper right corner of the diagram

L_{A/R} ⊗^L_A (A ⊗_R B) ⟶ L_{A ⊗_R B/B}      ⟶ E
            ‖                     ↑                ↑
L_{A/R} ⊗^L_A (A ⊗_R B) ⟶ L_{A ⊗_R B/R}      ⟶ L_{A ⊗_R B/A}
                                  ↑                ↑
                      L_{B/R} ⊗^L_B (A ⊗_R B) ═ L_{B/R} ⊗^L_B (A ⊗_R B)

whose top row and right column are distinguished triangles and whose squares commute.

theorem exists_tensorProduct_nine_diagram
    {u : cotangentComplexDerivedBaseChange R (CommAlgCat.of R A) (A ⊗[R] B) ⟶
      cotangentComplexDerived R (CommAlgCat.of R (A ⊗[R] B))}
    {p : cotangentComplexDerived R (CommAlgCat.of R (A ⊗[R] B)) ⟶
      cotangentComplexDerived A (CommAlgCat.of A (A ⊗[R] B))}
    {d₁ : cotangentComplexDerived A (CommAlgCat.of A (A ⊗[R] B)) ⟶
      (cotangentComplexDerivedBaseChange R (CommAlgCat.of R A) (A ⊗[R] B))⟦(1 : ℤ)⟧}
    (h₁ : Triangle.mk u p d₁ ∈ distTriang _)
    {v : cotangentComplexDerivedBaseChange R (CommAlgCat.of R B) (A ⊗[R] B) ⟶
      cotangentComplexDerived R (CommAlgCat.of R (A ⊗[R] B))}
    {q : cotangentComplexDerived R (CommAlgCat.of R (A ⊗[R] B)) ⟶
      cotangentComplexDerived B (CommAlgCat.of B (A ⊗[R] B))}
    {d₂ : cotangentComplexDerived B (CommAlgCat.of B (A ⊗[R] B)) ⟶
      (cotangentComplexDerivedBaseChange R (CommAlgCat.of R B) (A ⊗[R] B))⟦(1 : ℤ)⟧}
    (h₂ : Triangle.mk v q d₂ ∈ distTriang _) :
    ∃ (E : DerivedCategory (ModuleCat.{max u v} (A ⊗[R] B)))
      (a : cotangentComplexDerived B (CommAlgCat.of B (A ⊗[R] B)) ⟶ E)
      (b : cotangentComplexDerived A (CommAlgCat.of A (A ⊗[R] B)) ⟶ E)
      (e₁ : E ⟶ (cotangentComplexDerivedBaseChange R (CommAlgCat.of R A) (A ⊗[R] B))⟦(1 : ℤ)⟧)
      (e₂ : E ⟶ (cotangentComplexDerivedBaseChange R (CommAlgCat.of R B) (A ⊗[R] B))⟦(1 : ℤ)⟧),
      Triangle.mk (u ≫ q) a e₁ ∈ distTriang _ ∧
      Triangle.mk (v ≫ p) b e₂ ∈ distTriang _ ∧
      q ≫ a = p ≫ b ∧ b ≫ e₁ = d₁ ∧ a ≫ e₂ = d₂

CommAlgCat.exists_canonical_tensorProduct_nine_diagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TensorProductNineDiagramCanonical.lean, line 206. The attribute's comment: “the diagram 92.15.0.1 on the canonical maps, with nothing assumed: the middle row and column are the fundamental triangles of Proposition 08QX for R → A → A ⊗_R B and R → B → A ⊗_R B, with the functoriality maps of Tag 08PN and their own connecting maps; the top-row and right-column first maps are the 08PN maps of the squares (R → B, A → A ⊗_R B) and (R → A, B → A ⊗_R B); the left and lower squares commute; and an object E makes the top row and the right column distinguished, with the upper right square commuting”.

Stacks 09D9, Equation 92.15.0.1, on the canonical maps. Let A and B be algebras over a ring R. In D(A ⊗_R B) consider

L_{A/R} ⊗^L_A (A ⊗_R B) ⟶ L_{A ⊗_R B/B}      ⟶ E
            ‖                     ↑                ↑
L_{A/R} ⊗^L_A (A ⊗_R B) ⟶ L_{A ⊗_R B/R}      ⟶ L_{A ⊗_R B/A}
                                  ↑                ↑
                      L_{B/R} ⊗^L_B (A ⊗_R B) ═ L_{B/R} ⊗^L_B (A ⊗_R B)

The middle row is the fundamental triangle of R → A → A ⊗_R B and the middle column is the fundamental triangle of R → B → A ⊗_R B. Both are distinguished, with the functoriality maps of Tag 08PN (CommAlgCat.fundamentalMor₁, CommAlgCat.fundamentalMor₂) and the connecting maps CommAlgCat.productFundamentalMor₃. The first map of the top row is the canonical map CommAlgCat.cotangentTensorProductBaseChangeMap, and the first map of the right column is CommAlgCat.cotangentTensorProductBaseChangeMapRight. The left and the lower squares commute. There is an object E in the upper right corner that makes the top row and the right column distinguished triangles, makes the upper right square commute, and has connecting maps that recover those of the middle row and the middle column.

theorem exists_canonical_tensorProduct_nine_diagram :
    Triangle.mk (fundamentalMor₁ R A (A ⊗[R] B)) (fundamentalMor₂ R A (A ⊗[R] B))
        (productFundamentalMor₃ R A (A ⊗[R] B)) ∈ distTriang _ ∧
    Triangle.mk (fundamentalMor₁ R B (A ⊗[R] B)) (fundamentalMor₂ R B (A ⊗[R] B))
        (productFundamentalMor₃ R B (A ⊗[R] B)) ∈ distTriang _ ∧
    fundamentalMor₁ R A (A ⊗[R] B) ≫ fundamentalMor₂ R B (A ⊗[R] B) =
      cotangentTensorProductBaseChangeMap R A B ∧
    fundamentalMor₁ R B (A ⊗[R] B) ≫ fundamentalMor₂ R A (A ⊗[R] B) =
      cotangentTensorProductBaseChangeMapRight R A B ∧
    ∃ (E : DerivedCategory (ModuleCat.{u} (A ⊗[R] B)))
      (a : cotangentComplexDerived B (CommAlgCat.of B (A ⊗[R] B)) ⟶ E)
      (b : cotangentComplexDerived A (CommAlgCat.of A (A ⊗[R] B)) ⟶ E)
      (e₁ : E ⟶ (cotangentComplexDerivedBaseChange R (CommAlgCat.of R A) (A ⊗[R] B))⟦(1 : ℤ)⟧)
      (e₂ : E ⟶ (cotangentComplexDerivedBaseChange R (CommAlgCat.of R B) (A ⊗[R] B))⟦(1 : ℤ)⟧),
      Triangle.mk (cotangentTensorProductBaseChangeMap R A B) a e₁ ∈ distTriang _ ∧
      Triangle.mk (cotangentTensorProductBaseChangeMapRight R A B) b e₂ ∈ distTriang _ ∧
      fundamentalMor₂ R B (A ⊗[R] B) ≫ a = fundamentalMor₂ R A (A ⊗[R] B) ≫ b ∧
      b ≫ e₁ = productFundamentalMor₃ R A (A ⊗[R] B) ∧
      a ≫ e₂ = productFundamentalMor₃ R B (A ⊗[R] B)

Tag 09DA, a lemma

Tag 09DA in the Stacks Project.

CommAlgCat.cotangentComplex_tensorProduct_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TensorProductTorIndependent.lean, line 544.

If A and B are Tor independent R-algebras, then the object E of Equation 92.15.0.1 — the cone of the map of complexes L_{A/R} ⊗_R B ⊕ L_{B/R} ⊗_R A ⟶ L_{A ⊗_R B/R} given by the functoriality maps — is zero; the canonical map L_{A/R} ⊗^L_A (A ⊗_R B) ⊕ L_{B/R} ⊗^L_B (A ⊗_R B) ⟶ L_{A ⊗_R B/R} is an isomorphism in D(A ⊗_R B); and this is represented by the complex L_{A/R} ⊗_R B ⊕ L_{B/R} ⊗_R A of A ⊗_R B-modules, the map of complexes being a quasi-isomorphism.

theorem cotangentComplex_tensorProduct_of_torIndependent
    (hTor : RingTheory.TorIndependence.TorIndependent R A B) :
    IsZero (tensorProductCotangentCone R A B) ∧
      IsIso (biprod.desc (cotangentTensorProductLeftMap R A B)
        (cotangentTensorProductRightMap R A B)) ∧
      QuasiIso (cotangentTensorProductComplexMap R A B)

Tag 09DB, a lemma

Tag 09DB in the Stacks Project.

CommAlgCat.isZero_homology_of_tensorProduct_nine_diagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TensorProductCohomology.lean, line 182. The attribute's comment: “the vanishing in degrees i ≥ 1 only, which is the exact ceiling of what the nine diagram of Tag 09D9 determines in this library. The source asserts it for i ≥ -1 and identifies H^{-2}(E) with Tor_1^R(A, B); neither is a consequence of the 09D9 conclusion as formalized here, because exists_tensorProduct_nine_diagram leaves the morphisms of the two fundamental triangles arbitrary -- its host file sits upstream of the proof of Tag 08QX and so cannot name the display's own map L_{A ⊗ B/R} ⟶ L_{A ⊗ B/A} -- and two distinguished triangles on the given objects do not pin those maps down to anything that fixes their homology. At i = 0 the long exact sequence leaves coker H^0(v ≫ p), which the abstract data does not force to vanish”.

The cohomology of the object E of the nine diagram of Tag 09D9 vanishes in degrees ≥ 1.

Only the middle column L_{B/R} ⊗^L_B (A ⊗_R B) ⟶ L_{A ⊗_R B/R} ⟶ L_{A ⊗_R B/B} and the right column L_{B/R} ⊗^L_B (A ⊗_R B) ⟶ L_{A ⊗_R B/A} ⟶ E of the diagram are used, together with the vanishing of the cohomology of a cotangent complex in positive degrees.

This is weaker than Tag 09DB, which asserts the vanishing in all degrees ≥ -1; see the module documentation for why the extra two degrees are not available from the nine diagram alone.

theorem isZero_homology_of_tensorProduct_nine_diagram
    (h₂ : Triangle.mk v q d₂ ∈ distTriang _)
    (hE₂ : Triangle.mk (v ≫ p) b e₂ ∈ distTriang _) (i : ℤ) (hi : 1 ≤ i) :
    IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} (A ⊗[R] B)) i).obj E)

CommAlgCat.tensorProduct_rightColumn_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TensorProductCohomologyCanonical.lean, line 145. The attribute's comment: “for every object E in a distinguished triangle on the canonical map L_{B/R} ⊗^L_B (A ⊗_R B) → L_{A ⊗_R B/A} of the right column of Equation 92.15.0.1, which is how the source's proof describes E: H^i(E) = 0 for i ≥ -1 and H^{-2}(E) ≅ Tor_1^R(A, B) as A ⊗_R B-modules, Tor_1 with its canonical module structure”.

Stacks 09DB, for every cone E of the canonical map L_{B/R} ⊗^L_B (A ⊗_R B) ⟶ L_{A ⊗_R B/A} of the right column of Equation 92.15.0.1: H^i(E) = 0 for i ≥ -1 and H^{-2}(E) ≅ Tor_1^R(A, B) as A ⊗_R B-modules.

theorem tensorProduct_rightColumn_homology
    (hE : Triangle.mk (cotangentTensorProductBaseChangeMapRight R A B) b e ∈ distTriang _) :
    (∀ i : ℤ, -1 ≤ i →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A ⊗[R] B)) i).obj E)) ∧
      Nonempty ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A ⊗[R] B)) (-2)).obj E ≅
        torOneTensorProductModule R A B)

CommAlgCat.canonicalTensorProductNineDiagram_upperRight_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/TensorProductCohomologyCanonical.lean, line 190. The attribute's comment: “the object E of the nine diagram of Tag 09D9, CommAlgCat.canonicalTensorProductNineDiagram: H^i(E) = 0 for i ≥ -1 and H^{-2}(E) ≅ Tor_1^R(A, B) as A ⊗_R B-modules, Tor_1 with its canonical module structure (CommAlgCat.torOneTensorProductModule); the isomorphism itself is CommAlgCat.homologyNegTwoCanonicalUpperRightIsoTorOne”.

Stacks 09DB. Let R be a ring and let A, B be R-algebras. The object E of Equation 92.15.0.1 satisfies H^i(E) = 0 for i ≥ -1 and H^{-2}(E) = Tor_1^R(A, B), the latter as an isomorphism of A ⊗_R B-modules.

theorem canonicalTensorProductNineDiagram_upperRight_homology :
    (∀ i : ℤ, -1 ≤ i →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A ⊗[R] B)) i).obj
        (canonicalTensorProductNineDiagram R A B).upperRight)) ∧
      Nonempty ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A ⊗[R] B)) (-2)).obj
          (canonicalTensorProductNineDiagram R A B).upperRight ≅
        torOneTensorProductModule R A B)

Sources

• Section 92.15, Tag 09D8
• AxiomMath/Stacks at 5ed82d14

LeanCommAlgCat.exists_tensorProduct_nine_diagram · CommAlgCat.exists_canonical_tensorProduct_nine_diagram · CommAlgCat.cotangentComplex_tensorProduct_of_torIndependent · CommAlgCat.isZero_homology_of_tensorProduct_nine_diagram · CommAlgCat.tensorProduct_rightColumn_homology · CommAlgCat.canonicalTensorProductNineDiagram_upperRight_homology

Section92.16 Deformations of ring maps and the cotangent complex#

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

Tag 08SN, an equation

Tag 08SN in the Stacks Project.

Stacks.Deformation.SquareZeroExtensionProblem.CompatibleExtension, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/SquareZero/Problem.lean, line 107. The attribute's comment: “the same extension problem diagram”.

A solution of a square-zero extension problem.

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

public structure CompatibleExtension (S : SquareZeroExtensionProblem)

Tag 08SP, a lemma

Tag 08SP in the Stacks Project.

Stacks.Deformation.SquareZeroExtensionProblem.isoFittingMapEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/CotangentAutomorphisms.lean, line 285. The attribute's comment: “automorphisms are the fitting maps of the self-comparison diagram”.

The automorphisms of a solution of a square-zero extension problem which induce the identity on B and on N are exactly the maps filling the diagram comparing the problem with itself.

noncomputable def isoFittingMapEquiv (X : S.CompatibleExtension.{w}) :
    CompatibleExtension.Iso X X ≃ (comparisonDiagram X X).FittingMap

Stacks.Deformation.SquareZeroExtensionProblem.automorphismsExtEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/CotangentAutomorphisms.lean, line 304. The attribute's comment: “automorphisms”. References: EGA 0 (20.1.4), “Commutative case”; SGA 7 VI (4.16), “(a), affine case”.

Stacks 08SP, part (3). For a solution B' of a square-zero extension problem, the automorphisms of B' inducing the identity on B and on N are canonically Ext⁰_B(L_{B/A}, N).

The equivalence carries the identity automorphism to 0 and composition to addition, so it is an isomorphism of groups, and the class attached to f is the one whose associated differential map sends d (b' mod N) to f(b') - b'.

noncomputable def automorphismsExtEquiv (X : S.CompatibleExtension.{w}) :
    {e : CompatibleExtension.Iso X X ≃ S.cotangentExt 0 //
      e (CompatibleExtension.Iso.refl X) = 0 ∧
      (∀ f g : CompatibleExtension.Iso X X, e (f.trans g) = e f + e g) ∧
      ∀ (f : CompatibleExtension.Iso X X) (b' : X.B'),
        ((X.kernelEquiv (S.cotangentExtZeroToHom (e f)
            (KaehlerDifferential.D S.A S.B (X.toB b'))) :
          RingHom.ker X.toB.toRingHom) : X.B') = f.toAlgEquiv b' - b'}

Stacks.Deformation.SquareZeroExtensionProblem.cotangentObstructionClass_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/CotangentObstruction.lean, line 111. The attribute's comment: “(1): there is a class in Ext²_B(L_{B/A}, N) whose vanishing is necessary and sufficient for the existence of a solution”.

Stacks 08SP, part (1). The class ξ ∈ Ext²_B(L_{B/A}, N) vanishes if and only if the square-zero extension problem has a solution.

theorem cotangentObstructionClass_eq_zero_iff :
    S.cotangentObstructionClass = 0 ↔ Nonempty (S.CompatibleExtension.{u})

Stacks.Deformation.SquareZeroExtensionProblem.isomorphismClassesCotangentTorsor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Deformation/RingThickening/CotangentTorsor.lean, line 50. The attribute's comment: “(2): if a solution exists, the isomorphism classes of solutions form a principal homogeneous space under Ext¹_B(L_{B/A}, N)”.

Stacks 08SP, part (2). If the square-zero extension problem has a solution, its set of isomorphism classes of solutions is a principal homogeneous space under Ext¹_B(L_{B/A}, N).

The action is that of Tag 08S7 under Ext¹_B(NL_{B/A}, N), read through the identification Ext¹_B(NL_{B/A}, N) = Ext¹_B(L_{B/A}, N) of cotangentExtOneEquiv.

noncomputable def isomorphismClassesCotangentTorsor
    (h : Nonempty (S.CompatibleExtension.{w})) :
    AddTorsor (S.cotangentExt 1)
      (CompatibleExtension.IsomorphismClasses.{u₁, u₂, max u₂ v, u₄, w} S)

Sources

• Section 92.16, Tag 08SM
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Deformation.SquareZeroExtensionProblem.CompatibleExtension · Stacks.Deformation.SquareZeroExtensionProblem.isoFittingMapEquiv · Stacks.Deformation.SquareZeroExtensionProblem.automorphismsExtEquiv · Stacks.Deformation.SquareZeroExtensionProblem.cotangentObstructionClass_eq_zero_iff · Stacks.Deformation.SquareZeroExtensionProblem.isomorphismClassesCotangentTorsor

Section92.17 The Atiyah class of a module#

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

Tag 09DD, an equation

Tag 09DD in the Stacks Project.

CommAlgCat.polynomialAtiyahTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClass.lean, line 282. The attribute's comment: “the triangle”.

Stacks 09DD. The Atiyah triangle of a B-module M: the image under Lπ_! : D(𝒪) ⟶ D(B) of the sequence of first principal parts of M on C_{B/A}.

def polynomialAtiyahTriangle :
    Triangle (DerivedCategory (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))))

CommAlgCat.polynomialAtiyahTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClass.lean, line 289. The attribute's comment: “the triangle is distinguished”.

Stacks 09DD. The Atiyah triangle is distinguished.

theorem polynomialAtiyahTriangle_distinguished :
    polynomialAtiyahTriangle A B M ∈ distinguishedTriangles

CommAlgCat.polynomialAtiyahClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClass.lean, line 303. The attribute's comment: “the Atiyah class, the last arrow of the triangle”.

Stacks 09DD. The Atiyah class of M: the last arrow of the Atiyah triangle.

def polynomialAtiyahClass :
    (polynomialAtiyahTriangle A B M).obj₃ ⟶ (polynomialAtiyahTriangle A B M).obj₁⟦(1 : ℤ)⟧

CommAlgCat.polynomialAtiyahTriangle_distinguished_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClass.lean, line 312. The attribute's comment: “the displayed triangle”.

Stacks 09DD. The Atiyah triangle written with its first and third terms replaced by objects identified with them: for L identified with Lπ_!(Ω_{𝒪/A} ⊗_𝒪 M) and N identified with Lπ_!(M), the sequence L ⟶ Lπ_!(P¹_{𝒪/A}(M)) ⟶ N ⟶ L[1] is a distinguished triangle, whose last arrow is the Atiyah class of M.

theorem polynomialAtiyahTriangle_distinguished_of_iso
    (L N : DerivedCategory (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))))
    (e₁ : (polynomialAtiyahTriangle A B M).obj₁ ≅ L)
    (e₃ : (polynomialAtiyahTriangle A B M).obj₃ ≅ N) :
    Triangle.mk (e₁.inv ≫ (polynomialAtiyahTriangle A B M).mor₁)
        ((polynomialAtiyahTriangle A B M).mor₂ ≫ e₃.hom)
        (e₃.inv ≫ (polynomialAtiyahTriangle A B M).mor₃ ≫
          (shiftFunctor (DerivedCategory (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))))
            (1 : ℤ)).map e₁.hom) ∈
      distinguishedTriangles

CommAlgCat.exists_atiyahDisplayedTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClassBigSiteDisplayed.lean, line 247. The attribute's comment: “the displayed triangle L_{B/A} ⊗^L_B M → Lπ_!(P¹(M)) → M → [1] at the site C_{B/A} itself, with both endpoint identifications proved rather than assumed”.

Stacks 09DD, the displayed triangle. For a ring map A → B and a B-module M there is an identification e₁ of the first term of the Atiyah triangle on the site C_{B/A} with L_{B/A} ⊗^𝐋_B M for which

L_{B/A} ⊗^𝐋_B M ⟶ Lπ_!(P¹_{𝒪/A}(M)) ⟶ M ⟶ (L_{B/A} ⊗^𝐋_B M)[1]

is a distinguished triangle, the third term being identified with M by the canonical CommAlgCat.polynomialAtiyahTriangleObj₃Iso.

Nothing is assumed: the first identification is CommAlgCat.nonempty_atiyahFirstVertexDerivedTensorIso, the chain of [Stacks, Tag 08PT] and [Tag 08PU] together with the universe-lift comparison of the sections of B̲ ⊗_𝒪 Ω_{𝒪/A}, and the third is [Tag 08QE] through Stacks.ChaoticSite.derivedColimitWithCoefficientsRestrictScalarsIso. It is e₁ that is existentially quantified rather than named, because the K-flat resolution computing the derived tensor product is chosen and not canonical.

theorem exists_atiyahDisplayedTriangle_distinguished :
    ∃ e₁ : (polynomialAtiyahTriangle A B M).obj₁ ≅ atiyahDisplayedObj₁ A B M,
      Triangle.mk (e₁.inv ≫ (polynomialAtiyahTriangle A B M).mor₁)
          ((polynomialAtiyahTriangle A B M).mor₂ ≫
            (polynomialAtiyahTriangleObj₃Iso A B M).hom)
          ((polynomialAtiyahTriangleObj₃Iso A B M).inv ≫
            (polynomialAtiyahTriangle A B M).mor₃ ≫
              (shiftFunctor
                (DerivedCategory (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))))
                (1 : ℤ)).map e₁.hom) ∈
        distinguishedTriangles

Tag 09DE, a definition

Tag 09DE in the Stacks Project.

CommAlgCat.polynomialAtiyahClassOfIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClass.lean, line 333. The attribute's comment: “the Atiyah class; the source's identifications Lπ_!(Ω_{𝒪/A} ⊗_𝒪 M) = L_{B/A} ⊗_B^L M (Tag 08PT) and Lπ_!(M) = M (Tag 08QE) are not available here, so they are carried as the extra hypotheses e₁ and e₃, which the source does not have”.

Stacks 09DE. The Atiyah class of M, in the form displayed by the source. For L identified with Lπ_!(Ω_{𝒪/A} ⊗_𝒪 M) and N identified with Lπ_!(M) this is the last arrow N ⟶ L[1] of the distinguished triangle of Tag 09DD. Under the source's identifications L = L_{B/A} ⊗_B^𝐋 M and N = M it is the Atiyah class M ⟶ L_{B/A} ⊗_B^𝐋 M[1]. That it is the last arrow of the displayed triangle is CommAlgCat.polynomialAtiyahClassOfIso_mem_distinguished.

def polynomialAtiyahClassOfIso
    (L N : DerivedCategory (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))))
    (e₁ : (polynomialAtiyahTriangle A B M).obj₁ ≅ L)
    (e₃ : (polynomialAtiyahTriangle A B M).obj₃ ≅ N) : N ⟶ L⟦(1 : ℤ)⟧

CommAlgCat.exists_atiyahDisplayedClass_mem_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/AtiyahClassBigSiteDisplayed.lean, line 292. The attribute's comment: “the Atiyah class M → (L_{B/A} ⊗^L_B M)[1] at the site C_{B/A} itself, as the last arrow of the displayed distinguished triangle of (92.17.0.1); both endpoint identifications are proved rather than assumed”.

Stacks 09DE, the Atiyah class of a module. For a ring map A → B and a B-module M there is an identification e₁ of the first term of the Atiyah triangle on the site C_{B/A} with L_{B/A} ⊗^𝐋_B M for which the Atiyah class of M,

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

is the last arrow of the distinguished triangle displayed by [Stacks, Tag 09DD]:

L_{B/A} ⊗^𝐋_B M ⟶ Lπ_!(P¹_{𝒪/A}(M)) ⟶ M ⟶ (L_{B/A} ⊗^𝐋_B M)[1].

The class itself is CommAlgCat.polynomialAtiyahClassOfIso, the last arrow Lπ_!(M̲) ⟶ Lπ_!(Ω_{𝒪/A} ⊗_𝒪 M̲)[1] of the Atiyah triangle read through identifications of the endpoints, instantiated at the displayed endpoints: the third by the canonical CommAlgCat.polynomialAtiyahTriangleObj₃Iso, [Stacks, Tag 08QE] at this site, and the first by e₁. Nothing is assumed — e₁ is produced inside the proof from CommAlgCat.nonempty_atiyahFirstVertexDerivedTensorIso, the chain of [Tag 08PT] and [Tag 08PU] at this site — and this is the whole of the definition: the arrow, its source M, its target (L_{B/A} ⊗^𝐋_B M)[1], and its being the last arrow of the triangle of (92.17.0.1).

e₁ is existentially quantified rather than named because the K-flat resolution computing the derived tensor product is chosen and not canonical, so there is no canonical identification of the first term to name. That costs nothing: by CommAlgCat.polynomialAtiyahClassOfIso_mem_distinguished the conclusion holds for every such identification, so the existential asserts only that one exists. The module documentation records why naming one by Classical.choice instead would fix a non-canonical choice.

theorem exists_atiyahDisplayedClass_mem_distinguished :
    ∃ e₁ : (polynomialAtiyahTriangle A B M).obj₁ ≅ atiyahDisplayedObj₁ A B M,
      Triangle.mk (e₁.inv ≫ (polynomialAtiyahTriangle A B M).mor₁)
          ((polynomialAtiyahTriangle A B M).mor₂ ≫
            (polynomialAtiyahTriangleObj₃Iso A B M).hom)
          (polynomialAtiyahClassOfIso A B M (atiyahDisplayedObj₁ A B M)
            ((DerivedCategory.singleFunctor
              (ModuleCat.{u + 1} (ULift.{u + 1} (B : Type u))) 0).obj M) e₁
            (polynomialAtiyahTriangleObj₃Iso A B M)) ∈
        distinguishedTriangles

Sources

• Section 92.17, Tag 09DC
• AxiomMath/Stacks at 5ed82d14

LeanCommAlgCat.polynomialAtiyahTriangle · CommAlgCat.polynomialAtiyahTriangle_distinguished · CommAlgCat.polynomialAtiyahClass · CommAlgCat.polynomialAtiyahTriangle_distinguished_of_iso · CommAlgCat.exists_atiyahDisplayedTriangle_distinguished · CommAlgCat.polynomialAtiyahClassOfIso · CommAlgCat.exists_atiyahDisplayedClass_mem_distinguished

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.