windingChainMap_singularOneChainFreeToChain_sum
plain-language theorem explainer
The winding chain map sends the free edge-chain of any finite family of singular 1-simplices on S¹ to the sum of their individual windings. Anyone packaging multi-edge directed cycles from cyclic edge families cites this additivity step. The argument is a short sum-congruence: both maps are linear, so the claim reduces termwise to the free-generator case.
Claim. For any $k\in\mathbb{N}$ and any family $e:\mathrm{Fin}\,k\to\{\text{singular }1\text{-simplices on }S^1\}$, if $\Phi$ is the free-to-singular chain map $C_1^{\mathrm{free}}\to C_1(S^1;\mathbb{Z})$ and $W$ is the winding chain map, then $W(\Phi(\sum_i\langle e_i\rangle))=\sum_i w(e_i)$, where $w(e_i)$ is the singular winding of the $i$-th edge.
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, yielding a homology invariant on $1$-cycles. A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. The free module on those generators maps back into the integer singular chain group $C_1(S^1;\mathbb{Z})$ by sending each free basis vector to the matching coproduct summand.
The winding chain map is the chain-level extension of singular winding (displacement divided by $2\pi$). Upstream, the free-boundary vanishing theorem shows that a cyclically connected edge family has vanishing free boundary, so its free sum is a genuine $1$-cycle. The present statement is the companion linearity fact: winding of a free sum is the sum of windings, with no connectivity hypothesis required.
proof idea
Both the free-to-chain map and the winding chain map are module homomorphisms, so each preserves finite sums. Rewrite the left-hand side by applying map_sum twice, then use Finset.sum_congr to reduce to a single free generator. Each summand is discharged by the already-proved free-generator identity that winding of the image of $\langle e_i\rangle$ equals $w(e_i)$. No homotopy or boundary computation appears.
why it matters
Downstream, directedCycleFreeTerm_of_cyclicFamily packages a cyclically connected finite edge family into a DirectedCycleFreeTerm: free edge-chain lifts to a genuine degree-$1$ cycle (by free-boundary vanishing) whose winding is an integer. This theorem supplies the additive evaluation of winding on that free sum, so the packaged term carries the correct total winding.
In the broader Recognition foundation, the module is building the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ from the covering-space winding invariant, with no axioms or sorry. Cyclic extraction is the homological half of finite-flow decomposition; once this linearity and the cyclic integrality lemma are in place, only the combinatorial task of exhibiting a cyclic family inside a balanced flow remains. The generation/surjectivity half of the isomorphism is still open (Mathlib lacks the simplicial prism operator).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.