oneSimplexPath_ofPath
plain-language theorem explainer
Reading a continuous path on the circle as a singular 1-simplex and then back as a path recovers the original map. Anyone equating path-level winding with simplex-level displacement cites this left inverse. The proof is pointwise: unfold the two reparameterisations and simplify against the standard homeomorphism Δ¹ ≃ I and its inverse.
Claim. For every continuous path $\gamma : I \to S^1$, converting $\gamma$ to a singular $1$-simplex via the standard homeomorphism $\Delta^1 \simeq I$ and then reading that simplex back as a unit-interval path yields $\gamma$ again.
background
The module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of $S^1$, so that displacement becomes a homology invariant. The key objects are continuous maps $f : \Delta^1 \to S^1$ (singular 1-simplices) and continuous paths $\gamma : I \to S^1$ on the unit interval.
intervalToSimplex is the continuous reparameterisation $t \mapsto (1-t, t)$ of $I$ onto the standard 1-simplex; it is the inverse of Mathlib's stdSimplexHomeomorphUnitInterval. Composing a 1-simplex with that map yields a path; composing a path with the homeomorphism itself yields a 1-simplex. SphereOne is the carrier of TopCat.sphere 1.
This identity is the left inverse half of that dictionary: path to simplex to path is the identity on $C(I,S^1)$. The companion right inverse (simplex to path to simplex) sits beside it in the same file.
proof idea
Pointwise equality of continuous maps. Extend both sides at a parameter $t \in I$, unfold the definitions of the path-from-simplex map, the simplex-from-path map, and the interval-to-simplex reparameterisation, then simplify. The homeomorphism $\Delta^1 \simeq I$ and its continuous inverse cancel under composition, so the original path is recovered.
why it matters
Without a clean dictionary between unit-interval paths and singular 1-simplices, the path-level displacement of CircleWinding cannot be promoted to simplexDisplacement on $C(\Delta^1,S^1)$. That promotion is what the module needs for the chain-level identity: the alternating face sum of displacement on every singular 2-simplex vanishes ("winding kills boundaries").
Together with the fact that path winding sends the once-around generator to 1, the simplex-level invariant 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}$. No downstream theorem currently cites this lemma directly; it is infrastructure for that dictionary and for the telescoping argument on 2-simplices. The generation (surjectivity) half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.