fundamentalSphereOneSingularOneSimplex
plain-language theorem explainer
Defines the once-around singular 1-simplex of $S^1$ inside Mathlib's singular simplicial set $\mathrm{Sing}(S^1)$. Anyone computing $H_1(S^1;\mathbb{Z})$ or comparing winding chains cites this as the geometric generator. Construction is a one-line transport of the continuous once-around path across $\mathrm{TopCat.toSSetObjEquiv}$.
Claim. Let $\sigma_1$ be the continuous once-around path $\Delta^1\to S^1$ sending the second barycentric coordinate $t$ to the point at angle $2\pi t$. The fundamental singular 1-simplex is the image of $\sigma_1$ under the canonical equivalence identifying $C(\Delta^1,S^1)$ with the set of 1-simplices of $\mathrm{Sing}(S^1)$.
background
The module builds the once-around singular 1-simplex inside the actual singular simplicial set TopCat.toSSet.obj (TopCat.sphere 1) and shows its two faces meet at a fixed basepoint. That object is the geometric input to the later integer singular chain complex of $S^1$.
Upstream, fundamentalCirclePathMap is the continuous map $\Delta^1_{\mathbb{R}}\to S^1$ given by $x\mapsto(\cos(2\pi x_1),\sin(2\pi x_1))$, so endpoints land at angles $0$ and $2\pi$. Mathlib's TopCat.toSSetObjEquiv identifies such continuous maps with 1-simplices of the singular simplicial set; the present definition simply applies the inverse of that equivalence.
Face maps on singular simplices are the usual compositions with the topological face inclusions $\Delta^{n}\hookrightarrow\Delta^{n+1}$ (skipping a vertex). Those faces are proved equal to the constant basepoint simplex in sibling lemmas.
proof idea
Pure definitional transport: apply the inverse of TopCat.toSSetObjEquiv at the 1-simplex level of $S^1$ to the already-constructed continuous path fundamentalCirclePathMap. No tactics; the body is that single application of .symm.
why it matters
This is the geometric generator candidate for the strict $H_1(S^1;\mathbb{Z})$ computation. Downstream face lemmas show $\delta_0$ and $\delta_1$ both equal the constant basepoint 0-simplex, hence the two faces coincide (fundamentalSphereOneSingularOneSimplex_faces_eq). That equal-faces fact lifts to the chain-level statement that the corresponding degree-1 singular chain has vanishing boundary, so it is a 1-cycle in sphereOneSingularIntChainComplex.
The same simplex is the coproduct summand selected by fundamentalSphereOneSingularOneChain, and winding-chain comparisons identify free geodesic chains with integer multiples of this fundamental cycle. In the Recognition forcing chain the circle's first homology is the algebraic witness underlying the eight-tick octave and the $D=3$ spatial step (T7–T8); this definition supplies the concrete singular generator those later arguments quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.