singularTwoSimplexOfMap_delta
plain-language theorem explainer
The i-th simplicial face of the Mathlib singular 2-simplex built from a continuous map F : Δ² → S¹ equals the singular 1-simplex built from the geometric face of F. Anyone computing boundaries of free generators on S¹ cites this transport. The proof injects through TopCat.toSSetObjEquiv and rewrites by the combinatorial-vs-geometric face bridge.
Claim. For every continuous map $F : \Delta^2 \to S^1$ and every face index $i \in \{0,1,2\}$, the simplicial face operator $\delta_i$ applied to the singular $2$-simplex associated to $F$ equals the singular $1$-simplex associated to the geometric face $F \circ \iota_i$, where $\iota_i : \Delta^1 \hookrightarrow \Delta^2$ is the $i$-th affine face inclusion.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for any continuous $F : \Delta^2 \to S^1$, the alternating face sum of displacements vanishes. That identity is the chain-level reason winding is a homology invariant and supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Here a TwoSimplex is just a continuous map $C(\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3), S^1)$. Its geometric $i$-th face is $F$ composed with the affine face inclusion induced by skipping vertex $i$. The maps singularTwoSimplexOfMap and singularOneSimplexOfMap send these concrete continuous simplices into Mathlib's singular simplicial set via TopCat.toSSetObjEquiv.
Upstream, toSSetObjEquiv_delta already states the converse transport: after applying the equivalence, the simplicial face of a singular $2$-simplex is the geometric face of the underlying continuous map. The present lemma is the dual orientation needed when one starts from a continuous $F$ and wants faces in the chain complex.
proof idea
Short term-mode argument. Apply injectivity of TopCat.toSSetObjEquiv on $1$-simplices of $S^1$. Rewrite the left-hand side by toSSetObjEquiv_delta, which converts the simplicial face into the geometric face of the continuous map recovered from the singular simplex. Unfold both singularOneSimplexOfMap and singularTwoSimplexOfMap (each is symm of the equivalence) and cancel the two apply_symm_apply pairs. No case split on $i$ is required.
why it matters
Every free-boundary computation that builds a singular $2$-simplex from a continuous map and then reads its chain-complex boundary needs this face transport. Downstream it feeds the geodesic composition law (singularTwoBoundaryFree_freeMk_linearSingularTwoSimplex), the path-backtrack prism, the cone-over-edge shells, and the continuous-map handoff closedSingularOneCycle_bounds_of_cone_map that turns a geometric cone filling into an actual bounding chain.
In the module's programme this is plumbing for the "winding kills boundaries" identity and the subsequent left-inverse to the fundamental class on $H_1(S^1)$. It does not itself touch the Recognition forcing chain (T5–T8) or the mass ladder; it is pure singular-homology infrastructure that makes the circle's winding homomorphism rigorous in Lean. The remaining open half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ (generation / surjectivity) still needs a prism or subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.