reducedCellularCircleChainModelH1IsoInt
plain-language theorem explainer
The reduced cellular chain model of the circle has first homology isomorphic to ℤ as a ℤ-module. Algebraic topologists and anyone wiring the finite circle models into the H₁(S¹;ℤ)≅ℤ workbench cite this. The proof is a one-line wrapper: the model is definitionally the single-supported degree-1 integer complex, whose H₁ is already known to be ℤ.
Claim. The reduced cellular chain complex of the circle (one $\mathbb{Z}$ generator in degree $1$, zero elsewhere) satisfies $H_1 \cong \mathbb{Z}$ as $\mathbb{Z}$-modules.
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 TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to Mathlib 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 reduced cellular circle model is the finite chain complex with a single integer generator in degree 1 and zero elsewhere. It is an abbreviation for the single-supported integer complex in degree 1, not a topological replacement for the circle. Upstream, the degree-1 homology of that single-supported complex is already identified with the integer module via the standard single-object homology self-isomorphism.
proof idea
One-line wrapper. The reduced model is definitionally the single degree-1 integer complex, so the claim is exactly the upstream isomorphism that the homology in degree 1 of that complex is ModuleCat.of ℤ ℤ, obtained from HomologicalComplex.singleObjHomologySelfIso.
why it matters
This is the reduced-model half of the algebraic $H_1\cong\mathbb{Z}$ atom in the circle workbench. Downstream it feeds the comparison that the ordinary two-cell cellular circle model and the reduced model have the same first homology (an algebraic comparison independent of any claim about TopCat.sphere 1), and the proposition-facing nonempty-isomorphism form used as a citation surface. In the broader Recognition stack this sits under Foundation scaffolding toward T8 ($D=3$) and circle/octave geometry; the module doc is explicit that nothing here yet bridges to Mathlib singular homology or the strict T8 path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.