singularHomologyFunctorSphereOneIntIsoOfHomotopyEquivOrdinaryCellularAtOne
plain-language theorem explainer
Given a chain homotopy equivalence between Mathlib's singular chains on the circle and the ordinary two-cell cellular model, degree-1 singular homology of S¹ with integer coefficients is isomorphic to ℤ. Anyone packaging the MathlibCohomologyBridge proposition for circle H₁ cites this atom. The construction is a two-step composite: the degree-1 homology iso induced by the homotopy equivalence, then the already-proved cellular H₁ ≅ ℤ.
Claim. If $e$ is a chain homotopy equivalence between the singular chain complex of $S^1$ (integer coefficients) and the ordinary two-cell cellular circle model, and the singular complex admits homology in degree $1$, then $H_1^{\mathrm{sing}}(S^1;\mathbb{Z}) \cong \mathbb{Z}$ as objects of $\mathbf{Mod}_{\mathbb{Z}}$.
background
This module is the local workbench for the missing computation $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not yet replace Mathlib's TopCat.sphere 1 object, and it does not feed the strict T8 bridge until a genuine equivalence to the imported singular homology is proved. The algebraic core already established is that a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The ordinary cellular circle model is the finite two-cell complex with one integer generator in degree 0, one in degree 1, vanishing higher groups, and zero differential. Its first homology is already identified with $\mathbb{Z}$. The singular side is Mathlib's singular chain complex of the topological 1-sphere with coefficients in $\mathbb{Z}$; that is the exact chain-level object whose degree-1 homology is the strict target.
The present definition sits between those two models: it assumes only a chain homotopy equivalence and the existence of degree-1 homology on the singular side, which is weaker than a global quasi-isomorphism hypothesis.
proof idea
One-line composite of two isomorphisms. First apply the degree-1 homology isomorphism induced by the given chain homotopy equivalence (the standard toHomologyIso at degree 1). Then right-compose with the already-constructed isomorphism identifying the ordinary cellular model's first homology with $\mathbb{Z}$. No further diagram chase or spectral-sequence argument is needed; the cellular $H_1\cong\mathbb{Z}$ atom does the algebraic work.
why it matters
This is the degree-local homotopy-equivalence bridge in the exact proposition shape expected by the Mathlib cohomology bridge. Downstream, it is wrapped into the named bridge proposition circleH1ZIsoInt (the form the rest of the stack consumes), and it supplies the witness for the nonempty-isomorphism theorem under a geometric bridge hypothesis.
In the Recognition forcing chain the circle computation is infrastructure toward the eight-tick octave and the $D=3$ step (T7–T8): a strict identification $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is the classical topological input those later bridges quote. The module itself is explicit that this atom does not yet close the strict T8 feed; it only packages the conditional isomorphism once a homotopy equivalence (or geometric bridge) is supplied. The open question remains existence of that equivalence to Mathlib's imported singular object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.