Čech cohomology of quasi-coherent sheaves as modules over the base ring

Let X be a scheme over a commutative ring S and let M be a sheaf of modules on X. Its sections over every open are S-modules, through the global functions Γ(X, ⊤), and the restriction maps are S-linear; this is the presheaf of S-modules (Scheme.Modules.sectionsBasePresheafFunctor S).obj M of TauCeti.AlgebraicGeometry.Modules.Sections. Its Čech complex for a family of opens is therefore a complex of S-modules, and so is its cohomology.

Let X be a scheme, M quasi-coherent and U a finite family of opens covering X whose nonempty finite intersections are affine. Leray's theorem identifies the Čech cohomology of M for U with the cohomology Hⁿ(X, M) as abelian groups (Scheme.Modules.homologyCechComplexIsoCohomology). This file shows that the identification is S-linear (Scheme.Modules.homologyCechComplexLinearEquiv): the Čech complex of the presheaf of S-modules computes Hⁿ(X, M) as an S-module. Linear-algebraic operations on the Čech complex, such as extension of scalars along a flat ring map, thus become available for cohomology.

The underlying complex of abelian groups of the Čech complex of a presheaf of modules is the Čech complex of the underlying presheaf of abelian groups (TauCeti.CategoryTheory.cechComplexFunctorMapIso), and forgetting the module structure preserves homology. The action of s : S on the Čech cohomology is induced by multiplication by s on the presheaf, which is the endomorphism of M given by multiplication by the global function s, and Leray's comparison is natural in the coefficient sheaf.

Main definitions

• AlgebraicGeometry.Scheme.Modules.homologyCechComplexLinearEquiv: the S-linear equivalence between the Čech cohomology of this presheaf for a finite cover with affine intersections and Hⁿ(X, M).

Main statements

• AlgebraicGeometry.Scheme.Modules.homologyCechComplexLinearEquiv_apply: its underlying map is Leray's comparison homologyCechComplexIsoCohomology.
• AlgebraicGeometry.Scheme.Modules.homologyCechComplexLinearEquiv_naturality: it is natural in the quasi-coherent sheaf.

References

• R. Hartshorne, Algebraic Geometry, Theorem III.4.5.

noncomputable def AlgebraicGeometry.Scheme.Modules.homologyCechComplexLinearEquiv {S : Type u} [CommRing S] {X : Scheme} [X.Over (Spec ↧S)] {ι : Type u} [Finite ι] (U : ι → X.Opens) (hU : ∀ (s : Finset ι), s.Nonempty → IsAffineOpen (s.inf U)) (hcover : ⨆ (i : ι), U i = ⊤) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) : ↑(HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj ((sectionsBasePresheafFunctor S).obj M)) n) ≃ₗ[S] TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n

Čech cohomology computes cohomology, linearly over the base ring. Let X be a scheme over S, M a quasi-coherent sheaf of modules on X and U a finite family of opens covering X whose nonempty finite intersections are affine. Then the cohomology of the Čech complex of the presheaf of S-modules of sections of M for U is S-linearly equivalent to Hⁿ(X, M), for every n. The underlying additive equivalence is Leray's comparison homologyCechComplexIsoCohomology.

theorem AlgebraicGeometry.Scheme.Modules.homologyCechComplexLinearEquiv_apply {S : Type u} [CommRing S] {X : Scheme} [X.Over (Spec ↧S)] {ι : Type u} [Finite ι] (U : ι → X.Opens) (hU : ∀ (s : Finset ι), s.Nonempty → IsAffineOpen (s.inf U)) (hcover : ⨆ (i : ι), U i = ⊤) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) (x : ↑(HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj ((sectionsBasePresheafFunctor S).obj M)) n)) : (homologyCechComplexLinearEquiv U hU hcover M n) x = (CategoryTheory.ConcreteCategory.hom (homologyCechComplexIsoCohomology U hU hcover M n).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((TauCeti.CategoryTheory.cechComplexFunctorMapIso U (CategoryTheory.forget₂ (ModuleCat S) Ab)).app ((sectionsBasePresheafFunctor S).obj M) ≪≫ (CategoryTheory.cechComplexFunctor U).mapIso (sectionsBasePresheafCompForget₂Iso S M)).hom n)) ((CategoryTheory.ConcreteCategory.hom ((HomologicalComplex.sc ((CategoryTheory.cechComplexFunctor U).obj ((sectionsBasePresheafFunctor S).obj M)) n).mapHomologyIso (CategoryTheory.forget₂ (ModuleCat S) Ab)).inv) x))

The underlying map of homologyCechComplexLinearEquiv is Leray's comparison homologyCechComplexIsoCohomology, after forgetting the module structure, which commutes with taking homology and with forming Čech complexes.

theorem AlgebraicGeometry.Scheme.Modules.homologyCechComplexLinearEquiv_naturality {S : Type u} [CommRing S] {X : Scheme} [X.Over (Spec ↧S)] {ι : Type u} [Finite ι] (U : ι → X.Opens) (hU : ∀ (s : Finset ι), s.Nonempty → IsAffineOpen (s.inf U)) (hcover : ⨆ (i : ι), U i = ⊤) {M N : X.Modules} [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] (f : M ⟶ N) (n : ℕ) (x : ↑(HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj ((sectionsBasePresheafFunctor S).obj M)) n)) : (homologyCechComplexLinearEquiv U hU hcover N n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((CategoryTheory.cechComplexFunctor U).map ((sectionsBasePresheafFunctor S).map f)) n)) x) = (CategoryTheory.ConcreteCategory.hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X n).map f)) ((homologyCechComplexLinearEquiv U hU hcover M n) x)

homologyCechComplexLinearEquiv is natural in the quasi-coherent sheaf.