pathBacktrackSingularTwoSimplex
plain-language theorem explainer
Associates to any continuous path on the circle the singular 2-simplex of its triangular backtrack prism. Homology workers cite it when building free chains whose boundary is reverse-path minus constant edge plus original path. The body is a one-line packaging of the concrete continuous map into Mathlib's singular simplicial set.
Claim. Given a continuous path $\gamma : I \to S^1$, form the singular $2$-simplex in the singular simplicial set of $S^1$ corresponding to the triangular backtrack prism of $\gamma$ (the continuous map $\Delta^2 \to S^1$ sending $x$ to $\gamma$ of the first barycentric coordinate).
background
The module lifts path-level winding and displacement on $S^1$ to singular simplices and proves that displacement kills boundaries: for every singular $2$-simplex $F$, the alternating face sum of displacements vanishes. That identity, with the generator evaluation on the once-around loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
SphereOne is the carrier of Mathlib's TopCat.sphere 1. A singular $2$-simplex is an element of the degree-$2$ object of the singular simplicial set of that sphere. The upstream map pathBacktrackMap builds the concrete continuous prism $x \mapsto \gamma(x_1)$ on the standard $2$-simplex; its three faces are the reversed path, the constant initial edge, and the original path. singularTwoSimplexOfMap transports such a continuous map into the actual singular simplex via the toSSet equivalence.
proof idea
One-line definitional wrapper: apply singularTwoSimplexOfMap to pathBacktrackMap γ. No further tactics or lemmas; the continuous prism is already assembled upstream, and the equivalence packages it as a singular $2$-simplex.
why it matters
Feeds the free generator used by singularTwoBoundaryFree_freeMk_pathBacktrack, which states that the singular boundary of this prism is reverse path minus constant initial edge plus original path. That identity is the chain-level witness for cancelling a path against its reverse in free singular chains, the elementary move needed when reducing $1$-cycles toward multiples of the fundamental loop.
It also appears in the OrientedSingularEdge apparatus for oriented edge bookkeeping. In the module's larger program this is scaffolding for the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding already kills boundaries and hits the generator; prism and subdivision operators (not yet in Mathlib singular homology) are what remain for surjectivity. No Recognition forcing-chain step (T0–T8) is touched directly; the declaration is pure circle homology infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.