Registry · Proposition II.P20 tau-effective formalized

II.P20 — Čech-to-Derived Comparison

Čech cohomology agrees with derived functor cohomology on the primorial tower. The cylinder cover is acyclic (ultrametric: intersections are empty or cylinders).

Book II Part 9 Ch. 50

Dependency Graph

Depends on (3)

Lean Formalization

Module: TauLib.BookII.CentralTheorem.SheafCohomology

Symbol: cech_derived_2