Cohomology of sheaves of modules on a scheme

Mathlib defines the cohomology CategoryTheory.Sheaf.H of an abelian sheaf on a site as an Ext group from the constant sheaf ℤ. This file applies that construction to the underlying abelian sheaf of an 𝒪_X-module and packages the result in the scheme-module API.

For a scheme X and M : X.Modules, the main declarations are:

• Scheme.Modules.Cohomology M i, the group Hⁱ(X, M);
• Scheme.Modules.cohomologyFunctor X i, functoriality in the coefficient sheaf;
• Scheme.Modules.cohomologyZeroEquiv, the canonical equivalence H⁰(X, M) ≃+ Γ(M, ⊤) with global sections;
• Scheme.Modules.cohomologyOn M n U, the cohomology Hⁿ(U, M) of an open subset, Scheme.Modules.cohomologyOnRes its restriction maps, and Scheme.Modules.cohomologyOnTopIso the identification of Hⁿ(⊤, M) with Hⁿ(X, M).

The construction is stated for every sheaf of modules, which is the natural generality of sheaf cohomology. In particular it applies to finitely presented sheaves through their underlying objects, and hence supplies the Hⁱ(X, ℱ) used for coherent sheaves in TauCetiRoadmap/JacobianChallenge/README.md, Layer B. Finite-dimensionality for proper schemes, vanishing on curves, and the comparison with Čech cohomology remain later Layer B work.

No formalization is vendored. The definitions reuse Mathlib's Sheaf.H, Sheaf.functorH, Sheaf.H.equiv₀ and Sheaf.H', and the comparison at the terminal open subset is TauCeti/CategoryTheory/Sites/SheafCohomology/Terminal.lean.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology {X : AlgebraicGeometry.Scheme} (M : X.Modules) (i : ℕ) : Type u

The ith cohomology group Hⁱ(X, M) of a sheaf of modules on a scheme.

This is sheaf cohomology on the small Zariski site of X, obtained by forgetting the 𝒪_X-module structure and applying Mathlib's CategoryTheory.Sheaf.H.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i = ((SheafOfModules.toSheaf X.ringCatSheaf).obj M).H i

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor (X : AlgebraicGeometry.Scheme) (i : ℕ) : CategoryTheory.Functor X.Modules AddCommGrpCat

Degree-i cohomology as an additive functor from sheaves of modules to abelian groups.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X i = (SheafOfModules.toSheaf X.ringCatSheaf).comp (CategoryTheory.Sheaf.functorH (Opens.grothendieckTopology ↥X) i)

instance TauCeti.AlgebraicGeometry.Scheme.Modules.instAdditiveModulesAddCommGrpCatCohomologyFunctor (X : AlgebraicGeometry.Scheme) (i : ℕ) : (cohomologyFunctor X i).Additive

Degreewise scheme-module cohomology preserves addition and zero morphisms.

noncomputable def TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyZeroEquiv {X : AlgebraicGeometry.Scheme} (M : X.Modules) : Cohomology M 0 ≃+ ↑(M.presheaf.obj (Opposite.op ⊤))

Zeroth cohomology is canonically equivalent to the group of global sections.

Naturality in the coefficient sheaf follows from CategoryTheory.Sheaf.H.equiv₀_naturality and CategoryTheory.Sheaf.H.equiv₀_symm_naturality, applied to isTerminalTop and the underlying sheaf morphism.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyZeroEquiv M = CategoryTheory.Sheaf.H.equiv₀ ((SheafOfModules.toSheaf X.ringCatSheaf).obj M) CategoryTheory.Limits.isTerminalTop

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyZeroEquiv_naturality {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (f : M ⟶ N) (x : Cohomology M 0) : (cohomologyZeroEquiv N) ((CategoryTheory.ConcreteCategory.hom ((cohomologyFunctor X 0).map f)) x) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app f ⊤)) ((cohomologyZeroEquiv M) x)

The degree-zero cohomology equivalence is natural in the coefficient sheaf.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOn {X : AlgebraicGeometry.Scheme} (M : X.Modules) (n : ℕ) (U : TopologicalSpace.Opens ↥X) : AddCommGrpCat

The cohomology Hⁿ(U, M) of an open subset U of a scheme X with coefficients in a sheaf of modules M, as an abelian group.

This is CategoryTheory.Sheaf.H' applied to the underlying abelian sheaf of M. At U = ⊤ it agrees with Scheme.Modules.Cohomology, by Scheme.Modules.cohomologyOnTopIso.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOn M n U = ((SheafOfModules.toSheaf X.ringCatSheaf).obj M).H' n U

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOnRes {X : AlgebraicGeometry.Scheme} (M : X.Modules) (n : ℕ) {U V : TopologicalSpace.Opens ↥X} (h : U ≤ V) : cohomologyOn M n V ⟶ cohomologyOn M n U

Restriction in cohomology along an inclusion of open subsets.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOnRes M n h = (((SheafOfModules.toSheaf X.ringCatSheaf).obj M).cohomologyPresheaf n).map (CategoryTheory.homOfLE h).op

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOnRes_refl {X : AlgebraicGeometry.Scheme} (M : X.Modules) (n : ℕ) (U : TopologicalSpace.Opens ↥X) : cohomologyOnRes M n ⋯ = CategoryTheory.CategoryStruct.id (cohomologyOn M n U)

@[simp]

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOnRes_comp {X : AlgebraicGeometry.Scheme} (M : X.Modules) (n : ℕ) {U V W : TopologicalSpace.Opens ↥X} (hUV : U ≤ V) (hVW : V ≤ W) : CategoryTheory.CategoryStruct.comp (cohomologyOnRes M n hVW) (cohomologyOnRes M n hUV) = cohomologyOnRes M n ⋯

theorem TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOnRes_comp_assoc {X : AlgebraicGeometry.Scheme} (M : X.Modules) (n : ℕ) {U V W : TopologicalSpace.Opens ↥X} (hUV : U ≤ V) (hVW : V ≤ W) {Z : AddCommGrpCat} (h : cohomologyOn M n U ⟶ Z) : CategoryTheory.CategoryStruct.comp (cohomologyOnRes M n hVW) (CategoryTheory.CategoryStruct.comp (cohomologyOnRes M n hUV) h) = CategoryTheory.CategoryStruct.comp (cohomologyOnRes M n ⋯) h

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOnTopIso {X : AlgebraicGeometry.Scheme} (M : X.Modules) (n : ℕ) : cohomologyOn M n ⊤ ≅ ↧(Cohomology M n)

The cohomology of the whole space is the cohomology of the scheme.

Equations

• TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyOnTopIso M n = ((SheafOfModules.toSheaf X.ringCatSheaf).obj M).cohomologyPresheafObjIsoH n CategoryTheory.Limits.isTerminalTop