circleH1ZIsoIntOfGeometricBridge
plain-language theorem explainer
Assuming a chain-homotopy equivalence between Mathlib's singular chains on S¹ and the ordinary two-cell cellular circle model, the first singular homology is isomorphic to ℤ as a ℤ-module. Cited by anyone closing the Mathlib H₁ certificate for the strict T8 handoff. Proof unpacks the nonempty bridge and applies the degree-local homotopy-equivalence lemma.
Claim. If Mathlib's singular chain complex of $S^1$ is chain-homotopy equivalent to the ordinary two-cell cellular circle model, then $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules (nonempty isomorphism in $\mathrm{ModuleCat}$).
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 object and does not feed the strict T8 bridge until a real equivalence to the imported singular homology 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. The target certificate circleH1ZIsoInt is the strong Mathlib closure proposition: nonempty isomorphism of the circle's first singular homology with the integer module.
Upstream, the degree-local lemma already converts any concrete such homotopy equivalence (with homology at degree 1) into that exact certificate shape used by the Mathlib cohomology bridge.
proof idea
One-line unpack-and-apply. The hypothesis is a Nonempty of a chain homotopy equivalence; rcases extracts a witness e. The conclusion is then exactly circleH1ZIsoIntOfHomotopyEquivOrdinaryCellularAtOne e, which packages the singular-homology functor isomorphism induced by that equivalence into the Mathlib bridge certificate.
why it matters
Closes the exact proposition shape demanded by the Mathlib cohomology bridge once the geometric chain-level bridge is assumed. Downstream, circleH1MathlibComputationOfGeometricBridge turns this into the Mathlib computation certificate used by the strict T8 handoff, and mathlibCircleLinkingBackendOfGeometricBridge builds the circle-linking backend from the same iso.
In the Recognition forcing chain, T8 forces $D=3$ spatial dimensions; the circle $H_1$ computation is part of the topological bookkeeping that the T8 handoff imports rather than re-proves. The geometric bridge itself remains the open geometric atom; this theorem is the pure logical glue from that atom to the imported certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.