fundamentalCirclePathMap
plain-language theorem explainer
Continuous once-around path from the topological standard 1-simplex into the exact circle object S¹, driven by the second barycentric coordinate so the endpoints sit at angles 0 and 2π. Anyone building the geometric generator of singular H₁(S¹) or the winding chain cites this map. Continuity is a short composition of the trigonometric circle parametrization with a continuous multiple of that barycentric coordinate.
Claim. There is a continuous map $f\colon \Delta^1_{\mathrm{top}}\to S^1$ (into Mathlib's exact sphere object) defined by $f(x)=\gamma(2\pi\, x_1)$, where $\gamma$ is the standard trigonometric parametrization of the circle and $x_1$ is the second barycentric coordinate on the standard 1-simplex. Endpoints therefore evaluate at angles $0$ and $2\pi$.
background
The module builds the once-around singular 1-simplex inside the actual singular simplicial set of Mathlib's sphere object TopCat.sphere 1, and later shows its two faces meet at a fixed basepoint.
The standard topological 1-simplex $\Delta^1$ is realized as stdSimplex ℝ (Fin 2). Points are barycentric coordinates $(x_0,x_1)$ with $x_0+x_1=1$ and $x_i\ge 0$. The second coordinate $x_1$ runs from $0$ at one vertex to $1$ at the other, so the angle $2\pi x_1$ runs once around the circle.
Upstream, trigCirclePoint is the once-around trigonometric map $\mathbb{R}\to S^1$ into the exact sphere object, and continuous_trigCirclePoint records that this parametrization is continuous. The present definition packages that parametrization on $\Delta^1$ as a continuous map of topological spaces.
proof idea
The data field is immediate: send $x$ to trigCirclePoint of $2\pi$ times the second barycentric coordinate. Continuity is a one-step composition: apply continuous_trigCirclePoint.comp to the scalar map $x\mapsto 2\pi, x_1$. That scalar map is continuous because coordinate projection on the ambient $\mathrm{Fin},2\to\mathbb{R}$ (via continuous_apply 1 after continuous_subtype_val) is continuous, and multiplication by the constant $2\pi$ preserves continuity.
why it matters
This is the geometric path that becomes the fundamental singular 1-simplex of the circle: the sibling fundamentalSphereOneSingularOneSimplex is exactly this map transported across TopCat.toSSetObjEquiv. Face lemmas then show both $\delta_0$ and $\delta_1$ land on the constant basepoint 0-simplex, so the simplex is a closed loop in the singular chain complex.
Downstream in CircleWindingChain, the geodesic from $0$ to $2\pi$ is identified with this map; its path reading is the fundamental once-around loop; its displacement is one full turn $2\pi$; and the singular winding number of the fundamental simplex is $1$. It is therefore the concrete generator candidate for the later $H_1(S^1)$ computation in the Recognition foundation stack (circle as the geometric carrier of the eight-tick/octave period structure).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.