ordinaryCellularCircleChainModelH1IsoInt
plain-language theorem explainer
The ordinary two-cell cellular chain model of the circle has first homology isomorphic to ℤ as a ℤ-module. Anyone assembling the algebraic core of H₁(S¹; ℤ) ≅ ℤ via finite chain models cites this isomorphism. The proof is a two-step composite: homology equals cycles because the incoming differential vanishes, then cycles in degree 1 are identified with ℤ.
Claim. Let $C_\bullet$ be the ordinary two-cell cellular chain model of the circle (one $\mathbb{Z}$ generator in degree $0$, one in degree $1$, vanishing elsewhere, all differentials zero). Then there is a canonical isomorphism $H_1(C_\bullet) \cong \mathbb{Z}$ in the category of $\mathbb{Z}$-modules.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace Mathlib's TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to 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 finite complex with $C_0\cong\mathbb{Z}$, $C_1\cong\mathbb{Z}$, $C_n=0$ for $n\ge 2$, and every differential identically zero. Upstream, all differentials are proved zero by reflexivity, and the degree-1 cycles are therefore the whole degree-1 chain group, hence isomorphic to $\mathbb{Z}$.
proof idea
Two-step composite of isomorphisms. First apply the standard identification of homology with cycles when the incoming differential vanishes: isoHomologyπ at degrees $(2,1)$, using that $d_{2,1}=0$ (from the zero-differential theorem) and a trivial numeric side condition. Take the inverse of that iso, then compose with the already-built isomorphism from degree-1 cycles onto $\mathbb{Z}$. No further computation is needed; boundaries out of degree 1 are zero by construction of the model.
why it matters
This is the algebraic $H_1\cong\mathbb{Z}$ atom for the ordinary two-cell model. Downstream it feeds the comparison isomorphism between ordinary and reduced cellular models (same first homology, purely algebraic), the proposition-facing nonempty form of the same iso, and both singular-homology bridge constructors: one via a degree-1 quasi-isomorphism from Mathlib singular chains on the sphere, and one via a chain homotopy equivalence. Those bridges isolate the remaining geometric gap as a single chain-level hypothesis (QuasiIsoAt f 1 or a homotopy equivalence), after which the singular functor target is exactly $\mathbb{Z}$. In the Recognition stack this sits under the Circle $H_1$ workbench that must eventually support the T8 spatial-dimension forcing, but only after the topological bridge is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.