fundamentalCycleClass_generates_of_boundary_generates
plain-language theorem explainer
If every singular 1-cycle on S¹ is a 2-boundary plus an integer multiple of the fundamental cycle, then every 1-homology class equals that same multiple of the fundamental class. Anyone closing H₁(S¹;ℤ) ≅ ℤ from a concrete chain-level generation hypothesis cites this bridge. The proof pushes the decomposition through homologyπ; the toCycles summand vanishes, leaving only the fundamental class term.
Claim. Assume every degree-$1$ singular cycle $z$ on $S^1$ decomposes in the cycle module as $z = \partial_2 b + n\cdot\gamma$, where $\gamma$ is the fundamental once-around cycle and $n\in\mathbb{Z}$. Then for every such $z$ there exists $n\in\mathbb{Z}$ with $[z] = n\cdot[\gamma]$ in $H_1(S^1;\mathbb{Z})$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries of $2$-simplices. That identity supplies the retraction half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding sends the fundamental loop to $1$ and vanishes on boundaries.
The remaining half is generation: every $1$-cycle should be homologous to an integer multiple of the fundamental cycle. Two Prop-shaped statements package this. The stronger chain-level form asserts a concrete witness $b\in C_2(S^1;\mathbb{Z})$ and $n\in\mathbb{Z}$ with $z=\mathrm{toCycles}(b)+n\cdot\gamma$ inside cycles. The weaker class-level form only asks $[z]=n\cdot[\gamma]$ after projecting by $\mathrm{homology}\pi$.
The integer comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ is $n\mapsto n\cdot[\gamma]$, built by lifting the fundamental singular $1$-chain to cycles and composing with $\mathrm{homology}\pi$. The ambient complex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with $\mathbb{Z}$ coefficients.
proof idea
Term/tactic hybrid, not a bare wrapper. Introduce an arbitrary cycle $z$. From the boundary-generation hypothesis obtain $n$ and a $2$-chain $b$ with $z=\mathrm{toCycles}_{2,1}(b)+n\cdot\gamma$. Project both sides by $\mathrm{homology}\pi_1$ and use additivity of the hom. The composite $\mathrm{toCycles}\circ\mathrm{homology}\pi$ is zero by the standard chain-complex identity, so the $b$ term drops. The remaining term is exactly the definition of the fundamental homology class applied to $n$. A short simp on that definition finishes.
why it matters
This is the formal step that turns a geometric chain-level filling statement into the homology-class generation Prop needed for the integer comparison map to be surjective. Downstream, circleH1ZIsoInt_of_fundamentalCycle_boundary_generates composes it with the class-level iso constructor to obtain the final Mathlib $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ closure from the single hypothesis that boundaries generate the remainder.
In the Recognition forcing chain, a strict computation of $H_1(S^1;\mathbb{Z})$ anchors the circle/winding side of the foundation (the same circle that carries the eight-tick octave and the $D=3$ forcing arguments). The module doc is explicit that Mathlib still lacks the simplicial prism/subdivision operator that would discharge the boundary-generation hypothesis itself; this lemma isolates that remaining geometric debt so the algebraic half of the iso is already closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.