simplexDisplacement
plain-language theorem explainer
The displacement of a singular 1-simplex on the circle is the angular travel of that simplex read as a path on the unit interval: endpoint difference of its canonical real lift, equal to 2π times winding. Anyone building the singular-homology winding invariant on S¹ cites this as the bridge from path-level displacement to simplex-level data. The body is a one-line composition of the standard Δ¹ ≃ I reparameterization with the existing path displacement.
Claim. For a continuous map $f:\Delta^1\to S^1$ (a singular $1$-simplex on the circle), the displacement of $f$ is the path displacement of $f$ composed with the standard homeomorphism $I\simeq\Delta^1$. Explicitly, if $\gamma$ is that reparameterized path, the value is $\widetilde{\gamma}(1)-\widetilde{\gamma}(0)$ for the canonical real lift $\widetilde{\gamma}$, equal to $2\pi$ times the winding number of $f$.
background
This module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of the topological circle, and proves that the resulting assignment kills boundaries. A singular 1-simplex here is a continuous map $f:\Delta^1\to S^1$, where $\Delta^1=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$ is the standard topological 1-simplex.
Path displacement is the real number measuring how far the canonical lift of a path $\gamma:I\to S^1$ travels in $\mathbb{R}$: $\mathrm{pathLift},\gamma,1-\mathrm{pathLift},\gamma,0$. Lift independence says any continuous lift yields the same endpoint difference. The helper oneSimplexPath reads a singular 1-simplex as a unit-interval path by composing with the affine homeomorphism $I\to\Delta^1$.
The local goal is a chain-level invariant: assign a real displacement to every singular 1-simplex, then show the alternating face sum on every 2-simplex vanishes, so the assignment descends to homology and pairs with the fundamental class.
proof idea
Pure definitional wrapper: reparameterize the singular 1-simplex $f$ to a continuous path on $I$ via the standard homeomorphism $\Delta^1\simeq I$, then apply the existing path-level displacement (endpoint difference of the canonical real lift). No tactics, no lemmas beyond that composition.
why it matters
This is the simplex-level carrier of the winding invariant. Downstream, dividing by $2\pi$ defines the normalized winding number of a singular 1-simplex. The boundary theorem uses it to prove that for every singular 2-simplex $F$, the alternating sum of face displacements vanishes (the 2-simplex telescoping via homotopy invariance and path additivity inside the simply connected standard 2-simplex). That is the chain-level "winding kills boundaries" identity.
Together with the fact that the fundamental singular 1-simplex has displacement $2\pi$ (winding 1), the construction supplies a winding homomorphism on 1-cycles that is a left inverse to the fundamental class: the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Further uses include relating cone terminal sides to base-path displacement and equating singular winding with path displacement on loops. The surjectivity half (every 1-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism or subdivision operator not yet in Mathlib singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.