cycleWinding_closedSingularOneCycle
plain-language theorem explainer
For a closed singular 1-simplex on S¹ and an integer coefficient n, the winding of the cycle it generates equals n times the simplex winding. Anyone computing the winding homomorphism on generator cycles cites this. The proof unfolds the cycle-winding composite, cancels the cycles inclusion against the lift, and reduces to the span-singleton evaluation of the winding chain map.
Claim. Let $s$ be a singular $1$-simplex of $S^1$ whose two faces agree (so $s$ is closed). For any integer coefficient $n\in\mathbb{Z}$, the winding of the degree-$1$ cycle generated by $s$ with coefficient $n$ equals $n$ times the winding number of $s$: $\mathrm{wind}([n]\cdot s)=n\cdot\mathrm{wind}(s)$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1=\mathrm{TopCat.sphere},1$, and proves that winding kills boundaries, so it descends to a homology invariant. The target is the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular one-simplex is an element of the singular simplicial set of $S^1$ in degree $1$. It is closed when its two face maps agree ($\delta_0 s=\delta_1 s$). From such an $s$ one builds closedSingularOneCycle: the actual cycle object in the integer singular chain complex obtained by lifting the generator chain into the cycles subobject.
cycleWinding evaluates winding on a degree-$1$ cycle by including into $C_1(S^1;\mathbb{Z})$ and applying the winding chain map. singularWinding is the concrete winding number of the underlying singular simplex (via reparameterization to a path and path displacement $/2\pi$).
proof idea
Term-mode reduction, not a deep geometric argument. Unfold cycleWinding to the composite of the cycles inclusion with the winding chain map. Rewrite the left-hand side as the hom applied to closedSingularOneCycle s hfaces composed with that composite. The key rewrite is HomologicalComplex.liftCycles_i_assoc, which cancels the lift-into-cycles against the cycles inclusion, leaving the generator chain map applied to $n$. Then windingChainMap_ι identifies that map with the span-singleton of singularWinding s, and LinearMap.toSpanSingleton_apply yields the scalar product $(n:\mathbb{R})\cdot\mathrm{singularWinding},s$.
why it matters
This is the evaluation identity that makes generator cycles computable under the winding homomorphism: closed singular edges contribute exactly coefficient times simplex winding. Downstream it feeds ClosedSingularOneCycleTerm, the finite-sum term type in closed-generator decompositions of cycles, and cyclicSingularEdgeListTerm_of_loop, which treats a single closed singular edge as an already-cyclic edge-list term (no successor search).
In the module's program this is a brick in the left-inverse half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: winding on $1$-cycles is a left inverse to the fundamental class, using also pathWinding_fundamentalLoop (once-around maps to $1$) and the kills-boundaries identity simplexDisplacement_boundary. The converse generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. Framework-wise this sits in the Foundation circle-homology chain supporting the strict T8 spatial-dimension target via $H_1(S^1)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.