singularHomologyFunctorSphereOneIntNonemptyIsoOfGeometricBridge
plain-language theorem explainer
Under the geometric bridge (Mathlib singular chains on the circle chain-homotopy equivalent to the ordinary cellular circle model), degree-1 singular homology of S¹ with integer coefficients is isomorphic to ℤ as ℤ-modules. Anyone closing the strict T8 circle-H₁ step or feeding MathlibCohomologyBridge would cite this. The proof unpacks the Nonempty homotopy equivalence and applies the degree-local homology isomorphism built from that equivalence.
Claim. Assume Mathlib's singular chain complex on $S^1$ is chain homotopy equivalent to the ordinary two-cell cellular circle model. Then there exists an isomorphism of $\mathbb{Z}$-modules $H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\cong\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 TopCat.sphere 1 and does not feed the strict T8 bridge until a real equivalence to the imported singular homology object is proved. The algebraic core already shows that a chain complex supported by $\mathbb{Z}$ in degree 1 has degree-1 homology $\mathbb{Z}$.
The geometric bridge is the remaining chain-level hypothesis: Mathlib's singular chain complex for the circle is chain homotopy equivalent to the ordinary two-cell cellular circle model. A companion construction turns any such homotopy equivalence (with degree-1 homology available) into an explicit isomorphism from the imported singular-$H_1$ functor value on the circle to $\mathbb{Z}$, by composing the induced homology iso in degree 1 with the cellular model's $H_1\cong\mathbb{Z}$.
proof idea
Term-mode one-liner after unpacking. The hypothesis is a Nonempty of a chain homotopy equivalence between the singular and ordinary cellular circle complexes. Destructure that witness, then wrap the existing degree-local map that sends a homotopy equivalence to the composite isomorphism
e.toHomologyIso 1 ≪≫ ordinaryCellularCircleChainModelH1IsoInt
as a Nonempty inhabitant of the target iso type. No new algebraic work is done here; the theorem only packages the bridge Prop into the exact Nonempty-iso shape expected downstream.
why it matters
Closes the exact imported Mathlib singular-$H_1$ object as $\mathbb{Z}$ once the geometric bridge is assumed. The module doc states this workbench is aimed at the missing $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ atom needed before a real equivalence can feed the strict T8 bridge (T8 forces $D=3$ spatial dimensions in the forcing chain). The following doc-comment notes that the geometric bridge immediately closes the exact proposition used by MathlibCohomologyBridge.
No downstream consumers are wired yet (used_by is empty), so this is a terminal packaging lemma inside the circle-$H_1$ workbench: it converts the Prop-shaped bridge into the Nonempty-iso form that cohomology-bridge glue expects. The open obligation remains proving the bridge itself (homotopy equivalence of singular vs ordinary cellular chains on the circle).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.