Registry · Theorem II.T55 tau-effective formalized

II.T55 — H⁰ = Global Sections

H⁰ equals the space of global sections. For the constant sheaf, a 0-cochain is a global section iff it is constant. Non-constant functions have nonzero coboundary.

Book II Part 9 Ch. 50

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookII.CentralTheorem.SheafCohomology

Symbol: h0_global_2