singularWinding_eq_pathDisplacement
plain-language theorem explainer
The singular winding of a singular 1-simplex on S¹ equals the path displacement of its unit-interval reparameterization, divided by 2π. Anyone building the chain-level winding homomorphism on singular 1-cycles of the circle cites this bridge. The proof is purely definitional: four stacked unfolds reduce the equality to reflexivity.
Claim. For every singular $1$-simplex $s$ of $S^1$, the singular winding number of $s$ equals the path displacement of the associated continuous path $I\to S^1$, divided by $2\pi$.
background
This module lifts the path-level winding and displacement invariants of the circle to singular simplices of TopCat.sphere 1, and proves that displacement kills boundaries. The goal is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: a winding homomorphism on 1-cycles that is a left inverse to the fundamental class.
Path displacement is the net travel of the canonical real lift of a continuous path $\gamma:I\to S^1$, namely $\mathrm{pathLift},\gamma(1)-\mathrm{pathLift},\gamma(0)$. Simplex displacement reparameterizes a concrete singular 1-simplex $\Delta^1\to S^1$ to the unit interval and applies that path displacement; simplex winding is the same quantity divided by $2\pi$.
A singular one-simplex here is an actual 1-simplex in the singular simplicial set of the sphere. The singular edge path reads it as a continuous map $I\to S^1$. Singular winding is simplex winding after transporting through the equivalence that identifies the concrete simplex with Mathlib's singular simplicial set object.
proof idea
Definitional one-liner. Unfold singular winding (transport then simplex winding), simplex winding (displacement over $2\pi$), simplex displacement (path displacement of the one-simplex path), and the singular edge path (one-simplex path after the same transport). The two sides become identical terms, so rfl closes.
why it matters
This identity is the dictionary between the chain-complex presentation of a singular edge and the path-level displacement used throughout CircleWinding. Downstream, oriented winding reduces to it by case split on orientation; the null-homotopy theorem for closed singular edges of winding zero feeds on it to supply the path-level input to the singular prism construction; and the cyclic-walk integrality theorem uses it to convert a sum of singular windings into a sum of path displacements whose total is integral when faces chain.
Together with the fact that the once-around generator has winding 1, and with the kills-boundaries identity for 2-simplices, this supports the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The converse generation half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.