singularOneSimplex_delta_one_endpoint
plain-language theorem explainer
The δ₁ face of a singular 1-simplex on S¹ is its initial endpoint, after transport through the singular-set equivalence. Anyone relating Mathlib face operators to geometric endpoints of edges on the circle cites this. The proof unfolds the singular-set and face-map definitions, then reduces to the standard fact that face maps send vertices to vertices.
Claim. For every singular $1$-simplex $s$ on $S^1$, the unique point of the $0$-simplex obtained by applying the face operator $\delta_1$ equals the image under $s$ of the initial vertex of the standard $1$-simplex $\Delta^1$.
background
This module lifts path-level winding on 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 generator sending the once-around loop to winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an object of the singular simplicial set of $S^1$ in degree $1$: a continuous map $\Delta^1\to S^1$ packaged in Mathlib's TopCat.toSSet. Face operators $\delta_i$ restrict such a map to the $i$-th face of the simplex. The equivalence TopCat.toSSetObjEquiv converts between that abstract simplicial-set presentation and concrete continuous maps on standard simplices, so endpoint identities can be checked pointwise on vertices.
The geometric content is elementary: $\delta_1$ of a $1$-simplex is the initial endpoint. The lemma records that fact after the singular-set transport, which later lemmas need when they identify path endpoints with face data.
proof idea
Term-mode proof by definitional reduction. Unfold the singular-set equivalence, the restricted Yoneda presentation of toSSet, the simplicial face operator $\delta$, and the concrete-category homeomorphism packaging. After congr 1, the goal is an equality of vertices under stdSimplex.map along $\delta_1$. Apply stdSimplex.map_vertex (face maps send vertices to vertices) and finish by rfl on the resulting Fin index.
why it matters
Endpoint bookkeeping for the singular winding chain. Downstream, singularEdgePath_zero quotes it (symmetrized) to identify the path start of a singular edge with the $S^1$-point of its initial $0$-face. singularOneSimplexOfMap_faces_eq_of_endpoints uses the same face/endpoint dictionary to promote equal geometric endpoints to a closed singular $1$-simplex. singularWinding_loop_integral needs closed faces to conclude integer winding, the generator-level integrality input for cycleWinding_integral. The zero-winding cone theorem closedSingularOneCycle_bounds_of_zero_singularWinding sits further up the same stack.
In the module's program this is plumbing toward the homology invariant: winding as a left inverse to the fundamental class on $H_1(S^1)$. The module notes the converse generation half still needs a simplicial prism/subdivision operator Mathlib does not yet supply. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is pure singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.