windingChainMap_boundary_generator
plain-language theorem explainer
On each singular 2-simplex generator of the integer singular chains of S¹, the degree-2 boundary composed with the winding chain map is zero. Anyone building the winding homomorphism on H₁(S¹;ℤ) cites this generator-wise annihilation. The proof expands the alternating face differential, rewrites each face through the winding map, and finishes by the already-proved vanishing of the alternating winding sum on faces.
Claim. For every singular $2$-simplex $s$ on $S^1$, if $\iota_s$ is the coproduct inclusion of the corresponding free $\mathbb{Z}$-summand into the degree-$2$ singular chains, then $\iota_s \circ \partial_2 \circ W = 0$, where $W$ is the winding chain map from degree-$1$ singular chains to $\mathbb{Z}$.
background
The 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. A singular $2$-simplex is a continuous map $\Delta^2\to S^1$ in the singular simplicial set; its three faces $\delta_0 s,\delta_1 s,\delta_2 s$ are singular $1$-simplices.
The integer singular chain complex of $S^1$ is Mathlib's singular chain complex with coefficients in $\mathbb{Z}$. In degree $2$ it is a coproduct of free rank-one modules indexed by singular $2$-simplices; the differential $\partial_2$ is the alternating face map. The winding chain map $W$ sends each singular $1$-simplex to its integer winding (displacement over $2\pi$).
Upstream, singularWinding_boundary already states that for every singular $2$-simplex the alternating sum of face windings vanishes: $W(\delta_0 s)-W(\delta_1 s)+W(\delta_2 s)=0$. That identity is the numerical content of $\partial_2\circ W=0$ on a single generator.
proof idea
Unfold the singular chain complex and the alternating-face differential in degree $2$. The three-term face sum expands with signs $+,-,+$ (via $\mathrm{Fin.sum_univ_three}$ and the usual powers of $-1$). After simplifying coproduct inclusions and identities, each face composite is rewritten by the face-component formula for the winding chain map.
The resulting linear combination of three winding values is exactly the left-hand side of singularWinding_boundary s. Extensionality for morphisms of $\mathbb{Z}$-modules (and of maps out of $\mathbb{Z}$) reduces the categorical equality to a numerical one, which linarith discharges from that vanishing identity.
why it matters
This is the generator-wise half of the chain-level statement that winding annihilates $\partial_2$. The immediate parent is windingChainMap_boundary, which packages the family of generator identities into a single morphism equality $\partial_2\circ W=0$ by coproduct extensionality, and thereby shows that $W$ descends to homology $H_1(S^1;\mathbb{Z})$.
In the module narrative, together with the fact that winding sends the once-around fundamental loop to $1$, this supplies the split-injective half of the comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. That comparison is the strict algebraic target tied to the circle's first homology in the foundation layer (the T8-adjacent $H_1$ computation). Surjectivity still needs a prism/subdivision argument Mathlib does not yet supply; this lemma closes only the kills-boundaries direction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.