singularWinding
plain-language theorem explainer
Winding number of a Mathlib singular 1-simplex on S¹, obtained by transporting into the continuous-map presentation and normalising displacement by 2π. Downstream cone and cycle theorems cite it as the native singular-set form of the invariant. The body is a one-line transport into simplexWinding.
Claim. For a singular $1$-simplex $s$ in the singular simplicial set of $S^1$, the singular winding is the ordinary simplex winding of the continuous map $\Delta^1\to S^1$ obtained by transporting $s$ across the equivalence between that simplicial-set value and $C(\Delta^1,S^1)$. Equivalently, it is path displacement of the reparameterised edge, divided by $2\pi$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of Mathlib's $S^1$, and proves that the invariant kills boundaries. Concretely, simplexDisplacement assigns a real (displacement, i.e. $2\pi$ times winding) to every continuous map $f:C(\Delta^1,S^1)$ by reparameterising the standard $1$-simplex to the unit interval and taking pathDisplacement; simplexWinding is that quantity divided by $2\pi$.
SingularOneSimplex is the actual singular-set object: an element of $(\mathrm{Sing},S^1)_1$, not a hand-rolled continuous map. The module's central identity is simplexDisplacement_boundary: for every singular $2$-simplex the alternating face sum of displacements vanishes, by $2$-simplex telescoping plus homotopy invariance of pathDisplacement. Together with the fact that the once-around generator has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
Pure definitional wrapper. Apply the singular-set equivalence TopCat.toSSetObjEquiv at $S^1$ in degree $1$ to turn the SingularOneSimplex into a concrete OneSimplex (continuous map $\Delta^1\to S^1$), then evaluate simplexWinding, which is simplexDisplacement divided by $2\pi$. No tactics, no lemmas beyond that transport.
why it matters
Native singular-set form of the winding invariant, so consumers need not keep a parallel $C(\Delta^1,S^1)$ presentation. Downstream, closedSingularOneCycle_bounds_of_zero_singularWinding and its zsmul and list variants use zero singularWinding as the hypothesis that a closed generator (or finite sum of them) bounds via the cone construction. cycleWinding_closedSingularOneCycle multiplies the coefficient by singularWinding of the underlying simplex. OrientedSingularEdge and orientedWinding also route through it.
In the module narrative this is the singular-set face of the left inverse to the fundamental class: winding on $1$-cycles that sends the generator to $1$. The open half remains generation (every $1$-cycle homologous to an integer multiple of the fundamental cycle), which needs a simplicial prism/subdivision operator Mathlib singular homology does not yet supply. No RS forcing-chain landmark is proved here; the declaration is pure topological scaffolding for that $H_1$ comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.