zeroWindingCycles_bound_of_fundamentalHomologyClass_surjective
plain-language theorem explainer
Surjectivity of the fundamental circle class on first homology implies every singular 1-cycle of winding zero is a 2-boundary. Anyone closing the filling half of the circle homology computation cites this bridge. The proof is a two-step term composition: generation yields injectivity of the winding map on homology, and monicity of that map forces zero-winding cycles into the image of the boundary.
Claim. If the comparison morphism sending $n\in\mathbb{Z}$ to $n$ times the fundamental class of $S^1$ is surjective on $H_1(S^1;\mathbb{Z})$, then every singular $1$-cycle $z$ with winding number zero is the boundary of some singular $2$-chain.
background
The module lifts path-level winding on the circle to singular $1$-simplices of $S^1$ and proves that displacement kills boundaries: the alternating face sum of any $2$-simplex has vanishing displacement. Combined with the fact that the fundamental loop has winding $1$, this yields a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The remaining generation half is packaged as surjectivity of the fundamental homology class map: every degree-$1$ class is an integer multiple of the fundamental circle class. Separately, the zero-winding filling target asserts that every singular $1$-cycle of winding zero is a singular $2$-boundary. An intermediate lemma records that monicity of the homology-level winding map already closes that filling target, because zero winding forces the homology class to vanish and monicity then forces the cycle class itself to be zero (hence a boundary).
proof idea
One-line term wrapper. First apply the lemma that surjectivity of the fundamental class map implies the winding map on homology is monic (using the already-proved identity that the composite of fundamental class followed by winding is the identity on $\mathbb{Z}$). Then feed that monicity into the lemma that a monic winding map closes the zero-winding filling target.
why it matters
This sits in the CircleWindingChain foundation layer that builds the winding invariant as a homology-level left inverse to the fundamental class of $S^1$. The module doc notes that the split-injective half is already in hand; surjectivity (generation) is the remaining half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, and is not required for the strict T0–T8 frontier closure (which only needs nonvanishing).
Downstream, the sibling theorem that generation by the fundamental cycle class closes the filling target routes through this result after converting cycle-class generation into homology-class surjectivity. The filling target itself is the geometric subgoal that subdivision or prism machinery would supply directly; this declaration shows that homology generation is an equivalent route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.