ordinaryCellularCircleChainModel_d_eq_zero
plain-language theorem explainer
All differentials of the ordinary two-cell cellular chain model of the circle are zero. Anyone computing first homology of this finite algebraic model cites the fact to equate degree-1 cycles with the full degree-1 chain group. The proof is definitional reflexivity: the model is built with zero boundary maps.
Claim. For all natural numbers $i,j$, the differential $d_{i,j}$ of the ordinary cellular chain complex of the circle (one $\mathbb{Z}$ generator in degree $0$, one in degree $1$, and zero elsewhere) is the zero map.
background
This module is a Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace Mathlib's sphere object and does not feed the strict T8 bridge until a real equivalence to imported singular homology is proved. The first proved atom is algebraic: a chain complex supported by $\mathbb{Z}$ in degree $1$ has degree-$1$ homology $\mathbb{Z}$.
The ordinary cellular circle model is the two-cell complex with chain groups $\mathbb{Z}$ in degrees $0$ and $1$, zero elsewhere, and every boundary map set to zero by construction. It is an algebraic finite-chain stand-in for a CW structure on the circle (one $0$-cell, one $1$-cell) until a later theorem connects it to Mathlib's TopCat.sphere 1.
proof idea
One-line reflexivity. The ordinary cellular circle model is defined with every differential equal to the zero morphism, so $d_{i,j}=0$ holds by rfl for all degrees $i,j$.
why it matters
Zero differentials are the algebraic hinge for the ordinary model's first homology. Downstream, they identify degree-$1$ cycles with the whole degree-$1$ chain group $\mathbb{Z}$, and then yield $H_1\cong\mathbb{Z}$ for the ordinary model. The same fact builds the collapse chain map onto the reduced degree-$1$ model and proves that collapse is a quasi-isomorphism in degree $1$, via Mathlib's zero-differential short-complex criterion. The reverse inclusion map from the reduced model also relies on it. All of this stays internal to the algebraic workbench; the module explicitly withholds any claim on Mathlib singular homology or the T8 bridge until a real equivalence is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.