edgeCoeff_single
plain-language theorem explainer
On the free singular 1-chain module for S¹, the coefficient of a Dirac-supported generator equals the multiplicity at that edge and vanishes elsewhere. Anyone computing pointwise coefficients of oriented walks, edge-list chains, or two-edge parallel flows cites this as the base evaluation lemma. The proof is a short reduction through Finsupp single-point evaluation.
Claim. Let $a,e$ be singular $1$-simplices on $S^1$ and $b\in\mathbb{Z}$. The edge coefficient of the free chain with sole support $a\mapsto b$, evaluated at $e$, equals $b$ if $a=e$ and equals $0$ otherwise.
background
This module lifts path-level winding and displacement from CircleWinding to singular simplices of $S^1$, and proves that displacement kills boundaries of singular $2$-simplices. That identity, with the fundamental loop sending to winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A singular $1$-simplex is an element of the singular simplicial set of $\mathrm{TopCat.sphere},1$ in degree $1$. Free $1$-chains are finitely supported integer functions on those simplices. The edge coefficient of a free chain $c$ at an edge $e$ is simply the pointwise value $c(e)$.
The present lemma records how that coefficient interacts with a single-generator (Dirac) chain: support is exactly one edge, with prescribed integer weight.
proof idea
By definition the edge coefficient is the underlying function of the Finsupp chain. Rewrite the goal as evaluation of Finsupp.single a b at $e$, apply the standard identity that a single-point Finsupp evaluates to the multiplicity on the support point and to zero off it, then close by reflexivity. No topology or winding arithmetic is used.
why it matters
Pointwise coefficient control is the bookkeeping layer under every explicit free-chain construction in the winding-chain development. Downstream, oriented cyclic chains use it to pin coefficients to $\pm 1$ on the walk and $0$ off it; forward edge-list chains use it for nonnegativity; parallel two-edge flows use it for the $+1$ and $-1$ edge values and for exact two-point support.
Those lemmas feed the chain-level winding calculus that realises the left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$. The module still lacks the generation/surjectivity half (simplicial prism or subdivision), so this is infrastructure for the injective side, not a homology isomorphism by itself. No Recognition forcing step (T0–T8) is invoked; the link is foundational topology for circle invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.