singularHomologyFunctorSphereOneIntIsoOfHomotopyEquivOrdinaryCellular
plain-language theorem explainer
A chain homotopy equivalence from Mathlib's singular chains on the circle to the ordinary two-cell cellular model yields an isomorphism of first singular homology with integer coefficients to ℤ. Anyone packaging the strict H₁(S¹; ℤ) ≅ ℤ atom for the foundation bridge would cite this form. It is a one-line wrapper that feeds the forward map of the homotopy equivalence into the quasi-isomorphism version of the same bridge.
Claim. Given a chain homotopy equivalence $e$ between the singular chain complex of $S^1$ with coefficients in $\mathbb{Z}$ and the ordinary cellular circle model (one $\mathbb{Z}$ generator in degrees $0$ and $1$, vanishing differentials), and assuming that singular complex has homology in every degree, there is a canonical isomorphism $H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\cong\mathbb{Z}$ in $\mathbb{Z}$-modules.
background
This module is the local Mathlib-style workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Per the module doc, it does not replace the imported sphere object and does not feed the strict T8 bridge until a real equivalence to Mathlib's 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 $\mathbb{Z}$ in degrees $0$ and $1$, zero elsewhere, and zero boundary maps. The singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients is the exact chain-level object whose degree-$1$ homology is the final strict T8 target.
Upstream, a degree-$1$ quasi-isomorphism from those singular chains to the cellular model already computes the singular-homology functor target as $\mathbb{Z}$, isolating the remaining bridge as $\mathrm{QuasiIsoAt},f,1$. The present definition packages the stronger geometric input of a full homotopy equivalence.
proof idea
One-line wrapper. Extract the forward chain map of the given homotopy equivalence and pass it to the upstream quasi-isomorphism bridge. Homotopy equivalences induce quasi-isomorphisms in every degree, so the degree-$1$ quasi-iso hypothesis is available on that forward map; the upstream definition then composes the homology isomorphism at degree $1$ with the algebraic identification of the cellular model's $H_1$ with $\mathbb{Z}$.
why it matters
This packaging sits in the Circle $H_1$ workbench that prepares the missing $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ atom for the Recognition Science foundation. The module is explicit that nothing here feeds the strict T8 bridge (the D = 3 step of the forcing chain) until a genuine equivalence to Mathlib's imported singular homology object is proved.
No downstream consumers are wired yet. The definition isolates the geometric hypothesis as a homotopy equivalence rather than a bare quasi-isomorphism, matching the exact proposition shape used by the Mathlib cohomology bridge. It is interface packaging for a future geometric theorem, not that theorem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.