singularOneSimplexOfMap_geodesic_zero_twoPi
plain-language theorem explainer
The geodesic singular 1-simplex from lift 0 to 2π, viewed as a Mathlib singular simplex on S¹, equals the once-around fundamental singular 1-simplex. Anyone identifying the geometric generator of H₁(S¹) with the explicit geodesic free chain cites this. The proof rewrites by the path-map equality for that geodesic, then closes by definitional equality of the singular-simplex embedding.
Claim. The image of the geodesic singular $1$-simplex from lift value $0$ to $2\pi$ under the embedding of continuous maps $C(\Delta^1,S^1)$ into Mathlib's singular simplicial set equals the once-around fundamental singular $1$-simplex on $S^1$.
background
The module lifts path-level winding and displacement on the circle to singular simplices of $S^1$, and proves that displacement kills boundaries, so winding descends to a homology invariant. That invariant is a left inverse to the fundamental class, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A geodesic singular $1$-simplex from lifts $a$ to $b$ is the projection of the straight line in the universal cover $\mathbb{R}\to S^1$. The once-around fundamental singular $1$-simplex is the geometric generator candidate for the later $H_1$ computation. The map that turns a concrete continuous $1$-simplex into Mathlib's singular simplex is the inverse of the standard TopCat.toSSet equivalence on degree $1$.
Upstream, the geodesic from $0$ to $2\pi$ is already identified with the fundamental once-around continuous path map on $\Delta^1$. The present statement lifts that identification from continuous maps to singular simplices.
proof idea
One short rewrite-and-rfl argument. First apply the upstream equality that the geodesic $0\to 2\pi$ equals the fundamental continuous path map on $\Delta^1$. After that rewrite, both sides are the singular-simplex embedding of the same continuous map, so definitional equality finishes the proof.
why it matters
This is the bridge from the continuous geodesic generator to the singular-simplex generator used in free chains. Downstream, the geodesic free chain $0\to 2\pi$ is identified with the free module generator on the fundamental singular $1$-simplex by unfolding the free-chain construction and rewriting with this equality.
In the module's program, that identification feeds the winding homomorphism on $1$-cycles as a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No Recognition forcing-chain step (T0–T8) is invoked here; the result is pure circle homology scaffolding for later RS geometric arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.