oneSimplexOfPath
plain-language theorem explainer
Converts a continuous path γ : I → S¹ into a singular 1-simplex Δ¹ → S¹ by precomposing with the standard homeomorphism Δ¹ ≃ I. Anyone working the singular-chain lift of path winding cites this bridge. The body is a one-line continuous composition with that homeomorphism.
Claim. Given a continuous path $\gamma : I \to S^1$, define a singular $1$-simplex $\Delta^1 \to S^1$ by $\gamma \circ h$, where $h : \Delta^1 \xrightarrow{\simeq} I$ is the standard homeomorphism from the topological $1$-simplex to the unit interval.
background
The module lifts the path-level winding and displacement invariant of CircleWinding to singular simplices of $S^1$, then proves that displacement vanishes on boundaries so it descends to homology. A singular $1$-simplex here is a continuous map $C(\Delta^1, S^1)$ with $\Delta^1 = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$; $S^1$ is the carrier of TopCat.sphere 1.
Path-level invariants live on $C(I,S^1)$. To move them onto chains one needs a fixed identification of the parameter domains. The standard homeomorphism $\Delta^1 \simeq I$ supplies that identification; this definition is the induced map on continuous maps into $S^1$.
The inverse direction (simplex back to path) is the sibling oneSimplexPath. Together they set up the reparameterisation used by simplexDisplacement, which reads path displacement after transporting along this homeomorphism.
proof idea
One-line definition: compose the path $\gamma$ on the right with the continuous map underlying stdSimplexHomeomorphUnitInterval. No lemmas are applied; noncomputability is inherited from the homeomorphism package. The round-trip identities with the inverse conversion are proved separately by ext and simp.
why it matters
This is the path-to-simplex bridge that lets the module treat winding as a singular-chain invariant. Downstream, oneSimplexPath_ofPath and oneSimplexOfPath_oneSimplexPath show the conversion is inverse to reading a simplex as a path. Cone constructions use it as the base face: coneCirclePoint_faceMap_two and coneCircleMapOfContinuous_face_two_path identify the face $\delta_2$ of the path-parametric cone with oneSimplexOfPath γ.
Oriented singular edges and oriented cyclic family terms also route through this conversion when packaging closed walks of $1$-simplices. That packaging feeds the chain-level "winding kills boundaries" identity (simplexDisplacement_boundary), which with the once-around generator gives the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. 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.