mem_edgeSupport_iff
plain-language theorem explainer
Membership of a singular 1-simplex in the support of a free integer 1-chain is equivalent to a nonzero coefficient on that edge. Anyone working with support-cardinality peels, oriented cyclic extraction, or singleton-support generators on C₁(S¹) cites this. The proof unfolds the two local defs and applies the standard Finsupp support membership lemma.
Claim. For every free integer 1-chain $c$ on singular 1-simplices of $S^1$ and every singular 1-simplex $e$, one has $e \in \mathrm{supp}(c)$ if and only if the coefficient of $e$ in $c$ is nonzero.
background
The module works at the level of singular chains on TopCat.sphere 1. A singular 1-simplex is a continuous map $\Delta^1 \to S^1$ in the singular simplicial set; free 1-chains are the free $\mathbb{Z}$-module on that set of simplices (realized as finitely supported functions).
edgeCoeff c e is the integer coefficient of edge $e$ in $c$, and edgeSupport c is the finite set of edges with nonzero coefficient (the Finsupp support). The module's larger goal is the winding invariant on singular 1-simplices and the kills-boundaries identity that makes winding a homology invariant, feeding the injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Support membership is the basic bookkeeping predicate used throughout oriented-cycle peels and $\ell^1$ decrease arguments on balanced flows.
proof idea
One-line term proof. Unfold edgeSupport and edgeCoeff (which are definitionally the Finsupp support and the pointwise evaluation c.toFun e). The goal becomes the library statement Finsupp.mem_support_iff, which is applied directly.
why it matters
This is the dictionary between set-theoretic support and coefficient nonvanishing for free edge-chains. Downstream results lean on it constantly: edgeSupport_orientedCyclicChain rewrites support of an oriented closed walk via this iff; eq_zsmul_freeMk_of_edgeSupport_eq_single classifies singleton-support chains; positivity facts such as edgeContribution_pos_at_oriented_terminal and orientedCoeff_pos_of_mem_edgeSupport take support membership as hypothesis; and the cyclic-peel bookkeeping theorems (edgeSupportCard_sub_lt_of_supported_exact_cancel, edgeSupportCard_sub_scaled_orientedCyclic_lt, chainL1_sub_orientedCyclic) use it to track which edges survive subtraction.
In the Recognition foundation stack this sits inside the hand-built injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (winding as left inverse to the fundamental class). Surjectivity (generation by the once-around loop) remains open and needs a simplicial prism/subdivision operator Mathlib does not yet supply. The lemma itself is pure chain algebra, not a physics claim, but it is load-bearing for every support-shrinkage step in that homology argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.