Leray's theorem: Čech cohomology of a Leray cover computes sheaf cohomology

Let F be a sheaf of abelian groups on a topological space X and let U be a finite open cover of X such that F has no cohomology in positive degrees on any nonempty finite intersection of members of U (a Leray cover for F). Then the Čech cohomology Hⁿ(U, F), the cohomology of the Čech complex Č(U, F), is isomorphic to the sheaf cohomology Hⁿ(X, F) in every degree.

The proof is by dimension shifting. Embed F into an injective sheaf I, with cokernel Q.

• On every finite intersection V of members of U, the sequence of sections 0 ⟶ F(V) ⟶ I(V) ⟶ Q(V) ⟶ 0 is exact, because H¹(V, F) = 0; so the Čech complexes form a short exact sequence 0 ⟶ Č(U, F) ⟶ Č(U, I) ⟶ Č(U, Q) ⟶ 0.
• I is flasque, so Č(U, I) has no cohomology in positive degrees (TopCat.Sheaf.quasiIso_cechAugmentation_of_isFlasque), and neither has I sheaf cohomology. The two long exact sequences then give Hⁿ⁺¹(U, F) ≅ Hⁿ(U, Q) and Hⁿ⁺¹(X, F) ≅ Hⁿ(X, Q) for n ≥ 1, while in degree one both H¹(U, F) and H¹(X, F) are the cokernel of I(X) ⟶ Q(X), since H⁰(U, -) and H⁰(X, -) are both global sections.
• Q is again acyclic on the finite intersections, as Hᵏ(V, Q) ≅ Hᵏ⁺¹(V, F) for k ≥ 1.

Induction on the degree, for all sheaves at once, concludes. The comparison is defined by this recursion, using a fixed choice of the injective sheaf I for each F. It is natural in F: a morphism F ⟶ G extends to a morphism of the chosen sequences (TauCeti.injectiveCokernelSequenceMap), and the connecting maps of both long exact sequences are natural. In particular the comparison commutes with every endomorphism of F, so it respects any module structure on both sides that is induced by an action of a ring on F.

Main results

• TauCeti.Topology.homologyCechComplexIsoH: for a finite Leray cover U of X, Hⁿ(U, F) ≅ Hⁿ(X, F) for every n;
• TauCeti.Topology.homologyMap_comp_homologyCechComplexIsoH_hom: this isomorphism is natural in F;
• TauCeti.Topology.homologyCechComplexIsoH_zero: in degree 0 it is the identification of both groups with the global sections.
• TauCeti.Topology.δ_comp_homologyCechComplexIsoH_one_hom: in degree 1 the comparison intertwines the connecting maps of the Čech and sheaf injective cokernel sequences.

References

• R. Hartshorne, Algebraic Geometry, Exercise III.4.11, and the proof of Theorem III.4.5.

@[reducible, inline]

noncomputable abbrev TauCeti.Topology.cechSeq {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) : CategoryTheory.ShortComplex (CochainComplex AddCommGrpCat ℕ)

The sequence of Čech complexes of 0 ⟶ F ⟶ I ⟶ Q ⟶ 0 for the cover U.

noncomputable def TauCeti.Topology.cechSeqMap {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (f : F ⟶ G) : cechSeq U F ⟶ cechSeq U G

A morphism F ⟶ G induces a morphism of the sequences of Čech complexes of the chosen injective cokernel sequences, through TauCeti.injectiveCokernelSequenceMap.

@[simp]

theorem TauCeti.Topology.cechSeqMap_τ₁ {X : TopCat} {ι : Type u} {U : ι → TopologicalSpace.Opens ↑X} {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (f : F ⟶ G) : (cechSeqMap U f).τ₁ = (CategoryTheory.cechComplexFunctor U).map f.hom

On the first term, the chosen Čech sequence map is the original coefficient morphism.

@[simp]

theorem TauCeti.Topology.cechSeqMap_τ₂ {X : TopCat} {ι : Type u} {U : ι → TopologicalSpace.Opens ↑X} {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (f : F ⟶ G) : (cechSeqMap U f).τ₂ = (CategoryTheory.cechComplexFunctor U).map (injectiveCokernelSequenceMap f).τ₂.hom

On the injective term, the Čech sequence map is induced by the chosen injective lift.

@[simp]

theorem TauCeti.Topology.cechSeqMap_τ₃ {X : TopCat} {ι : Type u} {U : ι → TopologicalSpace.Opens ↑X} {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (f : F ⟶ G) : (cechSeqMap U f).τ₃ = (CategoryTheory.cechComplexFunctor U).map (injectiveCokernelSequenceMap f).τ₃.hom

On the quotient term, the Čech sequence map is induced by the chosen quotient map.

noncomputable def TauCeti.Topology.homologyCechComplexIsoH {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : ⨆ (i : ι), U i = ⊤) [Finite ι] (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) (hF : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(F.H' (k + 1) (s.inf U))) (n : ℕ) : HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj F.obj) n ≅ ↧(F.H n)

Leray's theorem. Let U be a finite family of opens covering a topological space X, and let F be a sheaf of abelian groups on X with no cohomology in positive degrees on any nonempty finite intersection of members of U. Then the Čech cohomology Hⁿ(U, F), the cohomology of the Čech complex of F for U, is isomorphic to the sheaf cohomology Hⁿ(X, F), for every n, naturally in F (TauCeti.Topology.homologyMap_comp_homologyCechComplexIsoH_hom).

@[simp]

theorem TauCeti.Topology.homologyCechComplexIsoH_zero {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : ⨆ (i : ι), U i = ⊤) [Finite ι] (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) (hF : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(F.H' (k + 1) (s.inf U))) : homologyCechComplexIsoH U hU F hF 0 = homologyZeroCechIso U hU F

In degree 0, the comparison of Leray's theorem is the identification of both groups with the global sections.

theorem TauCeti.Topology.δ_comp_homologyCechComplexIsoH_one_hom {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : ⨆ (i : ι), U i = ⊤) [Finite ι] (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) (hF : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(F.H' (k + 1) (s.inf U))) (hS : (((injectiveCokernelSequence F).map (CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)).map (CategoryTheory.cechComplexFunctor U)).ShortExact) : CategoryTheory.CategoryStruct.comp (hS.δ 0 1 ⋯) (homologyCechComplexIsoH U hU F hF 1).hom = CategoryTheory.CategoryStruct.comp (homologyZeroCechIso U hU (CategoryTheory.Limits.cokernel (CategoryTheory.Injective.ι F))).hom (AddCommGrpCat.ofHom (CategoryTheory.Sheaf.H.δ ⋯ 0 1 ⋯))

In degree one, the all-degree Leray comparison intertwines the connecting maps of the Čech and sheaf injective cokernel sequences. The short exactness witness may be any one.

theorem TauCeti.Topology.δ_comp_homologyCechComplexIsoH_one_hom_assoc {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : ⨆ (i : ι), U i = ⊤) [Finite ι] (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) (hF : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(F.H' (k + 1) (s.inf U))) (hS : (((injectiveCokernelSequence F).map (CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)).map (CategoryTheory.cechComplexFunctor U)).ShortExact) {Z : AddCommGrpCat} (h : ↧(F.H 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (hS.δ 0 1 ⋯) (CategoryTheory.CategoryStruct.comp (homologyCechComplexIsoH U hU F hF 1).hom h) = CategoryTheory.CategoryStruct.comp (homologyZeroCechIso U hU (CategoryTheory.Limits.cokernel (CategoryTheory.Injective.ι F))).hom (CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom (CategoryTheory.Sheaf.H.δ ⋯ 0 1 ⋯)) h)

In degree one, the all-degree Leray comparison intertwines the connecting maps of the Čech and sheaf injective cokernel sequences. The short exactness witness may be any one.

theorem TauCeti.Topology.homologyMap_comp_homologyCechComplexIsoH_hom {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : ⨆ (i : ι), U i = ⊤) [Finite ι] {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (hF : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(F.H' (k + 1) (s.inf U))) (hG : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(G.H' (k + 1) (s.inf U))) (f : F ⟶ G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((CategoryTheory.cechComplexFunctor U).map f.hom) n) (homologyCechComplexIsoH U hU G hG n).hom = CategoryTheory.CategoryStruct.comp (homologyCechComplexIsoH U hU F hF n).hom (AddCommGrpCat.ofHom (CategoryTheory.Sheaf.H.map f n))

Naturality of Leray's theorem. The comparison Hⁿ(U, F) ≅ Hⁿ(X, F) commutes with the maps induced by a morphism F ⟶ G of sheaves which both satisfy the hypotheses of Leray's theorem.

theorem TauCeti.Topology.homologyMap_comp_homologyCechComplexIsoH_hom_assoc {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : ⨆ (i : ι), U i = ⊤) [Finite ι] {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (hF : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(F.H' (k + 1) (s.inf U))) (hG : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(G.H' (k + 1) (s.inf U))) (f : F ⟶ G) (n : ℕ) {Z : AddCommGrpCat} (h : ↧(G.H n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((CategoryTheory.cechComplexFunctor U).map f.hom) n) (CategoryTheory.CategoryStruct.comp (homologyCechComplexIsoH U hU G hG n).hom h) = CategoryTheory.CategoryStruct.comp (homologyCechComplexIsoH U hU F hF n).hom (CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom (CategoryTheory.Sheaf.H.map f n)) h)

Naturality of Leray's theorem. The comparison Hⁿ(U, F) ≅ Hⁿ(X, F) commutes with the maps induced by a morphism F ⟶ G of sheaves which both satisfy the hypotheses of Leray's theorem.