singularHomologyFunctorSphereOneIntIsoOfQuasiIsoAtOrdinaryCellular
plain-language theorem explainer
A degree-1 quasi-isomorphism from Mathlib singular chains on S¹ to the ordinary two-cell cellular circle model yields H₁(S¹; ℤ) ≅ ℤ as the singularHomologyFunctor value. Anyone closing the circle homology bridge cites this packaging. The body is a two-step composite: homology of a quasi-iso at degree 1, then the model's known H₁ ≅ ℤ.
Claim. If $f$ is a chain map from the integer singular chain complex of $\mathrm{TopCat.sphere}\,1$ to the ordinary two-cell cellular circle model, and $f$ is a quasi-isomorphism in degree $1$, then $$H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\cong\mathbb{Z}$$ as objects of $\mathrm{ModuleCat}\,\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 replace Mathlib's sphere object and does not feed the strict T8 bridge until a real equivalence to the 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 model is the finite two-cell complex with one integer generator in degree 0, one in degree 1, no higher groups, and zero differential. Its first homology is already identified with $\mathbb{Z}$. The singular side is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with integer coefficients, the exact chain-level object whose degree-1 homology is the final strict target.
The remaining geometric content is isolated as a single hypothesis: a degree-1 quasi-isomorphism from that singular complex onto the ordinary cellular model.
proof idea
One-line composite of two isomorphisms. First apply the standard Mathlib fact that a quasi-isomorphism at degree 1 induces an isomorphism on homology in that degree (isoOfQuasiIsoAt f 1), sending singular $H_1$ to the ordinary model's $H_1$. Then compose with the already-constructed isomorphism ordinaryCellularCircleChainModelH1IsoInt, which identifies the model's first homology with $\mathbb{Z}$. No new homology computation occurs here.
why it matters
Packages the last algebraic step so that any future chain-level bridge (a degree-1 quasi-iso, or a full homotopy equivalence) immediately yields the singular homology target as $\mathbb{Z}$. Downstream, the homotopy-equivalence form applies this definition to the underlying map of a HomotopyEquiv, and the proposition-facing nonempty form wraps the same data as Nonempty of the iso.
In the Recognition forcing chain this sits under the circle $H_1$ work needed before a strict link to Mathlib singular homology can support T8 ($D=3$). The module doc is explicit: nothing here feeds the strict T8 bridge until that real equivalence exists. The declaration isolates the missing geometric theorem as the single remaining hypothesis QuasiIsoAt f 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.