circleH1ZIsoIntOfHomotopyEquivOrdinaryCellular
plain-language theorem explainer
Given a chain-level homotopy equivalence from the integer singular chains of the circle to the ordinary two-cell cellular model, the first singular homology of S¹ is isomorphic to ℤ. Anyone packaging the Mathlib cohomology-bridge certificate for the circle cites this form. The proof is a one-line wrapper that feeds the underlying chain map of the homotopy equivalence into the quasi-isomorphism bridge.
Claim. If $e$ is a homotopy equivalence of chain complexes from the integer singular chain complex of $S^1$ to the ordinary cellular circle model ($\mathbb{Z}$ in degrees $0$ and $1$, zero differentials), and that singular complex has homology in every degree, then there is a nonempty isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
background
This module is the local Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not replace Mathlib's topological circle and does not feed the strict T8 bridge until a real equivalence to Mathlib's imported singular homology object 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 chain model is the finite algebraic complex with one integer generator in degree 0, one in degree 1, no higher groups, and zero boundary. It remains an algebraic model until a later theorem connects it to Mathlib's topological circle. The singular side is Mathlib's singular chain complex of that circle with integer coefficients: the exact chain-level object whose degree-1 homology is the final strict T8 target.
Upstream, the bridge certificate is the proposition that the circle's first singular homology is nonempty-isomorphic to the integer module. The quasi-iso form of the bridge already reduces that certificate to a degree-1 quasi-isomorphism into the ordinary cellular model, leaving the bridge file untouched until the comparison is unconditional.
proof idea
One-line term wrapper. A homotopy equivalence of chain complexes supplies a quasi-isomorphism via its underlying morphism, so the proof applies the quasi-iso bridge at the ordinary cellular model to that morphism. That upstream theorem routes through the singular-homology functor comparison at degree 1 against the ordinary cellular model and discharges the bridge proposition asserting a nonempty isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
why it matters
The declaration restates the homotopy-equivalence hypothesis in the exact proposition shape expected by the Mathlib cohomology bridge, so the bridge file can stay untouched until an unconditional chain-level comparison exists. Module docs are explicit that this workbench does not yet feed the strict T8 bridge (the forcing-chain step that pins $D=3$ spatial dimensions) until a real equivalence to Mathlib's imported singular homology object is proved.
No downstream consumers are wired yet. The result is the homotopy-equivalence entry point for the missing pinned-Mathlib computation of $H_1(S^1;\mathbb{Z})$, which the bridge intends to import from Mathlib rather than replace with a project-local substitute. Closing an unconditional homotopy equivalence (or quasi-iso) from the singular complex to the ordinary cellular model would discharge the certificate without further local scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.