Grothendieck's vanishing theorem

Grothendieck's vanishing theorem (Hartshorne III.2.7): for a Noetherian topological space X of dimension n and any sheaf F of abelian groups on X, Hⁱ(X, F) = 0 for all i > n.

Main results

• GrothendieckVanishing — the headline theorem.
• reducible_vanishing — reduction to the irreducible case.
• grothendieck_vanishing_of_irreducible — the irreducible-case wrapper that performs the base-case split between dim X = 0 and dim X > 0.

The dimension-zero base case is proved here; the positive-dimensional irreducible step lives in IrreducibleStep.lean.

Reduction to irreducible spaces

theorem reducible_vanishing (X : TopCat) [TopologicalSpace.NoetherianSpace ↑X] (n : ℕ) (hn : ↑n > topologicalKrullDim ↑X) (F : TopCat.Sheaf AddCommGrpCat X) : ¬IrreducibleSpace ↑X → ∀ [Nonempty ↑X] (ih_irred : ∀ (Y : TopCat) [TopologicalSpace.NoetherianSpace ↑Y] [IrreducibleSpace ↑Y] (G : TopCat.Sheaf AddCommGrpCat Y), topologicalKrullDim ↑Y ≤ topologicalKrullDim ↑X → ↑n > topologicalKrullDim ↑Y → Subsingleton (CategoryTheory.Sheaf.H G n)), Subsingleton (CategoryTheory.Sheaf.H F n)

theorem grothendieck_vanishing_of_irreducible (X : TopCat) [TopologicalSpace.NoetherianSpace ↑X] (n : ℕ) (hn : ↑n > topologicalKrullDim ↑X) (F : TopCat.Sheaf AddCommGrpCat X) (ih_irred : ∀ (Y : TopCat) [TopologicalSpace.NoetherianSpace ↑Y] [IrreducibleSpace ↑Y] (m : ℕ) (G : TopCat.Sheaf AddCommGrpCat Y), topologicalKrullDim ↑Y ≤ topologicalKrullDim ↑X → ↑m > topologicalKrullDim ↑Y → Subsingleton (CategoryTheory.Sheaf.H G m)) : Subsingleton (CategoryTheory.Sheaf.H F n)

Main theorem

theorem GrothendieckVanishing (X : TopCat) [TopologicalSpace.NoetherianSpace ↑X] (n : ℕ) (h : ↑n > topologicalKrullDim ↑X) (F : TopCat.Sheaf AddCommGrpCat X) : Subsingleton (CategoryTheory.Sheaf.H F n)

Grothendieck's vanishing theorem (Hartshorne III, Theorem 2.7).