fundamentalHomologyClass_mono
plain-language theorem explainer
The comparison map Z → H₁(S¹;Z) sending n to n times the fundamental once-around class is a monomorphism: distinct integer multiples are never homologous. Anyone assembling the split-injective half of H₁(S¹;Z) ≅ Z cites this. The argument shows the composite with the winding map to R is the standard inclusion n ↦ n, hence mono, then cancels the second arrow.
Claim. The comparison morphism $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ given by $n\mapsto n\cdot[\gamma]$, where $[\gamma]$ is the singular homology class of the fundamental once-around loop on the circle, is a monomorphism of $\mathbb{Z}$-modules. Equivalently, $[\gamma]$ has infinite order in $H_1(S^1;\mathbb{Z})$.
background
This module lifts the path-level winding (displacement) invariant of the circle to singular 1-simplices on $S^1$ and proves that winding kills boundaries: for every singular 2-simplex the alternating face sum of displacements vanishes. That identity lets winding descend to a homology map $H_1(S^1;\mathbb{Z})\to\mathbb{R}$.
The integer comparison map is the morphism $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$ sending $n$ to $n$ times the class of the fundamental singular 1-cycle (the once-around generator). The winding homology map is the descent of simplex displacement through opcycles. Their composite is identified with the standard span-singleton inclusion $\mathbb{Z}\to\mathbb{R}$, $n\mapsto n\cdot 1$: the winding number is a left inverse to the fundamental class at the level of homology.
Together these give the split-injective half of the classical isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity (generation by the fundamental loop) is a separate statement and needs prism or subdivision machinery not yet available in Mathlib's singular homology.
proof idea
First establish that the composite of the comparison map with the winding homology map is mono. Rewrite that composite via the retraction identity: it equals the module map $\mathbb{Z}\to\mathbb{R}$ given by span-singleton at $1$. Injectivity of that map is immediate (equality of real images forces equality of integers after casting).
Then apply the categorical cancellation lemma: if $f\gg g$ is mono then $f$ is mono. Taking $f$ to be the comparison map and $g$ the winding map yields the claim. No generation or filling hypothesis is used.
why it matters
This is the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, obtained from the covering-space winding invariant with no project-local circle replacement. Downstream, bijectivity of the comparison map under a surjectivity hypothesis instantiates this monomorphism and pairs it with the epi half; the corresponding ModuleCat isomorphism is built the same way (mono from winding, epi from generation, modules balanced).
In the Recognition foundation stack the result anchors the winding retraction as a genuine left inverse on homology, so the once-around generator is detected by a real-valued invariant and cannot be torsion. That underwrites later uses of circle winding as a discrete counting invariant (related in spirit to the eight-tick octave T7, though this lemma itself is pure singular homology). The open half remains generation: every 1-cycle homologous to an integer multiple of the fundamental cycle, packaged as the zero-winding-cycles-are-boundaries filling statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.