singularWinding_singularOneSimplexOfMap
plain-language theorem explainer
Transporting a concrete continuous map Δ¹ → S¹ into Mathlib's singular simplicial set leaves its winding number unchanged. Anyone comparing the path-level winding invariant with the singular-chain version cites this equality. The proof is a two-line unfold plus the equivalence inverse law.
Claim. For every continuous map $f : \Delta^1 \to S^1$, the winding number of the corresponding singular $1$-simplex equals the concrete simplex winding of $f$: if $s$ is the image of $f$ under the standard equivalence between $C(\Delta^1,S^1)$ and the degree-$1$ singular simplices of $S^1$, then $\mathrm{wind}(s) = \mathrm{wind}(f)$.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that winding kills boundaries, the chain-level fact needed for a homology invariant.
A concrete singular $1$-simplex is a continuous map $f : \Delta^1 \to S^1$, where $\Delta^1 = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},2)$. Its simplex winding is the path displacement of the reparameterised map, divided by $2\pi$. Mathlib's singular simplicial set packages the same data as an element of the singular set in degree $1$; the bridge is the standard equivalence TopCat.toSSetObjEquiv between continuous maps out of the topological simplex and singular simplices.
singularWinding is defined by pushing a Mathlib singular $1$-simplex back across that equivalence and applying concrete simplex winding. The present lemma records that the round-trip is invisible to the invariant.
proof idea
Term-mode proof by definition chase. Unfold singularWinding and singularOneSimplexOfMap: the former applies the forward equivalence then simplexWinding, the latter is the inverse equivalence applied to $f$. The composite is equiv (equiv.symm f), which equals $f$ by Equiv.apply_symm_apply. No geometric content is used.
why it matters
This is the transport lemma that lets every later statement about Mathlib singular $1$-simplices be rewritten in the concrete $C(\Delta^1,S^1)$ language where winding is defined. The immediate parent is singularWinding_coneTerminalSide, which computes the winding of the cone's terminal-return side as minus the base path displacement; that proof is exactly one rewrite by this lemma followed by the concrete cone identity.
In the broader module arc, winding on singular $1$-simplices plus the kills-boundaries identity (simplexDisplacement_boundary) yield a homomorphism on $1$-cycles that is a left inverse to the fundamental class: the injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Surjectivity (generation by the once-around loop) remains open and needs a prism/subdivision operator Mathlib does not yet supply. No Recognition forcing-chain step (T0–T8) is touched directly; the result is pure foundational topology supporting the circle homology comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.