parallelTwoEdgeFlow_coeff_left
plain-language theorem explainer
In the free singular 1-chain that is the generator of edge e minus the generator of a distinct edge f, the coefficient of e is +1. Anyone building or citing the two-edge parallel-flow obstruction on C₁(S¹) needs this evaluation. The proof unfolds the difference, applies coefficient linearity and the free-generator self-coefficient, then kills the off-diagonal term by distinctness.
Claim. Let $e$ and $f$ be distinct singular $1$-simplices on $S^1$. Write $c = [e] - [f]$ for the corresponding free integer $1$-chain. Then the coefficient of $e$ in $c$ equals $1$.
background
The module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$, aiming at the 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$. Free $1$-chains are finitely supported integer combinations of those simplices; edgeCoeff reads the integer multiplicity of a chosen edge.
The two-edge parallel flow is the elementary obstruction shape $[e]-[f]$: one edge with coefficient $+1$ and another with $-1$. Upstream facts record that free generators have self-coefficient $1$, that single-support chains evaluate by an if-then, and that coefficients are linear under subtraction. Distinctness of $e$ and $f$ is the only geometric input needed for the off-support vanishing.
proof idea
Unfold the parallel flow to freeMk $e$ minus freeMk $f$. Rewrite the target coefficient via linearity of coefficients under subtraction, then replace the first summand by the self-coefficient lemma (value $1$). For the second summand, expand freeMk $f$ as a single Finsupp and apply the single-support coefficient formula; the equality test $f=e$ fails by the hypothesis $e\neq f$ (symmetrized), so that coefficient is $0$. Finish with $1-0=1$ by norm_num.
why it matters
This is the left-edge evaluation that feeds parallelTwoEdgeFlow_ne_zero: if the flow vanished, its coefficient on $e$ would be $0$, contradicting the value $1$. Nonvanishing of distinct two-edge flows is part of the hand-built chain-level toolkit for the winding invariant on singular $1$-cycles.
In the module narrative, winding kills boundaries on $2$-simplices and sends the once-around generator to $1$, giving a left inverse to the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity via prism/subdivision remains open in Mathlib's singular homology. The lemma itself is pure free-module bookkeeping, not a new topological identity, but it is the coefficient pin that makes the parallel-flow obstruction usable downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.