edgeSupportCard_eq_zero_iff
plain-language theorem explainer
A free singular 1-chain on S¹ has support-cardinality zero exactly when it is the zero chain. Downstream cyclic edge-list extraction cites this to discharge the empty-support base case. The proof unfolds the card definition and applies the standard Finsupp fact that empty support means the zero element.
Claim. Let $c$ be an element of the free $\mathbb{Z}$-module on singular $1$-simplices of $S^1$. Then the cardinality of the support of $c$ is zero if and only if $c=0$.
background
The module CircleWindingChain lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Here one works in the free $\mathbb{Z}$-module on actual singular $1$-simplices of TopCat.sphere 1. The support-cardinality of such a free edge-chain is the ordinary finite-set cardinality of its Finsupp support: how many singular edges carry a nonzero coefficient.
The companion fact that empty support characterises the zero element of a Finsupp module is the algebraic content being packaged for this chain type.
proof idea
Term-mode, three steps. Unfold the definition of support-cardinality (support card of the underlying Finsupp). Rewrite the goal with Finset.card_eq_zero, reducing to emptiness of the support set. Finish by Finsupp.support_eq_empty, the library characterisation that a Finsupp is zero iff its support is empty.
why it matters
Base case for the cyclic edge-list decomposition of free edge-flows on $S^1$. Downstream, supportCard_zero_decomposesIntoCyclicEdgeLists applies the forward direction to reduce empty support to the zero chain, then quotes the empty-list decomposition of zero. The sibling extraction step supportCard_le_one_extractionStep handles the nonzero card-$\le 1$ case of the same induction.
That decomposition sits inside the generation half of the winding comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: every balanced free edge-flow is assembled from cyclic edge lists whose total winding recovers the homology class. The module already has the kills-boundaries identity (simplexDisplacement_boundary); this lemma is bookkeeping that lets support-size induction close on free chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.