singularTwoSimplexOfMap
plain-language theorem explainer
Continuous maps $F:\Delta^2\to S^1$ are transported to genuine singular 2-simplices in Mathlib's singular simplicial set of the circle, via the inverse of the standard TopCat-to-sSet object equivalence at dimension 2. Cone fillings, lift-affine triangles, and free-boundary shells in the circle winding chain all route through this bridge. The body is a one-line application of that equivalence inverse.
Claim. Given a continuous map $F:\Delta^2\to S^1$ (a concrete topological $2$-simplex into the circle), return the corresponding singular $2$-simplex of $S^1$ obtained by applying the inverse of Mathlib's equivalence between $C(\Delta^2,S^1)$ and the degree-$2$ component of the singular simplicial set of $\mathrm{TopCat.sphere}\,1$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves the chain-level identity that winding kills boundaries: for every continuous $F:\Delta^2\to S^1$, the alternating face sum of displacements vanishes. That identity, together with the fact that the once-around generator has winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Two presentations of a $2$-simplex coexist. A concrete topological simplex is a continuous map $F:\Delta^2\to S^1$ with $\Delta^2=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},3)$. A Mathlib singular $2$-simplex is an element of the degree-$2$ object of $\mathrm{TopCat.toSSet.obj}(\mathrm{TopCat.sphere},1)$. The face operators on the concrete side are ordinary composition with the topological face inclusions $\Delta^1\hookrightarrow\Delta^2$; on the singular side they are the simplicial $\delta_i$ of the singular set.
Mathlib supplies an objectwise equivalence identifying the two presentations. This definition is the inverse direction of that equivalence at simplex degree $2$, so every concrete continuous $F$ becomes a genuine generator of the singular chain complex.
proof idea
One-line definition: apply the inverse of TopCat.toSSetObjEquiv for TopCat.sphere 1 at SimplexCategory.mk 2 to the continuous map $F$. No further rewriting; the equivalence already identifies $C(\Delta^2,S^1)$ with the singular-set component.
why it matters
This is the universal handoff from concrete continuous $2$-simplices into $S^1$ to Mathlib singular generators. Downstream cone, linear, and backtrack constructions all build a continuous $F$ first, then call this transport: the path-cone singular simplex, the lift-affine linear singular simplex, and the triangular backtrack prism are direct wrappers. Free-boundary theorems (cone boundary shell, zero-winding specialization) and the continuous-map handoff for closed singular $1$-cycles that bound likewise feed the transported simplex into the free chain complex.
The face-commutation companion (the simplicial $\delta_i$ of the transported simplex equals the transport of the concrete face) is what lets boundary identities proved on continuous maps descend to the actual singular chain complex. In the module's larger program, that descent is required for the kills-boundaries identity and thus for the winding homomorphism on $1$-cycles that left-inverts the fundamental class. The generation/surjectivity half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ still needs prism/subdivision operators Mathlib does not yet provide; this definition is only the presentation bridge, not that missing operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.