windingChainMap_boundary
plain-language theorem explainer
The winding chain map W : C₁(S¹;ℤ) → ℝ annihilates every degree-2 boundary, so ∂₂ ≫ W = 0. Anyone building the winding homomorphism on H₁(S¹;ℤ) cites this identity: it is the chain-level fact that lets W descend to homology. The proof is a coproduct extension: reduce to each singular 2-simplex generator via Sigma.hom_ext and quote the per-generator vanishing lemma.
Claim. Let $C_\bullet(S^1;\mathbb{Z})$ be the singular chain complex of the circle with integer coefficients, and let $W : C_1(S^1;\mathbb{Z}) \to \mathbb{R}$ be the winding chain map (sending each singular $1$-simplex generator to its winding number). Then the composite of the degree-$2$ boundary $\partial_2 : C_2 \to C_1$ with $W$ is the zero map: $\partial_2 \circ W = 0$.
background
The module lifts the path-level winding invariant of the circle to singular simplices of $S^1$ and proves that winding kills boundaries, so it becomes a homology invariant. On a singular $1$-simplex $f : \Delta^1 \to S^1$, one reparameterizes $\Delta^1$ to the unit interval and takes path displacement (equivalently $2\pi$ times winding). The key geometric input is that for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes: $\mathrm{disp}(\delta_0 F) - \mathrm{disp}(\delta_1 F) + \mathrm{disp}(\delta_2 F) = 0$, by telescoping along a homotopy in the convex standard $2$-simplex.
The object sphereOneSingularIntChainComplex is Mathlib's singular chain complex of $\mathrm{TopCat.sphere},1$ with coefficients in $\mathbb{Z}$. The winding chain map $W$ is the coproduct (Sigma) descent that on the free generator indexed by a singular $1$-simplex $s$ acts by $n \mapsto n \cdot$ (winding number of $s$). The per-generator lemma already states that $W$ annihilates $\partial_2$ of each singular $2$-simplex summand inclusion.
proof idea
One short tactic proof. Apply Limits.Sigma.hom_ext to the coproduct presentation of the degree-$2$ chains, so it suffices to check the composite on each singular $2$-simplex generator $s$. After simplifying the zero composite, invoke the already-proved per-generator identity windingChainMap_boundary_generator s, which states that the inclusion of summand $s$, followed by $\partial_2$, followed by $W$, is zero.
why it matters
This is the chain-level "winding kills boundaries" identity that lets the winding map factor through $H_1(S^1;\mathbb{Z})$. Downstream, windingHomologyMap is defined by descending $W$ through opcycles using exactly this vanishing; the doc-comment there states that because $W$ annihilates $\partial_2$, it factors through degree-$1$ homology. Together with windingChainMap_fundamental (which sends the fundamental cycle to $1$), it exhibits the integer comparison $\mathbb{Z} \to H_1(S^1;\mathbb{Z})$ as split-injective: the fundamental class has infinite order.
In the module's program this is the "split-injective half" of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$, feeding the strict T8 target (three spatial dimensions via the circle's first homology). It is also used by constant-simplex vanishing, oriented cyclic family bookkeeping, and the conditional zero-winding filling theorem that isolates the remaining generation half (fundamentalCycle_boundary_generates).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.