simplexDisplacement_fundamental
plain-language theorem explainer
The displacement of the once-around fundamental singular 1-simplex on S¹ equals one full turn 2π. Anyone building the winding homomorphism on singular 1-chains cites this as the generator evaluation. The proof is a three-step rewrite: unfold the simplex displacement, identify the reparameterised path with the fundamental loop, and apply the known path-level displacement.
Claim. Let $f_{\mathrm{fund}}:\Delta^1\to S^1$ be the continuous once-around singular $1$-simplex that sends the second barycentric coordinate $t$ to the point at angle $2\pi t$. Its displacement (angular travel of any continuous lift) equals $2\pi$.
background
This module lifts the path-level displacement invariant of CircleWinding to singular $1$-simplices of the topological circle $S^1=\mathrm{TopCat.sphere},1$. Displacement of a singular $1$-simplex $f:C(\Delta^1,S^1)$ is defined by reparameterising the standard $1$-simplex $\Delta^1$ onto the unit interval and taking the path displacement of the resulting loop; the result is lift-independent and equals $2\pi$ times the integer winding number.
The fundamental singular $1$-simplex is the continuous map that evaluates the second barycentric coordinate against the trigonometric embedding of the circle, so its endpoints sit at angles $0$ and $2\pi$. Upstream, the path-level theorem already records that the once-around fundamental loop has displacement exactly $2\pi$. A companion identification shows that the unit-interval reparameterisation of this fundamental simplex is definitionally that same fundamental loop.
The local goal is the chain-level statement that displacement kills boundaries of singular $2$-simplices, which together with the generator evaluation yields a left inverse to the fundamental class in $H_1(S^1;\mathbb{Z})$.
proof idea
Pure rewrite proof in three steps. Unfold the definition of simplex displacement, which is path displacement of the unit-interval reparameterisation. Replace that reparameterisation of the fundamental singular simplex by the fundamental once-around loop, using the identification theorem that equates them pointwise via the barycentric-coordinate formula. Finish by invoking the path-level result that the fundamental loop has displacement $2\pi$. No further arithmetic or continuity arguments are required.
why it matters
This is the generator evaluation that makes the simplex-level winding a left inverse to the fundamental class. The immediate parent is the normalised statement that the winding number of the fundamental singular $1$-simplex equals $1$, obtained by dividing the present identity by $2\pi$.
Together with the sibling theorem that displacement vanishes on boundaries of singular $2$-simplices, it supplies the "split-injective" half of the classical isomorphism $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module documentation is explicit that the converse (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial prism or subdivision operator not yet in Mathlib, so this lemma closes only the evaluation side of the comparison map.
In the broader Recognition foundation stack the result anchors the topological circle as a calibrated generator before any physical forcing (T5–T8) is invoked; it uses no project-local circle replacements and no axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.