singularOneSimplexOfMap_constantOneSimplex
plain-language theorem explainer
Converting the constant continuous edge at a point p on S¹ into Mathlib's singular 1-simplex yields exactly the constant singular 1-simplex at p. Anyone equating concrete ContinuousMap edges with singular-set edges cites this. The proof is a short injectivity argument through TopCat.toSSetObjEquiv after unfolding both sides.
Claim. For every point $p$ on $S^1$, the singular $1$-simplex associated to the constant continuous map $\Delta^1\to S^1$ with value $p$ equals the constant singular $1$-simplex at $p$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of TopCat.sphere 1, and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\partial_0 F)-\mathrm{disp}(\partial_1 F)+\mathrm{disp}(\partial_2 F)=0$. That identity, with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
SphereOne is the carrier of the exact Mathlib object TopCat.sphere 1. A concrete OneSimplex is a continuous map $C(\Delta^1,S^1)$. The constant edge at $p$ is ContinuousMap.const on the standard $1$-simplex. Mathlib's singular simplicial set stores $1$-simplices via the equivalence TopCat.toSSetObjEquiv; singularOneSimplexOfMap is the inverse direction of that equivalence, and constantSingularOneSimplex p is the same inverse applied to the constant map.
proof idea
Term-mode proof by injectivity of the forward map of TopCat.toSSetObjEquiv at dimension $1$. Unfold the three definitions: both sides become the inverse-equiv applied to the same constant continuous map. Rewrite with Equiv.apply_symm_apply so the two images under the forward map agree, hence the singular simplices agree.
why it matters
Bookkeeping bridge between the concrete ContinuousMap presentation of edges and Mathlib's free singular chains. Downstream, geodesicFreeChain_self_bounds rewrites a degenerate geodesic (equal endpoints) through this identity to show it is the boundary of a constant $2$-simplex. The same conversion appears in the triangular backtrack prism identity singularTwoBoundaryFree_freeMk_pathBacktrack, whose boundary is reverse path minus constant initial edge plus original path. Those prism and geodesic facts feed the chain-level winding calculus that realizes the "kills boundaries" half of the $H_1(S^1)$ comparison. No Recognition forcing step (T0–T8) is invoked here; the lemma is pure singular-homology infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.