singularWinding_fundamentalSimplex
plain-language theorem explainer
The winding number of the once-around fundamental singular 1-simplex on S¹ equals 1. Anyone proving the split-injective half of H₁(S¹;ℤ) ≅ ℤ via the winding chain map cites this evaluation. The argument transports the singular simplex through the TopCat-to-sSet equivalence and reduces to the already-proved path-level fundamental winding identity.
Claim. The winding number of the fundamental singular $1$-simplex on $S^1$ equals $1$. Writing $s$ for the once-around generator in the singular simplicial set of the topological circle, one has $\mathrm{winding}(s)=1$.
background
This module lifts the path-level winding invariant on the circle to singular simplices of $\mathrm{TopCat.sphere},1$, then proves that the resulting assignment kills boundaries, so it descends to homology. Concretely, every continuous map $f:\Delta^1\to S^1$ is reparameterized to a path on the unit interval; its displacement (equal to $2\pi$ times winding) is recorded by $\mathrm{simplexDisplacement}$, and $\mathrm{simplexWinding}$ is that quantity divided by $2\pi$.
The fundamental singular $1$-simplex is built from the continuous once-around map that sends the second barycentric coordinate $t$ of the standard $1$-simplex to the point at angle $2\pi t$ on $S^1$. The singular-set version is obtained by transporting that map across the equivalence between continuous maps out of the topological simplex and $1$-simplices in $\mathrm{TopCat.toSSet}$.
Upstream, the path-level statement already records that the winding of this once-around map is exactly $1$. The present theorem is the same numerical claim stated on the singular-simplex side of the equivalence.
proof idea
Unfold the definition of singular winding: it applies ordinary simplex winding after transporting the singular $1$-simplex across $\mathrm{TopCat.toSSetObjEquiv}$. The transport of the fundamental singular simplex is definitionally the fundamental circle path map (by $\mathrm{apply_symm_apply}$ on that equivalence). The goal therefore reduces exactly to the upstream identity that simplex winding of the fundamental path map equals $1$, which is invoked as a one-line exact.
why it matters
Downstream, the winding chain map theorem uses this evaluation to show that the chain map sends the fundamental singular $1$-cycle to the generator $1\in\mathbb{R}$. Paired with the already-proved fact that the same chain map annihilates all degree-$2$ boundaries, one obtains a left inverse to the integer comparison map $\mathbb{Z}\to H_1(S^1;\mathbb{Z})$. That is precisely the split-injective half of the classical isomorphism: the fundamental class has infinite order.
In the Recognition Science foundation layer this supplies the covering-space half of the circle's first homology without axioms or sorry. The converse generation statement (every $1$-cycle homologous to an integer multiple of the fundamental cycle) remains open and needs a simplicial prism or subdivision operator that Mathlib's singular homology does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.