vertexBoundaryCoeff
plain-language theorem explainer
Extracts the integer coefficient of a chosen vertex in the singular boundary of a free edge-chain on S¹. Anyone proving local balance or Kirchhoff-type identities for free 1-chains cites it. The body is a one-line composition: apply the free boundary map, then read the vertex coefficient in C₀.
Claim. For a free singular $1$-chain $c$ on $S^1$ and a singular $0$-simplex $v$, write $\partial c$ via the free boundary (each directed edge maps to its terminal $0$-face minus its initial $0$-face). The boundary coefficient of $c$ at $v$ is the integer coefficient of $v$ in that $0$-chain.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact behind the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here one works with the free $\mathbb{Z}$-modules on actual singular simplices of $\mathrm{TopCat.sphere},1$. A free edge-chain is an element of the free module on singular $1$-simplices. The free boundary sends each directed edge to terminal face minus initial face. The vertex coefficient of a free $0$-chain is simply its value at a chosen singular $0$-simplex.
Composing those two operations gives the net algebraic multiplicity with which a vertex appears in $\partial c$, the standard local incidence reading used in discrete homology and flow balance.
proof idea
One-line definitional wrapper. Apply the free singular boundary homomorphism to the edge-chain $c$, then evaluate the resulting free $0$-chain at the vertex $v$ via the plain coefficient extractor. No further lemmas are invoked at the definition site; downstream theorems unfold this composition against the free-generator description of the boundary.
why it matters
This is the local $C_0$ reading of $\partial c$ used throughout the free-chain incidence calculus in the module. It feeds the single-edge evaluation (boundary coefficient is $+1$ at the terminal endpoint, $-1$ at the initial, and their algebraic sum if endpoints coincide), the target local-balance proposition equating boundary coefficients to finite incidence sums over support, the proof that that balance holds by Finsupp induction, and the corollary that every free-boundary-zero flow has vanishing incidence sum at each vertex.
Those identities are the discrete bookkeeping half of the winding-kills-boundaries story: once boundary coefficients match incidence sums, vanishing of $\partial c$ becomes Kirchhoff balance at every vertex, which is what lets the displacement/winding functional descend to homology and serve as a left inverse to the fundamental class. The module still notes that the converse generation half (every $1$-cycle homologous to an integer multiple of the fundamental cycle) needs a simplicial prism or subdivision operator not yet in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.