20.22 Cohomology on spectral… to 20.33 Unbounded Mayer-Vietoris

Section20.22 Cohomology on spectral spaces#

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

Tag 0A3D, a lemma

Tag 0A3D in the Stacks Project.

Stacks.Topology.isIso_cohomologyOfGeneralizationsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CompactSubset/GeneralizationsOfCohomology.lean, line 534. The attribute's comment: “cohomology_of_neighbourhoods”.

Let X be a spectral space, let F be an abelian sheaf on X, let E ⊆ X be quasi-compact and let W be the set of points of X which specialize to a point of E. Then for every p the canonical map

colim_{E ⊆ U quasi-compact open} H^p(U, F) ⟶ H^p(W, F|_W)

is an isomorphism.

theorem isIso_cohomologyOfGeneralizationsMap (hE : IsCompact E)
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}) (p : ℕ) :
    IsIso (cohomologyOfGeneralizationsMap E F p)

Stacks.Topology.isIso_cohomologyOfComplementGeneralizationsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CompactSubset/GeneralizationsOfComplementCohomology.lean, line 340. The attribute's comment: “cohomology_of_complements”.

[Stacks, Tag 0A3D] (2). Let X be a spectral space, let F be an abelian sheaf on X, let E ⊆ X be quasi-compact and constructible and let W be the set of points of X which specialize to a point of E. Then for every p the canonical map

colim_{E ⊆ U quasi-compact open} H^p(U \ E, F|_{U \ E}) ⟶ H^p(W \ E, F|_{W \ E})

is an isomorphism.

theorem isIso_cohomologyOfComplementGeneralizationsMap (hE : Topology.IsConstructible E)
    (hEc : IsCompact E) (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}) (p : ℕ) :
    IsIso (cohomologyOfComplementGeneralizationsMap E F p)
Tag 0A3E, a lemma

Tag 0A3E in the Stacks Project.

Stacks.Topology.higherDirectImageStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CompactSubset/HigherDirectImageStalk.lean, line 369.

Let f : X ⟶ Y be a spectral map of spectral spaces, let y be a point of Y, let E be the set of points of Y specializing to y and let F be a sheaf of abelian groups on X. Then for every p the stalk at y of the p-th higher direct image of F is the p-th cohomology of the restriction of F to f⁻¹(E):

(R^p f_* F)_y = H^p(f⁻¹(E), F|_{f⁻¹(E)}).

Here f⁻¹(E) is Stacks.Topology.specializationFiber f y, the set of points of X whose image specializes to y, and cohomology is the right derived functor of global sections.

def higherDirectImageStalkIso (hf : IsSpectralMap f) (p : ℕ)
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}) :
    ((pushforwardSheafFunctor f).rightDerived p ⋙ sheafStalkFunctor y).obj F ≅
      ((sectionsFunctor (TopCat.of (specializationFiber f y))).rightDerived p).obj
        ((restrictionFunctor X (specializationFiber f y)).obj F)
Tag 0A3F, a lemma

Tag 0A3F in the Stacks Project.

Stacks.CohomologyVanishing.cohomology_subsingleton_of_isProfiniteStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/AboveTheDimension.lean, line 352. The attribute's comment: “sheaf cohomology as Ext out of the constant sheaf”.

Stacks 0A3F. On a profinite space every positive-degree sheaf cohomology group of every abelian sheaf vanishes.

Global sections is exact on a profinite space, because local lifts along a cover may be refined to lifts along a disjoint finite clopen cover (Stacks 08ZZ) and those glue with no compatibility to check. Sheaf cohomology is Ext out of the constant sheaf ℤ, and the constant-sheaf functor is left adjoint to global sections, so exactness of global sections makes that constant sheaf projective and every Ext out of it vanishes in positive degree.

This is the Sheaf.H (that is, Ext) formulation; the right-derived-functor formulation is Stacks.CohomologyVanishing.isZero_abelianSheafCohomology_of_isProfiniteStacks.

theorem cohomology_subsingleton_of_isProfiniteStacks
    [HasSheafify (Opens.grothendieckTopology X) AddCommGrpCat.{w}]
    [HasExt.{w'} (Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{w})]
    (hX : IsProfiniteStacks X)
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{w})
    (q : ℕ) (hq : 0 < q) : Subsingleton (Sheaf.H.{w', w, u, u} F q)

Stacks.CohomologyVanishing.isZero_abelianSheafCohomology_of_isProfiniteStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/ProfiniteSpaces.lean, line 184.

Stacks 0A3F. If X is profinite, then every positive-degree cohomology group of every abelian sheaf on X is zero.

theorem isZero_abelianSheafCohomology_of_isProfiniteStacks
    [(Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (hX : IsProfiniteStacks X)
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{w})
    (q : ℕ) (hq : 0 < q) :
    IsZero (abelianSheafCohomology q F)
Tag 0A3G, a proposition

Tag 0A3G in the Stacks Project.

Stacks.CohomologyVanishing.cohomology_subsingleton_of_topologicalKrullDim_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/AboveTheDimension.lean, line 767. The attribute's comment: “clause (1) for dimension zero”.

Stacks 0A3G, clause (1) in dimension zero. Let X be a spectral space of Krull dimension 0 and let F be an abelian sheaf on X. Then H^q(X, F) = 0 for every q > 0.

This is the base case of the induction on the dimension in Stacks 0A3G: a zero-dimensional spectral space is profinite (isProfiniteStacks_of_topologicalKrullDim_eq_zero), and on a profinite space positive-degree cohomology vanishes (cohomology_subsingleton_of_isProfiniteStacks).

The hypotheses are satisfiable: X = Spec R for a zero-dimensional ring such as a field, a finite product of fields, or ZMod 4, has topologicalKrullDim X = 0, and the conclusion is then a genuine statement about every abelian sheaf on a nontrivial space.

theorem cohomology_subsingleton_of_topologicalKrullDim_eq_zero
    [HasSheafify (Opens.grothendieckTopology X) AddCommGrpCat.{w}]
    [HasExt.{w'} (Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{w})]
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{w})
    (q : ℕ) (hX : topologicalKrullDim X = ((0 : ℕ) : WithBot ℕ∞)) (hq : 0 < q) :
    Subsingleton (Sheaf.H.{w', w, u, u} F q)

Stacks.CohomologyVanishing.subsingleton_sheafH_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/SpectralSpaces.lean, line 203. The attribute's comment: “clause (1): on a spectral space, sheaf cohomology vanishes above the dimension”.

Let Y be a spectral space of Krull dimension at most d and let G be an abelian sheaf on Y. Then H^q(Y, G) = 0 for every q > d.

theorem subsingleton_sheafH_of_topologicalKrullDim_le :
    ∀ (d : ℕ) (Y : Type u) [TopologicalSpace Y] [SpectralSpace Y]
      (_hs : HasSheafify (Opens.grothendieckTopology Y) AddCommGrpCat.{u})
      (_he : HasExt.{u} (Sheaf (Opens.grothendieckTopology Y) AddCommGrpCat.{u}))
      (G : Sheaf (Opens.grothendieckTopology Y) AddCommGrpCat.{u}) (q : ℕ),
      topologicalKrullDim Y ≤ (d : WithBot ℕ∞) → d < q →
        Subsingleton (Sheaf.H.{u, u, u, u} G q)

Stacks.CohomologyVanishing.subsingleton_sheafH_above_topologicalKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/SpectralSpaces.lean, line 242. The attribute's comment: “clause (1): on a spectral space of Krull dimension at most d, sheaf cohomology vanishes in every degree above d. The same statement as the induction carrier subsingleton_sheafH_of_topologicalKrullDim_le, whose explicit HasSheafify and HasExt arguments are instance arguments here”.

Let Y be a spectral space of Krull dimension at most d and let G be an abelian sheaf on Y. Then H^q(Y, G) = 0 for every q > d.

theorem subsingleton_sheafH_above_topologicalKrullDim {Y : Type u} [TopologicalSpace Y]
    [SpectralSpace Y]
    [HasSheafify (Opens.grothendieckTopology Y) AddCommGrpCat.{u}]
    [HasExt.{u} (Sheaf (Opens.grothendieckTopology Y) AddCommGrpCat.{u})]
    (G : Sheaf (Opens.grothendieckTopology Y) AddCommGrpCat.{u}) (d q : ℕ)
    (hdim : topologicalKrullDim Y ≤ (d : WithBot ℕ∞)) (hq : d < q) :
    Subsingleton (Sheaf.H.{u, u, u, u} G q)

Stacks.CohomologyVanishing.surjective_cohomologyPresheaf_map_top_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/SpectralSpaces.lean, line 310. The attribute's comment: “clause (2): surjectivity of the restriction H^d(X,F) → H^d(U,F) for U quasi-compact open”.

Let X be a spectral space of Krull dimension at most d and let F be an abelian sheaf on X. Then the restriction H^d(X, F) → H^d(U, F) is surjective for every quasi-compact open U ⊆ X.

theorem surjective_cohomologyPresheaf_map_top_of_topologicalKrullDim_le
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}) (d : ℕ)
    (hdim : topologicalKrullDim X ≤ (d : WithBot ℕ∞)) (U : Opens X)
    (hU : IsCompact (U : Set X)) :
    Function.Surjective
      ((F.cohomologyPresheaf d).map (homOfLE (show U ≤ ⊤ from le_top)).op)

Stacks.CohomologyVanishing.subsingleton_sheafH_and_surjective_and_subsingleton_supported_of_topologicalKrullDim_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/SpectralSpacesFullStatement.lean, line 91. The attribute's comment: “the whole proposition: (1) sheaf cohomology on a spectral space of Krull dimension d vanishes above degree d, (2) restriction to a quasi-compact open is surjective in degree d, and (3) cohomology with support in a constructible closed subset vanishes above degree d”.

[Stacks, Tag 0A3G]. Let X be a spectral space of Krull dimension d and let F be an abelian sheaf on X. Then

  1. H^q(X, F) = 0 for q > d;
  2. H^d(X, F) ⟶ H^d(U, F) is surjective for every quasi-compact open U ⊆ X;
  3. H^q_Z(X, F) = 0 for q > d and every constructible closed subset Z ⊆ X.

Cohomology is Mathlib's CategoryTheory.Sheaf.H, the Ext-groups out of the constant abelian sheaf ℤ on the site of opens; cohomology over an open is the value of CategoryTheory.Sheaf.cohomologyPresheaf, so that clause (2) is a statement about the restriction map of that presheaf; and cohomology with support in Z is the right derived functor of the sections over X of the subsheaf of sections supported on Z.

Each clause is proved in the file named beside it below, where it is proved under the weaker hypothesis that d bounds the dimension rather than equalling it. Here they are put together under the source's hypothesis.

theorem subsingleton_sheafH_and_surjective_and_subsingleton_supported_of_topologicalKrullDim_eq
    {X : TopCat.{u}} [SpectralSpace X]
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}) (d : ℕ)
    (hdim : topologicalKrullDim X = (d : WithBot ℕ∞)) :
    (∀ q : ℕ, d < q → Subsingleton (Sheaf.H.{u, u, u, u} F q)) ∧
      (∀ U : Opens X, IsCompact (U : Set X) → Function.Surjective
        ((F.cohomologyPresheaf d).map (homOfLE (show U ≤ ⊤ from le_top)).op)) ∧
      (∀ Z : Set X, IsClosed Z → IsConstructible Z → ∀ q : ℕ, d < q →
        Subsingleton (((supportedSectionsEvaluation Z ⊤).rightDerived q).obj F))

Stacks.CohomologyVanishing.subsingleton_rightDerived_supportedSections_of_topologicalKrullDim_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Vanishing/SpectralSupportVanishing.lean, line 130. The attribute's comment: “clause (3): cohomology with support in a constructible closed subset vanishes above the dimension”.

[Stacks, Tag 0A3G], clause (3). Let X be a spectral space of Krull dimension at most d, let F be an abelian sheaf on X and let Z be a constructible closed subset of X. Then the cohomology of F with support in Z vanishes in every degree q > d.

Cohomology with support in Z is the right derived functor of the sections over X of the subsheaf of sections supported on Z. The proof is the source's: the long exact sequence of the pair (X, X ∖ Z), built on an injective resolution, together with clause (1) for H^q(X, F) and clause (2) for the surjectivity of H^{q-1}(X, F) → H^{q-1}(X ∖ Z, F), the complement of a constructible closed set being a quasi-compact open.

theorem subsingleton_rightDerived_supportedSections_of_topologicalKrullDim_le
    [SpectralSpace X]
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}) (d q : ℕ)
    (hdim : topologicalKrullDim X ≤ (d : WithBot ℕ∞)) (Z : Set X) (hZ : IsClosed Z)
    (hZc : IsConstructible Z) (hq : d < q) :
    Subsingleton (((supportedSectionsEvaluation Z ⊤).rightDerived q).obj F)
Sources
LeanStacks.Topology.isIso_cohomologyOfGeneralizationsMap · Stacks.Topology.isIso_cohomologyOfComplementGeneralizationsMap · Stacks.Topology.higherDirectImageStalkIso · Stacks.CohomologyVanishing.cohomology_subsingleton_of_isProfiniteStacks · Stacks.CohomologyVanishing.isZero_abelianSheafCohomology_of_isProfiniteStacks · Stacks.CohomologyVanishing.cohomology_subsingleton_of_topologicalKrullDim_eq_zero · Stacks.CohomologyVanishing.subsingleton_sheafH_of_topologicalKrullDim_le · Stacks.CohomologyVanishing.subsingleton_sheafH_above_topologicalKrullDim

Section20.23 The alternating Čech complex#

Section 20.23 of the Stacks Project, Tag 01FG. 7 tags here are carried by 27 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01FG, the section

Tag 01FG in the Stacks Project.

CechCochains.alternatingSubgroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingCochainGroups.lean, line 193. The attribute's comment: “the group Č_alt^p(𝒰, ℱ) of alternating cochains”.

The alternating cochains form a subgroup Č_alt^p ⊆ Č^p.

def alternatingSubgroup (p : ℕ) : AddSubgroup (Cochain U ℱ p)

CechCochains.cechD_mem_alternating, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingCochainGroups.lean, line 687. The attribute's comment: “d maps Č_alt^p into Č_alt^{p+1}, the verification the source omits”.

The differential cechD preserves the alternating subgroup, so the latter is a subcomplex of the full Čech complex.

theorem cechD_mem_alternating (p : ℕ) (s : Cochain U ℱ p) (hs : IsAlternating U ℱ s) :
    IsAlternating U ℱ (cechD U ℱ p s)
Tag 01FH, a definition

Tag 01FH in the Stacks Project.

Stacks.Cech.alternatingCechComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingComplex.lean, line 129. References: EGA 0 (12.1.2), “alternating Čech complex”.

Stacks 01FH. The alternating Čech complex associated to an abelian presheaf and an indexed family of open subsets.

noncomputable def alternatingCechComplex : CochainComplex Ab ℕ

Stacks.Cech.alternatingCechInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingComplex.lean, line 153. The attribute's comment: “the canonical inclusion”.

Stacks 01FH. The canonical inclusion of the alternating Čech complex into the usual Čech complex: in each degree it is the inclusion of the subgroup of alternating cochains.

noncomputable def alternatingCechInclusion :
    alternatingCechComplex U ℱ ⟶ cechComplex U ℱ
Tag 01FI, a definition

Tag 01FI in the Stacks Project.

Stacks.Cech.orderedCechComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/OrderedComplex.lean, line 57.

The ordered Čech cochain complex of an abelian presheaf with respect to a linearly ordered family of open subsets.

noncomputable def orderedCechComplex (U : I → Opens X)
    (ℱ : TopCat.Presheaf AddCommGrpCat.{w} X) :
    CochainComplex AddCommGrpCat.{max v w} ℕ
Tag 01FJ, a lemma

Tag 01FJ in the Stacks Project.

CechCochains.cAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingCochainGroups.lean, line 498. The attribute's comment: “the degreewise isomorphism”.

(3) [Stacks, Tag 01FJ], the degreewise clause. In every degree, c corestricted to the alternating subgroup is an isomorphism of abelian groups Č_ord^p ≃+ Č_alt^p, with inverse the projection π.

This is the degreewise statement only: it says nothing about the differentials. That c commutes with them is c_chainMap, and the two clauses are assembled into the isomorphism of cochain complexes the source asserts by Stacks.Cech.orderedIsoAlternatingCechComplex.

noncomputable def cAddEquiv (p : ℕ) : OrdCochain U ℱ p ≃+ alternatingSubgroup U ℱ p

CechCochains.c_chainMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingCochainGroups.lean, line 803. The attribute's comment: “c is a morphism of complexes”.

(1) [Stacks, Tag 01FJ], the chain-map clause. c is a chain map: c ∘ d = d ∘ c.

This is the first half of what the source asserts about c; the degreewise bijectivity is cAddEquiv, and Stacks.Cech.orderedIsoAlternatingCechComplex assembles the two into the isomorphism of cochain complexes Č_ord^• → Č_alt^•.

theorem c_chainMap (p : ℕ) (s : OrdCochain U ℱ p) :
    c U ℱ (p + 1) (ordD U ℱ p s) = cechD U ℱ p (c U ℱ p s)

Stacks.Cech.orderedIsoAlternatingCechComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/OrderedAlternatingComparison.lean, line 91. The attribute's comment: “the induced isomorphism of complexes”.

The ordered Čech complex is the alternating Čech complex. The degreewise comparison of Stacks 01FJ is an isomorphism of cochain complexes, because CechCochains.c is a chain map.

This is the second assertion of the source: the degreewise isomorphism CechCochains.cAddEquiv and the chain-map property CechCochains.c_chainMap together induce an isomorphism of the complexes themselves.

def orderedIsoAlternatingCechComplex :
    orderedCechComplex U ℱ ≅ alternatingCechComplex U ℱ
Tag 01FK, a lemma

Tag 01FK in the Stacks Project.

Stacks.CategoryTheory.CechComplex.Alternating.cechProj_comp_cechDiff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternating.lean, line 579. The attribute's comment: “(1)”.

The projection π : C^• → C^•_ord is a morphism of complexes: it commutes with the differentials, π ∘ d = d ∘ π.

theorem cechProj_comp_cechDiff (P : Cᵒᵖ ⥤ AddCommGrpCat.{w'}) (U : ι → C) (p : ℕ) :
    (Alternating.cechProj P U (p+1)).comp (Alternating.cechDiff P U p)
      = (Alternating.cechDiffOrd P U p).comp (Alternating.cechProj P U p)

Stacks.CategoryTheory.CechComplex.Alternating.cechProj_comp_cechComp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternating.lean, line 587. The attribute's comment: “(3)”.

π is a left inverse to the comparison map c: π ∘ c = id on the ordered cochains.

theorem cechProj_comp_cechComp (P : Cᵒᵖ ⥤ AddCommGrpCat.{w'}) (U : ι → C) (p : ℕ) :
    (Alternating.cechProj P U p).comp (Alternating.cechComp P U p) =
      AddMonoidHom.id (Alternating.CechCochainOrd P U p)

Stacks.CategoryTheory.CechComplex.Alternating.cechProjAltEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternating.lean, line 626. The attribute's comment: “(2)”.

The restriction of the projection to the alternating cochains, π : C^•_alt → C^•_ord, is an isomorphism of abelian groups in each degree, with inverse the comparison map c.

noncomputable def cechProjAltEquiv (P : Cᵒᵖ ⥤ AddCommGrpCat.{w'}) (U : ι → C) (p : ℕ) :
    Alternating.CechCochainAlt P U p ≃+ Alternating.CechCochainOrd P U p

Stacks.CategoryTheory.CechComplex.Alternating.cechProjAlt_comp_cechDiffAlt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternating.lean, line 639. The attribute's comment: “(2)”.

The isomorphism π : C^•_alt → C^•_ord commutes with the differentials, hence is an isomorphism of complexes. Equivalently, the comparison map c : C^•_ord → C^•_alt is a morphism of complexes (c ∘ d_ord = d_alt ∘ c), exhibiting c as the inverse morphism of complexes.

theorem cechProjAlt_comp_cechDiffAlt (P : Cᵒᵖ ⥤ AddCommGrpCat.{w'}) (U : ι → C)
    (hU : ∀ i, IsSubterminal (U i)) (p : ℕ) :
    (Alternating.cechProjAlt P U (p+1)).comp (Alternating.cechDiffAlt P U hU p)
      = (Alternating.cechDiffOrd P U p).comp (Alternating.cechProjAlt P U p)

Stacks.CategoryTheory.CechComplex.Alternating.cechProjAltComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternatingHomotopy.lean, line 826. The attribute's comment: “(2) as an isomorphism of complexes”.

[Stacks, Tag 01FK] (2) as an isomorphism of complexes. The projection π from the alternating to the ordered Čech cochains is an isomorphism of complexes.

def cechProjAltComplexIso (hU : ∀ i, IsSubterminal (U i)) :
    cechCochainComplexAlt P U hU ≅ cechCochainComplexOrd P U

cechProj_comp_cechDiff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingProjection.lean, line 665. The attribute's comment: “(1)”.

Statement 1. The projection π : C^• → C^•_ord is a morphism of complexes: each π in degree p is a homomorphism of abelian groups (built into cechProj) and it commutes with the differentials, π ∘ d = d ∘ π.

theorem cechProj_comp_cechDiff (F : AbelianPresheaf X) (U : I → Opens X) (p : ℕ) :
    (cechProj F U (p+1)).comp (cechDiff F U p)
      = (cechDiffOrd F U p).comp (cechProj F U p)

cechProj_comp_cechComp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingProjection.lean, line 675. The attribute's comment: “(3)”.

Statement 3 (left inverse). π is a left inverse to the comparison map c: π ∘ c = id on the ordered complex. (For a strictly increasing tuple the sorting permutation is the identity, so c(s) agrees with s there.)

theorem cechProj_comp_cechComp (F : AbelianPresheaf X) (U : I → Opens X) (p : ℕ) :
    (cechProj F U p).comp (cechComp F U p) = AddMonoidHom.id (CechCochainOrd F U p)

cechProjAltEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingProjection.lean, line 716. The attribute's comment: “(2)”.

Statement 2. The restriction of the projection to the alternating subcomplex, π : C^•_alt → C^•_ord, is an isomorphism of abelian groups in each degree, with inverse the comparison map c. (Together with Statement 2 below — that this isomorphism commutes with the differentials — this is the asserted isomorphism of complexes.)

noncomputable def cechProjAltEquiv (F : AbelianPresheaf X) (U : I → Opens X) (p : ℕ) :
    CechCochainAlt F U p ≃+ CechCochainOrd F U p

cechProjAlt_comp_cechDiffAlt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingProjection.lean, line 729. The attribute's comment: “(2)”.

Statement 2 (isomorphism of complexes). The isomorphism π : C^•_alt → C^•_ord commutes with the differentials, hence is an isomorphism of complexes. Equivalently, the comparison map c : C^•_ord → C^•_alt is a morphism of complexes (c ∘ d_ord = d_alt ∘ c), exhibiting c as the inverse morphism of complexes.

theorem cechProjAlt_comp_cechDiffAlt (F : AbelianPresheaf X) (U : I → Opens X) (p : ℕ) :
    (cechProjAlt F U (p+1)).comp (cechDiffAlt F U p)
      = (cechDiffOrd F U p).comp (cechProjAlt F U p)
Tag 01FM, a lemma

Tag 01FM in the Stacks Project.

Crystalline.GlobalCrystallineSituation.SmallSite.CrystallineThickening.restrictCechAltInclusionHomotopyEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/OrdCechRestrictCover.lean, line 221. The attribute's comment: “for a restriction cover of an object of the small crystalline site”.

[Stacks, Tag 01FM] for a restriction cover of an object of Cris(X/S). The canonical inclusion of the alternating Čech cochain complex of the cover into the full Čech cochain complex is a homotopy equivalence; signed sorting is a homotopy inverse.

The family of opens is arbitrary: it need not cover the ambient scheme, exactly as at the space level. The hypothesis of the lifted theory is discharged by isSubterminal_ambientOpen and nothing is assumed here.

def restrictCechAltInclusionHomotopyEquiv :
    HomotopyEquiv (restrictCechComplexAlt A V F) (restrictCechComplex A V F)

Crystalline.GlobalCrystallineSituation.SmallSite.CrystallineThickening.restrictCechAltInclusion_homotopyEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Crystalline/SmallSite/OrdCechRestrictCover.lean, line 229. The attribute's comment: “a restriction cover's alternating inclusion lies in homotopyEquivalences”.

[Stacks, Tag 01FM] for a restriction cover of an object of Cris(X/S), in the homotopyEquivalences morphism-property spelling.

theorem restrictCechAltInclusion_homotopyEquivalence :
    (HomologicalComplex.homotopyEquivalences AddCommGrpCat.{max w w'} (ComplexShape.up ℕ))
      (restrictCechAltInclusion A V F)

Stacks.CategoryTheory.CechComplex.Alternating.cechAltHomotopyEquivCechComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternatingComparison.lean, line 160. The attribute's comment: “in the cechComplexFunctor model”.

[Stacks, Tag 01FM] in the cechComplexFunctor model. The alternating Čech cochain complex of a family of subterminal objects is homotopy equivalent to the Čech complex of the family.

def cechAltHomotopyEquivCechComplex (hU : ∀ i, IsSubterminal (U i)) :
    HomotopyEquiv (cechCochainComplexAlt P U hU) ((cechComplexFunctor U).obj P)

Stacks.CategoryTheory.CechComplex.Alternating.cechComparisonProjectionHomotopy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternatingHomotopy.lean, line 725. The attribute's comment: “c after projection is homotopic to the identity”.

[Stacks, Tag 01FM] for a family in an arbitrary category, chain-level form. An explicit homotopy from the endomorphism c ∘ π to the identity of the full Čech cochain complex. Its component from degree j + 1 to degree j is cochainHomotopy.

def cechComparisonProjectionHomotopy (hU : ∀ i, IsSubterminal (U i)) :
    Homotopy (cechComparisonProjection P U hU) (𝟙 (cechCochainComplex P U))

Stacks.CategoryTheory.CechComplex.Alternating.cechAltInclusionHomotopyEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternatingHomotopy.lean, line 756. The attribute's comment: “the canonical inclusion is a homotopy equivalence”. References: EGA 0 (11.8.7), “more general”.

[Stacks, Tag 01FM] for a family in an arbitrary category. The canonical inclusion of the alternating Čech cochain complex into the full Čech cochain complex is a homotopy equivalence; signed sorting c ∘ π, corestricted to the alternating cochains, is a homotopy inverse. The family need not cover anything.

def cechAltInclusionHomotopyEquiv (hU : ∀ i, IsSubterminal (U i)) :
    HomotopyEquiv (cechCochainComplexAlt P U hU) (cechCochainComplex P U)

Stacks.CategoryTheory.CechComplex.Alternating.cechAltInclusion_homotopyEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechComplexAlternatingHomotopy.lean, line 790. The attribute's comment: “the canonical inclusion lies in homotopyEquivalences”.

[Stacks, Tag 01FM] for a family in an arbitrary category, in the homotopyEquivalences morphism-property spelling.

theorem cechAltInclusion_homotopyEquivalence (hU : ∀ i, IsSubterminal (U i)) :
    (HomologicalComplex.homotopyEquivalences AddCommGrpCat.{max w w'} (ComplexShape.up ℕ))
      (cechAltInclusion P U hU)

Stacks.Cech.cechComparisonProjection_homotopic_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingHomotopyEquivalence.lean, line 110. The attribute's comment: “c after projection is homotopic to the identity”.

The endomorphism c ∘ π is homotopic to the identity on the usual Čech complex.

theorem cechComparisonProjection_homotopic_id :
    Nonempty (Homotopy (cechComparisonProjection U F)
      (𝟙 (cechComplex U F)))

Stacks.Cech.alternatingCechInclusion_homotopyEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AlternatingHomotopyEquivalence.lean, line 143. The attribute's comment: “the canonical inclusion is a homotopy equivalence”.

The canonical inclusion of alternating Čech cochains into the usual Čech complex is a homotopy equivalence: the signed-sorting projection is a homotopy inverse.

theorem alternatingCechInclusion_homotopyEquivalence
    (G : TopCat.Presheaf Ab.{max v w} X) :
    (HomologicalComplex.homotopyEquivalences AddCommGrpCat (ComplexShape.up ℕ))
      (alternatingCechInclusion U G)
Tag 0G6T, a lemma

Tag 0G6T in the Stacks Project.

Stacks.Cech.alternatingCechComplex_augment_homotopyEquiv_zero_of_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AugmentationContractible.lean, line 652. The attribute's comment: “alternating complex”.

If a family of opens contained in U contains U, its extended alternating Čech complex is homotopy equivalent to zero.

lemma alternatingCechComplex_augment_homotopyEquiv_zero_of_eq
    (X : TopCat.{u}) (F : TopCat.Presheaf Ab.{w} X)
    {I : Type v} {U : Opens X} (V : I → Opens X) (hV : ∀ i, V i ≤ U)
    (i : I) (hi : V i = U) :
    ∃ (w : alternatingCechAugmentation X F V hV ≫
        (alternatingCechComplex V F).d 0 1 = 0),
      Nonempty (HomotopyEquiv
        ((alternatingCechComplex V F).augment
          (alternatingCechAugmentation X F V hV) w)
        (HomologicalComplex.zero : CochainComplex Ab.{max v w} ℕ))

Stacks.Cech.orderedCechComplex_augment_homotopyEquiv_zero_of_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/AugmentationContractible.lean, line 681. The attribute's comment: “ordered complex”.

For any ordering, if a family of opens contained in U contains U, its extended ordered Čech complex is homotopy equivalent to zero.

lemma orderedCechComplex_augment_homotopyEquiv_zero_of_eq
    (X : TopCat.{u}) (F : TopCat.Presheaf Ab.{w} X)
    {I : Type v} [LinearOrder I] {U : Opens X} (V : I → Opens X) (hV : ∀ i, V i ≤ U)
    (i : I) (hi : V i = U) :
    ∃ (w : orderedCechAugmentation X F V hV ≫
        (orderedCechComplex V F).d 0 1 = 0),
      Nonempty (HomotopyEquiv
        ((orderedCechComplex V F).augment
          (orderedCechAugmentation X F V hV) w)
        (HomologicalComplex.zero : CochainComplex Ab.{max v w} ℕ))
Sources
LeanCechCochains.alternatingSubgroup · CechCochains.cechD_mem_alternating · Stacks.Cech.alternatingCechComplex · Stacks.Cech.alternatingCechInclusion · Stacks.Cech.orderedCechComplex · CechCochains.cAddEquiv · CechCochains.c_chainMap · Stacks.Cech.orderedIsoAlternatingCechComplex

Section20.24 Alternative view of the Čech complex#

Section 20.24 of the Stacks Project, Tag 02FR. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02FU, a lemma

Tag 02FU in the Stacks Project.

Stacks.AlgebraicGeometry.CoveringResolutionQuasiIso.exists_coveringResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoveringResolutionQuasiIso/Main.lean, line 153.

Stacks Project, Tag 02FU. Every open covering of a ringed space gives a canonical augmented Čech resolution, functorial in the module sheaf: the complex, its augmentation, the product coordinates of its terms with Equation 01EE for the differential, the existence of homology, and the quasi-isomorphism.

theorem exists_coveringResolution (hU : ⨆ i, U i = ⊤) :
    Nonempty (CoveringResolution.{u, v, w, t} X R U)
Tag 02FS, a definition

Tag 02FS in the Stacks Project.

Declarations registered for the tag:

Tag 02FT, a remark

Tag 02FT in the Stacks Project.

Stacks.LocallyFiniteCover.isColimitCofanProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/LocallyFiniteCoproductSections.lean, line 393. The attribute's comment: “(second displayed formula: ⨁ (j_i)_ F_i = ∏ (j_i)_ F_i)”.

Stacks Project, Tag 02FT, second displayed formula. Let X = ⋃ i, U i be a locally finite open covering of a topological space, let j i : U i → X be the inclusions and let F i be an abelian sheaf on U i. Then the product of the (j i)_* (F i), equipped with the canonical injections deltaInj, is a coproduct of the (j i)_* (F i): that is ⨁ i, (j i)_* (F i) = ∏ i, (j i)_* (F i).

noncomputable def isColimitCofanProduct (_hcov : IsOpenCover U)
    (hlf : LocallyFinite fun i => (U i : Set X)) : IsColimit (productCofan U F)

Stacks.LocallyFiniteCover.isIso_coproductToProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/LocallyFiniteCoproductSections.lean, line 431. The attribute's comment: “(second displayed formula, as an isomorphism from ∐ to ∏)”.

Stacks Project, Tag 02FT, second displayed formula. For a locally finite open covering the canonical map from the direct sum of the (j i)_* (F i) to their direct product is an isomorphism.

theorem isIso_coproductToProduct (hcov : IsOpenCover U)
    (hlf : LocallyFinite fun i => (U i : Set X)) : IsIso (coproductToProduct U F)

Stacks.LocallyFiniteCover.isIso_sectionsComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/LocallyFiniteCoproductSections.lean, line 456. The attribute's comment: “(first displayed formula: Γ(V, 𝒢) = ∏ F_i(V ∩ U_i))”.

Stacks Project, Tag 02FT, first displayed formula. With X = ⋃ i, U i a locally finite open covering and 𝒢 = ⨁ i, (j i)_* (F i), for every open V of X the canonical comparison from Γ (V, 𝒢) to ∏ i, (F i) (V ∩ U i) is an isomorphism: the sections of the direct sum over V are the product of the groups (F i) (V ∩ U i).

The comparison is the sections over V of the canonical map from the direct sum to the product, followed by the canonical comparison from the sections of a product of sheaves to the product of their sections. The i-th factor of the target is (sectionsFunctor V).obj (pushforwardOpen U F i), which is (F i) (V ∩ U i) by Stacks.LocallyFiniteCover.sectionsFunctor_obj_pushforwardOpen.

theorem isIso_sectionsComparison (hcov : IsOpenCover U)
    (hlf : LocallyFinite fun i => (U i : Set X)) (V : Opens X) :
    IsIso ((sectionsFunctor V).map (coproductToProduct U F) ≫
      piComparison (sectionsFunctor V) (fun i => pushforwardOpen U F i))
Sources
LeanStacks.AlgebraicGeometry.CoveringResolutionQuasiIso.exists_coveringResolution · LocallyFinite · Stacks.LocallyFiniteCover.isColimitCofanProduct · Stacks.LocallyFiniteCover.isIso_coproductToProduct · Stacks.LocallyFiniteCover.isIso_sectionsComparison

Section20.25 Čech cohomology of complexes#

Section 20.25 of the Stacks Project, Tag 01FP. 7 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07M9, an equation

Tag 07M9 in the Stacks Project.

Stacks.Cech.Linear.sectionsToTotalCech, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/ModuleValuedTotalComplex.lean, line 111. The attribute's comment: “the augmentation, with module coefficients”.

Restriction of a section over U into Čech degree zero, followed by the inclusion of that summand of the total complex: the map Γ(U, K^•) ⟶ Tot(Č^•(Ui, K^•)) of complexes of O_X(U)-modules, natural in K^•.

def sectionsToTotalCech :
    sectionsComplexFunctor X O U ⟶ totalCechComplexFunctor X O U Ui hU

Stacks.Cech.globalSectionsToCech, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryA/GlobalSectionsToCech.lean, line 250.

Stacks Project, Tag 07M9. Restriction into Čech degree zero, followed by inclusion into the total complex.

noncomputable def globalSectionsToCech :
    globalSectionsComplexFunctor X ⟶ cechTotalComplexFunctor U
Tag 08BM, an equation

Tag 08BM in the Stacks Project.

Stacks.Cech.cechTotalComplexRefinement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/Cech/TotalComplexRefinement.lean, line 148. References: EGA III (6.6.7), “partial”.

Stacks 08BM. A refinement t : V ⟶ U induces, naturally in a complex of presheaves, the restriction map Tot(Č^•(U, F^•)) ⟶ Tot(Č^•(V, F^•)).

noncomputable def cechTotalComplexRefinement {I J : Type w} (U : I → C) (V : J → C)
    (t : FormalCoproduct.mk J V ⟶ FormalCoproduct.mk I U) :
    CechRefinementTransformation U V t
Tag 08BN, a lemma

Tag 08BN in the Stacks Project.

Stacks.Cech.exists_cechToDerivedComparison_and_cechSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechSpectralSequence/BoundedBelowComplexFullStatement.lean, line 86. The attribute's comment: “the whole lemma: the canonical map Tot(Č(U, F)) ⟶ RΓ(X, F), functorial in F and compatible with the augmentation of (20.25.0.1) = Tag 07M9 and the refinement map of (20.25.0.2) = Tag 08BM, together with the spectral sequence E_2^{p,q} = H^p(Tot(Č(U, H^q(F)))) abutting to H^{p+q}(X, F) -- for a ringed space, an open covering of X and a bounded below complex of O_X-modules, which are the lemma's three inputs and all of them”.

Tag 08BN. Let (X, O_X) be a ringed space, let U : X = ⋃_{i ∈ I} U_i be an open covering and let F^• be a bounded below complex of O_X-modules. Then

  1. there is a canonical map Tot(Č^•(U, F^•)) ⟶ RΓ(X, F^•), functorial in F^• -- it is a morphism of functors on bounded below complexes -- and compatible both with the augmentation of equation (20.25.0.1) ([Stacks, Tag 07M9]) and with the refinement map of equation (20.25.0.2) ([Stacks, Tag 08BM]); and
  2. there is a cohomological spectral sequence with E_2^{p,q} = H^p(Tot(Č^•(U, H^q(F^•)))) abutting to H^{p+q}(X, F^•), where H^q(F^•) is the complex n ↦ R^q i(F^n) of cohomology presheaves of [Stacks, Tag 01ER].

Both halves are read off the library's wider statements: the comparison from the system of comparisons for all coverings at once, cechToDerivedGlobalSections, and the spectral sequence from exists_cechSpectralSequence.

theorem exists_cechToDerivedComparison_and_cechSpectralSequence
    {I : Type u} (U : I → Opens X) (hU : ⊤ = iSup U)
    (K : CochainComplex.Plus (SheafOfModules.{u} R)) :
    ((globalSectionsToCechDerived X R U).app K ≫
          ((cechToDerivedGlobalSections X R).map U hU).app K =
          globalSectionsToDerived X R K ∧
        ∀ (J : Type u) (V : J → Opens X) (hV : ⊤ = iSup V)
            (t : FormalCoproduct.mk J V ⟶ FormalCoproduct.mk I U),
          cechRefinementDerived X R U V t ≫ (cechToDerivedGlobalSections X R).map V hV =
            (cechToDerivedGlobalSections X R).map U hU) ∧
      ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u} 2,
        (∀ p q : ℤ,
          Nonempty ((E.page 2).X (p, q) ≅
            ((cechTotalComplexFunctor U).obj
              ((((underlyingPresheafFunctor X R).rightDerivedPlus q).mapHomologicalComplex
                (up ℤ)).obj K.1)).homology p)) ∧
          SpectralSequence.AbutsTo E (fun n =>
            (DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
              ((derivedGlobalSectionsFunctor X R).obj K))

Stacks.Cech.exists_cechSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechSpectralSequence/BoundedBelowComplexSpectralSequence.lean, line 210. The attribute's comment: “the tag's spectral sequence: E_2^{p,q} = H^p(Tot(Č(U, H^q(F)))), both coordinates ranging over ℤ, abutting to H^{p+q}(X, F), for a ringed space, an open covering of X and a bounded below complex of O_X-modules. The tag's comparison map Tot(Č(U, F)) ⟶ RΓ(X, F), with its Tag 07M9 and Tag 08BM compatibilities, is Stacks.Cech.cechToDerivedGlobalSections, and the two halves are asserted together at the lemma's own three inputs by Stacks.Cech.exists_cechToDerivedComparison_and_cechSpectralSequence”.

For a ringed space (X, O_X), an open covering U : I → Opens X of X and a bounded below complex F^• of O_X-modules there is a cohomological spectral sequence, starting on page two, with

E_2^{p,q} = H^p(Tot(Č^•(U, H^q(F^•))))

where H^q(F^•) is the complex n ↦ R^q i(F^n) of cohomology presheaves, abutting to H^{p+q}(X, F^•).

theorem exists_cechSpectralSequence {I : Type u} (U : I → Opens X) (hU : ⊤ = iSup U)
    (K : CochainComplex.Plus (SheafOfModules.{u} R)) :
    ∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u} 2,
      (∀ p q : ℤ,
        Nonempty ((E.page 2).X (p, q) ≅
          ((cechTotalComplexFunctor U).obj
            ((((underlyingPresheafFunctor X R).rightDerivedPlus q).mapHomologicalComplex
              (up ℤ)).obj K.1)).homology p)) ∧
      SpectralSequence.AbutsTo E (fun n =>
        (DerivedCategory.homologyFunctor AddCommGrpCat.{u} n).obj
          ((derivedGlobalSectionsFunctor X R).obj K))

Stacks.Cech.cechToDerivedGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/DerivedGlobalSections.lean, line 537. The attribute's comment: “the tag's comparison map: the total Čech complex of a bounded below complex of O_X-modules maps canonically to its derived global sections, functorially in the complex -- the map is a morphism of functors on bounded below complexes -- and compatibly both with the Tag 07M9 augmentation and with the Tag 08BM refinement map, simultaneously for every open covering of X. The tag's spectral sequence E_2^{p,q} = H^p(Tot(Č(U, H^q(F)))) abutting to H^{p+q}(X, F) is Stacks.Cech.exists_cechSpectralSequence, and the two halves are asserted together at the lemma's own three inputs by Stacks.Cech.exists_cechToDerivedComparison_and_cechSpectralSequence”.

Tag 08BN, the comparison map. For a ringed space (X, O_X) the total Čech complex of a bounded below complex of O_X-modules has a canonical map to its derived global sections, functorial in the complex, compatible with the augmentation of Tag 07M9 — hence independent of the covering — and compatible with the refinement map of Tag 08BM.

noncomputable def cechToDerivedGlobalSections
    (R : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) :
    CechToDerivedGlobalSectionsSystem X R

Stacks.Cech.Linear.cechToDerivedSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/ModuleValuedDerivedSections.lean, line 440. The attribute's comment: “the tag's comparison map, generalised to module coefficients over an arbitrary open: for a ringed space (X, O_X) and an open U, the total Čech complex of a bounded below complex of O_X-modules maps canonically to its derived sections in D(O_X(U)), functorially in the complex and compatibly with the Tag 07M9 augmentation, simultaneously for every open covering of U. The tag's own statement -- the comparison over X, compatible with both the Tag 07M9 and the Tag 08BM maps, together with the tag's spectral sequence -- is Stacks.Cech.cechToDerivedGlobalSections and Stacks.Cech.exists_cechSpectralSequence, conjoined at the lemma's three inputs by Stacks.Cech.exists_cechToDerivedComparison_and_cechSpectralSequence”.

Stacks 08BN, the comparison map with module coefficients. For a ringed space (X, O_X) and an open subset U the total Čech complex of a bounded below complex of O_X-modules has a canonical map to its derived sections over U, a morphism of D(O_X(U)) functorial in the complex and compatible with the augmentation of [Stacks, Tag 07M9] -- hence independent of the covering.

def cechToDerivedSections : CechToDerivedSectionsSystem X O U
Tag 0FLH, a lemma

Tag 0FLH in the Stacks Project.

Stacks.Cech.isIso_cechToDerivedGlobalSections_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/AcyclicCoveringComputesDerivedSections.lean, line 447. The attribute's comment: “the vanishing condition is the one of Tag 01ET: the higher right derived functors of sections over each intersection vanish on each term of the complex”.

[Stacks, Tag 0FLH] Let (X, O_X) be a ringed space, let U : I → Opens X be an open covering of X and let K^• be a bounded below complex of O_X-modules with H^i(U_{i_0 … i_p}, K^q) = 0 for all i > 0, all tuples i_0, …, i_p of members of the covering, and all degrees q. Then the comparison map Tot(Č^•(U, K^•)) ⟶ RΓ(X, K^•) of Tag 08BN is an isomorphism.

theorem isIso_cechToDerivedGlobalSections_app
    (R : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) (hU : ⊤ = iSup U)
    (K : CochainComplex.Plus (SheafOfModules.{u} R))
    (hacyclic : ∀ (n : ℕ) (s : Fin (n + 1) → I) (q : ℤ) (i : ℕ), 0 < i →
      IsZero (((SheafOfModules.evaluation.{u} R
        (op (⨅ k, U (s k)))).rightDerived i).obj (K.1.X q))) :
    IsIso (((cechToDerivedGlobalSections X R).map U hU).app K)
Tag 07MB, an equation

Tag 07MB in the Stacks Project.

Stacks.Cech.LinearCupProduct.cechCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/LinearCupProduct.lean, line 1109. The attribute's comment: “at module coefficients over a base ring, relative to a coefficient pairing”.

The Čech cup product at coefficients in presheaves of modules over a base ring R: the signed Alexander--Whitney map

Tot(Tot(Č(W,K)) ⊗_R Tot(Č(W,L))) ⟶ Tot(Č(W,M))

attached to a pairing D of the coefficient complexes. On the summand on which the first factor has total degree n, the target has Čech degree p, and the front face has Čech degree r, its coefficient is cupProductSign n p r = (-1)^((p+r)n+rp+r).

The source tensors over R; the pairing D is where the coefficients are tensored, and it is not required to be a tensor product over R.

noncomputable def cechCupProduct (D : ComplexPairing R K L M) :
    HomologicalComplex.mapBifunctor ((totalCechComplexFunctor W R).obj K)
        ((totalCechComplexFunctor W R).obj L) (tensorModules R) (up ℤ) ⟶
      (totalCechComplexFunctor W R).obj M

Stacks.Cech.LinearCupProduct.cechCupProduct_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/LinearCupProduct.lean, line 1122. The attribute's comment: “the signed Alexander--Whitney formula at module coefficients over a base ring”.

On homogeneous summands the cup product is the front/back restriction formula with the sign (-1)^((p+r)n+rp+r), the restrictions being paired by D.

theorem cechCupProduct_ι (D : ComplexPairing R K L M) (r s : ℕ) (a b : ℤ) :
    tensorModulesMap R (ιTotalCech W R K r a) (ιTotalCech W R L s b) ≫
        HomologicalComplex.ιMapBifunctor ((totalCechComplexFunctor W R).obj K)
          ((totalCechComplexFunctor W R).obj L) (tensorModules R) (up ℤ)
          ((r : ℤ) + a) ((s : ℤ) + b) (((r : ℤ) + a) + ((s : ℤ) + b)) rfl ≫
        (cechCupProduct W R D).f (((r : ℤ) + a) + ((s : ℤ) + b)) =
      cupProductSign ((r : ℤ) + a) ((r : ℤ) + (s : ℤ)) (r : ℤ) •
        (cechAlexanderWhitney W R (D.μ a b (a + b) rfl) r s ≫
          ιTotalCech W R M (r + s) (a + b) ≫
          eqToHom (congrArg (((totalCechComplexFunctor W R).obj M).X) (by push_cast; ring)))

Stacks.Cech.ModuleCupProduct.cechCupProductA, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/ModuleCupProduct.lean, line 140. The attribute's comment: “at 𝒪_X-module coefficients over the ring of sections”.

The Čech cup product at 𝒪_X-module coefficients. The signed Alexander--Whitney cup-product map

Tot(Tot(Č(U,K)) ⊗_A Tot(Č(U,L))) ⟶ Tot(Č(U,M))

for A = 𝒪_X(V), attached to a pairing D of the coefficient sections presheaves into those of M. On a homogeneous summand it is the front/back restriction formula with the Alexander--Whitney sign cupProductSign n p r = (-1)^((p+r)n+rp+r).

noncomputable abbrev cechCupProductA
    (D : ComplexPairing (CoeffRing O V) ((sectionsComplexFunctor O V).obj K)
      ((sectionsComplexFunctor O V).obj L) ((sectionsComplexFunctor O V).obj M))

Stacks.Cech.SheafTensorPairing.cechCupProductSheafTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/SheafTensorPairing.lean, line 360. The attribute's comment: “the sheaf-tensor instantiation: source over the section ring, coefficients over the structure sheaf”.

The Čech cup product at sheaf-tensor coefficients: the signed Alexander--Whitney cup-product map

Tot(Tot(Č(𝒰,𝒦)) ⊗_A Tot(Č(𝒰,ℳ))) ⟶ Tot(Č(𝒰, Tot(𝒦 ⊗_{𝒪_X} ℳ)))

for a covering 𝒰 of V and A = 𝒪_X(V). This is the left-hand column of the diagram of Stacks Tag 0FKV: the source tensors the two total Čech complexes over the ring A of sections on V, while in the target the coefficients are tensored over the structure sheaf, the coefficient pairing being sheafTensorComplexPairing.

Its value on a homogeneous summand is the front/back restriction formula with the Alexander--Whitney sign cupProductSign n p r = (-1)^((p+r)n+rp+r): see Stacks.Cech.LinearCupProduct.cechCupProduct_ι, which applies by Stacks.Cech.ModuleCupProduct.cechCupProductA_eq.

noncomputable def cechCupProductSheafTensor :
    HomologicalComplex.mapBifunctor ((totalCechComplexFunctorA O V U hU).obj K)
        ((totalCechComplexFunctorA O V U hU).obj L) (tensorModules (CoeffRing O V)) (up ℤ) ⟶
      (totalCechComplexFunctorA O V U hU).obj
        (HomologicalComplex.mapBifunctor K L (sheafTensor O) (up ℤ))

Stacks.Cech.CupProduct.cechCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryC/CechCupProduct/CupProductMap.lean, line 810.

The signed Alexander--Whitney cup-product map

Tot(Tot(Č(U,F)) ⊗_ℤ Tot(Č(U,G))) ⟶ Tot(Č(U,Tot(F ⊗_ℤ G))).

On the summand on which α has total degree n, the target has Čech degree p, and the front face of α has Čech degree r, its coefficient is cupProductSign n p r = (-1)^((p+r)n+rp+r).

noncomputable def cechCupProduct
    (F : CochainComplex (ZPresheaf.{u, max u v w} X) ℤ)
    (G : CochainComplex (ZPresheaf.{u, max u v w'} X) ℤ) :
    HomologicalComplex.mapBifunctor ((totalCechComplexFunctor.{u, v, max u w} X U).obj F)
        ((totalCechComplexFunctor.{u, v, max u w'} X U).obj G)
        (tensorModules.{max u v w, max u v w'} ℤ) (up ℤ) ⟶
      (totalCechComplexFunctor.{u, v, max u w w'} X U).obj
        (tensorSheafComplex.{u, max v w, max v w'} X F G)

Stacks.Cech.CupProduct.cechCupProduct_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryC/CechCupProduct/CupProductMap.lean, line 826. The attribute's comment: “the signed Alexander--Whitney formula”.

On homogeneous summands the cup product is the front/back restriction formula with the sign (-1)^((p+r)n+rp+r).

theorem cechCupProduct_ι (F : CochainComplex (ZPresheaf.{u, max u v w} X) ℤ)
    (G : CochainComplex (ZPresheaf.{u, max u v w'} X) ℤ) (r s : ℕ) (a b : ℤ) :
    tensorModulesMap ℤ (ιTotalCech.{u, v, max u w} X U F r a)
      (ιTotalCech.{u, v, max u w'} X U G s b) ≫
        HomologicalComplex.ιMapBifunctor ((totalCechComplexFunctor.{u, v, max u w} X U).obj F)
          ((totalCechComplexFunctor.{u, v, max u w'} X U).obj G)
          (tensorModules.{max u v w, max u v w'} ℤ)
          (up ℤ) (r + a) (s + b) ((r + a) + (s + b)) rfl ≫
        (cechCupProduct.{u, v, w, w'} X U F G).f ((r + a) + (s + b)) =
      cupProductSign (r + a) (r + s) r •
        (cechAlexanderWhitney.{u, v, max u w, max u w'} X U (F.X a) (G.X b) r s ≫
          cechCochainsMap.{u, v, max u w w'} X U
            (ιTensorSheafComplex.{u, max v w, max v w'} X F G a b) (r + s) ≫
          ιTotalCech.{u, v, max u w w'} X U
            (tensorSheafComplex.{u, max v w, max v w'} X F G) (r + s) (a + b) ≫
          eqToHom (congrArg
            (((totalCechComplexFunctor.{u, v, max u w w'} X U).obj
              (tensorSheafComplex.{u, max v w, max v w'} X F G)).X)
            (by push_cast; ring)))
Tag 07MC, a lemma

Tag 07MC in the Stacks Project.

Stacks.Cech.Hypercohomology.cup_boundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/HypercohomologyCupBoundaryTensor.lean, line 199. The attribute's comment: “for complexes of modules over an arbitrary sheaf of commutative rings 𝒪_X and ⊗_{𝒪_X}; the source's abelian sheaves and ⊗_𝐙 are the case 𝒪_X = 𝐙_X, whose modules are the abelian sheaves (Stacks.Cech.Hypercohomology.isEquivalence_toSheaf_integerRingSheaf) and whose tensor product is ⊗_𝐙. cup is the cup product of Čech cocycles on a common covering and boundary the connecting map of the long exact cohomology sequence”.

[Stacks, Tag 07MC]. Let 0 ⟶ F₁ ⟶ F₂ ⟶ F₃ ⟶ 0 (the short complex S) and 0 ⟶ G₃ ⟶ G₂ ⟶ G₁ ⟶ 0 (the short complex T) be short exact sequences of bounded below complexes of 𝒪_X-modules, H a bounded below complex and γᵢ : Tot(Fᵢ ⊗_{𝒪_X} Gᵢ) ⟶ H maps of complexes such that the squares

γ₁ ∘ Tot(1 ⊗ (G₂ → G₁)) = γ₂ ∘ Tot((F₁ → F₂) ⊗ 1) and γ₂ ∘ Tot(1 ⊗ (G₃ → G₂)) = γ₃ ∘ Tot((F₂ → F₃) ⊗ 1)

commute. If Čech cohomology agrees with cohomology for the sheaves Fᵢᵖ and Gⱼ^q, then for a₃ ∈ Hⁿ(X, F₃) and b₁ ∈ Hᵐ(X, G₁)

γ₁(∂a₃ ∪ b₁) = (-1)^{n+1} γ₃(a₃ ∪ ∂b₁) in H^{n+m+1}(X, H).

The source states this for complexes of abelian sheaves and ⊗_𝐙. That is the case where 𝒪_X is the constant sheaf of rings 𝐙_X: sheaves of 𝐙_X-modules are the abelian sheaves (Stacks.Cech.Hypercohomology.isEquivalence_toSheaf_integerRingSheaf), and ⊗_{𝐙_X} is ⊗_𝐙, since both are the sheafification of presheaves whose stalks are Fₓ ⊗_𝐙 Gₓ.

theorem cup_boundary
    (S : ShortComplex (CochainComplex.Plus (SheafOfModules.{u} (ringSheaf O))))
    (hS : (toSC S).ShortExact)
    (T : ShortComplex (CochainComplex.Plus (SheafOfModules.{u} (ringSheaf O))))
    (hT : (toSC T).ShortExact) (H : CochainComplex.Plus (SheafOfModules.{u} (ringSheaf O)))
    (γ₁ : letI : (Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{u} :=
        inferInstance
      HomologicalComplex.mapBifunctor S.X₁.obj T.X₃.obj (sheafTensor O) (up ℤ) ⟶ H.obj)
    (γ₂ : letI : (Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{u} :=
        inferInstance
      HomologicalComplex.mapBifunctor S.X₂.obj T.X₂.obj (sheafTensor O) (up ℤ) ⟶ H.obj)
    (γ₃ : letI : (Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{u} :=
        inferInstance
      HomologicalComplex.mapBifunctor S.X₃.obj T.X₁.obj (sheafTensor O) (up ℤ) ⟶ H.obj)
    (h₁ : letI : (Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{u} :=
        inferInstance
      HomologicalComplex.mapBifunctorMap (𝟙 S.X₁.obj) T.g.hom (sheafTensor O) (up ℤ) ≫ γ₁ =
      HomologicalComplex.mapBifunctorMap S.f.hom (𝟙 T.X₂.obj) (sheafTensor O) (up ℤ) ≫ γ₂)
    (h₂ : letI : (Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{u} :=
        inferInstance
      HomologicalComplex.mapBifunctorMap (𝟙 S.X₂.obj) T.f.hom (sheafTensor O) (up ℤ) ≫ γ₂ =
      HomologicalComplex.mapBifunctorMap S.g.hom (𝟙 T.X₁.obj) (sheafTensor O) (up ℤ) ≫ γ₃)
    (hF₁ : ∀ p, CechComputesSheaf O (S.X₁.obj.X p)) (hF₂ : ∀ p, CechComputesSheaf O (S.X₂.obj.X p))
    (hF₃ : ∀ p, CechComputesSheaf O (S.X₃.obj.X p)) (hG₁ : ∀ q, CechComputesSheaf O (T.X₃.obj.X q))
    (hG₂ : ∀ q, CechComputesSheaf O (T.X₂.obj.X q)) (hG₃ : ∀ q, CechComputesSheaf O (T.X₁.obj.X q))
    (n m : ℤ) (a₃ : hypercohomology O S.X₃ n) (b₁ : hypercohomology O T.X₃ m) :
    cup O (cechComputes_of_terms O _ hF₁) (cechComputes_of_terms O _ hG₁) (tensorPairing O γ₁)
        (n + 1) m (n + m + 1) (by omega) (boundary O S hS n (n + 1) rfl a₃) b₁ =
      ((n + 1).negOnePow : ℤ) •
        cup O (cechComputes_of_terms O _ hF₃) (cechComputes_of_terms O _ hG₃) (tensorPairing O γ₃)
          n (m + 1) (n + m + 1) (by omega) a₃ (boundary O T hT m (m + 1) rfl b₁)
Tag 0B8S, a lemma

Tag 0B8S in the Stacks Project.

Stacks.Cohomology.SquareZeroBoundary.SquareZeroKernel.moduleCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SquareZeroExtensionBoundaryDerivation.lean, line 770. The attribute's comment: “the H⁰(X, O)-module structure on H¹(X, I)”.

Stacks 0B8S, first clause: M = H¹(X, I) is a module over R = H⁰(X, O). The kernel is a sheaf of O-modules (Stacks.Cohomology.SquareZeroBoundary.SquareZeroKernel.incl_smul), and a global section of O acts on M through the endomorphism of the kernel it induces.

noncomputable def moduleCohomology :
    Module (ToType (O.obj (op (⊤ : Opens X)))) (cohomologyOne I)

Stacks.Cohomology.SquareZeroBoundary.SquareZeroKernel.boundary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SquareZeroExtensionBoundaryDerivation.lean, line 874. The attribute's comment: “the boundary map, in the Čech description of Stacks 02AP”.

The boundary map ∂ : H⁰(X, O) → H¹(X, I) of the short exact sequence 0 → I → O' → O → 0, in the Čech description of Stacks 02AP: the class of the cocycle of differences of local lifts, transported to H¹(X, I) by the comparison of Stacks 01EQ.

noncomputable def boundary (f : ToType (O.obj (op (⊤ : Opens X)))) : cohomologyOne I

Stacks.Cohomology.SquareZeroBoundary.SquareZeroKernel.boundary_leibniz, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SquareZeroExtensionBoundaryDerivation.lean, line 1012. The attribute's comment: “the Leibniz rule for the boundary map”.

Stacks 0B8S, the Leibniz rule. On a covering over which both f and g lift, the cocycle attached to f * g is α g + f β, where α and β are the cocycles attached to f and to g and the products are taken for the O-module structure on the kernel.

theorem boundary_leibniz (f g : ToType (O.obj (op (⊤ : Opens X)))) :
    E.boundary (f * g) =
      E.smulCohomology f (E.boundary g) + E.smulCohomology g (E.boundary f)

Stacks.Cohomology.SquareZeroBoundary.SquareZeroKernel.boundaryDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SquareZeroExtensionBoundaryDerivation.lean, line 1080. The attribute's comment: “the boundary map of the square-zero extension is a derivation”.

Stacks 0B8S. Let X be a topological space and π : O' ⟶ O a surjection of sheaves of commutative rings whose kernel I has square zero. Then M = H¹(X, I) is a module over R = H⁰(X, O), and the boundary map ∂ : R → M of the short exact sequence 0 → I → O' → O → 0 is a derivation.

noncomputable def boundaryDerivation :
    letI := E.moduleCohomology
    Derivation ℤ (ToType (O.obj (op (⊤ : Opens X)))) (cohomologyOne I)
Sources
LeanStacks.Cech.Linear.sectionsToTotalCech · Stacks.Cech.globalSectionsToCech · Stacks.Cech.cechTotalComplexRefinement · Stacks.Cech.exists_cechToDerivedComparison_and_cechSpectralSequence · Stacks.Cech.exists_cechSpectralSequence · Stacks.Cech.cechToDerivedGlobalSections · Stacks.Cech.Linear.cechToDerivedSections · Stacks.Cech.isIso_cechToDerivedGlobalSections_app

Section20.26 Flat resolutions#

Section 20.26 of the Stacks Project, Tag 06Y7. 17 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06Y8, a lemma

Tag 06Y8 in the Stacks Project.

main_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TensorComplex/ExactFunctor/IsTriangulated.lean, line 39. References: SGA 4 XVII (7.3.3), “special case”.

Statement 1. For a fixed complex G, the functor Tleft G : F ↦ Tot(G ⊗ F) on K(Mod(O_X)) can be equipped with a functorial isomorphism ξ (a CommShift ℤ datum) making it an exact functor of triangulated categories (Stacks Tag 06Y8, left version).

Here ξ is the canonical comparison isomorphism Tot(G ⊗ F[1]) ≅ Tot(G ⊗ F)[1] of Stacks Tag 0FNG, and Functor.IsTriangulated packages exactly the requirement of Definition 3: the CommShift natural isomorphism together with preservation of distinguished triangles.

Note the descent of the functor to K(Mod(O_X)) is asserted as content (via Tleft, which is built from TleftCochain_preservesHomotopyRel), not assumed as a hypothesis.

theorem main_left (G : CochainComplex C ℤ) :
    ∃ e : (Tleft G).CommShift ℤ,
      @Functor.IsTriangulated _ _ _ _ _ _ (Tleft G) e _ _ _ _ _ _ _ _

main_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TensorComplex/ExactFunctor/IsTriangulated.lean, line 52. References: SGA 4 XVII (7.3.3), “special case”.

Statement 2. For a fixed complex G, the functor Tright G : F ↦ Tot(F ⊗ G) on K(Mod(O_X)) can be equipped with a functorial isomorphism ξ making it an exact functor of triangulated categories (Stacks Tag 06Y8, right version). This is genuinely distinct from main_left (the two differ by the commutativity isomorphism with its sign (-1)^{pq}).

theorem main_right (G : CochainComplex C ℤ) :
    ∃ e : (Tright G).CommShift ℤ,
      @Functor.IsTriangulated _ _ _ _ _ _ (Tright G) e _ _ _ _ _ _ _ _
Tag 06Y9, a definition

Tag 06Y9 in the Stacks Project.

Stacks.SheafOfModules.IsKFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/Defs.lean, line 66.

A cochain complex K of sheaves of R-modules is K-flat if Tot(F ⊗_R K) is acyclic for every acyclic cochain complex F.

abbrev IsKFlat
    (K : CochainComplex (SheafOfModules (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ) : Prop
Tag 06YA, a lemma

Tag 06YA in the Stacks Project.

Stacks.SheafOfModules.IsKFlat.quasiIso_le_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 100. The attribute's comment: “on the homotopy category, as the tag states it”.

[Stacks, Tag 06YA]. For a K-flat complex K of 𝒪-modules, the exact functor F ↦ Tot(F ⊗_𝒪 K) of K(Mod(𝒪)) carries quasi-isomorphisms to quasi-isomorphisms.

theorem IsKFlat.quasiIso_le_inverseImage
    (K : CochainComplex (SheafOfModules (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
    (hK : IsKFlat R K) :
    HomotopyCategory.quasiIso
        (SheafOfModules (Stacks.SheafOfModules.Tensor.ringSheaf R)) (ComplexShape.up ℤ) ≤
      (HomotopyCategory.quasiIso
          (SheafOfModules (Stacks.SheafOfModules.Tensor.ringSheaf R))
          (ComplexShape.up ℤ)).inverseImage
        (Stacks.SheafOfModules.Tensor.Reduction.bifunctorPhiR
          (Stacks.SheafOfModules.Tensor.sheafTensor R) K)

Stacks.SheafOfModules.IsKFlat.quasiIso_rightTensorComplex_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/KFlat/TensorPreservesQuasiIso.lean, line 124. The attribute's comment: “at the level of complexes rather than of the homotopy category”.

[Stacks, Tag 06YA] at the level of complexes. For a K-flat complex K of 𝒪-modules and a quasi-isomorphism f : F₁ ⟶ F₂ of complexes of 𝒪-modules, the induced morphism Tot(F₁ ⊗_𝒪 K) ⟶ Tot(F₂ ⊗_𝒪 K) is a quasi-isomorphism.

The hypothesis is explicit rather than an instance: with the tensor-total functor applied to a consumer's own factorization, an instance argument is synthesized at a different spelling of the same type.

theorem IsKFlat.quasiIso_rightTensorComplex_map
    (K : CochainComplex (SheafOfModules (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
    (hK : IsKFlat R K)
    {F₁ F₂ : CochainComplex (SheafOfModules (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
    (f : F₁ ⟶ F₂) (hf : QuasiIso f) :
    QuasiIso ((Stacks.SheafOfModules.Tensor.rightTensorComplex R K).map f)
Tag 06YB, a lemma

Tag 06YB in the Stacks Project.

Stacks.SheafOfModules.KFlatStalkCriterion.kFlat_iff_stalkwise, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/StalkCriterion.lean, line 567.

Stacks 06YB. A complex of sheaves of modules on a ringed space is K-flat if and only if its complex of stalks at every point is K-flat over the stalk of the structure sheaf.

theorem kFlat_iff_stalkwise
    (K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} R)) ℤ)
      :
    letI := fun (left : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf R)) =>
      Stacks.SheafOfModules.Tensor.sheafTensor_obj_additive.{u, u, u, u, u} R left
    letI : ∀ (left right : CochainComplex
        (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ),
        HomologicalComplex.HasMapBifunctor left right
          (Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u} R) (ComplexShape.up ℤ) :=
      fun left right => Stacks.SheafOfModules.Tensor.hasMapBifunctor_sheafTensor R left right
    Stacks.SheafOfModules.KFlat.KFlat.{u, u, u} R K ↔ KFlatStalkwise R K
Tag 079R, a lemma

Tag 079R in the Stacks Project.

Stacks.SheafOfModules.kFlat_tensorComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/TensorProduct.lean, line 513.

Stacks 079R. The total tensor product of two K-flat complexes of sheaves of modules is K-flat.

theorem kFlat_tensorComplex
    {K L : CochainComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ}
    (hK : Stacks.SheafOfModules.IsKFlat R K) (hL : Stacks.SheafOfModules.IsKFlat R L) :
    Stacks.SheafOfModules.IsKFlat R (((Stacks.SheafOfModules.Tensor.tensorComplex R).obj K).obj L)
Tag 079S, a lemma

Tag 079S in the Stacks Project.

Declarations registered for the tag:

Tag 0G6U, a lemma

Tag 0G6U in the Stacks Project.

Declarations registered for the tag:

Tag 06YC, a lemma

Tag 06YC in the Stacks Project.

Stacks.SheafOfModules.KFlatPullback.kFlat_pullback_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/PullbackFromTheStalkCriterion.lean, line 61.

Stacks 06YC. The degreewise pullback of a K-flat complex of 𝒪_Y-modules along a morphism of ringed spaces is a K-flat complex of 𝒪_X-modules.

theorem kFlat_pullback_unconditional {X Y : AlgebraicGeometry.RingedSpace.{u, u}} (f : X ⟶ Y)
    (K : CochainComplex (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.sheaf)) ℤ)
    (hK : Stacks.SheafOfModules.IsKFlat Y.sheaf K) :
    Stacks.SheafOfModules.IsKFlat X.sheaf
      (((RingedSpaceModuleAdjunction.modulePullback f).mapHomologicalComplex
        (ComplexShape.up ℤ)).obj K)
Tag 06YD, a lemma

Tag 06YD in the Stacks Project.

Declarations registered for the tag:

Tag 06YE, a lemma

Tag 06YE in the Stacks Project.

Stacks.SheafOfModules.kFlat_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/SequentialColimits.lean, line 85.

A sequential colimit of K-flat complexes of sheaves of modules is K-flat.

theorem kFlat_colimit
    (K : ℕ ⥤ CochainComplex (SheafOfModules (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℤ)
    (hK : ∀ n : ℕ, IsKFlat R (K.obj n)) :
    IsKFlat R (colimit K)
Tag 079T, a lemma

Tag 079T in the Stacks Project.

Stacks.Cohomology.SpaceResolutionByExtensionsByZero.exists_resolutionByDirectSumsExtensionsByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RecoveryA/SpaceResolutionByExtensionsByZero.lean, line 354.

Every cochain complex G of O-modules on a ringed space admits a compatible system of bounded-above resolutions of its canonical truncations τ_{≤ n+1} G whose terms and successive cokernels are direct sums of extensions by zero j_{U!} O_U, and whose colimit maps quasi-isomorphically to G.

theorem exists_resolutionByDirectSumsExtensionsByZero
    (G : CochainComplex (SheafOfModules.{u} O) ℤ) :
    Nonempty (ResolutionByDirectSumsExtensionsByZero O G)
Tag 06YF, a lemma

Tag 06YF in the Stacks Project.

AlgebraicGeometry.RingedSpace.exists_isKFlat_isFlat_quasiIso_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RingedSpace/FlatKFlatResolution.lean, line 64.

Stacks 06YF. Every cochain complex G of 𝒪_X-modules on a ringed space receives a termwise surjective quasi-isomorphism from a K-flat complex whose terms are flat 𝒪_X-modules.

A ringed space is a ringed site, and this is the resolution built there ([Stacks, Tag 06YS]).

public theorem exists_isKFlat_isFlat_quasiIso_epi
    (G : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ) :
    ∃ (K : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ)
      (s : K ⟶ G),
      Stacks.SheafOfModules.IsKFlat X.sheaf K ∧
      (∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.sheaf) (K.X i)) ∧
      QuasiIso s ∧ ∀ i : ℤ, Epi (s.f i)
Tag 06YG, a lemma

Tag 06YG in the Stacks Project.

Declarations registered for the tag:

Tag 06YH, a definition

Tag 06YH in the Stacks Project.

Declarations registered for the tag:

Tag 08BP, a definition

Tag 08BP in the Stacks Project.

Stacks.Cohomology.tor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedTensor/Tor.lean, line 83. References: SGA 4½ Etat 0 (6.2), “Tor_i, ringed space”; SGA 4 XVII (4.1.8), “modules, not complexes”.

Tag 08BP. The O_X-module Tor_p^{O_X}(F, G) = H^{-p}(F ⊗_{O_X}^{L} G).

def tor (p : ℤ) (F G : OXMod.{u} X) : OXMod.{u} X
Tag 08BQ, a lemma

Tag 08BQ in the Stacks Project.

Stacks.Cohomology.flat_iff_forall_isZero_tor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedTensor/TorFlatness.lean, line 373. The attribute's comment: “(1) ⟺ (2) for a ringed space, with clause (2) stated in the source's own terms: the vanishing of the sheaf Tor_1^{O_X}(F, G) = H^{-1}(F ⊗^L_{O_X} G) of Tag 08BP, for every O_X-module G, and clause (1) sheaf-level flatness of Tag 05ND.”.

Tag 08BQ: Tor measures the deviation of flatness. Let (X, 𝒪_X) be a ringed space and ℱ an 𝒪_X-module. The following are equivalent:

  1. ℱ is a flat 𝒪_X-module, and
  2. Tor_1^{𝒪_X}(ℱ, 𝒢) = 0 for every 𝒪_X-module 𝒢.

Clause (1) is OXModule.Flat, Definition Tag 05ND: the genuine sheaf tensor endofunctor - ⊗_{𝒪_X} ℱ preserves monomorphisms, hence is exact. Clause (2) is the source's own Tor_1, the sheaf Stacks.Cohomology.tor X 1 ℱ 𝒢 of Tag 08BP, which is H^{-1}(ℱ ⊗^{L}_{𝒪_X} 𝒢) — not a stalkwise substitute for it.

Proof. Tag 05NE (OXModule.flat_iff_flat_stalk) replaces clause (1) by flatness of every stalk, and AlgebraicGeometry.SheafOfModules.flat_stalk_ringCat_iff_commRingCat reads that over the stalk ring the derived tensor product is formed relative to. Over that ring OXModule.module_flat_iff_tor1 turns flatness of a stalk into the vanishing of the module-theoretic Tor_1 against every module over it, every such module being a stalk by AlgebraicGeometry.SheafOfModules.stalkFunctor_essSurj; and isZero_derivedTensorHomology_iff_forall_isZero_tor turns the vanishing of those stalkwise Tor_1 into the vanishing of the sheaf Tor_1, which is clause (2).

No intermediate statement of stalkwise flatness over the RingCat-valued stalk ring is written down, and that is deliberate: writing Module.Flat Λ M for that ring forces the Semiring Λ inside the Module instance to be the one derived from StacksDraft.StalkTensor.commRing_stalk, while the ModuleCat Λ that M lives in carries the one derived from RingCat's own Ring. The two are definitionally equal but not syntactically, so instance synthesis fails on the resulting Module Λ M goal. Going through OXModule.module_flat_iff_tor1, whose ModuleCat is formed from its own CommRing binder, keeps the instances internally consistent.

theorem flat_iff_forall_isZero_tor (F : OXMod.{u, u} X) :
    OXModule.Flat F ↔ ∀ G : OXMod.{u, u} X, IsZero (tor X 1 F G)

OXModule.flat_iff_tor1_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/FlatModuleSheavesAndStalks/FlatIffTorOne.lean, line 506. The attribute's comment: “(1) ⟺ (2) with clause (2) read stalkwise: Tor_1 here is the module-theoretic Tor_1^{O_{X,x}}(F_x, G_x) at every point, not the sheaf Tor_1 of Tag 08BP. The tag's clause (2) in the source's own terms — the vanishing of Stacks.Cohomology.tor X 1 F G — is Stacks.Cohomology.flat_iff_forall_isZero_tor in StacksFrontier/Topology/Sheaves/Cohomology/DerivedTensor/TorFlatness.lean, and the two readings are identified there by isZero_derivedTensorHomology_iff_forall_isZero_tor.”. References: SGA 6 I (5.1.1), “special case”.

Theorem (Stacks Tag 08BQ — "Tor measures the deviation of flatness"). Let (X, O_X) be a ringed space and F an O_X-module. Then F is flat (Definition 2: the genuine tensor endofunctor - ⊗_{O_X} F is exact) if and only if Tor_1^{O_X}(F, G) is the zero O_X-module for every O_X-module G.

The tensor product (Definition 1) is formalized directly as the sheafification of the presheaf tensor product, and Flat is the genuine sheaf-level exactness of this tensor, so the left-hand side is the source's own notion (Tag 05ND).

The right-hand side is the stalk-level reading: Tor1IsZero F G says that the classical module-theoretic Tor_1^{O_{X,x}}(F_x, G_x) vanishes at every x. It is not the expression Stacks.Cohomology.tor X 1 F G (Tag 08BP), the genuine H^{-1}(F ⊗^{L}_{O_X} G), which is what the tag's clause (2) is about; and tor1IsZero_iff_stalk is Iff.rfl, so it supplies no part of the comparison.

The two readings are nevertheless the same statement, and that is now a theorem rather than a gap: Stacks.Cohomology.flat_iff_forall_isZero_tor in StacksFrontier/Topology/Sheaves/Cohomology/DerivedTensor/TorFlatness.lean states Tag 08BQ with clause (2) in the source's own terms, and Stacks.SheafOfModules.DerivedTensorStalk.isZero_derivedTensorHomology_iff_forall_isZero_tor there is the identification itself: the sheaf Tor_p of Tag 08BP vanishes exactly when the stalkwise module-theoretic Tor_p vanishes at every point. Its four ingredients are AlgebraicGeometry.SheafOfModules.isZero_iff_forall_isZero_stalkFunctor_obj (vanishing is stalkwise, Tag 01AG), CategoryTheory.Functor.mapDerivedCategoryHomologyIso (the exact stalk functor commutes with H^{-1}), Stacks.SheafOfModules.DerivedTensorStalk.derivedTensorStalkIso (the derived form of Tag 01CB) — all three of which already existed — and Stacks.DerivedTensor.homologyIsoTor (StacksFrontier/Homology/Tor/DerivedTensorTor.lean), the identification of H^{-p} of a derived tensor product of two modules over a commutative ring with their Tor_p, which is the one that had to be supplied.

So this declaration is the stalk-level half of the tag, kept because the rest of this file is written in the stalkwise vocabulary; the tag's own statement is the one in StacksFrontier/Topology/Sheaves/Cohomology/DerivedTensor/TorFlatness.lean.

Proof. By flat_iff_flat_stalk (Tag 05NE) sheaf flatness is equivalent to stalk-wise flatness F.FlatStalkwise, and by flatStalkwise_iff_forall_tor1 the latter is equivalent to the vanishing of all stalk-wise Tor₁.

theorem flat_iff_tor1_eq_zero (F : OXModule X) :
    F.Flat ↔ ∀ G : OXModule X, F.Tor1IsZero G
Tag 0G6V, a lemma

Tag 0G6V in the Stacks Project.

Stacks.SheafOfModules.exists_isKFlat_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/Factorization.lean, line 117. The attribute's comment: “the K-flat factorization”.

Tag 0G6V. A map a : K^• ⟶ L^• of complexes of O-modules with K^• K-flat factors, up to homotopy, through a K-flat complex N^• which maps to L^• by a quasi-isomorphism.

theorem exists_isKFlat_factorization
    {K L : CochainComplex
      (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ}
    (a : K ⟶ L) (hK : IsKFlat X.O K) :
    ∃ (N : CochainComplex
        (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ)
      (b : K ⟶ N) (c : N ⟶ L),
      IsKFlat X.O N ∧ QuasiIso c ∧ Nonempty (Homotopy a (b ≫ c))

Stacks.SheafOfModules.exists_isKFlat_isFlat_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/KFlat/Factorization.lean, line 132. The attribute's comment: “the factorization with flat terms”.

Tag 0G6V, second half. If in addition the terms of K^• are flat O-modules, then the intermediate complex of the factorization can be chosen with flat terms as well.

theorem exists_isKFlat_isFlat_factorization
    {K L : CochainComplex
      (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ}
    (a : K ⟶ L) (hK : IsKFlat X.O K)
    (hKflat : ∀ i : ℤ,
      AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (K.X i)) :
    ∃ (N : CochainComplex
        (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} X.O)) ℤ)
      (b : K ⟶ N) (c : N ⟶ L),
      IsKFlat X.O N ∧
        (∀ i : ℤ,
          AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) (N.X i)) ∧
        QuasiIso c ∧ Nonempty (Homotopy a (b ≫ c))
Sources
Leanmain_left · main_right · Stacks.SheafOfModules.IsKFlat · Stacks.SheafOfModules.IsKFlat.quasiIso_le_inverseImage · Stacks.SheafOfModules.IsKFlat.quasiIso_rightTensorComplex_map · Stacks.SheafOfModules.KFlatStalkCriterion.kFlat_iff_stalkwise · Stacks.SheafOfModules.kFlat_tensorComplex · Stacks.SheafOfModules.kFlat_of_second_third

Section20.27 Derived pullback#

Section 20.27 of the Stacks Project, Tag 06YI. 5 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06YJ, a lemma

Tag 06YJ in the Stacks Project.

Stacks.Cohomology.KFlatDerivedPullback.derivedPullback_commShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/Triangulated.lean, line 146. The attribute's comment: “compatibility with shifts”.

The derived pullback commutes with the shift. Lf^* is the total left derived functor of degreewise pullback along Qh; degreewise pullback and Qh both commute with the shift, and the quasi-isomorphisms of K(𝒪_Y) are stable under it, so the derived functor does too.

instance derivedPullback_commShift :
  (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).CommShift ℤ

Stacks.Cohomology.KFlatDerivedPullback.derivedPullback_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/Triangulated.lean, line 192. The attribute's comment: “exactness”.

The derived pullback is exact: Lf^* : D(𝒪_Y) ⥤ D(𝒪_X) carries distinguished triangles to distinguished triangles.

Every morphism of D(𝒪_Y) is, up to isomorphism of arrows, the image of a morphism between K-flat complexes: the K-flat objects resolve every object, so their inclusion is a localized equivalence and the induced functor is essentially surjective on arrows. Completing such a morphism to a distinguished triangle of K(𝒪_Y) leaves all three vertices K-flat, the third by isKFlat_obj₃_of_distTriang, and the comparison of Lf^* is invertible at each of them. That is exactly the input of CategoryTheory.Functor.isTriangulated_of_rightExtension.

instance derivedPullback_isTriangulated :
    (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).IsTriangulated

Stacks.Cohomology.KFlatDerivedPullback.isIso_derivedPullbackComparison_app_of_kFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/Unconditional.lean, line 98. The attribute's comment: “computation on K-flat complexes”.

A K-flat complex computes the derived pullback: on it the canonical comparison Lf^* K ⟶ f^* K is invertible. This is the clause of Tag 06YJ that says the construction agrees with degreewise pullback where degreewise pullback is already derived, and it holds for an arbitrary morphism of ringed spaces: the K-flat complexes are a resolving datum for f^*, and the comparison of a left derived functor is invertible on its resolving class.

The two models of the derived categories are binders rather than the file's pinned HasDerivedCategory.standard: every ingredient of the proof is model-free.

theorem isIso_derivedPullbackComparison_app_of_kFlat
    [HasDerivedCategory.{w₁} (SheafOfModules.{u} (structureSheafRing X))]
    [HasDerivedCategory.{w₂} (SheafOfModules.{u} (structureSheafRing Y))]
    (K : CochainComplex (SheafOfModules.{u} (structureSheafRing Y)) ℤ) (hK : KFlatComplex Y K) :
    IsIso ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullbackComparison f).app
      ((HomotopyCategory.quotient (SheafOfModules.{u} (structureSheafRing Y))
        (ComplexShape.up ℤ)).obj K))

Declarations registered for the tag:

Tag 0D5S, a lemma

Tag 0D5S in the Stacks Project.

Stacks.DerivedPullback.Composition.isIso_derivedPullbackCompComparisonCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/CompositionUnconditional.lean, line 152.

Stacks 0D5S. The canonical comparison from the composite of the derived pullbacks along g and f to the derived pullback along f ≫ g is an isomorphism, for arbitrary composable morphisms of ringed spaces.

Every hypothesis of isIso_derivedPullbackCompComparison is met at the K-flat classes on Z and on Y.

theorem isIso_derivedPullbackCompComparisonCanonical :
    IsIso (derivedPullbackCompComparisonCanonical f g)
Tag 079U, a lemma

Tag 079U in the Stacks Project.

Stacks.Cohomology.DerivedPullbackTensor.derivedPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/PullbackTensorComparison.lean, line 532.

Stacks 079U: derived pullback is monoidal. For a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) there is a canonical isomorphism

Lf^*(K ⊗^L_{𝒪_Y} L) ≅ Lf^*K ⊗^L_{𝒪_X} Lf^*L,

bifunctorial in K, L ∈ D(𝒪_Y).

It is constructed the way the source constructs it. On K-flat representatives both sides are computed by ordinary total tensor complexes — the K-flat comparison of Stacks 06YU and the fact that a K-flat complex computes Lf^* — and there the comparison is the degreewise isomorphism f^*(K^p ⊗_{𝒪_Y} L^q) ≅ f^*K^p ⊗_{𝒪_X} f^*L^q of Stacks 01CD assembled on total complexes. Since D(𝒪_Y) is the localization of the K-flat objects of the homotopy category at the quasi-isomorphisms (Stacks 06YS), the product of two copies of that localization descends the comparison from K-flat representatives to all of D(𝒪_Y) × D(𝒪_Y), which is what makes the statement bifunctorial.

def derivedPullbackTensorIso : pullbackOfTensor f ≅ tensorOfPullbacks f
Tag 08DE, a lemma

Tag 08DE in the Stacks Project.

Stacks.Cohomology.MixedDerivedTensorOnARingedSpace.spaceDerivedLinearMixedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/MixedDerivedTensorOnARingedSpace.lean, line 374. The attribute's comment: “the canonical bifunctorial isomorphism in D(O_X): the tensor product over the smaller sheaf of rings f⁻¹O_Y is an O_X-module through its first factor”.

Stacks 08DE, O_X-linearly. The canonical bifunctorial isomorphism

F ⊗^L_{O_X} Lf^*G ≅ F ⊗^L_{f⁻¹O_Y} f⁻¹G

in D(O_X), for a morphism f : (X, O_X) ⟶ (Y, O_Y) of ringed spaces, F in D(O_X) and G in D(O_Y). Both sides are objects of D(O_X): the tensor product over the smaller sheaf of rings f⁻¹O_Y inherits the O_X-action from F, and the mixed tensor product realising it is Stacks.MixedTensor.sheafMixedTensorRight, whose sections are F(U) ⊗_{f⁻¹O_Y(U)} f⁻¹G(U).

derivedMixedTensorIso above is the comparison read after restriction of scalars to D(f⁻¹O_Y).

def spaceDerivedLinearMixedTensorIso :
    spaceLinearDerivedTensorPullback f ≅ spaceLinearDerivedMixedTensor f

Stacks.Cohomology.MixedDerivedTensorOnARingedSpace.derivedLinearMixedTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/MixedDerivedTensorOnARingedSpace.lean, line 402. The attribute's comment: “the canonical bifunctorial isomorphism, in D(O_X)”.

Stacks 08DE, through the one-sided K-flat descent of the mixed tensor product. The canonical bifunctorial isomorphism

F ⊗^L_{O_X} Lf^*G ≅ F ⊗^L_{f⁻¹O_Y} f⁻¹G

in D(O_X), for a morphism f : (X, O_X) ⟶ (Y, O_Y) of ringed spaces, F in D(O_X) and G in D(O_Y). The right-hand side is the derived tensor product over f⁻¹O_Y of F and f⁻¹G, an object of D(O_X) through F. It is stated between the two uncurried bifunctors on D(O_X) × D(O_Y), so that bifunctoriality is part of its type, and the left-hand one is written with the ringed-space derived pullback of Tag 06YJ.

def derivedLinearMixedTensorIso :
    spaceLinearDerivedTensorPullback f ≅ spaceDerivedMixedTensorInverseImage f
Tag 0FP0, a lemma

Tag 0FP0 in the Stacks Project.

Stacks.Cohomology.DerivedPullbackTensor.derivedPullbackTensorIso_toTensor_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPullback/TensorPullCompatibility.lean, line 192.

Stacks 0FP0. Let f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) be a morphism of ringed spaces and let K, M be complexes of 𝒪_Y-modules. The diagram

Lf^*(K ⊗^L_{𝒪_Y} M)  ⟶  Lf^*Tot(K ⊗_{𝒪_Y} M)
        |                           |
        v                           v
Lf^*K ⊗^L_{𝒪_X} Lf^*M        f^*Tot(K ⊗_{𝒪_Y} M)
        |                           |
        v                           v
 f^*K ⊗^L_{𝒪_X} f^*M    ⟶   Tot(f^*K ⊗_{𝒪_X} f^*M)

commutes: the left hand column — Stacks 079U, then the comparison Lf^*(QN) ⟶ Q(f^*N) in each tensor factor — followed by the canonical map to the ordinary total tensor complex on X equals the top row — the derived pullback of the canonical map to the ordinary total tensor complex on Y — followed by the right hand column, the comparison Lf^*(QN) ⟶ Q(f^*N) at Tot(K ⊗_{𝒪_Y} M) and then the comparison of total complexes of Stacks 01CD.

This is derivedPullbackTensorIso_hom_app_comp_rightComparison_of_complexes with the right comparison written out: postcomposing with the comparison of total complexes cancels the inverse that the right comparison ends with, leaving the six arrows of the source's diagram.

theorem derivedPullbackTensorIso_toTensor_comm
    (K L : CochainComplex (AlgebraicGeometry.RingedSpace.KFlatDerivedPullback.Modules Y) ℤ) :
    (derivedPullbackTensorIso f).hom.app
          (DerivedCategory.Q.obj K, DerivedCategory.Q.obj L) ≫
        (Functor.uncurry.obj
              (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf)).map
            ((derivedPullbackNatTrans f).app K ×ₘ (derivedPullbackNatTrans f).app L) ≫
          (derivedToTensorNatTrans X).app
            ((pullbackComplex f).obj K, (pullbackComplex f).obj L) =
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback f).map
          ((derivedToTensorNatTrans Y).app (K, L)) ≫
        (derivedPullbackNatTrans f).app
            ((totalComplexPair (Stacks.SheafOfModules.Tensor.sheafTensor Y.sheaf)).obj (K, L)) ≫
          DerivedCategory.Q.map ((pullbackTensorComplexNatIso f).hom.app (K, L))
Sources
LeanStacks.Cohomology.KFlatDerivedPullback.derivedPullback_commShift · Stacks.Cohomology.KFlatDerivedPullback.derivedPullback_isTriangulated · Stacks.Cohomology.KFlatDerivedPullback.isIso_derivedPullbackComparison_app_of_kFlat · Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback · Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullbackComparison · Stacks.DerivedPullback.Composition.isIso_derivedPullbackCompComparisonCanonical · Stacks.Cohomology.DerivedPullbackTensor.derivedPullbackTensorIso · Stacks.Cohomology.MixedDerivedTensorOnARingedSpace.spaceDerivedLinearMixedTensorIso

Section20.28 Cohomology of unbounded complexes#

Section 20.28 of the Stacks Project, Tag 079V. 7 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 079W, a lemma

Tag 079W in the Stacks Project.

Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/AdjunctionUnconditional.lean, line 255. The attribute's comment: “derived adjunction”. References: SGA 4 XVII (2.3.7), “ringed spaces case”.

The adjunction Lf^* ⊣ Rf_* on the unbounded derived categories of sheaves of modules over ringed spaces, for an arbitrary morphism of ringed spaces.

def derivedAdjunction : derivedPullback f ⊣ derivedPushforward f

Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction_unit_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/AdjunctionUnconditional.lean, line 263. The attribute's comment: “canonical unit”.

The derived unit agrees with the ordinary unit after applying the canonical comparison maps.

theorem derivedAdjunction_unit_fac
    (M : HomotopyCategory (SheafOfModules.{u} (structureSheafRing Y)) (ComplexShape.up ℤ)) :
    (derivedAdjunction f).unit.app (DerivedCategory.Qh.obj M) ≫
        (derivedPushforward f).map ((derivedPullbackComparison f).app M) =
      DerivedCategory.Qh.map ((homotopyPullbackPushforwardAdjunction f).unit.app M) ≫
        (derivedPushforwardUnit f).app
          (((modulePullback f).mapHomotopyCategory (ComplexShape.up ℤ)).obj M)

Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction_counit_fac, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/AdjunctionUnconditional.lean, line 278. The attribute's comment: “canonical counit”.

The derived counit agrees with the ordinary counit after applying the canonical comparison maps.

theorem derivedAdjunction_counit_fac
    (K : HomotopyCategory (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)) :
    (derivedPullback f).map ((derivedPushforwardUnit f).app K) ≫
        (derivedAdjunction f).counit.app (DerivedCategory.Qh.obj K) =
      (derivedPullbackComparison f).app
          (((modulePushforward f).mapHomotopyCategory (ComplexShape.up ℤ)).obj K) ≫
        DerivedCategory.Qh.map
          ((homotopyPullbackPushforwardAdjunction f).counit.app K)
Tag 0D5T, a lemma

Tag 0D5T in the Stacks Project.

Stacks.Cohomology.DerivedPushforwardComposition.isIso_derivedPushforwardComparison_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/CompositionUnconditional.lean, line 473.

Stacks 0D5T. For composable morphisms f : X ⟶ Y and g : Y ⟶ Z of ringed spaces, the canonical comparison from a right derived pushforward along f ≫ g to the composite of right derived pushforwards along f and g is an isomorphism.

No hypothesis beyond the two morphisms and the three derived functors: the condition PushforwardComputesDerived, which isIso_derivedPushforwardComparison_iff shows to be equivalent to this statement, is discharged by pushforwardComputesDerived.

theorem isIso_derivedPushforwardComparison_unconditional
    [Rf.IsRightDerivedFunctor αf
      (HomotopyCategory.quasiIso (ModuleSheaves.{u} X) (ComplexShape.up ℤ))]
    [Rg.IsRightDerivedFunctor αg
      (HomotopyCategory.quasiIso (ModuleSheaves.{u} Y) (ComplexShape.up ℤ))]
    [Rgf.IsRightDerivedFunctor αgf
      (HomotopyCategory.quasiIso (ModuleSheaves.{u} X) (ComplexShape.up ℤ))] :
    IsIso (derivedPushforwardComparison f g Rf Rg Rgf αf αg αgf)
Tag 08HY, a remark

Tag 08HY in the Stacks Project.

Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/BaseChangeMap.lean, line 286. The attribute's comment: “derived_base_change_map”. References: SGA 4 XVII (4.1.5), “ringed spaces”; SGA 4 XVII (4.1.4), “ringed spaces case”.

The derived base change map Lg^* (Rf_* K) ⟶ Rf'_* (Lg'^* K) of a commutative square of ringed spaces, at an object of the unbounded derived category. It is adjoint to the derived pullback along g' of the derived counit Lf^* (Rf_* K) ⟶ K, after identifying the two iterated derived pullbacks.

def derivedBaseChangeMap (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g).obj
      ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K) ⟶
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f').obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g').obj K)

Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/BaseChangeMap.lean, line 299. The attribute's comment: “adjoint characterization of the canonical map”.

Under the derived adjunction Lf'^* ⊣ Rf'_*, the base change map is the derived pullback of the counit, transported across the two composition isomorphisms.

theorem derivedBaseChangeMap_adjoint
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction f').homEquiv
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g).obj
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K))
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g').obj K)).symm
        (derivedBaseChangeMap g' f' f g sq K) =
      (derivedPullbackCompIsoLeft g' f' f g sq).hom.app
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K) ≫
        (derivedPullbackCompIsoCanonical g' f).inv.app
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K) ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g').map
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction f).counit.app K)
Tag 0ATL, a remark

Tag 0ATL in the Stacks Project.

Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/BaseChangePasting.lean, line 590.

Tag 0ATL. Derived base change for an outer rectangle is the composite of derived base change for its two constituent squares.

For two vertically composable commutative squares of ringed spaces, the composite of the derived pullback along the lower horizontal morphism of the inverse composition isomorphism of Tag 079W, the derived base change map of the lower square, the derived pushforward along the upper square's right-hand vertical of the derived base change map of the upper square, and the composition isomorphism of Tag 079W for the rectangle's left-hand verticals, is the derived base change map of the rectangle.

theorem derivedBaseChangeMap_comp (sq₁ : k ≫ f = f' ≫ l) (sq₂ : l ≫ g = g' ≫ m)
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    (derivedPullback m).map ((derivedPushforwardCompIso f g).inv.app K) ≫
        derivedBaseChangeMap l g' g m sq₂ ((derivedPushforward f).obj K) ≫
        (derivedPushforward g').map (derivedBaseChangeMap k f' f l sq₁ K) ≫
        (derivedPushforwardCompIso f' g').hom.app ((derivedPullback k).obj K) =
      derivedBaseChangeMap k (f' ≫ g') (f ≫ g) m (comp_square k f' f l g' g m sq₁ sq₂) K
Tag 0ATM, a remark

Tag 0ATM in the Stacks Project.

Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap_comp_horizontal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/BaseChangePasting.lean, line 846.

Tag 0ATM. Derived base change for an outer rectangle is the composite of derived base change for its two constituent squares.

For two horizontally composable commutative squares of ringed spaces, the composite of the inverse composition isomorphism of Tag 0D5S for h' ≫ h, the derived pullback along h' of the derived base change map of the right-hand square, the derived base change map of the left-hand square, and the derived pushforward along f'' of the composition isomorphism of Tag 0D5S for g' ≫ g, is the derived base change map of the rectangle.

theorem derivedBaseChangeMap_comp_horizontal (sq₁ : g ≫ f = f' ≫ h)
    (sq₂ : g' ≫ f' = f'' ≫ h')
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    (derivedPullbackCompIsoCanonical h' h).inv.app ((derivedPushforward f).obj K) ≫
        (derivedPullback h').map (derivedBaseChangeMap g f' f h sq₁ K) ≫
        derivedBaseChangeMap g' f'' f' h' sq₂ ((derivedPullback g).obj K) ≫
        (derivedPushforward f'').map ((derivedPullbackCompIsoCanonical g' g).hom.app K) =
      derivedBaseChangeMap (g' ≫ g) f'' f (h' ≫ h)
        (hcomp_square g' g f'' f' f h' h sq₁ sq₂) K
Tag 0FP1, a lemma

Tag 0FP1 in the Stacks Project.

Declarations registered for the tag:

Tag 0B68, a remark

Tag 0B68 in the Stacks Project.

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProduct.lean, line 173.

The relative cup product Rf_*K ⊗^L_{𝒪_Y} Rf_*M ⟶ Rf_*(K ⊗^L_{𝒪_X} M): the adjoint transpose of the derived pullback-tensor comparison of Stacks 079U followed by the counit of Lf^* ⊣ Rf_* in both tensor factors. It is defined for arbitrary K, M ∈ D(𝒪_X).

def relativeCupProduct
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf).obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K)).obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj M) ⟶
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj
        (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).obj K).obj M)

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProduct.lean, line 227. The attribute's comment: “naturality in both complexes”.

The relative cup product is natural in both derived modules on the source.

theorem relativeCupProduct_natural
    {K K' M M' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    (k : K ⟶ K') (m : M ⟶ M') :
    (Functor.uncurry.obj
          (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf)).map
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map k ×ₘ
          (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map m) ≫
        relativeCupProduct f K' M' =
      relativeCupProduct f K M ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map
          ((Functor.uncurry.obj
            (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf)).map
              (k ×ₘ m))

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProduct.lean, line 250. The attribute's comment: “naturality in the first complex”.

The relative cup product is natural in the first derived module.

theorem relativeCupProduct_natural_left
    {K K' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    (k : K ⟶ K')
    (M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf).map
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map k)).app
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj M) ≫
        relativeCupProduct f K' M =
      relativeCupProduct f K M ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map
          (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).map k).app M)

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProduct.lean, line 271. The attribute's comment: “naturality in the second complex”.

The relative cup product is natural in the second derived module.

theorem relativeCupProduct_natural_right
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    {M M' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    (m : M ⟶ M') :
    ((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf).obj
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K)).map
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map m) ≫
        relativeCupProduct f K M' =
      relativeCupProduct f K M ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).map
          (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).obj K).map m)
Sources
LeanStacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction · Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction_unit_fac · Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction_counit_fac · Stacks.Cohomology.DerivedPushforwardComposition.isIso_derivedPushforwardComparison_unconditional · Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap · Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap_adjoint · Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap_comp · Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap_comp_horizontal

Section20.29 Cohomology of filtered complexes#

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

Tag 0BKK, a lemma

Tag 0BKK in the Stacks Project.

Stacks.Cohomology.FilteredComplex.spectralSequence_of_filteredKInjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/FilteredKInjectiveResolution.lean, line 523. The attribute's comment: “computation by a supplied filtered K-injective resolution”.

The spectral sequence of a filtered complex of module sheaves, computed by a supplied filtered K-injective resolution: its pages are presented by the cycle and boundary subobjects of the filtered complex of global sections, its first page is the hypercohomology of the graded pieces, and under the boundedness hypotheses it converges to the hypercohomology of the complex.

theorem spectralSequence_of_filteredKInjectiveResolution
    (hRΓ : RΓ.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)))
    (j : K ⟶ J)
    (hj : QuasiIso j.hom)
    (hjStep : ∀ p : ℤ, QuasiIso (j.natTrans.app (op p)))
    (hjGraded : ∀ p : ℤ, QuasiIso ((FilteredObject.gr p).map j))
    (hStepInjective : ∀ p n : ℤ, Injective ((J.filtration.obj (op p)).X n))
    (hKInjective : J.X.IsKInjective)
    (hStepKInjective : ∀ p : ℤ, (J.filtration.obj (op p)).IsKInjective)
    (hGradedKInjective : ∀ p : ℤ, ((FilteredObject.gr p).obj J).IsKInjective) :
    let E := CochainComplex.Filtered.spectralSequenceFunctor.obj
      (globalSectionsFilteredComplex X J)
    ∃ (F : ∀ (_p n : ℤ), Subobject ((globalSectionsFilteredComplex X J).X.X n))
        (Z D : ∀ (_r _p n : ℤ),
          Subobject ((globalSectionsFilteredComplex X J).X.X n)),
        (∀ p n : ℤ, F p n = Subobject.mk
          (((globalSectionsFilteredComplex X J).filtration.ι.app (op p)).f n)) ∧
        (∀ r p n : ℤ, Z r p n = F p n ⊓
          (Subobject.pullback ((globalSectionsFilteredComplex X J).X.d n (n + 1))).obj
            (F (p + r) (n + 1))) ∧
        (∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
          (Subobject.«exists» ((globalSectionsFilteredComplex X J).X.d (n - 1) n)).obj
            (Z (r - 1) (p - r + 1) (n - 1))) ∧
        (∃ e : ∀ (r p q n : ℤ) (hr : 0 ≤ r) (_ : n = p + q),
            (E.page r hr).X (p, q) ≅ cokernel
              (Subobject.ofLE _ _ (inf_le_right : D r p n ⊓ Z r p n ≤ Z r p n)),
          ∀ (r p q n : ℤ) (hr : 0 ≤ r) (hn : n = p + q),
            ∃ δ : (Z r p n : ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))) ⟶
                (Z r (p + r) (n + 1) : ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))),
              δ ≫ (Z r (p + r) (n + 1)).arrow =
                  (Z r p n).arrow ≫ (globalSectionsFilteredComplex X J).X.d n (n + 1) ∧
              cokernel.π (Subobject.ofLE _ _
                  (inf_le_right : D r p n ⊓ Z r p n ≤ Z r p n)) ≫
                    (e r p q n hr hn).inv ≫
                    (E.page r hr).d (p, q) (p + r, q - r + 1) =
                δ ≫ cokernel.π (Subobject.ofLE _ _
                    (inf_le_right : D r (p + r) (n + 1) ⊓ Z r (p + r) (n + 1) ≤
                      Z r (p + r) (n + 1))) ≫
                  (e r (p + r) (q - r + 1) (n + 1) hr (by omega)).inv) ∧
        (∀ p q : ℤ, Nonempty
          ((E.page 1 (by omega)).X (p, q) ≅
            hypercohomology X RΓ ((FilteredObject.gr p).obj K) (p + q))) ∧
        ((∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
            IsZero (hypercohomology X RΓ (K.filtration.obj (op p)) n)) →
          (∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
            IsIso (hypercohomologyMap X RΓ (K.filtration.ι.app (op p)) n)) →
          (∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 1 (by omega)).X (p, n - p))}.Finite) ∧
            ∃ (F : ∀ n : ℤ, ℤ → Subobject (hypercohomology X RΓ K.X n))
              (hF : ∀ n : ℤ, Antitone (F n)),
              (∀ n p : ℤ, F n p = imageSubobject
                (hypercohomologyMap X RΓ (K.filtration.ι.app (op p)) n)) ∧
              (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ F n a = ⊤ ∧ F n b = ⊥) ∧
              (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
              ∀ p q : ℤ, Nonempty
                (E.pageInfinity (p, q) ≅
                  cokernel (Subobject.ofLE (F (p + q) (p + 1)) (F (p + q) p)
                    (hF (p + q) (by omega)))))

Stacks.Cohomology.FilteredComplex.exists_spectralSequence_of_filteredComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/FilteredKInjectiveResolution.lean, line 598.

A filtered complex of modules on a ringed space has a cohomological spectral sequence whose first page is the hypercohomology of its graded pieces. If the hypercohomology of the filtration steps eventually vanishes on the right and maps isomorphically to that of the whole complex on the left, the spectral sequence is bounded and converges to the hypercohomology of the complex.

theorem exists_spectralSequence_of_filteredComplex :
    ∃ (RΓ : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
        DerivedCategory (ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))))
      (α : homotopySections (structureSheafRing X) (⊤ : Opens X.carrier) ⟶ DerivedCategory.Qh ⋙ RΓ),
      RΓ.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso
            (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)) ∧
      ∃ (J : CochainComplex.Filtered (SheafOfModules.{u} (structureSheafRing X))) (j : K ⟶ J),
      QuasiIso j.hom ∧
      (∀ p : ℤ, QuasiIso (j.natTrans.app (op p))) ∧
      (∀ p : ℤ, QuasiIso ((FilteredObject.gr p).map j)) ∧
      (∀ n : ℤ, Injective (J.X.X n)) ∧
      (∀ p n : ℤ, Injective ((J.filtration.obj (op p)).X n)) ∧
      (∀ p n : ℤ, Injective (((FilteredObject.gr p).obj J).X n)) ∧
      ∃ (E : CohomologicalSpectralSequence
          (ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))) 0)
        (F : ∀ (_p n : ℤ), Subobject ((globalSectionsFilteredComplex X J).X.X n))
        (Z D : ∀ (_r _p n : ℤ),
          Subobject ((globalSectionsFilteredComplex X J).X.X n)),
        (∀ p n : ℤ, F p n = Subobject.mk
          (((globalSectionsFilteredComplex X J).filtration.ι.app (op p)).f n)) ∧
        (∀ r p n : ℤ, Z r p n = F p n ⊓
          (Subobject.pullback ((globalSectionsFilteredComplex X J).X.d n (n + 1))).obj
            (F (p + r) (n + 1))) ∧
        (∀ r p n : ℤ, D r p n = Z (r - 1) (p + 1) n ⊔
          (Subobject.«exists» ((globalSectionsFilteredComplex X J).X.d (n - 1) n)).obj
            (Z (r - 1) (p - r + 1) (n - 1))) ∧
        (∃ e : ∀ (r p q n : ℤ) (hr : 0 ≤ r) (_ : n = p + q),
            (E.page r hr).X (p, q) ≅ cokernel
              (Subobject.ofLE _ _ (inf_le_right : D r p n ⊓ Z r p n ≤ Z r p n)),
          ∀ (r p q n : ℤ) (hr : 0 ≤ r) (hn : n = p + q),
            ∃ δ : (Z r p n : ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))) ⟶
                (Z r (p + r) (n + 1) : ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))),
              δ ≫ (Z r (p + r) (n + 1)).arrow =
                  (Z r p n).arrow ≫ (globalSectionsFilteredComplex X J).X.d n (n + 1) ∧
              cokernel.π (Subobject.ofLE _ _
                  (inf_le_right : D r p n ⊓ Z r p n ≤ Z r p n)) ≫
                    (e r p q n hr hn).inv ≫
                    (E.page r hr).d (p, q) (p + r, q - r + 1) =
                δ ≫ cokernel.π (Subobject.ofLE _ _
                    (inf_le_right : D r (p + r) (n + 1) ⊓ Z r (p + r) (n + 1) ≤
                      Z r (p + r) (n + 1))) ≫
                  (e r (p + r) (q - r + 1) (n + 1) hr (by omega)).inv) ∧
        (∀ p q : ℤ, Nonempty
          ((E.page 1 (by omega)).X (p, q) ≅
            hypercohomology X RΓ ((FilteredObject.gr p).obj K) (p + q))) ∧
        ((∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
            IsZero (hypercohomology X RΓ (K.filtration.obj (op p)) n)) →
          (∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
            IsIso (hypercohomologyMap X RΓ (K.filtration.ι.app (op p)) n)) →
          (∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 1 (by omega)).X (p, n - p))}.Finite) ∧
            ∃ (F : ∀ n : ℤ, ℤ → Subobject (hypercohomology X RΓ K.X n))
              (hF : ∀ n : ℤ, Antitone (F n)),
              (∀ n p : ℤ, F n p = imageSubobject
                (hypercohomologyMap X RΓ (K.filtration.ι.app (op p)) n)) ∧
              (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ F n a = ⊤ ∧ F n b = ⊥) ∧
              (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
              ∀ p q : ℤ, Nonempty
                (E.pageInfinity (p, q) ≅
                  cokernel (Subobject.ofLE (F (p + q) (p + 1)) (F (p + q) p)
                    (hF (p + q) (by omega)))))
Tag 0BKL, a remark

Tag 0BKL in the Stacks Project.

Stacks.Cohomology.FilteredComplex.exists_spectralSequence_of_boundedBelowFilteredComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HypercohomologySpectralSequence.lean, line 714. References: EGA 0 (13.7.3), “ringed space, bdd below”.

Stacks 0BKL. Let (X, O_X) be a ringed space and let K^• be a filtered complex of O_X-modules which is bounded below and whose filtration is finite in each degree. Then the spectral sequence of [Stacks, Tag 0BKK] can be built without a filtered K-injective resolution: a filtered quasi-isomorphism i : K^• ⟶ I^• as in [Stacks, Tag 05TW], with I^• bounded below, the filtration on each I^n finite and each gr^pI^n injective, gives the filtered complex Γ(X, I^•) with F^pΓ(X, I^•) = Γ(X, F^pI^•), whose spectral sequence has first page E_1^{p, q} = H^{p + q}(X, gr^pK^•) and is bounded and converges to H^*(X, K^•) with a finite induced filtration.

theorem exists_spectralSequence_of_boundedBelowFilteredComplex (X : RingedSpace.{u, u})
    (RΓ : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))))
    (α : homotopySections (structureSheafRing X) (⊤ : Opens X.carrier) ⟶ DerivedCategory.Qh ⋙ RΓ)
    (hRΓ : RΓ.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)))
    (K : CochainComplex.Filtered (SheafOfModules.{u} (structureSheafRing X))) (a : ℤ)
    (hK : K.X.IsStrictlyGE a) (hKfin : K.filtration.IsDegreewiseFinite) :
    ∃ (I : CochainComplex.Filtered (SheafOfModules.{u} (structureSheafRing X))) (i : K ⟶ I),
      I.X.IsStrictlyGE a ∧
      I.filtration.IsDegreewiseFinite ∧
      (∀ n : ℤ, (CochainComplex.evalFil I n).IsFilteredInjective) ∧
      (∀ p : ℤ, QuasiIso ((FilteredObject.gr p).map i)) ∧
      (∀ p : ℤ, QuasiIso (i.natTrans.app (op p))) ∧
      QuasiIso i.hom ∧
      (∀ p : ℤᵒᵖ, (globalSectionsFilteredComplex X I).filtration.obj p =
        (globalSectionsComplexFunctor X).obj (I.filtration.obj p)) ∧
      (∀ p q : ℤ, Nonempty
        (((globalSectionsSpectralSequence X I).page 1 (by omega)).X (p, q) ≅
          hypercohomology X RΓ ((FilteredObject.gr p).obj K) (p + q))) ∧
      (∀ n : ℤ, {p : ℤ | ¬ IsZero
        (((globalSectionsSpectralSequence X I).page 1 (by omega)).X (p, n - p))}.Finite) ∧
      ∃ (F : ∀ n : ℤ, ℤ → Subobject (hypercohomology X RΓ K.X n))
        (hF : ∀ n : ℤ, Antitone (F n)),
        (∀ n p : ℤ, F n p = imageSubobject
          (hypercohomologyMap X RΓ (K.filtration.ι.app (op p)) n)) ∧
        (∀ n : ℤ, ∃ b c : ℤ, b ≤ c ∧ F n b = ⊤ ∧ F n c = ⊥) ∧
        (∀ p q : ℤ, (globalSectionsSpectralSequence X I).HasPageInfinityAt (p, q)) ∧
        ∀ p q : ℤ, Nonempty
          ((globalSectionsSpectralSequence X I).pageInfinity (p, q) ≅
            cokernel (Subobject.ofLE (F (p + q) (p + 1)) (F (p + q) p)
              (hF (p + q) (by omega))))
Tag 0BKM, an example

Tag 0BKM in the Stacks Project.

Stacks.Cohomology.FilteredComplex.exists_canonicalTruncationSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HypercohomologySpectralSequence.lean, line 210. The attribute's comment: “truncation_e1_page”.

Stacks 0BKM. For every complex of modules on a ringed space, the canonical truncation filtration gives a spectral sequence with E_1^{p, q} = H^{p + q}(X, H^{-p}(K^•)[p]) = H^{2p + q}(X, H^{-p}(K^•)).

theorem exists_canonicalTruncationSpectralSequence (X : RingedSpace.{u, u})
    (K : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ) :
    Nonempty (CanonicalTruncationSpectralSequence X K)

Stacks.Cohomology.FilteredComplex.exists_boundedBelowTruncationSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HypercohomologySpectralSequence.lean, line 791. The attribute's comment: “truncation_e1_page”. References: EGA 0 (11.4.3), “''E₂, T = RΓ”; EGA 0 (12.4.1), “''E2, absolute case”.

Stacks 0BKM, through Remark 0BKL. For a bounded-below complex the canonical truncation spectral sequence can also be built from a bounded-below filtered replacement whose filtration is finite in every degree and whose graded terms are injective; the first-page formula is the same.

theorem exists_boundedBelowTruncationSpectralSequence (X : RingedSpace.{u, u})
    (K : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ)
    (hK : ∃ a : ℤ, K.IsStrictlyGE a) :
    ∃ (S : CanonicalTruncationSpectralSequence X K) (a : ℤ),
      S.injectiveReplacement.X.IsStrictlyGE a ∧
      S.injectiveReplacement.filtration.IsDegreewiseFinite ∧
      ∀ p q : ℤ, Nonempty
        (((globalSectionsSpectralSequence X S.injectiveReplacement).page 1
            (by omega)).X (p, q) ≅
          (DerivedCategory.homologyFunctor
            (ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))) (2 * p + q)).obj
              (S.RΓ.obj ((DerivedCategory.singleFunctor
                (SheafOfModules.{u} (structureSheafRing X)) 0).obj
                  ((DerivedCategory.homologyFunctor
                    (SheafOfModules.{u} (structureSheafRing X)) (-p)).obj
                      (DerivedCategory.Q.obj K)))))

Stacks.Cohomology.FilteredComplex.hypercohomologySpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HypercohomologySpectralSequence.lean, line 872. The attribute's comment: “hypercohomology_e2_page”.

Stacks 0BKM. The hypercohomology spectral sequence of an object of the derived category of module sheaves on a ringed space: take a representative, filter it by its canonical truncations, apply derived global sections, and renumber the resulting spectral sequence.

def hypercohomologySpectralSequence (X : RingedSpace.{u, u})
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    HypercohomologySpectralSequence X K

Stacks.Cohomology.FilteredComplex.hypercohomologySpectralSequence_e₂, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HypercohomologySpectralSequence.lean, line 882. The attribute's comment: “hypercohomology_e2_page”.

Stacks 0BKM. The second page of the hypercohomology spectral sequence is the hypercohomology of the cohomology objects of K: E_2^{i, j} = H^i(X, H^j(K)).

theorem hypercohomologySpectralSequence_e₂ (X : RingedSpace.{u, u})
    (K : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) (i j : ℤ) :
    Nonempty (((hypercohomologySpectralSequence X K).spectralSequence.page 2).X (i, j) ≅
      (DerivedCategory.homologyFunctor
          (ModuleCat.{u} ((structureSheafRing X).obj.obj (op ⊤))) i).obj
        ((hypercohomologySpectralSequence X K).truncation.RΓ.obj
          ((DerivedCategory.singleFunctor (SheafOfModules.{u} (structureSheafRing X)) 0).obj
            ((DerivedCategory.homologyFunctor
              (SheafOfModules.{u} (structureSheafRing X)) j).obj K))))

Stacks.Cohomology.FilteredComplex.exists_boundedBelowHypercohomologySpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HypercohomologySpectralSequence.lean, line 923. The attribute's comment: “bounded below: the renumbered sequence is bounded and converges to H^{i+j}(X, K)”. References: EGA 0 (11.4.3), “T = RΓ, bounded below”; EGA III (6.2.1), “absolute case, Y=point”; EGA 0 (12.4.1), “abutment, absolute case”.

Stacks 0BKM, the closing clause. If K^• is bounded below, the renumbered spectral sequence -- the one whose second page is H^i(X, H^j(K^•)) -- is bounded, and it converges to H^{i + j}(X, K^•): some finite decreasing filtration of H^n(X, K^•) has the terms E_∞^{i, n - i} of its infinity page as graded pieces.

The spectral sequence is the one of exists_boundedBelowTruncationSpectralSequence, i.e. the one built through Remark [Stacks, Tag 0BKL] from a bounded-below filtered replacement; boundedness and convergence of that sequence before the renumbering are boundedReplacement_convergence, which needs no hypothesis beyond degreewise finiteness of the replacement's filtration, and they are carried across the bidegree change (i, j) ↦ (-j, i + 2j) by CategoryTheory.SpectralSequence.truncationRenumber_finite_not_isZero_page_two and CategoryTheory.SpectralSequence.AbutsTo.truncationRenumberRestrictPages. The abutment is read on K^• itself rather than on the underlying complex of the filtration by CategoryTheory.SpectralSequence.AbutsTo.of_iso.

theorem exists_boundedBelowHypercohomologySpectralSequence (X : RingedSpace.{u, u})
    (K : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ)
    (hK : ∃ a : ℤ, K.IsStrictlyGE a) :
    ∃ S : HypercohomologySpectralSequence X (DerivedCategory.Q.obj K),
      IsBounded S.spectralSequence ∧
        SpectralSequence.AbutsTo S.spectralSequence
          (fun n => hypercohomology X S.truncation.RΓ K n)
Tag 0FLK, an example

Tag 0FLK in the Stacks Project.

Stacks.Cohomology.FilteredComplex.exists_stupidTruncationSpectralSequence_iso_cartanEilenbergFirst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/CartanEilenbergComparison.lean, line 287. The attribute's comment: “bounded below: boundedness, convergence to H^{i + j}(X, F) and the identification with the first spectral sequence of Cartan-Eilenberg (Tag 015J) for one and the same package — the tag's three bounded-below assertions together”. References: EGA 0 (11.4.3), “'E, T = RΓ, bdd below”; EGA 0 (12.4.1), “'E abutment, absolute”; EGA 0 (12.1.7), “boundedness”.

Clause (3) of [Stacks, Tag 0FLK] in the existential shape of clauses (1) and (2). For a bounded below complex of module sheaves there is a brutal-truncation package whose spectral sequence is bounded, converges to H^{i + j}(X, F^•), and is isomorphic to the first spectral sequence of every Cartan-Eilenberg resolution of F^•.

This is exists_boundedBelowStupidTruncationSpectralSequence with the comparison nonempty_spectralSequence_iso_cartanEilenbergFirst added for the package it produces.

theorem exists_stupidTruncationSpectralSequence_iso_cartanEilenbergFirst
    (F : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ) (a : ℤ)
    (hF : F.IsStrictlyGE a) :
    ∃ S : StupidTruncationSpectralSequence X F,
      IsBounded S.spectralSequence ∧
      SpectralSequence.AbutsTo S.spectralSequence (fun n => hypercohomology X S.RΓ F n) ∧
      ∀ I : F.CartanEilenbergResolution,
        Nonempty (S.spectralSequence ≅ cartanEilenbergFirstSpectralSequence X I)

Stacks.Cohomology.FilteredComplex.exists_stupidTruncationSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/StupidTruncationSpectralSequence.lean, line 268. The attribute's comment: “for every complex of module sheaves: the brutal truncation filtration gives a spectral sequence with E_1^{p, q} = H^{p + q}(X, F^p[-p]) = H^q(X, F^p). The tag's three further assertions concern F^• bounded below and are exists_boundedBelowStupidTruncationSpectralSequence and exists_stupidTruncationSpectralSequence_iso_cartanEilenbergFirst”.

Stacks 0FLK. For every complex of module sheaves on a ringed space, the brutal truncation filtration F^pF^• = σ_{≥ p}F^• gives a spectral sequence with E_1^{p, q} = H^{p + q}(X, F^p[-p]) = H^q(X, F^p).

theorem exists_stupidTruncationSpectralSequence (X : RingedSpace.{u, u})
    (F : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ) :
    Nonempty (StupidTruncationSpectralSequence X F)

Stacks.Cohomology.FilteredComplex.exists_boundedBelowStupidTruncationSpectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/StupidTruncationSpectralSequence.lean, line 293. The attribute's comment: “bounded below: the sequence is constructed via Remark 0BKL, is bounded and converges to H^{i + j}(X, F); the identification with the first spectral sequence of Cartan-Eilenberg (Tag 015J) is Stacks.Cohomology.FilteredComplex.exists_stupidTruncationSpectralSequence_iso_cartanEilenbergFirst”. References: EGA 0 (11.4.3), “'E, T = RΓ, bdd below”; EGA 0 (12.4.1), “'E abutment, absolute”.

Stacks 0FLK, the bounded below case. If F^• is bounded below, the brutal truncation spectral sequence can be built through Remark [Stacks, Tag 0BKL], from a bounded below filtered injective replacement whose filtration is finite in every degree, with no filtered K-injective resolution; and it is bounded and converges to H^{i + j}(X, F^•).

theorem exists_boundedBelowStupidTruncationSpectralSequence (X : RingedSpace.{u, u})
    (F : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ) (a : ℤ)
    (hF : F.IsStrictlyGE a) :
    ∃ S : StupidTruncationSpectralSequence X F,
      S.replacement.X.IsStrictlyGE a ∧
      S.replacement.filtration.IsDegreewiseFinite ∧
      (∀ n : ℤ, (CochainComplex.evalFil S.replacement n).IsFilteredInjective) ∧
      IsBounded S.spectralSequence ∧
      SpectralSequence.AbutsTo S.spectralSequence
        (fun n => hypercohomology X S.RΓ F n)
Tag 0FLL, a lemma

Tag 0FLL in the Stacks Project.

Stacks.Cohomology.FilteredComplex.relativeSpectralSequence_of_filteredKInjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HigherDirectImageSpectralSequence.lean, line 552. The attribute's comment: “computation by a supplied filtered K-injective resolution”.

Stacks 0FLL, the first page and the conditional bounded convergence, for a supplied filtered K-injective resolution. The right-derived pushforward, its unit and the resolution are fixed inputs, so all of the conclusions concern these same data.

theorem relativeSpectralSequence_of_filteredKInjectiveResolution
    (hRf : Rf.IsRightDerivedFunctor η
      (HomotopyCategory.quasiIso (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)))
    (j : K ⟶ J)
    (hj : QuasiIso j.hom)
    (hjStep : ∀ p : ℤ, QuasiIso (j.natTrans.app (op p)))
    (hjGraded : ∀ p : ℤ, QuasiIso ((FilteredObject.gr p).map j))
    (hStepInjective : ∀ p n : ℤ, Injective ((J.filtration.obj (op p)).X n))
    (hKInjective : J.X.IsKInjective)
    (hStepKInjective : ∀ p : ℤ, (J.filtration.obj (op p)).IsKInjective)
    (hGradedKInjective : ∀ p : ℤ, ((FilteredObject.gr p).obj J).IsKInjective) :
    let E := pushforwardSpectralSequence f J
    (∀ p q : ℤ, Nonempty
      ((E.page 1 (by omega)).X (p, q) ≅
        higherDirectImage (X := X) (Y := Y) Rf ((FilteredObject.gr p).obj K) (p + q))) ∧
      ((∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
          IsZero (higherDirectImage Rf (K.filtration.obj (op p)) n)) →
        (∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
          IsIso (higherDirectImageMap Rf (K.filtration.ι.app (op p)) n)) →
        (∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 1 (by omega)).X (p, n - p))}.Finite) ∧
          ∃ (F : ∀ n : ℤ, ℤ → Subobject (higherDirectImage Rf K.X n))
            (hF : ∀ n : ℤ, Antitone (F n)),
            (∀ n p : ℤ, F n p = imageSubobject
              (higherDirectImageMap Rf (K.filtration.ι.app (op p)) n)) ∧
            (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ F n a = ⊤ ∧ F n b = ⊥) ∧
            (∀ p q : ℤ, E.HasPageInfinityAt (p, q)) ∧
            ∀ p q : ℤ, Nonempty
              (E.pageInfinity (p, q) ≅
                cokernel (Subobject.ofLE (F (p + q) (p + 1)) (F (p + q) p)
                  (hF (p + q) (by omega)))))

Stacks.Cohomology.FilteredComplex.exists_relativeSpectralSequence_of_filteredComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/FilteredComplexSpectralSequence/HigherDirectImageSpectralSequence.lean, line 594.

Stacks 0FLL. A filtered complex of O_X-modules has a canonical cohomological spectral sequence of O_Y-modules, with d_r of bidegree (r, -r + 1), whose first page is E_1^{p, q} = R^{p + q}f_*gr^pF^•. If for every n the higher direct image R^nf_*F^pF^• vanishes for p ≫ 0 and maps isomorphically to R^nf_*F^• for p ≪ 0, the spectral sequence is bounded and converges to R^*f_*F^•.

theorem exists_relativeSpectralSequence_of_filteredComplex :
    ∃ (Rf : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
        DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
      (η : homotopyPushforward f ⟶ DerivedCategory.Qh ⋙ Rf),
      Rf.IsRightDerivedFunctor η
          (HomotopyCategory.quasiIso
            (SheafOfModules.{u} (structureSheafRing X)) (ComplexShape.up ℤ)) ∧
      ∃ (J : CochainComplex.Filtered (SheafOfModules.{u} (structureSheafRing X))) (j : K ⟶ J),
      QuasiIso j.hom ∧
      (∀ p : ℤ, QuasiIso (j.natTrans.app (op p))) ∧
      (∀ p : ℤ, QuasiIso ((FilteredObject.gr p).map j)) ∧
      (∀ n : ℤ, Injective (J.X.X n)) ∧
      (∀ p n : ℤ, Injective ((J.filtration.obj (op p)).X n)) ∧
      (∀ p n : ℤ, Injective (((FilteredObject.gr p).obj J).X n)) ∧
      (∀ p q : ℤ, Nonempty
        (((pushforwardSpectralSequence f J).page 1 (by omega)).X (p, q) ≅
          higherDirectImage (X := X) (Y := Y) Rf ((FilteredObject.gr p).obj K) (p + q))) ∧
      ((∀ n : ℤ, ∃ p₀ : ℤ, ∀ p : ℤ, p₀ ≤ p →
          IsZero (higherDirectImage Rf (K.filtration.obj (op p)) n)) →
        (∀ n : ℤ, ∃ p₁ : ℤ, ∀ p : ℤ, p ≤ p₁ →
          IsIso (higherDirectImageMap Rf (K.filtration.ι.app (op p)) n)) →
        (∀ n : ℤ, {p : ℤ | ¬ IsZero
          (((pushforwardSpectralSequence f J).page 1 (by omega)).X (p, n - p))}.Finite) ∧
          ∃ (F : ∀ n : ℤ, ℤ → Subobject (higherDirectImage Rf K.X n))
            (hF : ∀ n : ℤ, Antitone (F n)),
            (∀ n p : ℤ, F n p = imageSubobject
              (higherDirectImageMap Rf (K.filtration.ι.app (op p)) n)) ∧
            (∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ F n a = ⊤ ∧ F n b = ⊥) ∧
            (∀ p q : ℤ, (pushforwardSpectralSequence f J).HasPageInfinityAt (p, q)) ∧
            ∀ p q : ℤ, Nonempty
              ((pushforwardSpectralSequence f J).pageInfinity (p, q) ≅
                cokernel (Subobject.ofLE (F (p + q) (p + 1)) (F (p + q) p)
                  (hF (p + q) (by omega)))))
Sources
LeanStacks.Cohomology.FilteredComplex.spectralSequence_of_filteredKInjectiveResolution · Stacks.Cohomology.FilteredComplex.exists_spectralSequence_of_filteredComplex · Stacks.Cohomology.FilteredComplex.exists_spectralSequence_of_boundedBelowFilteredComplex · Stacks.Cohomology.FilteredComplex.exists_canonicalTruncationSpectralSequence · Stacks.Cohomology.FilteredComplex.exists_boundedBelowTruncationSpectralSequence · Stacks.Cohomology.FilteredComplex.hypercohomologySpectralSequence · Stacks.Cohomology.FilteredComplex.hypercohomologySpectralSequence_e₂ · Stacks.Cohomology.FilteredComplex.exists_boundedBelowHypercohomologySpectralSequence

Section20.30 Godement resolution#

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

Tag 0FKS, a lemma

Tag 0FKS in the Stacks Project.

AlgebraicGeometry.GodementResolution.isFlasque_iterate_modulePullbackPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/GodementResolution/Basic.lean, line 276. The attribute's comment: “each term f_ f^ ⋯ f_ f^ F is a flasque module”. References: SGA 4 XVII (4.2.3), “(i)”; SGA 4 XVII (4.2), “flasqueness of terms”.

Every positive iterate (f_* f^*)^(n+1) F of a morphism out of a discrete space is a flasque sheaf of modules: a sheaf on a discrete space is flasque, and pushforward preserves flasqueness.

theorem isFlasque_iterate_modulePullbackPushforward
    {Xdisc X : RingedSpace.{u, u}} (f : Xdisc ⟶ X) [DiscreteTopology Xdisc]
    (n : ℕ) (F : SheafOfModules.{u} (structureSheafRing X)) :
    TopCat.Sheaf.IsFlasque ((SheafOfModules.toSheaf (structureSheafRing X)).obj
      (((RingedSpaceModuleAdjunction.modulePullback f ⋙
        RingedSpaceModuleAdjunction.modulePushforward f).iterate (n + 1)).obj F))

AlgebraicGeometry.GodementResolution.exists_functorial_flasque_godementComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/GodementResolution/Basic.lean, line 518. The attribute's comment: “the functorial complex of flasque terms f_ f^ ⋯ f_ f^ F”. References: SGA 4 XVII (4.2.3), “(i)”; SGA 4 XVII (4.2), “functorial flasque terms”.

Stacks 0FKS, the complex and its flasque terms. For a ringed space (X, O_X) there is a functor G from sheaves of O_X-modules to cochain complexes, with an augmentation η from the complex concentrated in degree 0, whose term in degree n is the iterate (f_* f^*)^(n+1) F along the morphism f : X_disc ⟶ X from the points of X with the discrete topology, and each of whose terms is a flasque O_X-module.

theorem exists_functorial_flasque_godementComplex (X : RingedSpace.{u, u}) :
    ∃ (G : SheafOfModules.{u} (structureSheafRing X) ⥤
        CochainComplex
          (SheafOfModules.{u} (structureSheafRing X)) ℕ)
      (_η : CochainComplex.single₀
          (SheafOfModules.{u} (structureSheafRing X)) ⟶ G)
      (_termIso : ∀ n,
        G ⋙ HomologicalComplex.eval
            (SheafOfModules.{u} (structureSheafRing X))
            (ComplexShape.up ℕ) n ≅
          (RingedSpaceModuleAdjunction.modulePullback (fromDiscrete X) ⋙
            RingedSpaceModuleAdjunction.modulePushforward (fromDiscrete X)).iterate (n + 1)),
      ∀ F n, TopCat.Sheaf.IsFlasque
        ((SheafOfModules.toSheaf (structureSheafRing X)).obj
          ((G.obj F).X n))

AlgebraicGeometry.GodementResolution.homotopyEquivalences_stalk_godementAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/GodementResolution/StalkHomotopy.lean, line 520. The attribute's comment: “the stalkwise homotopy equivalence F_x[0] ≃ ((f_ f^ F)_x → ⋯)”. References: SGA 4 XVII (4.2.3), “(ii)”; SGA 4 XVII (4.2), “stalkwise homotopy”; SGA 4 XVII (4.2.9), “special case”.

Clause (5) of [Stacks, Tag 0FKS], at one sheaf and one point. The augmentation F[0] ⟶ (f_* f^* F → f_* f^* f_* f^* F → ⋯) of the Godement complex, read on the stalk at x, is a homotopy equivalence of complexes of 𝒪_{X,x}-modules.

This is hasNaturalStalkHomotopy_godementAugmentation evaluated at F: evaluation at F is an additive functor, so it carries the homotopy equivalence of complexes of functors to one of complexes of modules, and the compatibility clause identifies the result with the stalk of the augmentation up to the two isomorphisms i and j.

theorem homotopyEquivalences_stalk_godementAugmentation (x : X)
    (F : SheafOfModules.{u} (structureSheafRing X)) :
    HomologicalComplex.homotopyEquivalences (StalkModuleCat X x) (ComplexShape.up ℕ)
      (((SheafOfModules.stalkFunctor (structureSheafRing X) x).mapHomologicalComplex
        (ComplexShape.up ℕ)).map ((godementAugmentation X).app F))

AlgebraicGeometry.GodementResolution.quasiIso_godementAugmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/GodementResolution/StalkHomotopy.lean, line 558. The attribute's comment: “exactness of the augmented complex 0 → F → f_ f^ F → ⋯”. References: SGA 4 XVII (4.2.3), “(ii)”; SGA 4 XVII (4.2), “augmented exactness”.

Clause (3) of [Stacks, Tag 0FKS]: the augmented Godement complex is exact. The augmentation F[0] ⟶ G(F) is a quasi-isomorphism, so 0 → F → f_* f^* F → f_* f^* f_* f^* F → ⋯ is exact and the Godement complex is a flasque resolution of F.

Quasi-isomorphy is detected on stalks (quasiIso_of_forall_stalk_quasiIso_nat), and on each stalk the augmentation is a homotopy equivalence by homotopyEquivalences_stalk_godementAugmentation, hence a quasi-isomorphism.

theorem quasiIso_godementAugmentation (F : SheafOfModules.{u} (structureSheafRing X)) :
    QuasiIso ((godementAugmentation X).app F)
Tag 0FKT, a lemma

Tag 0FKT in the Stacks Project.

AlgebraicGeometry.GodementResolution.exists_quasiIso_boundedBelow_isFlasque_isHomotopyEquiv_stalk_godement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/GodementBoundedBelowResolution.lean, line 1223. The attribute's comment: “Godement resolution; all four clauses, including the stalkwise homotopy equivalence”.

[Stacks, Tag 0FKT], all four clauses, for the Godement resolution. For a bounded below complex F of 𝒪_X-modules there is a quasi-isomorphism F ⟶ G with G bounded below in the same degree, every term of G flasque, and, for every x ∈ X, the stalk map F_x ⟶ G_x a homotopy equivalence of complexes of 𝒪_{X,x}-modules. The map is godementComparisonMap onto the totalisation of the Godement double complex of F.

theorem exists_quasiIso_boundedBelow_isFlasque_isHomotopyEquiv_stalk_godement
    (hF : ∃ n : ℤ, F.IsStrictlyGE n) :
    ∃ (G : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ) (f : F ⟶ G),
      QuasiIso f ∧ (∃ n : ℤ, G.IsStrictlyGE n) ∧
        (∀ i : ℤ, TopCat.Sheaf.IsFlasque
          ((SheafOfModules.toSheaf (structureSheafRing X)).obj (G.X i))) ∧
        (∀ x : X, ∃ e : HomotopyEquiv ((stalkComplexFunctor X x).obj F)
            ((stalkComplexFunctor X x).obj G), e.hom = (stalkComplexFunctor X x).map f)
Sources
LeanAlgebraicGeometry.GodementResolution.isFlasque_iterate_modulePullbackPushforward · AlgebraicGeometry.GodementResolution.exists_functorial_flasque_godementComplex · AlgebraicGeometry.GodementResolution.homotopyEquivalences_stalk_godementAugmentation · AlgebraicGeometry.GodementResolution.quasiIso_godementAugmentation · AlgebraicGeometry.GodementResolution.exists_quasiIso_boundedBelow_isFlasque_isHomotopyEquiv_stalk_godement

Section20.31 Cup product#

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

Tag 0FKU, the section

Tag 0FKU in the Stacks Project.

Stacks.Cohomology.DerivedGlobalCupProduct.globalCupProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProduct.lean, line 216. The attribute's comment: “the global cup product μ : RΓ(X, K) ⊗^L_A RΓ(X, M) ⟶ RΓ(X, K ⊗^L M) in D(A), the first display of the section, built as the relative cup product of Tag 0B68 for the morphism to the one-point space with ring A; the one-point comparison itself (a left adjoint of RΓ(X, -) together with its tensor comparison) is the parameter OnePointComparison”.

The global cup product μ : RΓ(S, K) ⊗^𝐋_A RΓ(S, M) ⟶ RΓ(S, K ⊗^𝐋_{𝒪_S} M) in D(A) for A = Γ(S, 𝒪_S), as a morphism of bifunctors on D(𝒪_S) × D(𝒪_S): the relative cup product construction for the adjunction L ⊣ RΓ(S, -) and the tensor comparison of c.

def globalCupProduct (c : OnePointComparison S) : GlobalCupProduct S

Stacks.Cohomology.DerivedGlobalCupProduct.cupPairing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProduct.lean, line 275. The attribute's comment: “the induced pairings ∪ : H^i(X, K) × H^j(X, M) ⟶ H^{i+j}(X, K ⊗^L M), the second display of the section: the tensoring of classes of More on Algebra, Section 15.64 followed by H^{i+j}(μ); the global cup product μ is the parameter κ, which globalCupProduct produces from an OnePointComparison”.

The pairings ∪ : Hⁱ(S, K) ⊗_A Hʲ(S, M) ⟶ Hⁱ⁺ʲ(S, K ⊗^𝐋_{𝒪_S} M) induced by a global cup product κ: a class ξ ∈ Hⁱ(S, K) and a class η ∈ Hʲ(S, M) are tensored to a class ξ ⊗ η in Hⁱ⁺ʲ(RΓ(S, K) ⊗^𝐋_A RΓ(S, M)), and ξ ∪ η = κ(ξ ⊗ η).

def cupPairing (κ : GlobalCupProduct S)
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing S))) (i j : ℤ) :
    cohomologyModule K i ⊗ cohomologyModule M j ⟶
      cohomologyModule (((derivedTensorProductFunctor S.sheaf).obj K).obj M) (i + j)

Stacks.Cohomology.DerivedGlobalCupProduct.section_cupProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductSection.lean, line 86. The attribute's comment: “Section 20.31 IN FULL, both displays: the global cup product μ : RΓ(X, K) ⊗^L_A RΓ(X, M) ⟶ RΓ(X, K ⊗^L M) in D(A), CONSTRUCTED as the relative cup product of Tag 0B68 for the morphism to the one-point space with ring A (first conjunct), natural in both complexes jointly (second conjunct), and the pairings it induces, ∪ : H^i(X, K) × H^j(X, M) ⟶ H^{i+j}(X, K ⊗^L M), given by the source's two-step recipe ξ ∪ η = μ(ξ ⊗ η) with the tensoring step the pairing of classes of More on Algebra, Section 15.64 (third conjunct). The numbered items of the section are excluded, each having its own tag: 0FP2, 0G6W, 0FP3, 0FKV, 0FP4, 0FP5, 0FP6, 0H99. The one parameter is OnePointComparison, the identification D(pt, A) = D(A) that the source has and this repository does not”.

Cohomology, Section 0FKU in full: both displays of the section, for the global cup product built from a one-point comparison.

The conjuncts are, in the order the source states them:

  • the first display, μ : RΓ(S, K) ⊗^𝐋_A RΓ(S, M) ⟶ RΓ(S, K ⊗^𝐋_{𝒪_S} M), together with the source's definition of it — it is the relative cup product of Tag 0B68, namely the adjoint transpose of the tensor comparison followed by the counit of L ⊣ RΓ(S, -) in both tensor factors, which is what "we define it as the relative cup product for the morphism of ringed spaces f : (S, 𝒪_S) ⟶ (pt, A) via D(pt, A) = D(A)" says once Rf_* is read as RΓ(S, -);
  • that μ is natural in the two complexes jointly, so that it is a morphism of bifunctors on D(𝒪_S) × D(𝒪_S) and not a separate map for each pair;
  • the second display, the induced pairings ∪ : Hⁱ(S, K) ⊗_A Hʲ(S, M) ⟶ Hⁱ⁺ʲ(S, K ⊗^𝐋_{𝒪_S} M), together with the source's two-step recipe ξ ∪ η = μ(ξ ⊗ η): the tensoring step is a RingTheory.TorProducts.CohomologyTensorProduct, i.e. a pairing sending the tensor of the classes of two cocycles to the class of their tensor, which is Equation 15.64.0.1 of Tag 068H and is the source's "we can first tensor them, see More on Algebra, Section 15.64"; the second step is Hⁱ⁺ʲ(μ).

The one-point comparison c is the parameter discussed in the module docstring: it stands for the identification D(pt, A) = D(A), which the source has and this repository does not. It is a hypothesis of the two definitions this theorem is about, so this statement is exactly as conditional as they are and no more.

The remaining numbered items of Section 20.31 are not conjoined here because each carries its own tag: Lemma 20.31.1 is Tag 0FP2, Remark 20.31.2 is Tag 0G6W, Lemma 20.31.3 is Tag 0FP3, Lemma 20.31.4 is Tag 0FKV, and Lemmas 20.31.5 to 20.31.8 are Tags 0FP4, 0FP5, 0FP6 and 0H99. What is left to Tag 0FKU itself is the construction of the two displays, which is what this states.

theorem section_cupProduct (c : OnePointComparison S) :
    (∀ K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing S)),
      (globalCupProduct c).app (K, M) =
        adjunctionBitensorMap c.adjunction (Functor.uncurry.obj (tensorBase S))
          (Functor.uncurry.obj (derivedTensorProductFunctor S.sheaf)) c.tensorComparison K M) ∧
    (∀ K K' M M' : DerivedCategory (SheafOfModules.{u} (structureSheafRing S)),
      ∀ (k : K ⟶ K') (m : M ⟶ M'),
      (Functor.uncurry.obj (tensorBase S)).map
            ((baseSections S).map k ×ₘ (baseSections S).map m) ≫
          (globalCupProduct c).app (K', M') =
        (globalCupProduct c).app (K, M) ≫
          (baseSections S).map
            ((Functor.uncurry.obj (derivedTensorProductFunctor S.sheaf)).map (k ×ₘ m))) ∧
    (∀ (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing S))) (i j : ℤ),
      ∃ p : RingTheory.TorProducts.CohomologyTensorProduct ((baseSections S).obj K)
          ((baseSections S).obj M) i j,
        cupPairing (globalCupProduct c) K M i j =
          p.map ≫ (DerivedCategory.homologyFunctor (ModuleCat.{u} (baseRing S)) (i + j)).map
            ((globalCupProduct c).app (K, M)))
Tag 0FP2, a lemma

Tag 0FP2 in the Stacks Project.

Stacks.Cohomology.DerivedRelativeCupProduct.homEquiv_symm_relativeCupProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/CupProductOfCohomologyClasses.lean, line 159. The attribute's comment: “the identification-free core, at arbitrary objects of D(𝒪_Y) in place of the source's shifted structure sheaves, and for an arbitrary morphism of ringed spaces”.

The two constructions of the cup product agree: the adjunct of the tensor product ξ ⊗ η of two cohomology classes followed by the relative cup product of Stacks 0B68 is the derived pullback-tensor comparison of Stacks 079U followed by the tensor product ξ̃ ⊗ η̃ of their adjuncts.

theorem homEquiv_symm_relativeCupProduct
    {U V : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))}
    {K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    (ξ : U ⟶ (derivedPushforward f).obj K) (η : V ⟶ (derivedPushforward f).obj M) :
    ((derivedAdjunction f).homEquiv _ _).symm
        (((derivedTensorProductFunctor Y.sheaf).map ξ).app V ≫
          ((derivedTensorProductFunctor Y.sheaf).obj
              ((derivedPushforward f).obj K)).map η ≫
            relativeCupProduct f K M) =
      (pullbackTensorComparison f).app (U, V) ≫
        ((derivedTensorProductFunctor X.sheaf).map
              (((derivedAdjunction f).homEquiv U K).symm ξ)).app
            ((derivedPullback f).obj V) ≫
          ((derivedTensorProductFunctor X.sheaf).obj K).map
            (((derivedAdjunction f).homEquiv V M).symm η)

Stacks.Cohomology.DerivedRelativeCupProduct.homEquiv_symm_comp_relativeCupProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/CupProductOfCohomologyClasses.lean, line 183. The attribute's comment: “stated for an arbitrary morphism of ringed spaces, with the source's identification 𝒪_Y[-i-j] = 𝒪_Y[-i] ⊗ᴸ 𝒪_Y[-j] carried as an arbitrary morphism χ”.

Let χ : W ⟶ U ⊗^L_{𝒪_Y} V. The adjunct of χ followed by ξ ⊗ η and the relative cup product of Stacks 0B68 is Lf^*χ followed by the derived pullback-tensor comparison of Stacks 079U and by the tensor product ξ̃ ⊗ η̃ of the adjuncts.

theorem homEquiv_symm_comp_relativeCupProduct
    {W U V : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))}
    {K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))}
    (χ : W ⟶ ((derivedTensorProductFunctor Y.sheaf).obj U).obj V)
    (ξ : U ⟶ (derivedPushforward f).obj K) (η : V ⟶ (derivedPushforward f).obj M) :
    ((derivedAdjunction f).homEquiv _ _).symm
        (χ ≫ ((derivedTensorProductFunctor Y.sheaf).map ξ).app V ≫
          ((derivedTensorProductFunctor Y.sheaf).obj
              ((derivedPushforward f).obj K)).map η ≫
            relativeCupProduct f K M) =
      (derivedPullback f).map χ ≫ (pullbackTensorComparison f).app (U, V) ≫
        ((derivedTensorProductFunctor X.sheaf).map
              (((derivedAdjunction f).homEquiv U K).symm ξ)).app
            ((derivedPullback f).obj V) ≫
          ((derivedTensorProductFunctor X.sheaf).obj K).map
            (((derivedAdjunction f).homEquiv V M).symm η)
Tag 0G6W, a remark

Tag 0G6W in the Stacks Project.

Stacks.Cohomology.DerivedGlobalCupProduct.cupWithClassCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 106. The attribute's comment: “the construction of the map ξ ∪ - : RΓ(X, M)[-i] ⟶ RΓ(X, K ⊗^L M) attached to a class ξ ∈ H^i(X, K), the first clause of the remark, at the global cup product μ of Section 0FKU, globalCupProductCanonical, on an arbitrary ringed space”.

The map ξ ∪ - at the canonical global cup product. For a class ξ ∈ Hⁱ(X, K) it is the morphism

ξ ∪ - : RΓ(X, M)[-i] ⟶ RΓ(X, K ⊗^𝐋_{𝒪_X} M)

in D(A) for A = Γ(X, 𝒪_X), namely the composition of the identification RΓ(X, M)[-i] = A[-i] ⊗^𝐋_A RΓ(X, M), of ξ ⊗ 1 for the morphism representing ξ, and of the global cup product μ of Section 0FKU, globalCupProductCanonical.

def cupWithClassCanonical (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)))
    (i : ℤ) (ξ : ModuleCat.of (baseRing X) (baseRing X) ⟶ cohomologyModule K i) :
    ((baseSections X).obj M)⟦-i⟧ ⟶
      (baseSections X).obj (((derivedTensorProductFunctor X.sheaf).obj K).obj M)

Stacks.Cohomology.DerivedGlobalCupProduct.homologyFromSingle_cupWithClassCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 127. The attribute's comment: “the second clause of the remark: on cohomology ξ ∪ - is the cup product with ξ, for the global cup product globalCupProductCanonical. The cup product of two classes is in the composition shape of Section 0FKU and Tag 0FP2, A[-i-j] ⟶ A[-i] ⊗ᴸ A[-j] ⟶ RΓ(X, K) ⊗ᴸ RΓ(X, M) ⟶ RΓ(X, K ⊗ᴸ M), for every identification χ of A[-i-j] with A[-i] ⊗ᴸ A[-j]”.

On cohomology the map ξ ∪ - at the canonical global cup product is the cup product with ξ: for ξ ∈ Hⁱ(X, K) and η ∈ Hʲ(X, M), the map Hⁱ⁺ʲ(ξ ∪ -) carries the class of η, read in Hⁱ⁺ʲ(RΓ(X, M)[-i]) through the identifications A[-i-j] = A[-i] ⊗^𝐋_A A[-j] and A[-i] ⊗^𝐋_A RΓ(X, M) = RΓ(X, M)[-i], to the class of the cup product ξ ∪ η in the composition shape of Section 0FKU and Tag 0FP2.

theorem homologyFromSingle_cupWithClassCanonical
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) (i j : ℤ)
    (ξ : ModuleCat.of (baseRing X) (baseRing X) ⟶ cohomologyModule K i)
    (η : ModuleCat.of (baseRing X) (baseRing X) ⟶ cohomologyModule M j)
    (χ : baseShift X (i + j) ⟶ ((tensorBase X).obj (baseShift X i)).obj (baseShift X j)) :
    DerivedCategory.homologyFromSingleLinearEquiv (ModuleCat.of (baseRing X) (baseRing X))
          (((baseSections X).obj M)⟦-i⟧) (i + j) (baseRing X)
          (χ ≫ ((tensorBase X).obj (baseShift X i)).map (classRepresentative M j η) ≫
            (baseShiftTensorIso X i ((baseSections X).obj M)).hom) ≫
        (DerivedCategory.homologyFunctor (ModuleCat.{u} (baseRing X)) (i + j)).map
          (cupWithClassCanonical X K M i ξ) =
      DerivedCategory.homologyFromSingleLinearEquiv (ModuleCat.of (baseRing X) (baseRing X))
        ((baseSections X).obj (((derivedTensorProductFunctor X.sheaf).obj K).obj M)) (i + j)
        (baseRing X)
        (χ ≫ ((tensorBase X).map (classRepresentative K i ξ)).app (baseShift X j) ≫
          ((tensorBase X).obj ((baseSections X).obj K)).map (classRepresentative M j η) ≫
            (globalCupProductCanonical X).app (K, M))

Stacks.Cohomology.DerivedGlobalCupProduct.homologyFromSingle_cupWithClassCanonical_cupPairing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/GlobalCupProductCanonicalInstances.lean, line 155. The attribute's comment: “the second clause of the remark, with the cup product of two classes read against the cohomology-level pairing cupPairing of Section 0FKU at the global cup product globalCupProductCanonical: the tensoring of classes of Tag 068H followed by H^{i+j}(μ), which is how the source defines ∪. The source's identification A[-i-j] = A[-i] ⊗ᴸ A[-j] is pinnedSplitting”.

On cohomology, Hⁱ⁺ʲ(ξ ∪ -) at the canonical global cup product carries the class of η to ξ ∪ η as Stacks.Cohomology.DerivedGlobalCupProduct.cupPairing defines it for the canonical global cup product, the source's identification A[-i-j] = A[-i] ⊗^𝐋_A A[-j] being pinnedSplitting.

theorem homologyFromSingle_cupWithClassCanonical_cupPairing
    (K M : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) (i j : ℤ)
    (ξ : ModuleCat.of (baseRing X) (baseRing X) ⟶ cohomologyModule K i)
    (η : ModuleCat.of (baseRing X) (baseRing X) ⟶ cohomologyModule M j) :
    DerivedCategory.homologyFromSingleLinearEquiv (ModuleCat.of (baseRing X) (baseRing X))
          (((baseSections X).obj M)⟦-i⟧) (i + j) (baseRing X)
          (pinnedSplitting X i j ≫
            ((tensorBase X).obj (baseShift X i)).map (classRepresentative M j η) ≫
              (baseShiftTensorIso X i ((baseSections X).obj M)).hom) ≫
        (DerivedCategory.homologyFunctor (ModuleCat.{u} (baseRing X)) (i + j)).map
          (cupWithClassCanonical X K M i ξ) =
      (λ_ (ModuleCat.of (baseRing X) (baseRing X))).inv ≫ (ξ ⊗ₘ η) ≫
        cupPairing (globalCupProductCanonical X) K M i j
Tag 0FP3, a lemma

Tag 0FP3 in the Stacks Project.

Stacks.Cohomology.CupProductAndDerivedPushforwardOnRingedSpaces.naiveCupProduct_relativeCupProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/CupProductAndDerivedPushforward.lean, line 400.

Stacks 0FP3. For a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) and complexes 𝒦^•, ℳ^• of 𝒪_X-modules, the hexagon

f_*𝒦^• ⊗^L_{𝒪_Y} f_*ℳ^• ─────→ Rf_*𝒦^• ⊗^L_{𝒪_Y} Rf_*ℳ^•
          │                                │
          ↓                                ↓
Tot(f_*𝒦^• ⊗_{𝒪_Y} f_*ℳ^•)        Rf_*(𝒦^• ⊗^L_{𝒪_X} ℳ^•)
          │                                │
          ↓                                ↓
f_*Tot(𝒦^• ⊗_{𝒪_X} ℳ^•) ─────→ Rf_*Tot(𝒦^• ⊗_{𝒪_X} ℳ^•)

commutes in D(𝒪_Y). Its horizontal edges and its top right edge are the comparison f_* ⟶ Rf_*; the top left and bottom right edges are the canonical map from the derived tensor product to the ordinary total tensor complex of Stacks 06YU; the middle left edge is the naive cup product and the middle right edge is the relative cup product of Stacks 0B68.

theorem naiveCupProduct_relativeCupProduct :
    (derivedToTensorNatTrans Y).app
          ((pushforwardComplex f).obj K, (pushforwardComplex f).obj M) ≫
        DerivedCategory.Q.map (naiveCupProduct f K M) ≫
        pushforwardComparisonQ f ((totalComplexPair (sheafTensor X.sheaf)).obj (K, M)) =
      (Functor.uncurry.obj (derivedTensorProductFunctor Y.sheaf)).map
          (pushforwardComparisonQ f K ×ₘ pushforwardComparisonQ f M) ≫
        relativeCupProduct f (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj M) ≫
        (derivedPushforward f).map ((derivedToTensorNatTrans X).app (K, M))
Tag 0FKV, a lemma

Tag 0FKV in the Stacks Project.

Stacks.Cech.CupProductSquare.cupProductSquareCommutes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechTotalComplex/CupProductSquareCommutes.lean, line 279.

[Stacks, Tag 0FKV]. Let (X, 𝒪_X) be a ringed space, A = Γ(X, 𝒪_X), 𝒦^• and ℳ^• bounded below complexes of 𝒪_X-modules and 𝒰 : X = ⋃ Uᵢ an open covering. The diagram

Tot(Č(𝒰,𝒦)) ⊗^𝐋_A Tot(Č(𝒰,ℳ)) ─────────→ RΓ(X,𝒦) ⊗^𝐋_A RΓ(X,ℳ)
            │                                        │ μ
            ↓                                        ↓
Tot(Tot(Č(𝒰,𝒦)) ⊗_A Tot(Č(𝒰,ℳ)))          RΓ(X, 𝒦 ⊗^𝐋_{𝒪_X} ℳ)
            │                                        │
            ↓                                        ↓
Tot(Č(𝒰, Tot(𝒦 ⊗_{𝒪_X} ℳ))) ─────────────→ RΓ(X, Tot(𝒦 ⊗_{𝒪_X} ℳ))

commutes in D(A): the left-hand leg cechLeftLeg (the canonical map to the total tensor complex, then the Čech cup product of [Stacks, Tag 07MB], then the comparison of [Stacks, Tag 08BN]) equals the right-hand leg cechRightLeg (the comparison of Tag 08BN in both factors, then the global cup product μ, then RΓ(X, -) of the canonical map 𝒦^• ⊗^𝐋 ℳ^• ⟶ Tot(𝒦^• ⊗ ℳ^•)).

theorem cupProductSquareCommutes :
    cechLeftLeg S Ui hU K M = cechRightLeg S Ui hU K M
Tag 0FP4, a lemma

Tag 0FP4 in the Stacks Project.

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProductAssociativity.lean, line 343. The attribute's comment: “associativity of the relative cup product, for a morphism of ringed spaces and arbitrary K, L, M in D(O_X): the associativity constraints are those of Tag 0FPB (derivedAssociator), and their compatibility with the comparison of Tag 079U is pullbackTensorComparisonAssociative”.

The relative cup product is associative. For a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) and arbitrary K, L, M ∈ D(𝒪_X) the square

(Rf_*K ⊗^L Rf_*L) ⊗^L Rf_*M ⟶ Rf_*(K ⊗^L L) ⊗^L Rf_*M ⟶ Rf_*((K ⊗^L L) ⊗^L M)
            |                                                      |
            | a                                                    | Rf_*a
            v                                                      v
Rf_*K ⊗^L (Rf_*L ⊗^L Rf_*M) ⟶ Rf_*K ⊗^L Rf_*(L ⊗^L M) ⟶ Rf_*(K ⊗^L (L ⊗^L M))

commutes in D(𝒪_Y), where the four unlabelled arrows are relative cup products of Stacks 0B68 in one or the other tensor factor and a is the associativity constraint of Stacks 0FPB. The compatibility of the comparison of Stacks 079U with those constraints is pullbackTensorComparisonAssociative.

theorem relativeCupProduct_assoc
    (K L M : DerivedCategory (Mod X.sheaf)) :
    (Functor.uncurry.obj
            (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf)).map
        (relativeCupProduct f K L ×ₘ 𝟙 ((derivedPushforward f).obj M)) ≫
        relativeCupProduct f
            ((Functor.uncurry.obj
              (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf)).obj (K, L))
            M ≫
          (derivedPushforward f).map (derivedAssociator X K L M) =
      derivedAssociator Y ((derivedPushforward f).obj K) ((derivedPushforward f).obj L)
          ((derivedPushforward f).obj M) ≫
        (Functor.uncurry.obj
              (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf)).map
            (𝟙 ((derivedPushforward f).obj K) ×ₘ relativeCupProduct f L M) ≫
          relativeCupProduct f K
            ((Functor.uncurry.obj
              (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf)).obj (L, M))
Tag 0FP5, a lemma

Tag 0FP5 in the Stacks Project.

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_braiding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProductCommutativity.lean, line 242. The attribute's comment: “the whole tag: for a morphism of ringed spaces and arbitrary K, L in D(𝒪_X), the commutativity square of the relative cup product commutes. The commutativity constraints are derivedBraiding of Stacks 0FPB, and their compatibility with the Stacks 079U comparison is pullbackTensorComparisonBraided”.

The relative cup product is commutative. For a morphism of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) and arbitrary K, L ∈ D(𝒪_X) the square

Rf_*K ⊗^L Rf_*L ⟶ Rf_*(K ⊗^L L)
      |                  |
      ψ                 Rf_*ψ
      v                  v
Rf_*L ⊗^L Rf_*K ⟶ Rf_*(L ⊗^L K)

commutes in D(𝒪_Y), where the horizontal arrows are the relative cup product of Stacks 0B68 and ψ is the commutativity constraint of Stacks 0FPB. The compatibility of the comparison of Stacks 079U with those constraints is pullbackTensorComparisonBraided.

theorem relativeCupProduct_braiding (K L : DerivedCategory (Mod X.sheaf)) :
    derivedBraiding Y ((derivedPushforward f).obj K) ((derivedPushforward f).obj L) ≫
        relativeCupProduct f L K =
      relativeCupProduct f K L ≫ (derivedPushforward f).map (derivedBraiding X K L)
Tag 0FP6, a lemma

Tag 0FP6 in the Stacks Project.

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProductComposition.lean, line 228. The attribute's comment: “for the composite adjunction and the composite pullback-tensor comparison”.

The relative cup product is compatible with composition. For the composite adjunction Lg^*Lf^* ⊣ Rf_*Rg_* and the composite derived pullback-tensor comparison, the relative cup product of Stacks 0B68 is the relative cup product for g at the pair (Rf_*K, Rf_*L) followed by Rg_* of the relative cup product for f.

theorem relativeCupProduct_comp
    (K L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    adjunctionBitensorMap
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction g).comp
          (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction f))
        (Functor.uncurry.obj
          (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Z.sheaf))
        (Functor.uncurry.obj
          (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf))
        (pullbackTensorComparisonComp f g) K L =
      relativeCupProduct g
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K)
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj L) ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward g).map
          (relativeCupProduct f K L)

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_comp', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProductComposition.lean, line 275.

Stacks 0FP6: the relative cup product is compatible with composition. For composable morphisms of ringed spaces f : (X, 𝒪_X) ⟶ (Y, 𝒪_Y) and g : (Y, 𝒪_Y) ⟶ (Z, 𝒪_Z) and arbitrary K, L ∈ D(𝒪_X) the square

Rg_*Rf_*K ⊗^L Rg_*Rf_*L ⟶ R(g ∘ f)_*K ⊗^L R(g ∘ f)_*L
          |                            |
          |                            | relative cup product for f ≫ g
          v                            v
   Rg_*Rf_*(K ⊗^L L)     ⟶      R(g ∘ f)_*(K ⊗^L L)

commutes in D(𝒪_Z), where the horizontal arrows are the composition isomorphism Rf_* ⋙ Rg_* ≅ R(g ∘ f)_* of Stacks 0D5T — in each tensor factor on top and at the tensor product on the bottom — and the left vertical arrow is the relative cup product for g at (Rf_*K, Rf_*L) followed by Rg_* of the relative cup product for f.

This is the statement of the source, the two identifications being the composition isomorphism. It is relativeCupProduct_comp transported by adjunctionBitensorMap_transport, whose two inputs are Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedAdjunction_comp and Stacks.Cohomology.DerivedPullbackTensor.derivedPullbackTensorIso_comp.

theorem relativeCupProduct_comp'
    (K L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    (Functor.uncurry.obj
            (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Z.sheaf)).map
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforwardCompIso f
              g).hom.app K ×ₘ
            (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforwardCompIso f
              g).hom.app L) ≫
        relativeCupProduct (f ≫ g) K L =
      relativeCupProduct g
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj K)
          ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f).obj L) ≫
        (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward g).map
            (relativeCupProduct f K L) ≫
          (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforwardCompIso f
              g).hom.app
            (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).obj K).obj
              L)
Tag 0H99, a lemma

Tag 0H99 in the Stacks Project.

Stacks.Cohomology.DerivedRelativeCupProduct.relativeCupProduct_derivedBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/RelativeCupProductBaseChange.lean, line 473.

Stacks 0H99: the relative cup product is compatible with a commutative square of ringed spaces.

For a commutative square g' ≫ f = f' ≫ g of ringed spaces and arbitrary K, L ∈ D(𝒪_X), the hexagon RelativeCupProductBaseChangeSquare commutes at the relative cup product of Stacks 0B68 for f and for f' and the derived base change map of Stacks 08HY: the derived pullback along g of the cup product for f, followed by the base change map and by Rf'_* of the comparison of Stacks 079U for g', equals the comparison of Stacks 079U for g, followed by the base change map in each tensor factor and by the cup product for f'.

There is no boundedness, flatness or quasi-coherence hypothesis on K and L, and no associator or symmetry of ⊗^L is used: the hexagon has binary tensor products only.

theorem relativeCupProduct_derivedBaseChangeMap
    (K L : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    RelativeCupProductBaseChangeSquare
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f)
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPushforward f')
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g)
      (Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g')
      (Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y.sheaf))
      (Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf))
      (Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor Y'.sheaf))
      (Functor.uncurry.obj (Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X'.sheaf))
      (Stacks.Cohomology.DerivedProjectionFormula.pullbackTensorComparison g)
      (Stacks.Cohomology.DerivedProjectionFormula.pullbackTensorComparison g') K L
      (relativeCupProduct f K L)
      (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g' f' f g sq
        (((Stacks.DerivedTensor.RingedSite.derivedTensorProductFunctor X.sheaf).obj K).obj L))
      (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g' f' f g sq K)
      (Stacks.Cohomology.DerivedBaseChange.derivedBaseChangeMap g' f' f g sq L)
      (relativeCupProduct f'
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g').obj K)
        ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback g').obj L))
Sources
LeanStacks.Cohomology.DerivedGlobalCupProduct.globalCupProduct · Stacks.Cohomology.DerivedGlobalCupProduct.cupPairing · Stacks.Cohomology.DerivedGlobalCupProduct.section_cupProduct · Stacks.Cohomology.DerivedRelativeCupProduct.homEquiv_symm_relativeCupProduct · Stacks.Cohomology.DerivedRelativeCupProduct.homEquiv_symm_comp_relativeCupProduct · Stacks.Cohomology.DerivedGlobalCupProduct.cupWithClassCanonical · Stacks.Cohomology.DerivedGlobalCupProduct.homologyFromSingle_cupWithClassCanonical · Stacks.Cohomology.DerivedGlobalCupProduct.homologyFromSingle_cupWithClassCanonical_cupPairing

Section20.32 Some properties of K-injective complexes#

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

Tag 08BS, a lemma

Tag 08BS in the Stacks Project.

ExtensionByZeroModules.isKInjective_jStar, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/ExtensionByZero/RestrictionOfKInjectives.lean, line 54.

Restriction to an open subspace preserves K-injective complexes of sheaves of modules.

instance isKInjective_jStar
    (I : CochainComplex (SheafOfModules.{u} O) ℤ) [I.IsKInjective] :
    CochainComplex.IsKInjective
      (((jStar U O).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)
Tag 0D5V, a lemma

Tag 0D5V in the Stacks Project.

Stacks.Cohomology.OpenSubspace.cohomologyOnOpenIsoRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/CohomologyOnAnOpenSubspace.lean, line 251. The attribute's comment: “H^p(U, K) ≅ H^p(U, K|_U), natural in K in D(O_X), for every open U of a ringed space X and every degree p”.

Degree-p cohomology over an open agrees naturally with degree-p cohomology after restriction to that open. The component at K is the isomorphism H^p(U, K) ≅ H^p(U, K|_U).

public noncomputable def cohomologyOnOpenIsoRestriction {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) (U : Opens X)
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wU} (SheafOfModules.{u} (resRing U O))]
    [HasDerivedCategory.{wG} AddCommGrpCat.{u}] (p : ℤ) :
    derivedSectionsOnOpen O U ⋙ DerivedCategory.homologyFunctor AddCommGrpCat.{u} p ≅
      derivedRestriction O U ⋙ derivedSectionsOnOpenSubspace O U ⋙
        DerivedCategory.homologyFunctor AddCommGrpCat.{u} p
Tag 0BKJ, a lemma

Tag 0BKJ in the Stacks Project.

Stacks.Cohomology.CohomologyPresheaf.cohomologyPresheafEvaluationIsoRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/CohomologyPresheafOnOpenSubspace.lean, line 41. The attribute's comment: “values on opens: the value of the presheaf on U is H^q(U, K|_U)”.

Stacks Project, Tag 0BKJ, the value on an open as cohomology of the open subspace. The value on U of the presheaf U ↦ H^q(U, K) is H^q(U, K|_U), the degree-q cohomology of the open subspace U with coefficients in the derived restriction of K, naturally in K.

public def cohomologyPresheafEvaluationIsoRestriction {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) (U : Opens X)
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wU} (SheafOfModules.{u} (resRing U O))]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    [HasDerivedCategory.{wG} AddCommGrpCat.{u}]
    (q : ℤ) :
    derivedSectionsPresheaf O ⋙
          DerivedCategory.homologyFunctor (PresheafOfModules.{u} O.obj) q ⋙
          PresheafOfModules.evaluation O.obj (Opposite.op U) ⋙
          forget₂ (ModuleCat.{u} (O.obj.obj (Opposite.op U))) AddCommGrpCat.{u} ≅
      derivedRestriction O U ⋙ derivedSectionsOnOpenSubspace O U ⋙
          DerivedCategory.homologyFunctor AddCommGrpCat.{u} q

Stacks.Cohomology.CohomologyPresheaf.cohomologyPresheafEvaluationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/CohomologyPresheafSheafification.lean, line 213. The attribute's comment: “values on opens”.

The value on U of the cohomology presheaf is H^q(U, K).

public def cohomologyPresheafEvaluationIso {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) (U : Opens X)
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    [HasDerivedCategory.{wG} AddCommGrpCat.{u}]
    (q : ℤ) :
    derivedSectionsPresheaf O ⋙
          DerivedCategory.homologyFunctor (PresheafOfModules.{u} O.obj) q ⋙
          PresheafOfModules.evaluation O.obj (Opposite.op U) ⋙
          forget₂ (ModuleCat.{u} (O.obj.obj (Opposite.op U))) AddCommGrpCat.{u} ≅
      Stacks.Cohomology.OpenSubspace.derivedSectionsOnOpen O U ⋙
          DerivedCategory.homologyFunctor AddCommGrpCat.{u} q

Stacks.Cohomology.CohomologyPresheaf.sheafificationCohomologyPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/CohomologyPresheafSheafification.lean, line 258. The attribute's comment: “associated sheaf”.

Sheafifying the presheaf U ↦ H^q(U, K) gives the q-th cohomology sheaf of K, naturally in the derived object K.

public def sheafificationCohomologyPresheafIso {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    [HasDerivedCategory.{wX} (SheafOfModules.{u} O)]
    [HasDerivedCategory.{wP} (PresheafOfModules.{u} O.obj)]
    (q : ℤ) :
    derivedSectionsPresheaf O ⋙
          DerivedCategory.homologyFunctor (PresheafOfModules.{u} O.obj) q ⋙
          PresheafOfModules.sheafification (𝟙 O.obj) ≅
        DerivedCategory.homologyFunctor (SheafOfModules.{u} O) q
Tag 08FE, a lemma

Tag 08FE in the Stacks Project.

Stacks.Duality.OpenImmersion.isIso_quasiCoherentDerivedRestrictBaseChangeSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/OpenImmersion/TwistedInverseImageRestrictionBaseChange.lean, line 324. The attribute's comment: “invertibility of Stacks.Duality.OpenImmersion.quasiCoherentDerivedRestrictBaseChangeSquare, the mate of Stacks.Duality.quasiCoherentDerivedPushforwardSquareIso across the two restriction adjunctions, on the quasi-coherent derived categories of a cartesian square of schemes whose vertical arrows are open immersions, at the locally small model. The isomorphism of functors itself is Stacks.Cohomology.derivedPushforwardRestrictIso, for ringed spaces; what is added here is that this particular canonical map is the invertible one”.

The comparison (Rf_*K)|_V ⟶ Rf'_*(K|_U) of [Stacks, Tag 08FE] is invertible on the quasi-coherent derived categories. This is the slot that StacksFrontier/AlgebraicGeometry/Duality/OpenImmersion/TwistedInverseImageRestrictionConjugate.lean leaves open; see the module documentation for the argument.

theorem isIso_quasiCoherentDerivedRestrictBaseChangeSquare (sq : IsPullback j' f' f j) :
    IsIso (quasiCoherentDerivedRestrictBaseChangeSquare j' f' f j hpushj' hpushf hpushf' hpushj
      (fun K i => derivedCategoryB_derivedRestrict j K.obj K.property i)
      (fun K i => derivedCategoryB_derivedRestrict j' K.obj K.property i) sq.w)

AlgebraicGeometry.DerivedChow.derivedPushforwardRestrictOpenIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PseudoCoherentThree/DerivedChowFourierMukai.lean, line 198. The attribute's comment: “for the standard derived direct image and derived pullback of [Stacks, Tag 079W], at the inclusion of an open subscheme of the target of a morphism of schemes”.

[Stacks, Tag 08FE] at an open of the target of a morphism of schemes. Restricting the derived direct image along q to an open V of the target is the derived direct image along q ∣_ V of the restriction to q ⁻¹ᵁ V: "forming the total direct image commutes with localization".

def derivedPushforwardRestrictOpenIso :
    derivedPushforward (ofScheme q) ⋙ derivedPullback (ofScheme V.ι) ≅
      derivedPullback (ofScheme (q ⁻¹ᵁ V).ι) ⋙ derivedPushforward (ofScheme (q ∣_ V))

AlgebraicGeometry.schemeDerivedPushforwardRestrictOpenIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedPushforwardOpenBase.lean, line 84. The attribute's comment: “for schemes, at the derived direct image of Tag 079W, with restriction to an open subscheme on the restriction edges”.

[Stacks, Tag 08FE] for schemes. For a Cartesian square of schemes 

X' --f'--> T
|          |
g'         g
v          v
X ---f---> S
whose vertical sides are open immersions, the restriction to T of Rf_*E is the derived direct image along f' of the restriction of E to X'.

Restriction along an open immersion is exact, so both restriction edges are the functors induced on derived categories and carry no derivation.

def schemeDerivedPushforwardRestrictOpenIso {X S X' T : Scheme.{u}} (f : X ⟶ S) (g : T ⟶ S)
    [IsOpenImmersion g] (f' : X' ⟶ T) (g' : X' ⟶ X) (hsq : IsPullback g' f' f g)
    (E : DerivedCategory X.Modules) :
    letI : IsOpenImmersion g' := MorphismProperty.of_isPullback hsq.flip inferInstance
    (Scheme.Modules.restrictFunctor g).mapDerivedCategory.obj
        ((schemeDerivedPushforward f).obj E) ≅
      (schemeDerivedPushforward f').obj
        ((Scheme.Modules.restrictFunctor g').mapDerivedCategory.obj E)

AlgebraicGeometry.schemeDerivedPushforwardRestrictOpensIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/DerivedPushforwardOpenBase.lean, line 137. The attribute's comment: “for schemes, at the restriction of f to the preimage of an open of the base”.

[Stacks, Tag 08FE] for schemes, at an open of the base. The restriction to an open U ⊆ S of Rf_*E is the derived direct image along f ∣_ U : f ⁻¹ᵁ U ⟶ U of the restriction of E to f ⁻¹ᵁ U.

This is AlgebraicGeometry.schemeDerivedPushforwardRestrictOpenIso at the Cartesian square of AlgebraicGeometry.isPullback_morphismRestrict.

def schemeDerivedPushforwardRestrictOpensIso {X S : Scheme.{u}} (f : X ⟶ S) (U : S.Opens)
    (E : DerivedCategory X.Modules) :
    (Scheme.Modules.restrictFunctor U.ι).mapDerivedCategory.obj
        ((schemeDerivedPushforward f).obj E) ≅
      (schemeDerivedPushforward (f ∣_ U)).obj
        ((Scheme.Modules.restrictFunctor (f ⁻¹ᵁ U).ι).mapDerivedCategory.obj E)

Stacks.Cohomology.derivedPushforwardRestrictIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechAndResolutions/KInjectiveRestriction.lean, line 925.

Stacks 08FE. In a Cartesian square of ringed spaces 

U ----g---> V
|           |
i           j
|           |
v           v
X ----f---> Y
in which i and j are open immersions, restricting the derived direct image along j is naturally isomorphic to taking the derived direct image along g after restriction along i.

The four functors are arbitrary choices of right derived functors equipped with their canonical units; hence the result applies in particular to the standard choices of Rf_*, Rg_*, and the exact restriction functors.

noncomputable def derivedPushforwardRestrictIso
    {X Y U V : RingedSpace.{u, u}}
    (f : X ⟶ Y) (i : U ⟶ X) (j : V ⟶ Y) (g : U ⟶ V)
    [SheafedSpace.IsOpenImmersion i] [SheafedSpace.IsOpenImmersion j]
    (h : IsPullback i g f j)
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing Y))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing U))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing V))]
    (Rf : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (Rg : DerivedCategory (SheafOfModules.{u} (structureSheafRing U)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing V)))
    (Ri : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing U)))
    (Rj : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing V)))
    (αf : (modulePushforward f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (αg : (modulePushforward g).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rg)
    (αi : (modulePullback i).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Ri)
    (αj : (modulePullback j).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rj)
    [Rf.IsRightDerivedFunctor αf
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Rg.IsRightDerivedFunctor αg
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Ri.IsRightDerivedFunctor αi
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Rj.IsRightDerivedFunctor αj
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))] :
    Rf ⋙ Rj ≅ Ri ⋙ Rg

Stacks.Cohomology.derivedPushforwardRestrictIso_isCanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/CechAndResolutions/KInjectiveRestriction.lean, line 1004. The attribute's comment: “canonicality”.

The isomorphism derivedPushforwardRestrictIso is the canonical one: on a K-injective representative it is induced by the fixed adjunction mate pushforwardRestrictHomotopyMap and by the four specified derived-functor units.

theorem derivedPushforwardRestrictIso_isCanonical
    {X Y U V : RingedSpace.{u, u}}
    (f : X ⟶ Y) (i : U ⟶ X) (j : V ⟶ Y) (g : U ⟶ V)
    [SheafedSpace.IsOpenImmersion i] [SheafedSpace.IsOpenImmersion j]
    (h : IsPullback i g f j)
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing X))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing Y))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing U))]
    [HasDerivedCategory (SheafOfModules.{u} (structureSheafRing V))]
    (Rf : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (Rg : DerivedCategory (SheafOfModules.{u} (structureSheafRing U)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing V)))
    (Ri : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing U)))
    (Rj : DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing V)))
    (alpha_f : (modulePushforward f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rf)
    (alpha_g : (modulePushforward g).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rg)
    (alpha_i : (modulePullback i).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Ri)
    (alpha_j : (modulePullback j).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rj)
    [Rf.IsRightDerivedFunctor alpha_f
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Rg.IsRightDerivedFunctor alpha_g
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Ri.IsRightDerivedFunctor alpha_i
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Rj.IsRightDerivedFunctor alpha_j
      (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    (I : CochainComplex (SheafOfModules.{u} (structureSheafRing X)) ℤ) (_hI : I.IsKInjective) :
    alpha_j.app (((modulePushforward f).mapHomotopyCategory
          (ComplexShape.up ℤ)).obj ((HomotopyCategory.quotient _ _).obj I)) ≫
        Rj.map (alpha_f.app ((HomotopyCategory.quotient _ _).obj I)) ≫
        (derivedPushforwardRestrictIso f i j g h Rf Rg Ri Rj
          alpha_f alpha_g alpha_i alpha_j).hom.app
            (DerivedCategory.Qh.obj ((HomotopyCategory.quotient _ _).obj I)) =
      DerivedCategory.Qh.map
          ((pushforwardRestrictHomotopyMap f i j g h.w).app
            ((HomotopyCategory.quotient _ _).obj I)) ≫
        alpha_g.app (((modulePullback i).mapHomotopyCategory
          (ComplexShape.up ℤ)).obj ((HomotopyCategory.quotient _ _).obj I)) ≫
        Rg.map (alpha_i.app ((HomotopyCategory.quotient _ _).obj I))
Tag 0D5W, a lemma

Tag 0D5W in the Stacks Project.

Stacks.Cohomology.DerivedSectionsLeray.isIso_lerayComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/LerayForDerivedSections.lean, line 428. The attribute's comment: “over an open”.

Stacks 0D5W, over an open. For a morphism f : X ⟶ Y of ringed spaces and an open V ⊆ Y, derived sections over V after derived pushforward along f agree with derived sections over f⁻¹ V, as functors D(𝒪_X) ⥤ D(Γ(V, 𝒪_Y)): the canonical Leray comparison is an isomorphism, with no hypothesis on f.

theorem isIso_lerayComparison : IsIso (lerayComparison f V)

Stacks.Cohomology.DerivedSectionsLeray.isIso_lerayComparison_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/LerayForDerivedSections.lean, line 454. The attribute's comment: “global sections”.

Stacks 0D5W, global sections. R Γ(Y, -) ∘ Rf_* and R Γ(X, -) agree as functors D(𝒪_X) ⥤ D(Γ(Y, 𝒪_Y)): the Leray comparison at V = ⊤ is an isomorphism. Its source is derived sections over f⁻¹ ⊤ = ⊤, that is global derived sections on X, regarded as complexes of Γ(Y, 𝒪_Y)-modules by restriction of scalars along f^♯.

theorem isIso_lerayComparison_top : IsIso (lerayComparison f ⊤)

Stacks.Cohomology.DerivedSectionsLeray.isIso_lerayComparison_top_and_forall_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/LerayForDerivedSections.lean, line 464. The attribute's comment: “both statements, for a morphism of ringed spaces: RΓ(Y, -) ∘ Rf_* = RΓ(X, -), and RΓ(U, -) = RΓ(V, -) ∘ Rf_* for V ⊆ Y open and U = f⁻¹ V”.

Stacks 0D5W, the whole lemma, stated for an arbitrary morphism of ringed spaces f : X ⟶ Y with no further hypothesis. The canonical Leray comparison RΓ(X, -) ⟶ RΓ(Y, -) ∘ Rf_* of functors D(𝒪_X) ⥤ D(Γ(Y, 𝒪_Y)) is an isomorphism, and more generally for every open V ⊆ Y with U = f⁻¹ V the comparison RΓ(U, -) ⟶ RΓ(V, -) ∘ Rf_* of functors D(𝒪_X) ⥤ D(Γ(V, 𝒪_Y)) is an isomorphism.

theorem isIso_lerayComparison_top_and_forall_open {X₀ Y₀ : RingedSpace.{u, u}} (g : X₀ ⟶ Y₀) :
    IsIso (lerayComparison g ⊤) ∧ ∀ W : Opens Y₀.carrier, IsIso (lerayComparison g W)
Tag 0D5X, a lemma

Tag 0D5X in the Stacks Project.

Stacks.Cohomology.UnboundedHigherDirectImage.preimageCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/CohomologySheavesOfADerivedPushforward.lean, line 76. The attribute's comment: “preimage formula”.

Cohomology over the inverse image f⁻¹ V agrees with cohomology over V after derived pushforward: H^i(f⁻¹ V, K) = H^i(V, Rf_* K), naturally in K.

def preimageCohomologyIso (V : Opens Y.carrier) (i : ℤ) :
    derivedPreimageSections f V ⋙
        DerivedCategory.homologyFunctor (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op V))) i ≅
      derivedPushforward f ⋙ derivedSectionsOverOpen Y V ⋙
        DerivedCategory.homologyFunctor (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op V))) i

Stacks.Cohomology.UnboundedHigherDirectImage.preimageCohomologyEvaluationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/CohomologySheavesOfADerivedPushforward.lean, line 87. The attribute's comment: “values on opens”.

The value on an open V ⊆ Y of the presheaf derivedPreimageCohomologyPresheaf is the hypercohomology H^i(f⁻¹ V, K) of K over the inverse image of V, naturally in K.

def preimageCohomologyEvaluationIso (V : Opens Y.carrier) (i : ℤ) :
    derivedPushforward f ⋙
        Stacks.Cohomology.HypercohomologyEdge.derivedSectionsPresheaf (structureSheafRing Y) ⋙
        DerivedCategory.homologyFunctor (PresheafOfModules.{u} (structureSheafRing Y).obj) i ⋙
        PresheafOfModules.evaluation (structureSheafRing Y).obj (op V) ≅
      derivedPreimageSections f V ⋙
        DerivedCategory.homologyFunctor (ModuleCat.{u} ((structureSheafRing Y).obj.obj (op V))) i

Stacks.Cohomology.UnboundedHigherDirectImage.higherDirectImageIsoSheafifyPreimageCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/CohomologySheavesOfADerivedPushforward.lean, line 102. The attribute's comment: “associated sheaf”.

The i-th cohomology sheaf of Rf_* K is the sheaf associated to the presheaf V ↦ H^i(f⁻¹ V, K), naturally in K.

def higherDirectImageIsoSheafifyPreimageCohomology (i : ℤ) :
    derivedPushforward f ⋙
        DerivedCategory.homologyFunctor (SheafOfModules.{u} (structureSheafRing Y)) i ≅
      derivedPushforward f ⋙
        Stacks.Cohomology.HypercohomologyEdge.derivedSectionsPresheaf (structureSheafRing Y) ⋙
        DerivedCategory.homologyFunctor (PresheafOfModules.{u} (structureSheafRing Y).obj) i ⋙
        PresheafOfModules.sheafification (𝟙 (structureSheafRing Y).obj)
Tag 0D5Y, a lemma

Tag 0D5Y in the Stacks Project.

Stacks.Cohomology.UnderlyingAbelianSheaf.sectionsForgetComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/UnderlyingAbelianSheafCohomology.lean, line 422. The attribute's comment: “part (1)”.

Stacks 0D5Y, part (1). Unbounded derived sections of modules agree canonically and naturally with derived sections after forgetting to abelian sheaves: for every open U ⊆ X the canonical map RΓ(U, K) ⟶ RΓ(U, K_ab) is an isomorphism in D(Ab).

public theorem sectionsForgetComparison_isIso {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) (U : Opens X) :
    IsIso (sectionsForgetComparison O U)

Stacks.Cohomology.UnderlyingAbelianPushforward.pushforwardForgetComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedCategory/UnderlyingAbelianSheafPushforward.lean, line 309. The attribute's comment: “part (2)”.

Stacks 0D5Y, part (2). The unbounded derived pushforward of a complex of 𝒪_X-modules, with the module structure forgotten, agrees canonically and naturally with the unbounded derived pushforward of the underlying complex of abelian sheaves: Rf_* K ⟶ Rf_*(K_ab) is an isomorphism in D(Ab_Y).

The morphism f of ringed spaces is the only argument: there is no HasRightDerivedFunctor precondition here, both derived pushforwards being supplied by the proved instances abelianPushforward_hasRightDerivedFunctor and isRightDerivedFunctor_pushforwardForgetSource above.

theorem pushforwardForgetComparison_isIso :
    IsIso (Stacks.Cohomology.UnderlyingAbelianPushforward.pushforwardForgetComparison f)
Tag 08BT, a lemma

Tag 08BT in the Stacks Project.

Stacks.ExtensionByZero.exists_derivedJShriek_restriction_adjunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/ExtensionByZero/DerivedAdjunction.lean, line 105.

For an open subset U of a ringed space X, extension by zero and restriction to U are exact, and the functor on unbounded derived categories induced by extension by zero is left adjoint to the functor induced by restriction to U.

theorem exists_derivedJShriek_restriction_adjunction
    (X : SheafedSpace RingCat.{u}) (U : Opens X.carrier) :
    ∃ (h₁ : (jShriek00A7 X U).Additive)
      (h₂ : PreservesFiniteLimits (jShriek00A7 X U))
      (h₃ : PreservesFiniteColimits (jShriek00A7 X U))
      (h₄ : (restMod X U).Additive)
      (h₅ : PreservesFiniteLimits (restMod X U))
      (h₆ : PreservesFiniteColimits (restMod X U)),
      letI := h₁
      letI := h₂
      letI := h₃
      letI := h₄
      letI := h₅
      letI := h₆
      Nonempty ((jShriek00A7 X U).mapDerivedCategory ⊣ (restMod X U).mapDerivedCategory)
Tag 0D5Z, a lemma

Tag 0D5Z in the Stacks Project.

RingedSpaceModuleAdjunction.isKInjective_modulePushforward_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/DerivedPushforward/FlatPushforwardOfKInjectives.lean, line 49.

Stacks 0D5Z. If f : X ⟶ Y is a flat morphism of ringed spaces and ℐ^• is a K-injective complex of 𝒪_X-modules, then f_* ℐ^• is K-injective as a complex of 𝒪_Y-modules.

theorem isKInjective_modulePushforward_of_isFlat {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (hf : AlgebraicGeometry.IsFlat f)
    (I : CochainComplex (_root_.SheafOfModules.{u} (structureSheafRing X)) ℤ)
    (hI : I.IsKInjective) :
    CochainComplex.IsKInjective
      (((modulePushforward f).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)
Sources
LeanExtensionByZeroModules.isKInjective_jStar · Stacks.Cohomology.OpenSubspace.cohomologyOnOpenIsoRestriction · Stacks.Cohomology.CohomologyPresheaf.cohomologyPresheafEvaluationIsoRestriction · Stacks.Cohomology.CohomologyPresheaf.cohomologyPresheafEvaluationIso · Stacks.Cohomology.CohomologyPresheaf.sheafificationCohomologyPresheafIso · Stacks.Duality.OpenImmersion.isIso_quasiCoherentDerivedRestrictBaseChangeSquare · AlgebraicGeometry.DerivedChow.derivedPushforwardRestrictOpenIso · AlgebraicGeometry.schemeDerivedPushforwardRestrictOpenIso

Section20.33 Unbounded Mayer-Vietoris#

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

Tag 08BU, a lemma

Tag 08BU in the Stacks Project.

Stacks.ExtensionByZero.distinguished_extensionRestriction_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/ExtensionByZero/MayerVietorisTriangle.lean, line 1386. The attribute's comment: “the whole statement: the distinguished triangle, for every choice of the three derived functors R(j_!j^*) and their units — the degreewise one of Section 20.32 included — with the two maps out of the intersection term pinned by the adjunction counits, the second with the Mayer--Vietoris sign”.

Stacks 08BU. For a cover by two open subspaces, extension by zero of the restrictions to their intersection and to the two opens forms a distinguished triangle, naturally in the object of the unbounded derived category.

public theorem distinguished_extensionRestriction_triangle {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    (U V : Opens X) (hUV : U ⊔ V = ⊤)
    (DU DV DUV : DerivedCategory (SheafOfModules.{u} O) ⥤
      DerivedCategory (SheafOfModules.{u} O))
    (aU : homotopyExtensionRestriction O U ⟶ DerivedCategory.Qh ⋙ DU)
    (aV : homotopyExtensionRestriction O V ⟶ DerivedCategory.Qh ⋙ DV)
    (aUV : homotopyExtensionRestriction O (U ⊓ V) ⟶ DerivedCategory.Qh ⋙ DUV)
    [DU.IsRightDerivedFunctor aU
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))]
    [DV.IsRightDerivedFunctor aV
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))]
    [DUV.IsRightDerivedFunctor aUV
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))] :
    ∃ (iU : DUV ⟶ DU) (iV : DUV ⟶ DV)
      (δ : 𝟭 (DerivedCategory (SheafOfModules.{u} O)) ⟶
        DUV ⋙ shiftFunctor (DerivedCategory (SheafOfModules.{u} O)) (1 : ℤ)),
      (iU ≫ derivedExtensionRestrictionCounit O U DU aU =
          derivedExtensionRestrictionCounit O (U ⊓ V) DUV aUV) ∧
      (iV ≫ derivedExtensionRestrictionCounit O V DV aV =
          -derivedExtensionRestrictionCounit O (U ⊓ V) DUV aUV) ∧
      (∀ E, Triangle.mk (biprod.lift (iU.app E) (iV.app E))
        (biprod.desc ((derivedExtensionRestrictionCounit O U DU aU).app E)
          ((derivedExtensionRestrictionCounit O V DV aV).app E)) (δ.app E) ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O)))

Stacks.ExtensionByZero.distinguished_derivedExtensionRestriction_triangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/ExtSequence.lean, line 383. The attribute's comment: “the whole statement at the presentation built in this file: the three clauses of distinguished_extensionRestriction_triangle for derivedExtensionRestriction, derivedExtensionRestrictionFactorsh and the instance derivedExtensionRestriction_isRightDerivedFunctor, with the maps to the identity functor the canonical derived adjunction counits of Stacks 08BT and the two maps out of the intersection term pinned by composing them with those counits, the second with the Mayer--Vietoris sign”.

Let X be a ringed space which is the union of two open subspaces U and V. Then there are comparison maps out of D(j_!)D(j^*) for U ∩ V into the ones for U and for V, and a connecting transformation, such that for every object of D(𝒪_X) the resulting triangle is distinguished. The three derived functors are derivedExtensionRestriction, the maps to the identity functor are the canonical derived adjunction counits derivedExtensionRestrictionCanonicalCounit, and the two comparison maps are determined by composing them with those counits, the second with a sign.

public theorem distinguished_derivedExtensionRestriction_triangle {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) (U V : Opens X)
    (hUV : U ⊔ V = ⊤) :
    ∃ (iU : derivedExtensionRestriction O (U ⊓ V) ⟶ derivedExtensionRestriction O U)
      (iV : derivedExtensionRestriction O (U ⊓ V) ⟶ derivedExtensionRestriction O V)
      (δ : 𝟭 (DerivedCategory (SheafOfModules.{u} O)) ⟶
        derivedExtensionRestriction O (U ⊓ V) ⋙
          shiftFunctor (DerivedCategory (SheafOfModules.{u} O)) (1 : ℤ)),
      (iU ≫ derivedExtensionRestrictionCanonicalCounit O U =
          derivedExtensionRestrictionCanonicalCounit O (U ⊓ V)) ∧
      (iV ≫ derivedExtensionRestrictionCanonicalCounit O V =
          -derivedExtensionRestrictionCanonicalCounit O (U ⊓ V)) ∧
      (∀ E, Triangle.mk (biprod.lift (iU.app E) (iV.app E))
        (biprod.desc ((derivedExtensionRestrictionCanonicalCounit O U).app E)
          ((derivedExtensionRestrictionCanonicalCounit O V).app E)) (δ.app E) ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O)))
Tag 08BV, a lemma

Tag 08BV in the Stacks Project.

Stacks.Duality.Coherator.isMayerVietorisApex_restrictPushforward_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/UnboundedMayerVietoris.lean, line 77. The attribute's comment: “the scheme-level form: U, V opens of a scheme inside their union, with the terms Rj_{W,*}(K|_W) of D(𝒪_X) at the locally small model”.

[Stacks, Tag 08BV] for a scheme. For opens U, V of a scheme X and any object K of the unbounded derived category D(𝒪_X) there is a distinguished triangle

Rj_{U ∪ V,*}(K|_{U ∪ V}) ⟶ Rj_{U,*}(K|_U) ⊕ Rj_{V,*}(K|_V) ⟶ Rj_{U ∩ V,*}(K|_{U ∩ V}) ⟶

in D(𝒪_X), where j_W : W → X are the inclusions of the open subschemes.

This is Stacks.Duality.Coherator.exists_distTriang_restrictPushforward_sup, read in the vocabulary of Stacks.Duality.Coherator.IsMayerVietorisApex.

theorem isMayerVietorisApex_restrictPushforward_sup (K : DerivedCategory X.Modules) :
    IsMayerVietorisApex X U V K (restrictPushforward (U ⊔ V) K)

Stacks.Duality.Coherator.isMayerVietorisApex_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/UnboundedMayerVietoris.lean, line 90. The attribute's comment: “the scheme-level form for a cover of the whole scheme, with K itself as the first term of the triangle”.

[Stacks, Tag 08BV] for a scheme, in the form of the source. If the opens U, V cover the scheme X, then every object K of D(𝒪_X) itself sits in a distinguished triangle

K ⟶ Rj_{U,*}(K|_U) ⊕ Rj_{V,*}(K|_V) ⟶ Rj_{U ∩ V,*}(K|_{U ∩ V}) ⟶ K⟦1⟧.

This is Stacks.Duality.Coherator.exists_distTriang_self, read in the vocabulary of Stacks.Duality.Coherator.IsMayerVietorisApex.

theorem isMayerVietorisApex_self (hUV : U ⊔ V = ⊤) (K : DerivedCategory X.Modules) :
    IsMayerVietorisApex X U V K K

Stacks.Cohomology.MayerVietoris.exists_distinguished_triangle_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/MayerVietoris.lean, line 442.

Stacks 08BV. A two-open cover gives a distinguished Mayer--Vietoris triangle, naturally in every object of the unbounded derived category of modules.

theorem exists_distinguished_triangle_of_cover
    (U V : Opens X) (hUV : U ⊔ V = ⊤)
    (RU RV RUV : DerivedCategory (SheafOfModules.{u} O) ⥤
      DerivedCategory (SheafOfModules.{u} O))
    (aU : homotopyToDerived O U ⟶ DerivedCategory.Qh ⋙ RU)
    (aV : homotopyToDerived O V ⟶ DerivedCategory.Qh ⋙ RV)
    (aUV : homotopyToDerived O (U ⊓ V) ⟶ DerivedCategory.Qh ⋙ RUV)
    [RU.IsRightDerivedFunctor aU
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))]
    [RV.IsRightDerivedFunctor aV
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))]
    [RUV.IsRightDerivedFunctor aUV
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))] :
    ∃ (qU : homotopyToDerived O U ⟶ homotopyToDerived O (U ⊓ V))
      (qV : homotopyToDerived O V ⟶ homotopyToDerived O (U ⊓ V))
      (rU : (CategoryTheory.Functor.id (DerivedCategory (SheafOfModules.{u} O)) :
        DerivedCategory (SheafOfModules.{u} O) ⥤
          DerivedCategory (SheafOfModules.{u} O)) ⟶ RU)
      (rV : (CategoryTheory.Functor.id (DerivedCategory (SheafOfModules.{u} O)) :
        DerivedCategory (SheafOfModules.{u} O) ⥤
          DerivedCategory (SheafOfModules.{u} O)) ⟶ RV)
      (dU : RU ⟶ RUV) (dV : RV ⟶ RUV)
      (δ : RUV ⟶ (CategoryTheory.Functor.id (DerivedCategory (SheafOfModules.{u} O)) :
          DerivedCategory (SheafOfModules.{u} O) ⥤
            DerivedCategory (SheafOfModules.{u} O)) ⋙
        shiftFunctor (DerivedCategory (SheafOfModules.{u} O)) (1 : ℤ)),
      homotopyRestriction O U ≫ qU = homotopyRestriction O (U ⊓ V) ∧
      homotopyRestriction O V ≫ qV = homotopyRestriction O (U ⊓ V) ∧
      homotopyRestriction O U ≫ aU = Functor.whiskerLeft DerivedCategory.Qh rU ∧
      homotopyRestriction O V ≫ aV = Functor.whiskerLeft DerivedCategory.Qh rV ∧
      qU ≫ aUV = aU ≫ Functor.whiskerLeft DerivedCategory.Qh dU ∧
      -(qV ≫ aUV) = aV ≫ Functor.whiskerLeft DerivedCategory.Qh dV ∧
      ∀ E, Triangle.mk (biprod.lift (rU.app E) (rV.app E))
        (biprod.desc (dU.app E) (dV.app E)) (δ.app E) ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))

Stacks.Cohomology.MayerVietoris.exists_distinguished_triangle_of_cover_rightDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietorisAndLimits/MayerVietorisCanonical.lean, line 144. The attribute's comment: “the ringed-space form with the three derived pushforwards constructed by rightDerivedRestrictPush, at the standard model of D(O): no derived functor, comparison map or derived-functor hypothesis is taken as a parameter”.

Stacks 08BV. A two-open cover of a space carrying a sheaf of rings O gives a distinguished Mayer--Vietoris triangle

E ⟶ Rj_{U*}(E|_U) ⊞ Rj_{V*}(E|_V) ⟶ Rj_{(U ∩ V)*}(E|_{U ∩ V}) ⟶ E⟦1⟧

naturally in the object E of the unbounded derived category of O-modules, where the three derived pushforwards are the ones constructed by rightDerivedRestrictPush. The restriction maps rU, rV, the two difference maps dU, dV and the connecting map δ are maps of functors on D(O), which is the naturality in E, and the equations preceding the triangle identify them with the restriction and transition maps of the cover through the canonical comparisons, so that the triangle's maps and its Mayer--Vietoris sign are retained rather than merely asserted to exist.

theorem exists_distinguished_triangle_of_cover_rightDerived
    (U V : Opens X) (hUV : U ⊔ V = ⊤) :
    ∃ (qU : homotopyToDerived O U ⟶ homotopyToDerived O (U ⊓ V))
      (qV : homotopyToDerived O V ⟶ homotopyToDerived O (U ⊓ V))
      (rU : (CategoryTheory.Functor.id (DerivedCategory (SheafOfModules.{u} O)) :
        DerivedCategory (SheafOfModules.{u} O) ⥤
          DerivedCategory (SheafOfModules.{u} O)) ⟶ rightDerivedRestrictPush O U)
      (rV : (CategoryTheory.Functor.id (DerivedCategory (SheafOfModules.{u} O)) :
        DerivedCategory (SheafOfModules.{u} O) ⥤
          DerivedCategory (SheafOfModules.{u} O)) ⟶ rightDerivedRestrictPush O V)
      (dU : rightDerivedRestrictPush O U ⟶ rightDerivedRestrictPush O (U ⊓ V))
      (dV : rightDerivedRestrictPush O V ⟶ rightDerivedRestrictPush O (U ⊓ V))
      (δ : rightDerivedRestrictPush O (U ⊓ V) ⟶
        (CategoryTheory.Functor.id (DerivedCategory (SheafOfModules.{u} O)) :
          DerivedCategory (SheafOfModules.{u} O) ⥤
            DerivedCategory (SheafOfModules.{u} O)) ⋙
        shiftFunctor (DerivedCategory (SheafOfModules.{u} O)) (1 : ℤ)),
      homotopyRestriction O U ≫ qU = homotopyRestriction O (U ⊓ V) ∧
      homotopyRestriction O V ≫ qV = homotopyRestriction O (U ⊓ V) ∧
      homotopyRestriction O U ≫ rightDerivedRestrictPushUnit O U =
        Functor.whiskerLeft DerivedCategory.Qh rU ∧
      homotopyRestriction O V ≫ rightDerivedRestrictPushUnit O V =
        Functor.whiskerLeft DerivedCategory.Qh rV ∧
      qU ≫ rightDerivedRestrictPushUnit O (U ⊓ V) =
        rightDerivedRestrictPushUnit O U ≫ Functor.whiskerLeft DerivedCategory.Qh dU ∧
      -(qV ≫ rightDerivedRestrictPushUnit O (U ⊓ V)) =
        rightDerivedRestrictPushUnit O V ≫ Functor.whiskerLeft DerivedCategory.Qh dV ∧
      ∀ E, Triangle.mk (biprod.lift (rU.app E) (rV.app E))
        (biprod.desc (dU.app E) (dV.app E)) (δ.app E) ∈
          distTriang (DerivedCategory (SheafOfModules.{u} O))
Tag 08BW, a lemma

Tag 08BW in the Stacks Project.

Stacks.ExtensionByZero.exists_mayerVietoris_ext_longExactSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/ExtSequence.lean, line 426. The attribute's comment: “long exact sequence of the Ext groups on the two opens and their intersection”.

Let X be a ringed space covered by two open subspaces U and V, and let E and F be objects of D(𝒪_X). There are restriction, difference and connecting homomorphisms making the Mayer--Vietoris sequence

⋯ ⟶ Ext^\{n-1}(E|\_\{U∩V}, F|\_\{U∩V}) ⟶ Ext^n(E, F) ⟶ Ext^n(E|\_U, F|\_U) × Ext^n(E|\_V, F|\_V) ⟶ Ext^n(E|\_\{U∩V}, F|\_\{U∩V}) ⟶ ⋯

exact at each of its three kinds of spot and in every integer degree, the Ext groups of the restrictions being taken in the derived categories of the open subspaces.

public theorem exists_mayerVietoris_ext_longExactSequence {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) (U V : Opens X) (hUV : U ⊔ V = ⊤)
    (E F : DerivedCategory (SheafOfModules.{u} O)) :
    ∃ (restriction : ∀ n : ℤ, (E ⟶ F⟦n⟧) →+
          (((derivedRestriction O U).obj E ⟶ ((derivedRestriction O U).obj F)⟦n⟧) ×
            ((derivedRestriction O V).obj E ⟶ ((derivedRestriction O V).obj F)⟦n⟧)))
      (difference : ∀ n : ℤ,
        (((derivedRestriction O U).obj E ⟶ ((derivedRestriction O U).obj F)⟦n⟧) ×
            ((derivedRestriction O V).obj E ⟶ ((derivedRestriction O V).obj F)⟦n⟧)) →+
          ((derivedRestriction O (U ⊓ V)).obj E ⟶
            ((derivedRestriction O (U ⊓ V)).obj F)⟦n⟧))
      (boundary : ∀ n : ℤ,
        ((derivedRestriction O (U ⊓ V)).obj E ⟶
          ((derivedRestriction O (U ⊓ V)).obj F)⟦n⟧) →+ (E ⟶ F⟦n + 1⟧)),
      ∀ n : ℤ, Function.Exact (restriction n) (difference n) ∧
        Function.Exact (difference n) (boundary n) ∧
        Function.Exact (boundary n) (restriction (n + 1))

Stacks.ExtensionByZero.exists_mayerVietoris_hom_longExactSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/ExtSequence.lean, line 491. The attribute's comment: “long exact sequence, extension-by-zero form of the Ext groups”.

Let X be a ringed space covered by two open subspaces U and V, and let E and F be objects of D(𝒪_X). For every choice of the three derived functors of extension by zero of the restrictions there are comparison maps iU and iV out of the functor attached to U ∩ V, compatible with the canonical derived adjunction counits and carrying the Mayer--Vietoris sign, and connecting homomorphisms, such that the Mayer--Vietoris sequence

⋯ ⟶ Ext^\{n-1}(j\_\{U∩V,!}E|\_\{U∩V}, F) ⟶ Ext^n(E, F) ⟶ Ext^n(j\_\{U!}E|\_U, F) × Ext^n(j\_\{V!}E|\_V, F) ⟶ Ext^n(j\_\{U∩V,!}E|\_\{U∩V}, F) ⟶ ⋯

is exact at each of its three kinds of spot and in every integer degree.

public theorem exists_mayerVietoris_hom_longExactSequence {X : TopCat.{u}}
    (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    (U V : Opens X) (hUV : U ⊔ V = ⊤)
    (DU DV DUV : DerivedCategory (SheafOfModules.{u} O) ⥤
      DerivedCategory (SheafOfModules.{u} O))
    (aU : homotopyExtensionRestriction O U ⟶ DerivedCategory.Qh ⋙ DU)
    (aV : homotopyExtensionRestriction O V ⟶ DerivedCategory.Qh ⋙ DV)
    (aUV : homotopyExtensionRestriction O (U ⊓ V) ⟶ DerivedCategory.Qh ⋙ DUV)
    [DU.IsRightDerivedFunctor aU
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))]
    [DV.IsRightDerivedFunctor aV
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))]
    [DUV.IsRightDerivedFunctor aUV
      (HomotopyCategory.quasiIso (SheafOfModules.{u} O) (ComplexShape.up ℤ))] :
    ∃ (iU : DUV ⟶ DU) (iV : DUV ⟶ DV)
      (boundary : ∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
        (DUV.obj E ⟶ F⟦n⟧) →+ (E ⟶ F⟦n + 1⟧)),
      (iU ≫ derivedExtensionRestrictionCounit O U DU aU =
          derivedExtensionRestrictionCounit O (U ⊓ V) DUV aUV) ∧
      (iV ≫ derivedExtensionRestrictionCounit O V DV aV =
          -derivedExtensionRestrictionCounit O (U ⊓ V) DUV aUV) ∧
      ∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
        Function.Exact
            (fun x : E ⟶ F⟦n⟧ =>
              ((derivedExtensionRestrictionCounit O U DU aU).app E ≫ x,
                (derivedExtensionRestrictionCounit O V DV aV).app E ≫ x))
            (fun w : (DU.obj E ⟶ F⟦n⟧) × (DV.obj E ⟶ F⟦n⟧) =>
              iU.app E ≫ w.1 + iV.app E ≫ w.2) ∧
          Function.Exact
            (fun w : (DU.obj E ⟶ F⟦n⟧) × (DV.obj E ⟶ F⟦n⟧) =>
              iU.app E ≫ w.1 + iV.app E ≫ w.2)
            (boundary E F n) ∧
          Function.Exact (boundary E F n)
            (fun x : E ⟶ F⟦n + 1⟧ =>
              ((derivedExtensionRestrictionCounit O U DU aU).app E ≫ x,
                (derivedExtensionRestrictionCounit O V DV aV).app E ≫ x))

Stacks.ExtensionByZero.exists_mayerVietoris_ext_longExactSequence_restrictions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/ExtSequenceRestrictions.lean, line 495. The attribute's comment: “the long exact sequence, with its first map the pair of the restrictions to the two opens and its second map the difference of two restrictions to their intersection”.

Stacks 08BW, with every map of the sequence named. For a ringed space covered by two open subspaces U and V and objects E, F of D(𝒪_X), the Mayer--Vietoris sequence

⋯ ⟶ Ext^\{n-1}(E|\_\{U∩V}, F|\_\{U∩V}) ⟶ Ext^n(E, F) ⟶ Ext^n(E|\_U, F|\_U) × Ext^n(E|\_V, F|\_V) ⟶ Ext^n(E|\_\{U∩V}, F|\_\{U∩V}) ⟶ ⋯

is exact at each of its three kinds of spot and in every integer degree, its first map is the pair of the two restrictions and its second map is the difference of two further restrictions to the intersection.

theorem exists_mayerVietoris_ext_longExactSequence_restrictions (hUV : U ⊔ V = ⊤) :
    ∃ (restriction : ∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          (E ⟶ F⟦n⟧) →+
            (ShiftedHom ((derivedRestriction O U).obj E) ((derivedRestriction O U).obj F) n ×
              ShiftedHom ((derivedRestriction O V).obj E)
                ((derivedRestriction O V).obj F) n))
      (restrictionUW : ∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          ShiftedHom ((derivedRestriction O U).obj E) ((derivedRestriction O U).obj F) n →+
            ShiftedHom ((derivedRestriction O (U ⊓ V)).obj E)
              ((derivedRestriction O (U ⊓ V)).obj F) n)
      (restrictionVW : ∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          ShiftedHom ((derivedRestriction O V).obj E) ((derivedRestriction O V).obj F) n →+
            ShiftedHom ((derivedRestriction O (U ⊓ V)).obj E)
              ((derivedRestriction O (U ⊓ V)).obj F) n)
      (difference : ∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          (ShiftedHom ((derivedRestriction O U).obj E) ((derivedRestriction O U).obj F) n ×
              ShiftedHom ((derivedRestriction O V).obj E)
                ((derivedRestriction O V).obj F) n) →+
            ShiftedHom ((derivedRestriction O (U ⊓ V)).obj E)
              ((derivedRestriction O (U ⊓ V)).obj F) n)
      (boundary : ∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          ShiftedHom ((derivedRestriction O (U ⊓ V)).obj E)
              ((derivedRestriction O (U ⊓ V)).obj F) n →+ (E ⟶ F⟦n + 1⟧)),
      (∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ) (x : E ⟶ F⟦n⟧),
          restriction E F n x =
            (ShiftedHom.map x (derivedRestriction O U),
              ShiftedHom.map x (derivedRestriction O V))) ∧
      (∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ) (x : E ⟶ F⟦n⟧),
          restrictionUW E F n (ShiftedHom.map x (derivedRestriction O U)) =
            ShiftedHom.map x (derivedRestriction O (U ⊓ V))) ∧
      (∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ) (x : E ⟶ F⟦n⟧),
          restrictionVW E F n (ShiftedHom.map x (derivedRestriction O V)) =
            ShiftedHom.map x (derivedRestriction O (U ⊓ V))) ∧
      (∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ)
          (xU : ShiftedHom ((derivedRestriction O U).obj E)
            ((derivedRestriction O U).obj F) n)
          (xV : ShiftedHom ((derivedRestriction O V).obj E)
            ((derivedRestriction O V).obj F) n),
          difference E F n (xU, xV) =
            restrictionUW E F n xU - restrictionVW E F n xV) ∧
      (∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          Function.Exact (restriction E F n) (difference E F n)) ∧
      (∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          Function.Exact (difference E F n) (boundary E F n)) ∧
      (∀ (E F : DerivedCategory (SheafOfModules.{u} O)) (n : ℤ),
          Function.Exact (boundary E F n) (restriction E F (n + 1)))
Tag 08BX, a lemma

Tag 08BX in the Stacks Project.

Stacks.Cohomology.LinearMayerVietoris.linearUnboundedMayerVietoris, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/LinearUnboundedTriangle.lean, line 849. The attribute's comment: “the triangle in D(A), A = Γ(X, 𝒪_X)”.

Let X be a ringed space covered by two open subsets U and V, and let A = Γ(X, 𝒪_X). The restriction maps of the A-linear derived sections functors, with the usual sign on the overlap, fit into a distinguished triangle in the derived category of A-modules, naturally in the object of D(𝒪_X): the connecting map is a natural transformation and the other four maps are the right-derived restrictions.

theorem linearUnboundedMayerVietoris (hUV : U ⊔ V = ⊤) :
    ∃ δ : derivedLinearSections X (U ⊓ V) ⟶ derivedLinearSections X ⊤ ⋙
          shiftFunctor (DerivedCategory (ModuleCat.{u} (baseRing X))) (1 : ℤ),
      ∀ E, Triangle.mk
        (biprod.lift ((derivedLinearRestriction X (le_top : U ≤ ⊤)).app E)
          ((derivedLinearRestriction X (le_top : V ≤ ⊤)).app E))
        (biprod.desc ((derivedLinearRestriction X (inf_le_left : U ⊓ V ≤ U)).app E)
          (-((derivedLinearRestriction X (inf_le_right : U ⊓ V ≤ V)).app E)))
        (δ.app E) ∈ distTriang (DerivedCategory (ModuleCat.{u} (baseRing X)))

Stacks.Cohomology.SpaceMayerVietoris.relativeUnboundedMayerVietoris, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/UnboundedDerivedSections.lean, line 283. The attribute's comment: “for a pair of opens covering an arbitrary open, not only the whole space”.

Stacks 08BX for a cover of an arbitrary open. Let X be a ringed space and let W = U ∪ V be an open subset written as the union of two open subsets. For any choice of derived sections functors over W, U, V and U ∩ V — that is, any right derived functors of degreewise sections along the quasi-isomorphisms — the right-derived restriction maps, with the usual sign on the overlap, fit into a distinguished triangle in the derived category of abelian groups, naturally in the object of D(𝒪_X): the connecting map is a natural transformation and the other four maps are natural transformations of the given functors. Applying the cohomological functors gives the functorial Mayer--Vietoris long exact sequence.

public theorem relativeUnboundedMayerVietoris (X : RingedSpace.{u, u})
    (U V W : Opens X.carrier) (hUV : U ⊔ V = W)
    (RW RU RV RUV : DerivedCategory (ModuleSheaves X) ⥤ DerivedCategory AddCommGrpCat.{u})
    (aW : sectionsComplexDerived X W ⟶ DerivedCategory.Q ⋙ RW)
    (aU : sectionsComplexDerived X U ⟶ DerivedCategory.Q ⋙ RU)
    (aV : sectionsComplexDerived X V ⟶ DerivedCategory.Q ⋙ RV)
    (aUV : sectionsComplexDerived X (U ⊓ V) ⟶ DerivedCategory.Q ⋙ RUV)
    [RW.IsRightDerivedFunctor aW
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RU.IsRightDerivedFunctor aU
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RV.IsRightDerivedFunctor aV
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RUV.IsRightDerivedFunctor aUV
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))] :
    ∃ δ : RUV ⟶ RW ⋙ shiftFunctor (DerivedCategory AddCommGrpCat.{u}) (1 : ℤ),
      ∀ E, Triangle.mk
        (biprod.lift
          ((RW.rightDerivedNatTrans RU aW aU
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (le_sup_left.trans hUV.le : U ≤ W)))).app E)
          ((RW.rightDerivedNatTrans RV aW aV
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (le_sup_right.trans hUV.le : V ≤ W)))).app E))
        (biprod.desc
          ((RU.rightDerivedNatTrans RUV aU aUV
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (inf_le_left : U ⊓ V ≤ U)))).app E)
          (-((RV.rightDerivedNatTrans RUV aV aUV
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (inf_le_right : U ⊓ V ≤ V)))).app E)))
        (δ.app E) ∈ distTriang (DerivedCategory AddCommGrpCat.{u})

Stacks.Cohomology.SpaceMayerVietoris.unboundedMayerVietoris, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/UnboundedDerivedSections.lean, line 431.

Stacks 08BX. Let X be a ringed space covered by two open subsets U and V. For any choice of derived sections functors over X, U, V and U ∩ V — that is, any right derived functors of degreewise sections along the quasi-isomorphisms — the right-derived restriction maps, with the usual sign on the overlap, fit into a distinguished triangle in the derived category of abelian groups, naturally in the object of D(𝒪_X): the connecting map is a natural transformation and the other four maps are natural transformations of the given functors. Applying the cohomological functors gives the functorial Mayer--Vietoris long exact sequence.

public theorem unboundedMayerVietoris (X : RingedSpace.{u, u}) (U V : Opens X.carrier)
    (hUV : U ⊔ V = ⊤)
    (RX RU RV RUV : DerivedCategory (ModuleSheaves X) ⥤ DerivedCategory AddCommGrpCat.{u})
    (aX : sectionsComplexDerived X ⊤ ⟶ DerivedCategory.Q ⋙ RX)
    (aU : sectionsComplexDerived X U ⟶ DerivedCategory.Q ⋙ RU)
    (aV : sectionsComplexDerived X V ⟶ DerivedCategory.Q ⋙ RV)
    (aUV : sectionsComplexDerived X (U ⊓ V) ⟶ DerivedCategory.Q ⋙ RUV)
    [RX.IsRightDerivedFunctor aX
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RU.IsRightDerivedFunctor aU
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RV.IsRightDerivedFunctor aV
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))]
    [RUV.IsRightDerivedFunctor aUV
      (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))] :
    ∃ δ : RUV ⟶ RX ⋙ shiftFunctor (DerivedCategory AddCommGrpCat.{u}) (1 : ℤ),
      ∀ E, Triangle.mk
        (biprod.lift
          ((RX.rightDerivedNatTrans RU aX aU
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (le_top : U ≤ ⊤)))).app E)
          ((RX.rightDerivedNatTrans RV aX aV
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (le_top : V ≤ ⊤)))).app E))
        (biprod.desc
          ((RU.rightDerivedNatTrans RUV aU aUV
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (inf_le_left : U ⊓ V ≤ U)))).app E)
          (-((RV.rightDerivedNatTrans RUV aV aUV
            (HomologicalComplex.quasiIso (ModuleSheaves X) (ComplexShape.up ℤ))
            (sectionsRestrictionDerived X (homOfLE (inf_le_right : U ⊓ V ≤ V)))).app E)))
        (δ.app E) ∈ distTriang (DerivedCategory AddCommGrpCat.{u})
Tag 08HZ, a lemma

Tag 08HZ in the Stacks Project.

Stacks.Cohomology.RelativeMayerVietoris.canonicalPushforwardTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RelativeMayerVietoris/CanonicalDerivedTriangle.lean, line 139. The attribute's comment: “the triangle with no choices: the canonical derived functors of canonicalRightDerived and the canonical sequence of Tag 01EC, which is the form in which two such triangles can be compared”.

The relative Mayer--Vietoris triangle built from the canonical derived functors and the canonical relative Mayer--Vietoris sequence is distinguished at every object of the unbounded derived category.

public theorem canonicalPushforwardTriangle_distinguished
    (E : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))) :
    canonicalPushforwardTriangle f iU iV iW cover intersection E ∈
      distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))

Stacks.Cohomology.RelativeMayerVietoris.unboundedRelativeMayerVietoris, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RelativeMayerVietoris/UnboundedDerivedPushforward.lean, line 906.

Stacks 08HZ. For a morphism of ringed spaces and a cover of its source by two open subsets, the four derived pushforwards attached to the cover fit into a distinguished triangle, naturally in the object of the unbounded derived category. The four derived pushforwards are hypothesised only through CategoryTheory.Functor.IsRightDerivedFunctor, so the statement applies to every choice of them; applying a cohomological functor to the triangle gives the relative Mayer--Vietoris long exact sequence.

public theorem unboundedRelativeMayerVietoris (f : X ⟶ Y) (U V : Opens X) (hUV : U ⊔ V = ⊤)
    (Rf RU RV RUV : DerivedCategory (SheafOfModules.{u} (structureSheafRing X)) ⥤
      DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))
    (af : homotopyToDerived (modulePushforward f) ⟶ DerivedCategory.Qh ⋙ Rf)
    (aU : homotopyToDerived (restrictedPushforward f U) ⟶ DerivedCategory.Qh ⋙ RU)
    (aV : homotopyToDerived (restrictedPushforward f V) ⟶ DerivedCategory.Qh ⋙ RV)
    (aUV : homotopyToDerived (restrictedPushforward f (U ⊓ V)) ⟶ DerivedCategory.Qh ⋙ RUV)
    [Rf.IsRightDerivedFunctor af (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [RU.IsRightDerivedFunctor aU (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [RV.IsRightDerivedFunctor aV (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [RUV.IsRightDerivedFunctor aUV (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))] :
    ∃ (rU : Rf ⟶ RU) (rV : Rf ⟶ RV) (dU : RU ⟶ RUV) (dV : RV ⟶ RUV)
      (δ : RUV ⟶ Rf ⋙ shiftFunctor
        (DerivedCategory (SheafOfModules.{u} (structureSheafRing Y))) (1 : ℤ)),
      ∀ E, Triangle.mk (biprod.lift (rU.app E) (rV.app E))
        (biprod.desc (dU.app E) (dV.app E)) (δ.app E) ∈
          distTriang (DerivedCategory (SheafOfModules.{u} (structureSheafRing Y)))

Stacks.Cohomology.RelativeMayerVietoris.pushforwardTriangleMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/RelativeMayerVietoris/UnboundedDerivedPushforward.lean, line 1046. The attribute's comment: “functoriality of the triangle in E: the lemma's second assertion, which the existential form above cannot express because it hides the morphisms”.

The relative Mayer--Vietoris triangle is functorial in the derived object: a morphism e : E ⟶ E' induces a morphism of triangles whose components are the four derived functors applied to e.

public def pushforwardTriangleMap
    {E E' : DerivedCategory (SheafOfModules.{u} (structureSheafRing X))} (e : E ⟶ E') :
    pushforwardTriangle f iU iV iW S Rf RU RV RUV af aU aV aUV E ⟶
      pushforwardTriangle f iU iV iW S Rf RU RV RUV af aU aV aUV E'
Tag 08DF, a lemma

Tag 08DF in the Stacks Project.

Stacks.Cohomology.PushforwardRestriction.isIso_derivedOpenPushforward_restrictionUnit_app_of_supported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/PushforwardAndRestriction.lean, line 1067. The attribute's comment: “part (1)”.

Stacks Project, Tag 08DF, part (1). Let j : U → X be the inclusion of an open subspace of a ringed space and T ⊆ U a closed subset of X. If every cohomology sheaf of E ∈ D(O_X) is supported on T, then the canonical map E ⟶ Rj_*(E|_U) is an isomorphism.

theorem isIso_derivedOpenPushforward_restrictionUnit_app_of_supported
    {X : TopCat.{u}} (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    (U : Opens X) (T : Set X) (hT : IsClosed T) (hTU : T ⊆ U)
    [HasDerivedCategory (SheafOfModules.{u} O)]
    [HasDerivedCategory (SheafOfModules.{u} (resRing U O))]
    (E : DerivedCategory (SheafOfModules.{u} O))
    (hE : CohomologySupportedOn O T E) :
    IsIso ((derivedPushforwardRestrictionUnit O U (derivedOpenPushforward O U)
      (derivedOpenPushforwardUnit O U)).app E)

Stacks.Cohomology.PushforwardRestriction.isIso_extensionByZeroToDerivedOpenPushforward_app_of_supported, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/SupportedComplexes/PushforwardAndRestriction.lean, line 1084. The attribute's comment: “part (2)”.

Stacks Project, Tag 08DF, part (2). Let j : U → X be the inclusion of an open subspace of a ringed space and T ⊆ U a closed subset of X. If every cohomology sheaf of F ∈ D(O_U) is supported on T, then the canonical map j_! F ⟶ Rj_* F is an isomorphism.

theorem isIso_extensionByZeroToDerivedOpenPushforward_app_of_supported
    {X : TopCat.{u}} (O : Sheaf (Opens.grothendieckTopology X) RingCat.{u})
    (U : Opens X) (T : Set X) (hT : IsClosed T) (hTU : T ⊆ U)
    [HasDerivedCategory (SheafOfModules.{u} O)]
    [HasDerivedCategory (SheafOfModules.{u} (resRing U O))]
    (F : DerivedCategory (SheafOfModules.{u} (resRing U O)))
    (hF : CohomologySupportedOn (resRing U O)
      ((fun x : Usp U ↦ x.1) ⁻¹' T) F) :
    IsIso ((extensionByZeroToDerivedPushforward O U (derivedOpenPushforward O U)
      (derivedOpenPushforwardUnit O U)).app F)
Tag 0G6X, a lemma

Tag 0G6X in the Stacks Project.

Stacks.Cohomology.LinearCupProductTriangle.linearCupProductMayerVietoris, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/LinearCupProductTriangle.lean, line 717. The attribute's comment: “the map of triangles, with the vertices read on the chosen representatives”.

Stacks 0G6X. Let (X, 𝒪_X) be a ringed space, A = Γ(X, 𝒪_X), and let X = U ∪ V be a union of two open subsets. For a choice of resolutions of two complexes K and M of 𝒪_X-modules there is a map of distinguished triangles in D(A) from the Mayer--Vietoris triangle of RΓ(X, K) ⊗^𝐋_A RΓ(-, M) to the Mayer--Vietoris triangle of RΓ(-, K ⊗^𝐋_{𝒪_X} M) whose three vertical maps are the cup products over X, over U and V, and over U ∩ V.

theorem linearCupProductMayerVietoris (hUV : U ⊔ V = ⊤) :
    cupSourceTriangle U V d hUV ∈ distTriang (DerivedCategory (ModuleCat.{u} (baseRing X))) ∧
      cupTargetTriangle U V d hUV ∈
          distTriang (DerivedCategory (ModuleCat.{u} (baseRing X))) ∧
        (tensorRepresentative d).map
              (DerivedCategory.Q.map (coverFirstComplex X U V d.inj)) ≫
            derivedCupMiddle U V d =
          derivedCupMap d ⊤ ≫ DerivedCategory.Q.map (coverFirstComplex X U V d.tgt) ∧
        (tensorRepresentative d).map
              (DerivedCategory.Q.map (coverSecondComplex X U V d.inj)) ≫
            derivedCupMap d (U ⊓ V) =
          derivedCupMiddle U V d ≫ DerivedCategory.Q.map (coverSecondComplex X U V d.tgt) ∧
        cupBoundary U V d hUV ≫
            (shiftFunctor (DerivedCategory (ModuleCat.{u} (baseRing X))) (1 : ℤ)).map
              (derivedCupMap d ⊤) =
          derivedCupMap d (U ⊓ V) ≫
            DerivedCategory.triangleOfSESδ (shortExact_cupTarget U V d hUV)

Stacks.Cohomology.LinearCupProductTriangle.exists_cupData_linearCupProductMayerVietoris, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Cohomology/MayerVietoris/LinearCupProductTriangle.lean, line 742. The attribute's comment: “for arbitrary complexes, after replacing K by a K-injective resolution”.

Stacks 0G6X for arbitrary complexes. Every complex K of 𝒪_X-modules admits a quasi-isomorphism into a complex carrying a choice of resolutions, so that the map of Mayer--Vietoris triangles above exists for every object of D(𝒪_X).

theorem exists_cupData_linearCupProductMayerVietoris (hUV : U ⊔ V = ⊤)
    (K M : CochainComplex (Modules X) ℤ) :
    ∃ (K' : CochainComplex (Modules X) ℤ) (e : K ⟶ K') (d : CupData X K' M), QuasiIso e ∧
      cupSourceTriangle U V d hUV ∈
          distTriang (DerivedCategory (ModuleCat.{u} (baseRing X))) ∧
        cupTargetTriangle U V d hUV ∈
            distTriang (DerivedCategory (ModuleCat.{u} (baseRing X))) ∧
          (tensorRepresentative d).map
                (DerivedCategory.Q.map (coverFirstComplex X U V d.inj)) ≫
              derivedCupMiddle U V d =
            derivedCupMap d ⊤ ≫ DerivedCategory.Q.map (coverFirstComplex X U V d.tgt) ∧
          (tensorRepresentative d).map
                (DerivedCategory.Q.map (coverSecondComplex X U V d.inj)) ≫
              derivedCupMap d (U ⊓ V) =
            derivedCupMiddle U V d ≫ DerivedCategory.Q.map (coverSecondComplex X U V d.tgt) ∧
          cupBoundary U V d hUV ≫
              (shiftFunctor (DerivedCategory (ModuleCat.{u} (baseRing X))) (1 : ℤ)).map
                (derivedCupMap d ⊤) =
            derivedCupMap d (U ⊓ V) ≫
              DerivedCategory.triangleOfSESδ (shortExact_cupTarget U V d hUV)
Sources
LeanStacks.ExtensionByZero.distinguished_extensionRestriction_triangle · Stacks.ExtensionByZero.distinguished_derivedExtensionRestriction_triangle · Stacks.Duality.Coherator.isMayerVietorisApex_restrictPushforward_sup · Stacks.Duality.Coherator.isMayerVietorisApex_self · Stacks.Cohomology.MayerVietoris.exists_distinguished_triangle_of_cover · Stacks.Cohomology.MayerVietoris.exists_distinguished_triangle_of_cover_rightDerived · Stacks.ExtensionByZero.exists_mayerVietoris_ext_longExactSequence · Stacks.ExtensionByZero.exists_mayerVietoris_hom_longExactSequence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.