circleH1GeometricBridge
plain-language theorem explainer
Names the remaining geometric bridge for strict T8 circle-H1: Mathlib's singular integer chain complex of the topological circle is chain-homotopy equivalent to the ordinary two-cell cellular model. Anyone closing H₁(S¹; ℤ) ≅ ℤ against the imported singular object cites this proposition. It is a bare Prop packaging Nonempty of that homotopy equivalence; no proof is supplied here.
Claim. The geometric bridge asserts that there exists a chain homotopy equivalence between the singular integer chain complex of the topological 1-sphere and the ordinary two-cell cellular chain model of the circle (one $\mathbb{Z}$ generator in degree $0$, one in degree $1$, zero differentials).
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 ordinary cellular circle model is the finite complex with $\mathbb{Z}$ in degrees 0 and 1, zero elsewhere, and zero boundary maps. The singular side is Mathlib's singular chain complex of the topological 1-sphere with integer coefficients: the exact chain-level object whose degree-1 homology is the final strict T8 target. The bridge is the missing geometric identification between those two complexes.
proof idea
Definitional packaging only: the proposition is exactly the statement that the type of chain homotopy equivalences from the singular integer complex of the 1-sphere to the ordinary cellular circle model is nonempty. No tactics, no lemmas applied, no construction of the equivalence. Downstream theorems unpack a witness and transport homology isomorphisms along it.
why it matters
This is the remaining geometric chain-level bridge for strict T8 circle-H1 closure (T8 forces $D=3$ spatial dimensions; the circle computation is the 1-dimensional homology atom in that handoff). Four immediate parents consume it: the theorem that produces a nonempty isomorphism of the imported singular $H_1$ to $\mathbb{Z}$; the theorem that closes the exact circleH1ZIsoInt proposition used by the Mathlib cohomology bridge; the certificate filler circleH1MathlibComputationOfGeometricBridge for the strict T8 handoff; and the builder of the Mathlib circle-linking backend. Until a witness is supplied, the workbench stays off the strict T8 path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.