circleH1ZIsoIntOfHomotopyEquivOrdinaryCellularAtOne
plain-language theorem explainer
A chain homotopy equivalence from Mathlib's singular chains on S¹ to the ordinary two-cell cellular circle model yields the certificate that H₁(S¹; ℤ) ≅ ℤ. Anyone closing the MathlibCohomologyBridge import interface cites this. The proof is a one-line term that packages the degree-1 homology isomorphism induced by the homotopy equivalence into the Nonempty witness.
Claim. If $e$ is a chain homotopy equivalence between the singular chain complex of $S^1$ with $\mathbb{Z}$ coefficients and the ordinary cellular circle chain model (one $\mathbb{Z}$ generator in degree $0$, one in degree $1$, zero differentials), and the singular complex has homology in degree $1$, then $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules (nonemptiness of that isomorphism).
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 known is that 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 complex with $X_0\cong\mathbb{Z}$, $X_1\cong\mathbb{Z}$, all other degrees zero, and zero boundary maps. The singular side is Mathlib's singular chain complex of $S^1$ with integer coefficients: the exact chain-level object whose degree-$1$ homology is the final strict T8 target.
The bridge certificate circleH1ZIsoInt is the proposition that the Mathlib singular homology object in degree $1$ is isomorphic to $\mathrm{ModuleCat},\mathbb{Z},\mathbb{Z}$. Upstream, a degree-local homotopy equivalence already induces an explicit isomorphism of that homology group with $\mathbb{Z}$ via composition with the cellular model's $H_1\cong\mathbb{Z}$.
proof idea
One-line term proof. Apply the upstream construction that turns a chain homotopy equivalence $e$ between the singular complex and the ordinary cellular model into a degree-$1$ homology isomorphism
$$H_1^{\mathrm{sing}}(S^1;\mathbb{Z})\cong H_1(\text{cellular model})\cong\mathbb{Z},$$
using $e.toHomologyIso,1$ composed with the cellular $H_1\cong\mathbb{Z}$ iso. Package that isomorphism as a Nonempty witness for the bridge proposition. The instance that the singular complex has homology in degree $1$ is required so the homology functor is defined at that degree.
why it matters
This is the exact proposition-shaped closure step used by MathlibCohomologyBridge: once a homotopy equivalence to the ordinary cellular model exists, the certificate $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ is immediate. Downstream, the geometric-bridge theorem reduces to this by unpacking a geometric bridge into such an $e$, and the Nonempty-homotopy-equivalence variant is the same unpacking for a mere existence hypothesis.
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions and relies on circle/sphere homology facts in the topological backbone. The module doc is explicit that this workbench does not yet feed the strict T8 bridge; the remaining open step is to produce the actual homotopy equivalence (or geometric bridge) connecting Mathlib's singular chains on $S^1$ to the ordinary cellular model. This theorem is the thin logical hinge that turns that geometric input into the import-interface certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.