singularOneSimplexOfMap_oneSimplexOfPath_singularEdgePath
plain-language theorem explainer
Round-tripping a singular 1-simplex on S¹ through the unit-interval path reading and back yields the original generator. Anyone wiring chain-level edges to path-level winding or displacement cites this. The proof is a short injectivity argument via the singular-set equivalence, plus the concrete simplex–path inverse.
Claim. For every singular $1$-simplex $s$ in the singular simplicial set of $S^1$, converting $s$ to a continuous path $I\to S^1$ via the standard $\Delta^1\simeq I$ parameterisation and then reading that path back as a singular $1$-simplex recovers $s$.
background
The module lifts path-level winding and displacement on $S^1$ to singular simplices and proves that displacement vanishes on boundaries, so it descends to a homology invariant. A SingularOneSimplex is an actual $1$-simplex in Mathlib's singular simplicial set of TopCat.sphere 1. Concrete continuous maps $C(\Delta^1,S^1)$ are related to those generators by the equivalence TopCat.toSSetObjEquiv.
singularEdgePath reads a chain-level singular edge as a unit-interval path $I\to S^1$ (the bridge to pathDisplacement / winding). oneSimplexOfPath sends a path back to a concrete $1$-simplex via $\Delta^1\simeq I$. singularOneSimplexOfMap embeds a concrete continuous $1$-simplex into the singular simplicial set. Upstream, oneSimplexOfPath_oneSimplexPath already states that path-to-simplex-to-path recovers a concrete simplex.
proof idea
Term-mode proof by injectivity of the singular-set equivalence on $1$-simplices of $S^1$. Unfold the two conversion maps (singularOneSimplexOfMap, singularEdgePath), cancel the equivalence with Equiv.apply_symm_apply, then finish with the already-proved concrete inverse oneSimplexOfPath_oneSimplexPath. No homotopy or winding arithmetic is used; it is pure reparameterisation bookkeeping.
why it matters
This identity legitimates treating singular edges interchangeably as unit-interval paths when defining oriented edges and their initial/terminal vertices. Downstream it is used in the OrientedSingularEdge structure (a singular edge plus traversal orientation), which packages chain generators for the winding homomorphism on $1$-cycles.
In the module narrative, that homomorphism is the left inverse to the fundamental class: the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, paired with pathWinding_fundamentalLoop and the kills-boundaries identity simplexDisplacement_boundary. The generation/surjectivity half still needs a simplicial prism or subdivision operator not yet in Mathlib. The result is pure foundation topology; it does not itself invoke RS forcing steps T0–T8, but it underwrites the circle winding used in the eight-tick and phase-structure story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.