edgeSupport_eq_empty_iff
plain-language theorem explainer
A free singular 1-chain on S¹ has empty edge support exactly when it is the zero chain. Anyone extracting oriented closed walks from balanced nonzero edge-flows cites this equivalence. The proof is a one-line unfold of the support definition followed by the standard Finsupp support-empty criterion.
Claim. For every free singular $1$-chain $c$ on $S^1$ (i.e. an element of the free $\mathbb{Z}$-module on singular $1$-simplices), the finite support of $c$ is empty if and only if $c=0$.
background
The module CircleWindingChain lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$, and proves that displacement kills boundaries. Free singular $1$-chains are elements of the free $\mathbb{Z}$-module on the set of continuous maps $\Delta^1\to S^1$.
Edge support of such a chain $c$ is simply the ordinary Finsupp support: the finite set of singular $1$-simplices that appear with nonzero coefficient. The zero chain is the unique chain whose every coefficient vanishes.
This elementary support fact sits inside the larger program that builds a winding homomorphism on $1$-cycles as a left inverse to the fundamental class, giving the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
proof idea
One-line term proof. Unfold the definition of edge support (which is literally c.support) and apply the Mathlib lemma Finsupp.support_eq_empty, which states that a finitely supported function has empty support precisely when it is the zero function.
why it matters
The parent theorem exists_orientedCyclicFamily_of_balanced_nonzero needs a clean criterion that a balanced free edge-flow is nonzero exactly when its support is nonempty, so that an oriented cyclic family of edges can be extracted. Without the empty-support $\Leftrightarrow$ zero equivalence, the nonzero hypothesis on a balanced chain would not immediately yield a nonempty finite set of edges to walk around.
In the broader Recognition foundation this supports the hand-built injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via the covering-space winding invariant (no axioms, no sorry). The generation/surjectivity half remains open and requires a simplicial prism or subdivision operator not yet in Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.