Registry · Definition II.D86 tau-effective formalized

II.D86 — Čech Complex

Čech complex for the cylinder cover of Z/M_k Z. Coboundary δ⁰(f)(a,b) = f(b) - f(a). Satisfies δ² = 0 (alternating sum identity).

Book II Part 9 Ch. 50

Dependency Graph

Depends on (2)

II.D84 II.D47

Depended on by (2)

II.D87 II.P20

Lean Formalization

Module: TauLib.BookII.CentralTheorem.SheafCohomology

Symbol: cech_coboundary_0