geodesicOneSimplex_zero_twoPi
plain-language theorem explainer
The geodesic singular 1-simplex from angle 0 to 2π equals the fundamental once-around map Δ¹ → S¹. Anyone pinning the generator of H₁(S¹) to the geodesic lift cites this identification. The proof is pointwise: expand the geodesic formula, cancel the zero endpoint by ring, and match the fundamental map's barycentric parameterization.
Claim. The geodesic singular $1$-simplex from $0$ to $2\pi$ equals the fundamental once-around continuous map $\Delta^1 \to S^1$ that sends a barycentric point $x$ to the point on the circle at angle $2\pi \cdot x_1$.
background
The module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries. That chain-level fact, together with the once-around generator evaluating to winding 1, yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$.
A geodesic singular 1-simplex from lifts $a$ to $b$ is the continuous map $\Delta^1 \to S^1$ sending $x$ to the trig embedding of the linear path $(1-x_1)a + x_1 b$ in the universal cover $\mathbb{R}$. The fundamental once-around map is the special case that uses only the second barycentric coordinate: angle $2\pi \cdot x_1$, so endpoints land at $0$ and $2\pi$.
The present statement equates those two continuous maps when $(a,b)=(0,2\pi)$.
proof idea
Pointwise extensionality on $\Delta^1$. Unfold the geodesic evaluation lemma to get $\mathrm{trig}((1-x_1)\cdot 0 + x_1\cdot 2\pi)$. A one-line ring rewrite simplifies the linear combination to $2\pi \cdot x_1$. The resulting term is definitionally the fundamental once-around map, so rfl closes.
why it matters
This is the continuous-map identification that the singular-simplex wrapper immediately rewrites into: the singular 1-simplex of the geodesic $0\to 2\pi$ is the fundamental singular 1-simplex of the sphere. That parent theorem is the bridge from geodesic language to the singular-chain generator used by the winding homomorphism.
In the module's larger story, the winding invariant on 1-cycles is a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Matching the geodesic generator to the fundamental simplex is the concrete normalization step that makes that comparison map send the geometric once-around class to 1. The converse generation half still needs a simplicial prism/subdivision operator that Mathlib singular homology does not yet supply; this lemma does not touch that open half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.