toSSetObjEquiv_delta
plain-language theorem explainer
The i-th simplicial face of a singular 2-simplex on S¹, after transport through the continuous-map equivalence of the singular simplicial set, equals the geometric face obtained by precomposing with the affine edge map Δ¹→Δ². Anyone proving that winding annihilates singular boundaries cites this bridge. The proof is definitional: unfold the Yoneda/simplicial face and geometric face, then reflexivity.
Claim. For every singular $2$-simplex $s$ of $S^1$ and every $i\in\{0,1,2\}$, transporting the simplicial face $\delta_i s$ through the equivalence identifying singular simplices with continuous maps $C(\Delta^1,S^1)$ yields the geometric face of the continuous map corresponding to $s$ under the same equivalence (precomposition with the affine coface $\Delta^1\to\Delta^2$).
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries: for $F:C(\Delta^2,S^1)$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the generator sending the once-around loop to $1$, gives the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Two presentations of simplices sit side by side. SingularTwoSimplex is an object of Mathlib's singular simplicial set of TopCat.sphere 1. The geometric TwoSimplex is a continuous map $C(\Delta^2,S^1)$. The homeomorphism TopCat.toSSetObjEquiv identifies them levelwise.
Geometric faces are defined by precomposition: face F i := F ∘ faceMap i, where faceMap i is the affine map $\Delta^1\to\Delta^2$ induced by the coface $\delta_i:[1]\to[2]$. Simplicial faces are the face operators $\delta_i$ of the simplicial set. This theorem says the two agree after transport.
proof idea
Pointwise extensionality on the continuous map, then dsimp of the equivalence stack: toSSetObjEquiv, the restricted ULift Yoneda presentation of toSSet, the simplicial face SimplicialObject.δ, the concrete-category hom equivalence, and the geometric face/faceMap. After those unfoldings both sides are the same composition, so rfl closes. No external lemma is applied; the equality is definitional once the face operators are expanded.
why it matters
This is the bridge that lets chain-complex boundaries talk to the affine edge maps used in the $2$-simplex telescoping argument. Downstream, singularTwoSimplexOfMap_delta transports a concrete face equation through the equivalence by injectivity plus this identity. More importantly, singularWinding_boundary rewrites simplicial faces via toSSetObjEquiv_delta and reduces to the geometric vanishing simplexWinding_boundary, yielding $W\circ\partial_2=0$ on generators: the winding cochain annihilates boundaries.
In the module's program that is the chain-level half of the split injection $H_1(S^1;\mathbb{Z})\hookrightarrow\mathbb{Z}$. The converse generation half still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply. The result is pure foundation topology; it does not invoke the forcing chain T0–T8 or the Recognition Composition Law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.