edgeCoeff_sum
plain-language theorem explainer
The edge coefficient of a finite sum of free singular 1-chains on S¹ equals the sum of the individual edge coefficients. Anyone building explicit cycle representatives or oriented walks in the CircleWindingChain module cites this linearity. The proof is a one-line appeal to additivity of Finsupp evaluation at a fixed simplex.
Claim. For any $k \in \mathbb{N}$, any family $f : \mathrm{Fin}\, k \to C_1^{\mathrm{free}}(S^1;\mathbb{Z})$ of free singular $1$-chains, and any singular $1$-simplex $e$ on $S^1$, the coefficient of $e$ in $\sum_i f_i$ equals $\sum_i$ of the coefficient of $e$ in $f_i$.
background
The module CircleWindingChain lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$, aiming at the chain-level identity that winding kills boundaries. Free $1$-chains live in the free $\mathbb{Z}$-module on actual singular $1$-simplices of TopCat.sphere 1.
The edge coefficient of a free chain $c$ at a singular $1$-simplex $e$ is simply the value of the underlying finitely supported function at $e$. That evaluation is an additive group homomorphism $C_1^{\mathrm{free}} \to \mathbb{Z}$, so it automatically intertwines finite sums. The present lemma records that fact for finite indexed families, which is the form needed when assembling oriented cyclic walks from edge-by-edge contributions.
proof idea
Rewrite both sides via the definition of edge coefficient as Finsupp.applyAddHom e applied to the chain. The claim is then exactly map_sum for that additive homomorphism over Finset.univ. No case analysis on supports or simplices is required.
why it matters
Downstream, edgeCoeff_orientedCyclicChain uses this distributivity to compute the pointwise coefficient of an oriented closed walk: on the walk it is the sign-unit of the underlying flow, and off the walk it is zero. That coefficient formula is part of the explicit free-chain toolkit supporting the winding homomorphism on $1$-cycles.
In the module narrative, winding on singular $1$-simplices plus the kills-boundaries identity give a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Finite-sum linearity of coefficients is bookkeeping infrastructure for those cycle constructions; it does not itself touch the T0–T8 forcing chain or the Recognition Composition Law, but it sits inside the foundation layer that makes the circle's homology comparison rigorous without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.