homology
plain-language theorem explainer
For any integer 1-cycle on the singular chain complex of the circle, the homology-level winding map applied to its homology class equals the chain-level winding of that cycle. Anyone citing the descended winding homomorphism on H₁(S¹;ℤ) needs this compatibility. The proof is a short term rewrite: unfold the two maps and cancel via the standard π–ι and descOpcycles identities.
Claim. Let $z$ be a $1$-cycle in the singular chain complex of $S^1$ with integer coefficients. Applying the homology-level winding map to the homology class of $z$ recovers the chain-level winding number of $z$: $\mathrm{wind}_*( [z] ) = \mathrm{wind}(z)$.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that winding kills boundaries. The displacement of a singular $1$-simplex is obtained by reparameterizing $\Delta^1$ to the unit interval and taking path displacement; the key identity is that the alternating face sum of displacements on any singular $2$-simplex vanishes (telescoping via convexity of $\Delta^2$ and homotopy invariance of path displacement).
Once winding vanishes on boundaries, it descends from $1$-cycles to homology. The chain-level winding of a cycle is the integer obtained by summing coefficients times simplex windings. The homology-level map is the unique morphism on $H_1$ induced by the chain map that sends each generator to its winding (via the usual homology projection and the opcycle descent of that chain map).
Together with the fact that the once-around generator has winding $1$, this yields a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Term-mode proof by unfolding. Expand both cycleWinding and windingHomologyMap so the left-hand side becomes the composite of homology projection, homology inclusion into opcycles, and the descended winding chain map, applied to $z$. The right-hand side is the composite of the cycle inclusion with the winding chain map. The two composites agree after rewriting with the standard identities homology_π_ι_assoc and p_descOpcycles from the homological-complex API: projection followed by inclusion cancels against the opcycle descent of a chain map that already kills boundaries.
why it matters
This is the bookkeeping step that makes the descended winding map on homology agree with the concrete chain-level winding used elsewhere in the circle-winding chain. Without it, one only knows that winding kills boundaries and therefore induces some map on $H_1$; this lemma pins that induced map to the integer already computed on cycles.
In the module's larger program, the winding homomorphism is the left inverse to the fundamental class, giving injectivity of $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$. The converse (generation / surjectivity) still needs a simplicial prism or subdivision operator that Mathlib's singular homology does not yet supply. The result sits in the Foundation layer that underwrites topological invariants used by the Recognition forcing chain (circle geometry, eight-tick octave structure, and the $D=3$ spatial story), but it is pure algebraic topology: no Recognition-specific constants appear here.
No downstream dependents are recorded in the graph for this declaration; it is a local compatibility lemma inside the winding-homology package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.