Finitely generated vanishing reduction

On a Noetherian space, every sheaf is the filtered colimit of its finitely generated subsheaves, and sheaf cohomology commutes with filtered colimits. Combining the two reduces vanishing of Hⁿ for arbitrary sheaves to vanishing for finitely generated ones. This file packages that reduction; together with the Noetherian-shrinking step, it underlies the irreducible positive-dimensional case of Grothendieck vanishing.

Main definitions

• finsetGenFunctor — the filtered diagram of finitely generated subsheaves.
• finsetGenCocone, finsetGenCoconeIsColimit — exhibits K as the colimit.

Main results

• cohomology_vanishing_of_finitelyGenerated_vanishing — vanishing for f.g. subsheaves propagates to the whole sheaf via the filtered-colimit comparison.
• finsetGeneratedSheaf_vanishing — Finset.induction reducing vanishing for finitely generated subsheaves to vanishing for the epi-images of zeroOutsideInt V.
• directLimit_cohomology_vanishing — composes both above into the headline reduction.

The isFlasque_filtered_colimit and sheafHPreservesFilteredColimits building blocks live in the PresheafFilteredColimit modules.

Filtered diagram of finitely generated subsheaves

We build a functor Finset(SectionIndex K) ⥤ Sheaf(X) sending each finite set S of local sections to the subsheaf finsetGeneratedSheaf S. The transition maps (for S ⊆ S') are monomorphisms, and K is the colimit of this filtered diagram.

noncomputable def finsetGenFunctor {X : TopCat} {K : TopCat.Presheaf AddCommGrpCat X} (hK : K.IsSheaf) : CategoryTheory.Functor (Finset K.SectionIndex) (TopCat.Sheaf AddCommGrpCat X)

The functor Finset(SectionIndex K) ⥤ Sheaf(X) sending S ↦ finsetGeneratedSheaf S. Transition maps are the canonical image inclusions, which are monomorphisms.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def finsetGenCocone {X : TopCat} {K : TopCat.Presheaf AddCommGrpCat X} (hK : K.IsSheaf) : CategoryTheory.Limits.Cocone (finsetGenFunctor hK)

Cocone with vertex K: the cocone maps are image.ι : finsetGeneratedSheaf S ⟶ K.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def finsetGenCoconeIsColimit {X : TopCat} {K : TopCat.Presheaf AddCommGrpCat X} (hK : K.IsSheaf) : CategoryTheory.Limits.IsColimit (finsetGenCocone hK)

The cocone is a colimit: K is the filtered colimit of its finitely generated subsheaves. Proof: the canonical map colim → K is mono (by AB5 + mono transitions) and epi (since allSectionMap K factors through it), hence an isomorphism.

Equations

• finsetGenCoconeIsColimit hK = (CategoryTheory.Limits.colimit.isColimit (finsetGenFunctor hK)).ofPointIso

theorem cohomology_vanishing_of_finitelyGenerated_vanishing {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] {K : TopCat.Presheaf AddCommGrpCat X} (hK : K.IsSheaf) (m : ℕ) (hfg : ∀ (S : Finset K.SectionIndex) [inst : CategoryTheory.Limits.HasCoproduct fun (σ : ↥S) => TopCat.Sheaf.zeroOutsideInt (↑σ).fst], Subsingleton (CategoryTheory.Sheaf.H (TopCat.Presheaf.finsetGeneratedSheaf hK S) m)) : Subsingleton (CategoryTheory.Sheaf.H { obj := K, property := hK } m)

Hartshorne III, Ex. 2.9 core: on a Noetherian space, if H^m = 0 for all finitely generated subsheaves of K, then H^m(K) = 0. Uses the filtered-colimit comparison isomorphism for the diagram of finitely generated subsheaves and transports zero across it.

theorem finsetGeneratedSheaf_vanishing {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] {K : TopCat.Presheaf AddCommGrpCat X} (hK : K.IsSheaf) (m : ℕ) (hzero : ∀ {G : TopCat.Presheaf AddCommGrpCat X} (hG : G.IsSheaf) {V : TopologicalSpace.Opens ↑X} (f : (TopCat.Sheaf.zeroOutsideInt V).obj ⟶ G), TopCat.Presheaf.IsLocallySurjective f → Subsingleton (CategoryTheory.Sheaf.H { obj := G, property := hG } m)) (S : Finset K.SectionIndex) [CategoryTheory.Limits.HasCoproduct fun (σ : ↥S) => TopCat.Sheaf.zeroOutsideInt (↑σ).fst] : Subsingleton (CategoryTheory.Sheaf.H (TopCat.Presheaf.finsetGeneratedSheaf hK S) m)

Step 3B–3C: vanishing for finsetGeneratedSheaf S by Finset.induction.

theorem directLimit_cohomology_vanishing {X : TopCat} [TopologicalSpace.NoetherianSpace ↑X] {K : TopCat.Presheaf AddCommGrpCat X} (hK : K.IsSheaf) (m : ℕ) (hzero : ∀ {G : TopCat.Presheaf AddCommGrpCat X} (hG : G.IsSheaf) {V : TopologicalSpace.Opens ↑X} (f : (TopCat.Sheaf.zeroOutsideInt V).obj ⟶ G), TopCat.Presheaf.IsLocallySurjective f → Subsingleton (CategoryTheory.Sheaf.H { obj := G, property := hG } m)) : Subsingleton (CategoryTheory.Sheaf.H { obj := K, property := hK } m)

Step 3A (Hartshorne III.2.7): on a Noetherian space, if vanishing holds for all epi images of zeroOutsideInt V, then it holds for every sheaf. Assembles finsetGeneratedSheaf_vanishing (finite case) with cohomology_vanishing_of_finitelyGenerated_vanishing (colimit step).