ordinaryCellularCircleChainModelH1IsoReducedCellularH1
plain-language theorem explainer
The ordinary two-cell cellular chain model of the circle and the reduced one-cell model have isomorphic first homology. Algebraic comparisons of finite circle chain models cite this before any link to singular homology of S¹. The construction is a one-line composite of the two known isomorphisms from each H₁ onto ℤ.
Claim. There is a canonical isomorphism $H_1(C^{\mathrm{ord}}_\bullet)\cong H_1(C^{\mathrm{red}}_\bullet)$ between the degree-$1$ homology of the ordinary two-cell cellular chain model of the circle (one $\mathbb{Z}$ generator in degrees $0$ and $1$, zero differentials) and that of the reduced cellular model (one $\mathbb{Z}$ generator in degree $1$ only).
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It builds finite algebraic chain models and does not yet replace Mathlib's TopCat.sphere 1 or feed the strict T8 bridge.
The ordinary cellular circle model is the two-cell complex with chain groups $\mathbb{Z}$ in degrees $0$ and $1$, zero elsewhere, and all differentials zero. The reduced model is the single-degree complex with $\mathbb{Z}$ only in degree $1$. Upstream, each model already carries an explicit isomorphism of its first homology onto $\mathbb{Z}$ (as an object of ModuleCat ℤ).
The present definition compares those two algebraic models directly, without any topological claim about the circle.
proof idea
One-line wrapper. Compose the ordinary model's $H_1\cong\mathbb{Z}$ isomorphism with the inverse of the reduced model's $H_1\cong\mathbb{Z}$ isomorphism. Both target the same object ModuleCat.of ℤ ℤ, so the composite is an isomorphism $H_1(C^{\mathrm{ord}})\cong H_1(C^{\mathrm{red}})$ in degree $1$.
why it matters
Closes the algebraic comparison between the two finite circle chain models used in the $H_1(S^1;\mathbb{Z})$ workbench. Downstream it is wrapped as the proposition-facing Nonempty form of the same isomorphism, which is the form other developments can cite without carrying the concrete iso term.
In the Recognition framework this sits in the Foundation layer that must eventually support the eight-tick / $D=3$ forcing chain (T7–T8). The module doc is explicit that none of these finite models feed the strict T8 bridge until a real equivalence to Mathlib singular homology of the circle is proved. This definition is pure algebra on the chain models and keeps that topological gap honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.