edgeCoeff
plain-language theorem explainer
Extracts the integer coefficient of a singular 1-simplex inside a free C₁ chain on S¹. Anyone computing ℓ¹ size, boundary incidence, or peeling oriented cycles off a free edge-chain cites this. The body is the free-module evaluation map: read the underlying function at that edge.
Claim. Given a free integer $1$-chain $c$ on the singular $1$-simplices of $S^1$ and a singular $1$-simplex $e$, write $\mathrm{coeff}(c,e)\in\mathbb{Z}$ for the coefficient of $e$ in $c$.
background
The module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that displacement kills boundaries, giving 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 $S^1$ in degree $1$. The free $C_1$ object is the free $\mathbb{Z}$-module on that set of simplices (Mathlib ModuleCat.free). Free-module elements are finitely supported functions from edges to $\mathbb{Z}$; this definition names the pointwise value.
Upstream, the free module and the simplex type are pure abbreviations onto Mathlib singular data. No project-local $S^1$ stand-in is used.
proof idea
Definitional one-liner: evaluate the underlying function of the free-module element at the given singular $1$-simplex. No lemmas, no tactics.
why it matters
This is the atomic coefficient reader for every explicit free-chain calculation in the winding chain module. Downstream it feeds the incidence-sum identity (boundary incidence equals the finite support sum of edge contributions), the $\ell^1$ size of a free edge-chain, the exact $\ell^1$ count $k$ for an oriented injective $k$-cycle, and the $\ell^1$ decrease when peeling one directed cycle off a balanced flow. Those peeling lemmas are the combinatorial engine behind decomposing $1$-cycles into cyclic edge-list terms on the way to the integer comparison map for $H_1(S^1)$. It does not itself touch the T0–T8 forcing chain; it sits in the singular-homology half of the circle invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.