singularOneSimplexOfMap_faces_eq_of_endpoints
plain-language theorem explainer
Equal geometric endpoints on a continuous edge Δ¹ → S¹ force the two simplicial faces of the transported singular 1-simplex to agree. Anyone proving that a closed edge is a genuine singular 1-cycle (before applying winding or cone fillers) cites this. The proof reduces face equality to the endpoint hypothesis via the toSSet equivalence and the two face-endpoint lemmas.
Claim. Let $f : \Delta^1 \to S^1$ be continuous. If $f(v_1) = f(v_0)$ at the two vertices of the standard 1-simplex, then the faces $\delta_0$ and $\delta_1$ of the corresponding singular 1-simplex in the singular simplicial set of $S^1$ are equal.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level input to $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ (injective half). A OneSimplex is a continuous map $C(\Delta^1, S^1)$ with $\Delta^1 = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$. The transport singularOneSimplexOfMap sends such an $f$ to Mathlib's singular 1-simplex via TopCat.toSSetObjEquiv.
Face operators on the singular simplicial set evaluate at vertices after that transport. Upstream, singularOneSimplex_delta_zero_endpoint identifies $\delta_0$ with the terminal vertex image, and singularOneSimplex_delta_one_endpoint identifies $\delta_1$ with the initial vertex image. Equal geometric endpoints are therefore exactly the condition that those two 0-simplices coincide.
proof idea
Apply injectivity of TopCat.toSSetObjEquiv on 0-simplices, then ext on the unique point of $\Delta^0$. That point is forced to be the sole vertex by the sum-to-one identity on the standard simplex (fin_cases on Fin 1). Rewrite both faces with the two endpoint lemmas, unfold the transport definition, cancel the equivalence, and finish with the equal-endpoints hypothesis.
why it matters
Closed edges must be actual singular cycles before winding or cone arguments apply. Downstream theorems that bound zero-winding closed edges all take equal faces (or equal geometric endpoints) as input: closedSingularOneCycle_bounds_of_closed_cone_map, the continuous-cone and zero-winding cone variants, the generation-shaped cone form, and the pure singular form closedSingularOneCycle_bounds_of_zero_singularWinding. Those feed the integrality target cycleWinding_integral and the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity (generation by the fundamental loop) remains open pending a simplicial prism or subdivision operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.