edgeCoeff_zsmul
plain-language theorem explainer
Integer scalar multiplication on a free singular 1-chain multiplies every edge coefficient by the same integer. Anyone building or peeling cyclic free chains on S¹ cites this when moving scalars through coefficient extraction. The proof is definitional: both sides reduce to the free-module action on the underlying function.
Claim. For every integer $n$, every free singular $1$-chain $c$ on $S^1$, and every singular $1$-simplex $e$, the coefficient of $e$ in $n\cdot c$ equals $n$ times the coefficient of $e$ in $c$.
background
The module works at the level of singular chains on the topological circle $S^1=\mathrm{TopCat.sphere},1$. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$ in the singular simplicial set; the free $\mathbb{Z}$-module on those simplices is the explicit $C_1$ object used here.
Coefficient extraction is the evaluation map of that free module: the coefficient of an edge $e$ in a free chain $c$ is simply $c(e)\in\mathbb{Z}$. Scalar multiplication $n\cdot c$ is the module action, so the claim is the usual $\mathbb{Z}$-linearity of evaluation at a fixed basis element.
Upstream, the same free-module setup supports the winding/displacement invariant lifted from paths to singular $1$-simplices, and the kills-boundaries identity that makes winding a homology invariant (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$).
proof idea
One-line definitional proof. Unfold coefficient extraction on both sides: the left-hand side is the free-module action applied to $c$ and then evaluated at $e$, which is definitionally $n$ times $c(e)$. Close by rfl.
why it matters
Needed whenever free $1$-chains are scaled and then read edgewise. Downstream, the cyclic edge-list term structure records a global integer coefficient times a listed edge sum; this lemma lets that global scalar pass through coefficient extraction. It is also used in the support-cardinality inequality for exact cyclic peel: scaling a sign-selected oriented closed walk by the minimum absolute coefficient strictly shrinks support, and the scalar-coefficient identity is the bookkeeping step that cancels the minimum-coefficient edge without introducing new support.
In the module's larger program this is elementary free-module hygiene on the way to the winding homomorphism that left-inverts the fundamental class of $S^1$. It does not itself touch the open generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle), which still needs a simplicial prism or subdivision operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.