Čech cohomology of quasi-coherent sheaves for affine covers

Let X be a scheme and let M be a quasi-coherent sheaf of modules on X. Then M has no cohomology in positive degrees on affine opens (AlgebraicGeometry.Scheme.Modules.subsingleton_cohomologyOn_succ_of_isAffineOpen). So every finite open cover U of X whose nonempty finite intersections are affine is a Leray cover for M, and by Leray's theorem (TauCeti.Topology.homologyCechComplexIsoH) the Čech cohomology Hⁿ(U, M) of the underlying abelian sheaf of M is isomorphic to the cohomology Hⁿ(X, M). When X has affine diagonal, for instance when it is separated, finite intersections of affine opens are affine (AlgebraicGeometry.IsAffineOpen.biInf), so Hⁿ(X, M) can be computed from the Čech complex of any finite affine open cover.

The isomorphism is natural in the quasi-coherent sheaf M. In particular it intertwines the map on Čech cohomology induced by multiplication by a global function r on M with the action of r on Hⁿ(X, M) (Scheme.Modules.cohomologyModule), so it is compatible with the module structures of both sides over the ring of global functions, and hence over any base ring.

Main declarations

• AlgebraicGeometry.Scheme.Modules.homologyCechComplexIsoCohomology: for a finite open cover U of X with affine nonempty finite intersections, Hⁿ(U, M) ≅ Hⁿ(X, M) for every n;
• AlgebraicGeometry.Scheme.Modules.homologyMap_comp_homologyCechComplexIsoCohomology_hom: its naturality in M;
• AlgebraicGeometry.Scheme.Modules.homologyCechComplexIsoCohomology_hom_globalSectionsSmul: its compatibility with the action of global functions;
• AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardIsoOfIsAffineHom: for an affine morphism f : X ⟶ Y, where Y has affine diagonal and a finite affine open cover U, the isomorphism Hⁿ(Y, f_* M) ≅ Hⁿ(X, M) for quasi-coherent M;
• AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardIsoOfIsAffineHom_naturality: its naturality in M;
• AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquivOfIsAffineHom: the same isomorphism as a linear equivalence over a base ring;
• AlgebraicGeometry.Scheme.Modules.exists_mono_isQuasicoherent_subsingleton_cohomology: on a quasi-compact scheme with affine diagonal, every quasi-coherent sheaf embeds into a quasi-coherent sheaf with no cohomology in positive degrees, the step of a dimension-shifting argument.

Cohomology along affine morphisms

Let f : X ⟶ Y be an affine morphism and U a finite affine open cover of Y whose finite intersections are affine. The preimages f⁻¹ U i form a finite affine open cover of X with affine finite intersections, and the sections of f_* M over a finite intersection of members of U are the sections of M over its preimage. So the Čech complex of f_* M for U is the Čech complex of M for f⁻¹ U (TauCeti.CategoryTheory.cechComplexCompIso), and computing both sides by Čech cohomology gives Hⁿ(Y, f_* M) ≅ Hⁿ(X, M). This is the computation of cohomology along an affine morphism suggested by Hartshorne, Exercise III.4.1; it lets finiteness of cohomology be transferred from Y to schemes finite over Y. The isomorphism is built from the chosen cover U.

References

• R. Hartshorne, Algebraic Geometry, Theorem III.4.5 and Exercise III.4.1.

noncomputable def AlgebraicGeometry.Scheme.Modules.homologyCechComplexIsoCohomology {X : Scheme} {ι : Type u} (U : ι → X.Opens) (hU : ∀ (s : Finset ι), s.Nonempty → IsAffineOpen (s.inf U)) [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) : HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj ((SheafOfModules.toSheaf X.ringCatSheaf).obj M).obj) n ≅ ↧(TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n)

Čech cohomology computes the cohomology of a quasi-coherent sheaf. Let X be a scheme, M a quasi-coherent sheaf of modules on X, and U a finite family of opens covering X whose nonempty finite intersections are affine, for instance a finite affine open cover when X has affine diagonal. Then the Čech cohomology Hⁿ(U, M) of the underlying abelian sheaf of M is isomorphic to Hⁿ(X, M), for every n, naturally in M (homologyMap_comp_homologyCechComplexIsoCohomology_hom).

theorem AlgebraicGeometry.Scheme.Modules.homologyMap_comp_homologyCechComplexIsoCohomology_hom {X : Scheme} {ι : Type u} (U : ι → X.Opens) (hU : ∀ (s : Finset ι), s.Nonempty → IsAffineOpen (s.inf U)) [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) {M N : X.Modules} [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] (f : M ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((CategoryTheory.cechComplexFunctor U).map ((SheafOfModules.toSheaf X.ringCatSheaf).map f).hom) n) (homologyCechComplexIsoCohomology U hU hcover N n).hom = CategoryTheory.CategoryStruct.comp (homologyCechComplexIsoCohomology U hU hcover M n).hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X n).map f)

The comparison of Čech cohomology for a finite cover with affine intersections with the cohomology of a quasi-coherent sheaf is natural in the sheaf.

theorem AlgebraicGeometry.Scheme.Modules.homologyMap_comp_homologyCechComplexIsoCohomology_hom_assoc {X : Scheme} {ι : Type u} (U : ι → X.Opens) (hU : ∀ (s : Finset ι), s.Nonempty → IsAffineOpen (s.inf U)) [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) {M N : X.Modules} [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] (f : M ⟶ N) (n : ℕ) {Z : AddCommGrpCat} (h : ↧(TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology N n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((CategoryTheory.cechComplexFunctor U).map ((SheafOfModules.toSheaf X.ringCatSheaf).map f).hom) n) (CategoryTheory.CategoryStruct.comp (homologyCechComplexIsoCohomology U hU hcover N n).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (homologyCechComplexIsoCohomology U hU hcover M n).hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X n).map f)) h

The comparison of Čech cohomology for a finite cover with affine intersections with the cohomology of a quasi-coherent sheaf is natural in the sheaf.

theorem AlgebraicGeometry.Scheme.Modules.homologyCechComplexIsoCohomology_hom_globalSectionsSmul {X : Scheme} {ι : Type u} (U : ι → X.Opens) (hU : ∀ (s : Finset ι), s.Nonempty → IsAffineOpen (s.inf U)) [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↑(HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj ((SheafOfModules.toSheaf X.ringCatSheaf).obj M).obj) n)) : (CategoryTheory.ConcreteCategory.hom (homologyCechComplexIsoCohomology U hU hcover M n).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((CategoryTheory.cechComplexFunctor U).map ((SheafOfModules.toSheaf X.ringCatSheaf).map (M.globalSectionsSmul r)).hom) n)) x) = r • (CategoryTheory.ConcreteCategory.hom (homologyCechComplexIsoCohomology U hU hcover M n).hom) x

The comparison of Čech cohomology for a finite cover with affine intersections with the cohomology of a quasi-coherent sheaf M is linear over the global functions: it carries the map on Čech cohomology induced by multiplication by r on M to scalar multiplication by r on Hⁿ(X, M).

Cohomology along affine morphisms

noncomputable def AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardIsoOfIsAffineHom {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens) [IsAffineHom f] (hU : ∀ (i : ι), IsAffineOpen (U i)) [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) : ↧(TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) ≅ ↧(TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n)

Cohomology along an affine morphism. Let f : X ⟶ Y be an affine morphism of schemes, where Y has affine diagonal (for instance Y separated), and let U be a finite family of affine opens covering Y. For a quasi-coherent sheaf M on X, the cohomology Hⁿ(Y, f_* M) of its direct image is isomorphic to Hⁿ(X, M), naturally in M (cohomologyPushforwardIsoOfIsAffineHom_naturality). Both sides are computed by the same Čech complex, for the cover U of Y and for the cover of X by the preimages f⁻¹ U i.

theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardIsoOfIsAffineHom_naturality {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens) [IsAffineHom f] (hU : ∀ (i : ι), IsAffineOpen (U i)) [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) {M N : X.Modules} [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] (α : M ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor Y n).map ((Modules.pushforward f).map α)) (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover N n).hom = CategoryTheory.CategoryStruct.comp (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover M n).hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X n).map α)

The cohomology comparison along an affine morphism commutes with maps of quasi-coherent coefficient sheaves.

theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardIsoOfIsAffineHom_naturality_assoc {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens) [IsAffineHom f] (hU : ∀ (i : ι), IsAffineOpen (U i)) [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) {M N : X.Modules} [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] (α : M ⟶ N) (n : ℕ) {Z : AddCommGrpCat} (h : ↧(TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology N n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor Y n).map ((Modules.pushforward f).map α)) (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover N n).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover M n).hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X n).map α)) h

The cohomology comparison along an affine morphism commutes with maps of quasi-coherent coefficient sheaves.

theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardIsoOfIsAffineHom_hom_smul {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens) [IsAffineHom f] (hU : ∀ (i : ι), IsAffineOpen (U i)) [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) : (CategoryTheory.ConcreteCategory.hom (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover M n).hom) (r • x) = (CategoryTheory.ConcreteCategory.hom (appTop f)) r • (CategoryTheory.ConcreteCategory.hom (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover M n).hom) x

The cohomology comparison along an affine morphism carries the action of a global function on Y to the action of its pullback along f.

noncomputable def AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquivOfIsAffineHom {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens) [IsAffineHom f] (hU : ∀ (i : ι), IsAffineOpen (U i)) [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n ≃ₗ[R] TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n

Cohomology along an affine morphism, over a base ring. For an affine morphism f over a commutative ring R, the comparison Hⁿ(Y, f_* M) ≅ Hⁿ(X, M) of cohomologyPushforwardIsoOfIsAffineHom is R-linear.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquivOfIsAffineHom_apply {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens) [IsAffineHom f] (hU : ∀ (i : ι), IsAffineOpen (U i)) [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) : (cohomologyPushforwardBaseLinearEquivOfIsAffineHom f U hU hcover R M n) x = (CategoryTheory.ConcreteCategory.hom (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover M n).hom) x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquivOfIsAffineHom_symm_apply {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens) [IsAffineHom f] (hU : ∀ (i : ι), IsAffineOpen (U i)) [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from Y))] [Finite ι] (hcover : ⨆ (i : ι), U i = ⊤) (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) [SheafOfModules.IsQuasicoherent M] (n : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n) : (cohomologyPushforwardBaseLinearEquivOfIsAffineHom f U hU hcover R M n).symm x = (CategoryTheory.ConcreteCategory.hom (cohomologyPushforwardIsoOfIsAffineHom f U hU hcover M n).inv) x

theorem AlgebraicGeometry.Scheme.Modules.exists_mono_isQuasicoherent_subsingleton_cohomology {X : Scheme} [CompactSpace ↥X] [IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] (M : X.Modules) [SheafOfModules.IsQuasicoherent M] : ∃ (I : X.Modules) (i : M ⟶ I), SheafOfModules.IsQuasicoherent I ∧ CategoryTheory.Mono i ∧ ∀ (k : ℕ), Subsingleton (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology I (k + 1))

Every quasi-coherent sheaf M on a quasi-compact scheme with affine diagonal embeds into a quasi-coherent sheaf with no cohomology in positive degrees, namely the direct sum of the pushforwards of the restrictions of M to the members of a finite affine open cover.