singularWinding_boundary
plain-language theorem explainer
The winding number on singular 1-simplices of S¹ annihilates every singular 2-boundary: the alternating face sum of windings is zero. Anyone assembling the winding chain map on H₁(S¹;ℤ) cites this as the generator-wise identity W ∘ ∂₂ = 0. The proof transports combinatorial faces through the singular-set equivalence and quotes the geometric simplex-winding boundary theorem.
Claim. For every singular $2$-simplex $s$ in the singular simplicial set of $S^1$, the alternating sum of winding numbers of its three faces vanishes: $\mathrm{wind}(\delta_0 s) - \mathrm{wind}(\delta_1 s) + \mathrm{wind}(\delta_2 s) = 0$, where $\mathrm{wind}$ is the winding number of a singular $1$-simplex and $\delta_i$ are the simplicial face operators.
background
This module lifts the path-level winding invariant of the circle to singular simplices of TopCat.sphere 1 and proves that winding kills boundaries, the single identity that makes winding a homology invariant. A singular 2-simplex is an element of the degree-2 object of the singular simplicial set of S¹. The winding of a singular 1-simplex is defined by transporting it through the equivalence with continuous maps Δ¹ → S¹ and taking the geometric simplex winding (path displacement divided by 2π).
Upstream, the geometric identity already holds: for every continuous map F : Δ² → S¹ the alternating face sum of simplex windings is zero. That fact comes from 2-simplex telescoping inside the convex standard simplex (homotopy of the broken edge walk to the direct edge), combined with additivity and homotopy invariance of path displacement. The bridge lemma equates combinatorial faces in the singular set with geometric faces after transport through the singular-set equivalence.
proof idea
Short term-mode proof. Unfold the definition of singular winding (transport through the singular-set equivalence, then geometric simplex winding) and rewrite each combinatorial face via the bridge that identifies δᵢ with the geometric face map. The goal reduces exactly to the geometric kills-boundaries theorem on the transported continuous 2-simplex, which is applied directly.
why it matters
This is the chain-level statement W ∘ ∂₂ = 0 evaluated on a single generator: the winding cochain annihilates boundaries. Downstream it is the sole input to the theorem that the winding chain map kills the boundary of every singular 2-simplex generator (the per-generator form of ∂₂ ≫ W = 0 inside the singular integer chain complex of S¹).
Together with the fact that winding sends the once-around fundamental loop to 1, it supplies the split-injective half of H₁(S¹;ℤ) ≅ ℤ. The module doc notes that the converse generation half (every 1-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism or subdivision operator that Mathlib's singular homology does not yet provide. In the Recognition foundation stack this is pure topological scaffolding for the circle's first homology, not a forcing-chain step (T0–T8), but it underwrites any later use of winding as a discrete invariant on S¹.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.