windingHomologyMap_mono_of_zeroWindingCycles_homologyClass_zero
plain-language theorem explainer
Assuming every zero-winding singular 1-cycle on the circle is homologous to zero, the descended winding map on first homology is injective as a ℤ-module map. Cite this when closing the mono half of the winding comparison H₁(S¹;ℤ) → ℝ. The proof lifts two homology classes to cycles via the homology projection, subtracts, and feeds the zero-winding hypothesis through the commuting diagram with cycle winding.
Claim. If every singular $1$-cycle $z$ on $S^1$ with winding number zero represents the zero class in $H_1(S^1;\mathbb{Z})$, then the winding homomorphism $H_1(S^1;\mathbb{Z})\to\mathbb{R}$ is a monomorphism of $\mathbb{Z}$-modules.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$ and proves that winding kills boundaries: the alternating face sum of displacements on any singular $2$-simplex vanishes by a convex-simplex homotopy argument. That identity lets the winding chain map factor through opcycles and descend to a homology-level map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$.
Cycle winding evaluates that chain map on a degree-$1$ cycle. The homology-class zero-winding hypothesis asserts that any such cycle with winding $0$ has vanishing image under the canonical projection from cycles to $H_1$. The singular integer chain complex of $\mathrm{TopCat.sphere},1$ is the Mathlib object whose $H_1$ is the comparison target in this foundation layer.
Together with the fact that winding sends the once-around generator to $1$, injectivity of the descended map is the mono half of the classical isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Rewrite monicity in ModuleCat as injectivity of the underlying map. Given $x,y$ with equal winding images, surjectivity of the degree-$1$ homology projection (an epi) supplies cycles $z_x,z_y$ lifting them. The difference $z_x-z_y$ projects to $x-y$, and the winding of that difference is zero because the homology-level winding map kills $x-y$ and commutes with the projection via the cycle-winding identity. The zero-winding hypothesis then forces the homology class of $z_x-z_y$ to vanish, so $x-y=0$.
why it matters
Feeds the left-to-right direction of the parent equivalence zeroWindingCycles_bound_iff_windingHomologyMap_mono, which identifies the chain-level zero-winding filling theorem with injectivity of the homology winding map. That equivalence is the bridge between an explicit singular $2$-boundary construction and the mono half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the module narrative, winding already annihilates boundaries and hits the fundamental loop by $1$; mono is the remaining split-injective piece. The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. The sphere chain complex is flagged as the strict T8-adjacent $H_1(S^1)$ target in the foundation stack, so this mono step is load-bearing for the circle computation that underwrites the eight-tick and dimension-forcing story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.