singularOneSimplex_delta_zero_endpoint
plain-language theorem explainer
For any singular 1-simplex on S¹, the δ₀ face (a 0-simplex) is exactly the terminal endpoint of that edge, after transport through the singular simplicial-set equivalence. Algebraic topologists building the winding homomorphism on Mathlib singular chains cite this face-endpoint identity. The proof is a short definitional reduction: unfold the face and equivalence, apply vertex-map naturality, and finish by rfl.
Claim. Let $s$ be a singular $1$-simplex in the singular simplicial set of $S^1$. After transport through the equivalence identifying singular simplices with continuous maps out of standard simplices, the $\delta_0$ face of $s$ (a singular $0$-simplex) evaluated at the unique vertex of $\Delta^0$ equals $s$ evaluated at the terminal vertex of $\Delta^1$.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of TopCat.sphere 1, and proves that displacement kills boundaries: for every singular 2-simplex the alternating face sum of displacements vanishes. That identity, with the once-around generator mapping to 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular 1-simplex here is an object of the singular simplicial set of $S^1$ in degree 1, i.e. a continuous map $\Delta^1\to S^1$ packaged through Mathlib's toSSet. Face operators $\delta_i$ are the simplicial face maps; on a 1-simplex, $\delta_0$ and $\delta_1$ extract the two endpoint 0-simplices. The standard simplex vertices are the Dirac masses at the basis indices of $\mathrm{Fin},(n+1)$.
The companion statement (immediately below in the file) says that $\delta_1$ recovers the initial endpoint. Together they pin geometric endpoints to simplicial faces, which is needed before one can talk about closed singular edges or integer winding of loops.
proof idea
Term-mode proof by definitional simplification. Unfold the singular-set equivalence, the restricted Yoneda presentation of toSSet, the simplicial face operator $\delta$, and the concrete-category homeomorphism congruence. After congr 1, the goal reduces to an equality of points in the standard simplex: the image of the unique vertex of $\Delta^0$ under the geometric face map induced by $\mathrm{SimplexCategory}.\delta,0$ equals the terminal vertex of $\Delta^1$. Rewrite by stdSimplex.map_vertex (naturality of vertices under simplicial maps) and close with rfl.
why it matters
Face-endpoint matching is the bridge from continuous maps $C(\Delta^1,S^1)$ to Mathlib's actual singular simplicial set. Downstream, singularEdgePath_one uses the identity (symmetrized) to identify the terminal point of the edge path with the $S^1$-point of the terminal 0-face. singularOneSimplexOfMap_faces_eq_of_endpoints turns equal geometric endpoints into equal simplicial faces, producing closed singular 1-simplices. singularWinding_loop_integral then gets integer winding for any such closed singular edge, the generator-level integrality input for cycle winding. The zero-winding cone theorem in actual-singular form (closedSingularOneCycle_bounds_of_zero_singularWinding) likewise depends on face bookkeeping of this kind.
In the module's larger program this is scaffolding for the winding homomorphism that left-inverts the fundamental class on $H_1(S^1)$. The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma is on the proved, axiom-free side of that split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.