Mayer-Vietoris for the cohomology of a sheaf of modules on a scheme

TauCeti/AlgebraicGeometry/Cohomology/Basic.lean defines the cohomology Hⁿ(X, M) of a sheaf of modules on a scheme, and the cohomology Hⁿ(U, M) of an open subset. This file adds the long exact Mayer-Vietoris sequence of two open subsets U and V:

⋯ ⟶ Hⁿ(U ⊔ V, M) ⟶ Hⁿ(U, M) ⊞ Hⁿ(V, M) ⟶ Hⁿ(U ⊓ V, M) ⟶ Hⁿ⁺¹(U ⊔ V, M) ⟶ ⋯

together with the vanishing it gives when U and V cover X.

Main declarations

• Scheme.Modules.mayerVietorisSequence is the six-term piece of the long exact sequence, Scheme.Modules.mayerVietorisSequence_def identifies each of its objects and arrows with restriction maps and the connecting map Scheme.Modules.mayerVietorisδ, and Scheme.Modules.mayerVietorisSequence_exact is its exactness;
• Scheme.Modules.epi_mayerVietorisδ: if Hⁿ⁺¹(U, M) and Hⁿ⁺¹(V, M) vanish, then the connecting map Hⁿ(U ⊓ V, M) ⟶ Hⁿ⁺¹(U ⊔ V, M) is an epimorphism;
• Scheme.Modules.subsingleton_cohomologyOn_sup_succ: if moreover Hⁿ(U ⊓ V, M) vanishes, then Hⁿ⁺¹(U ⊔ V, M) vanishes; Scheme.Modules.subsingleton_cohomology_succ specializes this to Hⁿ⁺¹(X, M) when U ⊔ V = ⊤, and Scheme.Modules.subsingleton_cohomology_of_two_le applies this at degree n - 1 under uniform positive-degree acyclicity hypotheses;
• Scheme.Modules.subsingleton_cohomology_of_two_le_of_isAffineOpen applies affine-open acyclicity when U, V, and U ⊓ V are affine, while the _of_isAffineHom variant obtains the intersection hypothesis from an affine diagonal.

These statements are the shape in which Mayer-Vietoris is used on a curve. The general theorem accepts arbitrary coefficients and explicit acyclicity hypotheses. For quasi-coherent coefficients on a locally Noetherian scheme, the affine-open variants use the acyclicity of quasi-coherent sheaves on affine opens; users may either supply an affine intersection directly or obtain it from an affine diagonal.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer B, "coherent sheaves and cohomology Hⁱ(X, ℱ): … vanishing above dimension (H² = 0 on a curve)". No formalization is vendored: the long exact sequence is Mathlib's CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact, the square attached to two open subsets is Mathlib's TopologicalSpace.Opens.mayerVietorisSquare, and the comparison between the cohomology of the terminal open subset and the cohomology of the site comes from TauCeti/CategoryTheory/Sites/SheafCohomology/Terminal.lean through Scheme.Modules.cohomologyOnTopIso.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.Scheme.Modules.mayerVietorisδ {X : AlgebraicGeometry.Scheme} (M : X.Modules) (U V : TopologicalSpace.Opens ↥X) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : cohomologyOn M n₀ (U ⊓ V) ⟶ cohomologyOn M n₁ (U ⊔ V)

The connecting map Hⁿ⁰(U ⊓ V, M) ⟶ Hⁿ¹(U ⊔ V, M) of the Mayer-Vietoris sequence of two open subsets.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.mayerVietorisδ M U V n₀ n₁ h = (Opens.mayerVietorisSquare U V).δ ((SheafOfModules.toSheaf X.ringCatSheaf).obj M) n₀ n₁ h

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.Scheme.Modules.mayerVietorisSequence {X : AlgebraicGeometry.Scheme} (M : X.Modules) (U V : TopologicalSpace.Opens ↥X) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : CategoryTheory.ComposableArrows AddCommGrpCat 5

Six consecutive terms of the Mayer-Vietoris long exact sequence of two open subsets, running from Hⁿ⁰(U ⊔ V, M) to Hⁿ¹(U ⊓ V, M).

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.mayerVietorisSequence M U V n₀ n₁ h = (Opens.mayerVietorisSquare U V).sequence ((SheafOfModules.toSheaf X.ringCatSheaf).obj M) n₀ n₁ h

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.mayerVietorisSequence_def {X : AlgebraicGeometry.Scheme} (M : X.Modules) (U V : TopologicalSpace.Opens ↥X) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : mayerVietorisSequence M U V n₀ n₁ h = CategoryTheory.ComposableArrows.mk₅ (CategoryTheory.Limits.biprod.lift (cohomologyOnRes M n₀ ⋯) (cohomologyOnRes M n₀ ⋯)) (CategoryTheory.Limits.biprod.desc (cohomologyOnRes M n₀ ⋯) (-cohomologyOnRes M n₀ ⋯)) (mayerVietorisδ M U V n₀ n₁ h) (CategoryTheory.Limits.biprod.lift (cohomologyOnRes M n₁ ⋯) (cohomologyOnRes M n₁ ⋯)) (CategoryTheory.Limits.biprod.desc (cohomologyOnRes M n₁ ⋯) (-cohomologyOnRes M n₁ ⋯))

Every object and every arrow of the Mayer-Vietoris sequence: the two maps to a biproduct are the pairs of restriction maps from U ⊔ V, the two maps out of a biproduct are the differences of the restriction maps to U ⊓ V, and the middle map is the connecting map.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.mayerVietorisSequence_exact {X : AlgebraicGeometry.Scheme} (M : X.Modules) (U V : TopologicalSpace.Opens ↥X) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) : (mayerVietorisSequence M U V n₀ n₁ h).Exact

The Mayer-Vietoris sequence of two open subsets is exact.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.epi_mayerVietorisδ {X : AlgebraicGeometry.Scheme} (M : X.Modules) (U V : TopologicalSpace.Opens ↥X) (n : ℕ) (hU : Subsingleton ↑(cohomologyOn M (n + 1) U)) (hV : Subsingleton ↑(cohomologyOn M (n + 1) V)) : CategoryTheory.Epi (mayerVietorisδ M U V n (n + 1) ⋯)

If the degree n + 1 cohomology of both of two open subsets vanishes, then the Mayer-Vietoris connecting map onto Hⁿ⁺¹(U ⊔ V, M) is an epimorphism.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.subsingleton_cohomologyOn_sup_succ {X : AlgebraicGeometry.Scheme} (M : X.Modules) {U V : TopologicalSpace.Opens ↥X} (n : ℕ) (hInter : Subsingleton ↑(cohomologyOn M n (U ⊓ V))) (hU : Subsingleton ↑(cohomologyOn M (n + 1) U)) (hV : Subsingleton ↑(cohomologyOn M (n + 1) V)) : Subsingleton ↑(cohomologyOn M (n + 1) (U ⊔ V))

If the degree n + 1 cohomology of both of two open subsets vanishes, and their intersection has vanishing degree n cohomology, then their union has vanishing degree n + 1 cohomology.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_succ {X : AlgebraicGeometry.Scheme} (M : X.Modules) {U V : TopologicalSpace.Opens ↥X} (hUV : U ⊔ V = ⊤) (n : ℕ) (hInter : Subsingleton ↑(cohomologyOn M n (U ⊓ V))) (hU : Subsingleton ↑(cohomologyOn M (n + 1) U)) (hV : Subsingleton ↑(cohomologyOn M (n + 1) V)) : Subsingleton (Cohomology M (n + 1))

A scheme covered by two open subsets whose degree n + 1 cohomology vanishes, and whose intersection has vanishing degree n cohomology, has vanishing degree n + 1 cohomology.

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_of_two_le {X : AlgebraicGeometry.Scheme} (M : X.Modules) {U V : TopologicalSpace.Opens ↥X} (hUV : U ⊔ V = ⊤) (n : ℕ) (hn : 2 ≤ n) (hU : ∀ (i : ℕ), 0 < i → Subsingleton ↑(cohomologyOn M i U)) (hV : ∀ (i : ℕ), 0 < i → Subsingleton ↑(cohomologyOn M i V)) (hInter : ∀ (i : ℕ), 0 < i → Subsingleton ↑(cohomologyOn M i (U ⊓ V))) : Subsingleton (Cohomology M n)

A scheme covered by two open subsets which, together with their intersection, are acyclic in positive degrees has no cohomology in degrees at least two.

This is the form Mayer-Vietoris takes on a separated scheme covered by two affine opens: the intersection is then affine as well. For quasi-coherent M on a locally Noetherian scheme the hypotheses are the acyclicity of quasi-coherent sheaves on affine opens, which gives Scheme.Modules.subsingleton_cohomology_of_two_le_of_isAffineOpen; for a general M : X.Modules they have to come from elsewhere.

theorem AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_of_two_le_of_isAffineOpen {X : Scheme} (M : X.Modules) [IsLocallyNoetherian X] [SheafOfModules.IsQuasicoherent M] {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hInter : IsAffineOpen (U ⊓ V)) (hUV : U ⊔ V = ⊤) (n : ℕ) (hn : 2 ≤ n) : Subsingleton (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n)

A quasi-coherent sheaf of modules on a locally Noetherian scheme covered by two affine opens with affine intersection has no cohomology in degrees at least two.

theorem AlgebraicGeometry.Scheme.Modules.subsingleton_cohomology_of_two_le_of_isAffineOpen_of_isAffineHom {X : Scheme} (M : X.Modules) [IsLocallyNoetherian X] [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] [SheafOfModules.IsQuasicoherent M] {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hUV : U ⊔ V = ⊤) (n : ℕ) (hn : 2 ≤ n) : Subsingleton (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n)

A quasi-coherent sheaf of modules on a locally Noetherian scheme with affine diagonal (for instance a separated one) that is covered by two affine opens has no cohomology in degrees at least two.