circleH1ZIsoInt_of_fundamentalHomologyClass_surjective
plain-language theorem explainer
Assuming the fundamental class generates first singular homology of the circle, one obtains the Mathlib-facing certificate that H₁(S¹;ℤ) ≅ ℤ. Anyone closing the circle homology computation against Mathlib cites this handoff. The proof is a one-line term that symmetrizes the already-built comparison isomorphism under the surjectivity hypothesis.
Claim. If the comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$, $n\mapsto n\cdot[\gamma_{\mathrm{fund}}]$, is surjective on first singular homology, then there exists an isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in the category of $\mathbb{Z}$-modules.
background
This module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that displacement kills boundaries, so winding descends to a homology invariant. Combined with the fact that the once-around loop has winding $1$, one obtains a retraction of the integer comparison map: the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The comparison morphism itself is the map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ sending $n$ to $n$ times the homology class of the fundamental singular $1$-cycle. Surjectivity of that map is the remaining generation statement: every degree-$1$ class is an integer multiple of the fundamental class.
Upstream, if that surjectivity holds then the comparison is both mono (from the winding retraction) and epi, hence an isomorphism in ModuleCat because modules are balanced. The target certificate circleH1ZIsoInt is simply the proposition that $H_1(S^1;\mathbb{Z})$ is isomorphic to $\mathbb{Z}$ as a $\mathbb{Z}$-module.
proof idea
One-line term wrapper. Apply fundamentalHomologyClassIso_of_surjective to the given surjectivity hypothesis to obtain an isomorphism $\mathbb{Z}\cong H_1(S^1;\mathbb{Z})$ in ModuleCat, take its inverse, and package the resulting isomorphism as a witness of Nonempty for the Mathlib bridge proposition circleH1ZIsoInt.
why it matters
Doc-comment calls this the final handoff criterion for the remaining Mathlib element: the exact target $H_1(\mathrm{TopCat.sphere},1;\mathbb{Z})\cong\mathbb{Z}$ follows from the single still-open generation theorem that the fundamental class is surjective on first homology.
Downstream, circleH1ZIsoInt_of_fundamentalCycleClass_generates reduces the more geometric cycle-representative generation statement to this theorem via a surjectivity transfer lemma. That parent is described as the exact next theorem to prove geometrically.
In the broader Recognition chain this is infrastructure for identifying circle homology with $\mathbb{Z}$, not a T0–T8 forcing step. The module notes that nonvanishing alone already closes the strict T-frontier; full generation (and thus this iso certificate) is the stronger Mathlib-facing closure still open at the geometric level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.