fundamentalHomologyClass_surjective
plain-language theorem explainer
Names the remaining generation half of the circle homology isomorphism: every class in first singular homology of the circle is an integer multiple of the fundamental class. Stated as surjectivity of the already-built comparison map from the integers into that homology module. Anyone closing H1(S1;Z) ≅ Z, or upgrading nonvanishing to the full iso, cites this Prop. Body is a one-line definition wrapping Function.Surjective on the underlying module map.
Claim. The proposition that the integer comparison morphism $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$, sending $n$ to $n$ times the fundamental circle class, is surjective: every degree-$1$ homology class is an integer multiple of that fundamental class.
background
The module builds a winding invariant on singular 1-simplices of the topological circle and proves it kills boundaries, so winding descends to a homology map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$. Combined with the once-around generator mapping to 1, this yields a left inverse to the fundamental class and the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The comparison morphism itself is the integer map $n\mapsto n\cdot[\mathrm{fundamental}]$: the fundamental singular 1-chain is a cycle, so it projects to a homology class. The winding homology map is the factorization of the winding chain map through degree-1 opcycles and then through homology.
Module doc is explicit that the converse generation half (every 1-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. Nonvanishing alone closes the T1–T8 frontier; surjectivity is the stronger upgrade to the full isomorphism.
proof idea
Definitional, not a proved theorem. The body is the single proposition Function.Surjective applied to the underlying additive map of the already-constructed comparison morphism from $\mathbb{Z}$ into first singular homology of the circle. No tactics, no lemmas discharged here; downstream results assume this Prop as a hypothesis and derive mono/epi/iso consequences from it together with the already-proved winding retraction identity.
why it matters
This is the exact remaining generation statement for the Mathlib target $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream, assuming it yields: bijectivity of the comparison map; a ModuleCat isomorphism $\mathbb{Z}\cong H_1$; the final handoff criterion that produces the circle homology iso; injectivity of the homology-level winding map (via the identity that comparison composed with winding is $n\mapsto n$); and closure of the zero-winding filling target.
Doc-comment is clear this is not required for strict T1–T8 frontier closure, which only needs nonvanishing. Surjectivity upgrades that nonvanishing to the full integer isomorphism and is the open Mathlib-facing generation half flagged in the module introduction (prism/subdivision gap).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.