closedSingularOneCycle_bounds_of_zero_singularWinding
plain-language theorem explainer
Any closed singular 1-simplex on S¹ whose singular winding vanishes is a boundary in the integer singular chain complex. Homology workers cite it when killing zero-winding generators without leaving Mathlib's singular simplicial set. The proof transports the simplex to continuous-map form, applies the cone-over-lifted-path theorem, and pulls the bounding 2-chain back via injectivity of the cycles inclusion.
Claim. Let $s$ be a singular $1$-simplex of $S^1$ whose two face maps agree (so $s$ is closed), and suppose the singular winding of $s$ is zero. Then there exists a degree-$2$ integer singular chain $b$ on $S^1$ whose image under the cycles map equals the $1$-cycle generated by $s$.
background
The module lifts path-level winding on $S^1$ to singular simplices of TopCat.sphere 1. Displacement (equivalently $2\pi$ times winding) is assigned to each continuous map $\Delta^1\to S^1$ by reparameterizing to the unit interval; the key identity is that the alternating face sum of displacements on any singular $2$-simplex vanishes (winding kills boundaries).
A singular $1$-simplex here is an object of the Mathlib singular simplicial set of $S^1$. Closed means the two face maps $\delta_0 s=\delta_1 s$. The cycle constructor packages such an $s$ as a morphism into the degree-$1$ cycles of the integer singular chain complex of $S^1$. Singular winding is the simplex winding of the underlying continuous map.
Upstream, the continuous-map form already proves that a closed edge with zero simplex winding bounds by an explicit cone over its lifted path. The present statement is the consumer-facing version that works directly with Mathlib singular simplices.
proof idea
Translate $s$ across the singular-set equivalence to a continuous map $f:\Delta^1\to S^1$. Face equality of $s$ becomes endpoint equality of $f$ by comparing $\delta_0$ and $\delta_1$ endpoints via the $0$-simplex equivalence. Zero singular winding rewrites as zero simplex winding of $f$.
Apply the upstream cone theorem for continuous maps to obtain a bounding $2$-chain $b$. Recover $s$ from $f$ by the inverse equivalence, then show the two closed-cycle morphisms agree after composing with the cycles inclusion, using injectivity of that inclusion (mono in ModuleCat). Rewrite and conclude.
why it matters
This is the actual-singular-simplex form of the zero-winding cone theorem: consumers no longer need the $C(\Delta^1,S^1)$ presentation. It feeds the scalar extension that any integer multiple of a zero-winding closed singular generator bounds.
In the module's program, winding is a left inverse to the fundamental class (split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Bounding zero-winding closed generators is the local step that lets zero-winding cycles die in homology. The chain complex is the exact object whose degree-$1$ homology is the strict T8 target in the forcing chain (three spatial dimensions via the circle's first homology).
The generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma closes only the cone side for single closed edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.