singularEdgePath
plain-language theorem explainer
Converts a singular 1-simplex on S¹ into a continuous unit-interval path I → S¹. Anyone comparing chain-level edges to path winding or displacement cites this bridge. The body is a one-line transport through the singular simplicial-set equivalence, then reparameterization of Δ¹ onto I.
Claim. To each singular $1$-simplex $s$ of $S^1$ associate the continuous path $I\to S^1$ obtained by viewing $s$ as a map $\Delta^1\to S^1$ via the singular simplicial-set equivalence and composing with the standard homeomorphism $I\simeq\Delta^1$.
background
The module lifts path-level winding and displacement from CircleWinding to singular simplices of TopCat.sphere 1, aiming at the homology fact that displacement kills boundaries of $2$-simplices and thus descends to $H_1(S^1)$.
A singular $1$-simplex is an element of the degree-$1$ object of the singular simplicial set of $S^1$. The carrier of that sphere is abbreviated SphereOne. The sibling oneSimplexPath already turns a concrete continuous map $\Delta^1\to S^1$ into a path $I\to S^1$ by precomposing with the standard affine chart intervalToSimplex : I → Δ¹.
This definition is the missing adapter: singular generators live in the simplicial-set object, while winding and homotopy tools expect unit-interval paths. The equivalence TopCat.toSSetObjEquiv identifies those two presentations of a singular $1$-simplex.
proof idea
Definitional one-liner. Apply the singular simplicial-set equivalence at the $1$-simplex object of $S^1$ to obtain a continuous map $\Delta^1\to S^1$, then feed that map to oneSimplexPath, which composes with intervalToSimplex. No tactics, no lemmas beyond that composition.
why it matters
This is the chain-to-path bridge named in the module doc: every later comparison of singular winding with path displacement factors through it. Downstream, orientedEdgePath reads forward edges via this map and backward edges via its reverse; endpoint lemmas identify the path values at $0$ and $1$ with the $S^1$-points of the initial and terminal $0$-faces; the round-trip theorem shows reading out and back recovers the original singular generator.
It also feeds the null-homotopy criterion for closed edges of singular winding zero (input to the singular prism construction) and the equalities that identify singular winding with path displacement and with cyclic integral sums. In the larger story this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding on $1$-cycles is a left inverse to the fundamental class, once boundaries are killed and the once-around generator maps to $1$. Surjectivity still needs a prism/subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.