circleH1ZIsoIntOfNonemptyHomotopyEquivOrdinaryCellularAtOne
plain-language theorem explainer
Given only that Mathlib's singular chains on S¹ are chain-homotopy equivalent to the ordinary two-cell cellular circle model, the first singular homology is isomorphic to ℤ. Anyone closing the strict T8 circle-H₁ bridge cites this as the proposition-shaped target: produce the equivalence, obtain H₁(S¹; ℤ) ≅ ℤ. The proof unpacks Nonempty and applies the explicit-equivalence form.
Claim. If there exists a chain homotopy equivalence between the integer singular chain complex of $S^1$ and the ordinary two-cell cellular circle model (one $\mathbb{Z}$ generator in degrees $0$ and $1$, zero differentials), and degree-$1$ homology of the singular complex exists, then $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ as $\mathbb{Z}$-modules.
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 Mathlib's 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 one integer generator in degree $0$, one in degree $1$, no higher groups, and zero boundary. 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 first singular homology of the circle is nonempty-isomorphic to the integer module. The sibling theorem with an explicit homotopy equivalence already packages that certificate from a concrete equivalence; this declaration only weakens the hypothesis to existence.
proof idea
One-line unpacking wrapper. Destruct the Nonempty hypothesis to obtain an explicit chain homotopy equivalence $e$, then apply circleH1ZIsoIntOfHomotopyEquivOrdinaryCellularAtOne e. That upstream result builds the certificate as the singleton of the singular-homology isomorphism induced by the equivalence at degree $1$. No new algebraic work occurs here.
why it matters
This is the proposition-facing closure target for the geometric half of the circle-$H_1$ computation: "it is enough to produce a chain homotopy equivalence between Mathlib's singular chains on $S^1$ and the ordinary cellular circle model." Downstream of that geometric bridge sits the strict T8 circle-$H_1$ closure (forcing chain landmark T8: $D=3$ spatial dimensions, with the circle as the one-dimensional skeleton of the octave geometry).
The remaining open step, recorded in the module, is exactly that geometric chain-level bridge: prove Mathlib's singular complex for $S^1$ is chain-homotopy equivalent to the ordinary two-cell model. Once that equivalence is inhabited, this theorem discharges the Mathlib cohomology bridge certificate without further work. No parent theorems currently consume it (used_by is empty); it is the handoff surface for the missing geometric proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.