singularOneSimplexOfMap
plain-language theorem explainer
Converts a continuous map Δ¹ → S¹ into Mathlib's native singular 1-simplex of the circle. Anyone building winding or boundary arguments on singular chains of S¹ cites this bridge. The body is just the inverse of Mathlib's TopCat-to-simplicial-set equivalence at dimension one.
Claim. Given a continuous map $f : \Delta^1 \to S^1$ (a concrete singular $1$-simplex presented as a map out of the standard topological $1$-simplex), return the corresponding point of the singular simplicial set of $S^1$ in degree $1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact that makes winding a homology invariant. Concrete $1$-simplices are written as continuous maps $C(\Delta^1,S^1)$ with $\Delta^1 = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$. Mathlib's singular chains live in the simplicial set TopCat.toSSet.obj (TopCat.sphere 1), so the two presentations must be identified.
OneSimplex is the continuous-map presentation; SingularOneSimplex is the actual degree-$1$ object of that simplicial set. Mathlib supplies a natural equivalence TopCat.toSSetObjEquiv between continuous maps out of the topological simplex and simplicial-set simplices; this definition is the inverse direction at $n=1$.
proof idea
One-line definition: apply the inverse of Mathlib's equivalence TopCat.toSSetObjEquiv (TopCat.sphere 1) (op (SimplexCategory.mk 1)) to the continuous map $f$. No further proof obligations; noncomputable only because the ambient singular-set machinery is.
why it matters
This is the standard handoff from the continuous-map language used for winding (simplexWinding, cone fillings) into Mathlib's singular chain complex. Downstream, every closed-edge bounding theorem routes through it: closedSingularOneCycle_bounds_of_cone_map transports a continuous $2$-simplex filler after converting the base edge; the zero-winding cone family (closedSingularOneCycle_bounds_of_zero_winding_coneCirclePoint, ..._of_zero_singularWinding, generation form) and geodesicFreeChain likewise need the Mathlib simplex to state face equalities and boundaries. Together with simplexDisplacement_boundary (winding kills boundaries) and the fundamental-loop normalization, this supports the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Surjectivity still needs a prism/subdivision operator Mathlib does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.