fundamentalHomologyClass_surjective_of_cycleClass_generates
plain-language theorem explainer
If every singular 1-cycle on S¹ is homologous to an integer multiple of the once-around fundamental cycle, then the comparison map ℤ → H₁(S¹;ℤ) sending 1 to that fundamental class is surjective. Anyone closing the Mathlib isomorphism H₁(S¹;ℤ) ≅ ℤ from the geometric generation hypothesis cites this bridge. The proof lifts an arbitrary homology class to a cycle via epi of homologyπ, then applies the generation hypothesis.
Claim. Assume every degree-$1$ singular cycle $z$ on $S^1$ satisfies $[z] = n\,[\gamma]$ in $H_1(S^1;\mathbb{Z})$ for some $n\in\mathbb{Z}$, where $\gamma$ is the once-around fundamental cycle. Then the induced map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$, $n\mapsto n\,[\gamma]$, is surjective.
background
The module builds a winding/displacement invariant on singular 1-simplices of TopCat.sphere 1 and proves it kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The remaining half is generation: every 1-cycle is homologous to an integer multiple of the fundamental cycle.
Two Props package the two formulations. Cycle-class generation says every cycle representative $z$ has the same homology class as some integer multiple of the fundamental cycle. Homology-class surjectivity says the already-built comparison morphism from $\mathbb{Z}$ (sending $1$ to the fundamental class) hits every class in degree-1 homology of the Mathlib singular chain complex of $S^1$ with integer coefficients.
Mathlib's homologyπ is always an epimorphism of modules, so every homology class has some cycle representative. That fact turns the cycle-level generation statement into the homology-level surjectivity statement.
proof idea
Term/tactic hybrid, four steps. Fix an arbitrary degree-1 homology class $y$. Because homologyπ is epi in ModuleCat ℤ, it is surjective on underlying maps; pick a cycle representative $z$ with $\pi(z)=y$. Apply the generation hypothesis to $z$ to obtain an integer $n$ such that $\pi(z)$ equals the image of $n$ under the fundamental homology class map. Rewrite via $\pi(z)=y$ to conclude $y$ is hit. No geometric content: pure diagram chase from epi of homology projection plus the cycle-generation Prop.
why it matters
This is the formal hinge between the geometric missing theorem (every cycle bounds after subtracting its winding multiple of the fundamental cycle) and the homology-level surjectivity Prop that finishes $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ in Mathlib. Downstream, circleH1ZIsoInt_of_fundamentalCycleClass_generates composes this bridge with the already-proved injective half to obtain the full integer isomorphism from cycle-class generation alone; zeroWindingCycles_bound_of_fundamentalCycleClass_generates likewise closes the zero-winding filling target.
In the Recognition forcing chain the degree-1 singular homology of $S^1$ is the strict T8 target object (three spatial dimensions forced via the eight-tick octave and circle homology). Nonvanishing alone already closes the T-1-to-T8 frontier; full generation/surjectivity is the stronger Mathlib-native isomorphism, still open geometrically (needs a simplicial prism/subdivision operator Mathlib does not yet supply). This lemma isolates that remaining geometric obligation as a single Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.