edgeCoeff_freeMk_self
plain-language theorem explainer
On the free singular 1-chain module of S¹, the generator built from a singular edge e has coefficient exactly 1 at e. Anyone computing edge coefficients of free or difference chains cites this. The proof is a one-line unfold to the Finsupp singleton identity.
Claim. For every singular $1$-simplex $e$ on $S^1$, the coefficient of $e$ in the free generator chain associated to $e$ equals $1$.
background
The module develops the winding/displacement invariant at the level of singular simplices of $S^1=\mathrm{TopCat.sphere},1$, aiming at the chain-level fact that displacement kills boundaries and hence descends to a homology invariant on $H_1(S^1;\mathbb{Z})$.
A SingularOneSimplex is a singular $1$-simplex in the singular simplicial set of that sphere. The free $C_1$ module is realized explicitly by finitely supported integer functions on those simplices. The coefficient map edgeCoeff simply reads the value of such a chain at a chosen edge: $c\mapsto c(e)\in\mathbb{Z}$. The free generator on $e$ is the singleton Finsupp supported at $e$ with value $1$.
This lemma records the tautological evaluation of that generator on its own support point, which is the base case for every later coefficient computation on free sums and differences.
proof idea
Unfold the definitions of the coefficient extractor and of the free-generator constructor. Both reduce to the Finsupp singleton map. The claim is then exactly Finsupp.single_eq_same: the value of the Dirac mass at $e$ on the point $e$ is $1$. No case splits or induction.
why it matters
Parent results that apply it directly are the two-edge parallel-flow coefficient lemmas: the positive edge of a parallel flow has coefficient $+1$, and the negative edge has coefficient $-1$, each by subtracting free generators and invoking this identity. It also feeds nonnegativity of coefficients along forward edge-list chains.
In the broader CircleWindingChain program this is bookkeeping infrastructure for the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: once displacement is known to kill boundaries and to send the fundamental loop to $1$, one still needs clean coefficient arithmetic on free generators and elementary flows. The generation/surjectivity half remains open pending a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No forcing-chain landmark (T5–T8) is touched; the lemma is pure singular-chain algebra on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.