singularWinding_loop_integral
plain-language theorem explainer
A singular 1-simplex on S¹ whose two simplicial faces agree has integer winding number. Anyone building the integer-valued winding homomorphism on singular 1-cycles cites this as the generator-level integrality step toward cycleWinding_integral. The proof reduces to the continuous-map version by transporting equal faces to equal endpoints of the underlying path.
Claim. Let $s$ be a singular $1$-simplex of $S^1$ in the singular simplicial set of $\mathrm{TopCat.sphere}\,1$. If the two face maps agree, $\delta_0 s = \delta_1 s$, then the winding number of $s$ is an integer: there exists $k\in\mathbb{Z}$ with $\mathrm{winding}(s)=k$ as a real.
background
This module lifts the path-level winding invariant of CircleWinding to singular simplices of $S^1$ and proves that winding kills boundaries, the fact that makes it a homology invariant. Displacement of a singular $1$-simplex is $2\pi$ times winding, obtained by reparameterizing $\Delta^1$ to the unit interval and taking path displacement.
A SingularOneSimplex is an object of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. The winding singularWinding is defined by transporting that object through TopCat.toSSetObjEquiv and applying the continuous-map winding simplexWinding.
Upstream, simplexWinding_loop_integral already says a continuous $1$-simplex with equal endpoints has integer winding (via pathWinding_loop_integral). The face lemmas singularOneSimplex_delta_zero_endpoint and singularOneSimplex_delta_one_endpoint identify $\delta_0 s$ and $\delta_1 s$ with the terminal and initial endpoints of the transported map.
proof idea
One-line reduction after a short endpoint calculation. Unfold singularWinding to simplexWinding of the transported continuous map, then apply simplexWinding_loop_integral.
The remaining obligation is that the two endpoints of the transported map agree. Congruence of the equal-face hypothesis through TopCat.toSSetObjEquiv and evaluation at the unique vertex of $\Delta^0$ gives equality of the transported $0$-simplices. A three-step calc then chains singularOneSimplex_delta_zero_endpoint, that point equality, and singularOneSimplex_delta_one_endpoint to identify the $\mathrm{vertex},1$ and $\mathrm{vertex},0$ values of the transported $1$-simplex.
why it matters
Generator-level integrality for the winding homomorphism on singular $1$-cycles: closed singular edges (equal faces) contribute integer winding, which is the input needed for cycleWinding_integral and the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Downstream, ClosedSingularOneCycleTerm packages a singular $1$-simplex with equal faces and a $\mathbb{Z}$-coefficient as one summand in a closed-generator decomposition; this theorem supplies the integrality of that summand's winding. Likewise cyclicSingularEdgeListTerm_of_loop treats a self-closed singular edge as an already-cyclic edge-list term in the finite-flow extraction argument, again under the equal-face hypothesis.
Together with the kills-boundaries identity simplexDisplacement_boundary and pathWinding_fundamentalLoop (generator maps to $1$), this is the left-inverse half of the integer comparison map. The converse generation half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet provide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.