simplexWinding_fundamental
plain-language theorem explainer
The winding number of the once-around fundamental singular 1-simplex on S¹ equals 1. Anyone establishing the left-inverse half of H₁(S¹;ℤ) ≅ ℤ via the covering-space winding invariant cites this. The proof rewrites normalized winding as displacement over 2π, inserts the full-turn displacement identity, and simplifies the quotient.
Claim. Let $f:\Delta^1\to S^1$ be the fundamental once-around singular $1$-simplex (parameterized by the second barycentric coordinate, endpoints at angles $0$ and $2\pi$). Its winding number, defined as displacement divided by $2\pi$, equals $1$.
background
This module lifts the path-level winding and displacement invariant from continuous paths on $S^1$ to singular $1$-simplices of $\mathrm{TopCat.sphere},1$. Displacement of a singular $1$-simplex is the real number obtained by reparameterizing the standard $1$-simplex $\Delta^1$ to the unit interval and taking path displacement; winding is that quantity normalized by one full turn, i.e. divided by $2\pi$.
The fundamental singular $1$-simplex is the continuous once-around map from the topological standard $1$-simplex into the exact sphere object: the second barycentric coordinate runs the angle from $0$ to $2\pi$. An upstream theorem already records that its displacement equals one full turn, $2\pi$.
Together with the chain-level identity that displacement kills boundaries of singular $2$-simplices, the normalization-to-$1$ fact supplies a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class.
proof idea
Short tactic proof. Unfold the definition of simplex winding (displacement divided by $2\pi$). Rewrite the numerator via the upstream identity that the fundamental simplex has displacement $2\pi$. Discharge $2\pi\neq 0$ by positivity and finish with field simplification, yielding $1$.
why it matters
This is the normalization step that makes the winding invariant a left inverse to the fundamental class on singular $1$-simplices. Downstream it is re-packaged as the statement that the singular-set winding of the fundamental sphere $1$-simplex equals $1$, the form used when comparing against Mathlib singular chains.
In the module's program this is half of the split-injective side of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding sends the once-around generator to $1$, and (with the kills-boundaries identity) descends to homology. The converse generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) remains open here, pending a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No Recognition-Science forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked; the result is pure topological foundation for later circle-valued recognition arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.