oneSimplexOfPath_oneSimplexPath
plain-language theorem explainer
Converting a singular 1-simplex on the circle to a unit-interval path and back recovers the original continuous map. Anyone equating path-level and simplex-level winding data cites this left inverse. The proof is a short extensionality argument: unfold both reparameterisations and simplify through the standard homeomorphism Δ¹ ≃ I.
Claim. For every continuous map $f:\Delta^1\to S^1$, reading $f$ as a path on the unit interval via $t\mapsto(1-t,t)$ and converting that path back to a singular $1$-simplex recovers $f$.
background
This module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of $S^1$, and proves that displacement vanishes on boundaries. The goal is a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is a continuous map $f:\Delta^1\to S^1$ with $\Delta^1=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$. The map $t\mapsto(1-t,t)$ reparameterises the unit interval onto $\Delta^1$; it is the inverse of Mathlib's stdSimplexHomeomorphUnitInterval. Composing $f$ with that reparameterisation yields a unit-interval path; the reverse composition turns a path into a singular $1$-simplex.
The two conversions are definitional inverses up to the homeomorphism. This lemma is the simplex-to-path-to-simplex direction.
proof idea
Pointwise extensionality on $\Delta^1$. Unfold the path-of-simplex and simplex-of-path definitions together with the interval-to-simplex reparameterisation. After unfolding, both sides are compositions of $f$ with a homeomorphism and its inverse; simp closes the equality.
why it matters
The parent result singularOneSimplexOfMap_oneSimplexOfPath_singularEdgePath rewrites with this identity to show that reading a singular edge as a unit-interval path and back as a concrete singular $1$-simplex returns the original generator. That closes the bridge between singular-set generators and the concrete continuous maps on which simplexDisplacement and simplexWinding are defined.
Without this left inverse, displacement on singular $1$-simplices would not be interchangeable with the path-level invariant used in the $2$-simplex telescoping argument (simplexDisplacement_boundary). That vanishing-on-boundaries identity, together with the once-around generator mapping to $1$, is the chain-level half of the winding isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ sketched in the module doc. The generation (surjectivity) half remains open pending a simplicial prism or subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.