singularEdgePath_one
plain-language theorem explainer
The unit-interval path of a singular 1-simplex on S¹ ends, at time 1, at the sphere point of that simplex's terminal 0-face. Chain-level winding and oriented-edge arguments cite this endpoint identity when matching path endpoints to face data. The proof unfolds the path and face maps, applies the standard simplex endpoint at 1, and invokes the δ₀ face-evaluation lemma.
Claim. For every singular $1$-simplex $s$ on $S^1$, if $\gamma_s:I\to S^1$ is the unit-interval path obtained by reparameterizing $s$ via the standard homeomorphism $\Delta^1\simeq I$, then $\gamma_s(1)$ equals the point of $S^1$ corresponding to the terminal $0$-face $\partial_0 s$.
background
This module lifts path-level winding and displacement from CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries so the invariant descends to homology. A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. The bridge to path invariants is the unit-interval reading: compose the simplex map with the standard homeomorphism $\Delta^1\simeq I$ to get a continuous path $I\to S^1$.
The terminal vertex of a directed singular edge is the face $\delta_0$ of that $1$-simplex (matching the positive boundary term). The companion map sends a singular $0$-simplex to its underlying point of $S^1$. The identity here says those two constructions agree at the right endpoint of the path.
Upstream, the reparameterization sends $1\in I$ to the standard vertex $e_1\in\Delta^1$, and face evaluation identifies the image of that vertex under the singular simplex with the $\delta_0$ face.
proof idea
Term-mode proof by unfolding. Expand the path-of-edge definition, the vertex-point map, the terminal-face map, and the unit-interval reading of a $1$-simplex. Rewrite the composition at $1$ via continuous-map evaluation and the fact that the interval-to-simplex map sends $1$ to the standard vertex $e_1$. The remaining equality is the symmetric form of the lemma that evaluates a singular $1$-simplex at that vertex and recovers the $\delta_0$ face point.
why it matters
Endpoint bookkeeping for singular edges is required wherever path-level winding is glued to chain-level face data. Downstream, the oriented-edge terminal identity reduces the positive-orientation case to this lemma. The cyclic-walk integrality theorem uses it to match path endpoints along a closed chain of singular edges (terminal face of $e_i$ equals initial face of the next), so total winding is an integer. The zero-winding null-homotopy for closed singular edges likewise needs consistent basepoint identification at the path ends.
In the module's program this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding on $1$-cycles as a left inverse to the fundamental class, via path displacement plus the kills-boundaries identity on $2$-simplices. It does not itself touch the generation/surjectivity half (simplicial prism/subdivision), which remains outside Mathlib's singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.