edgeSupport

The module builds the winding invariant at the level of singular simplices of $S^1=\mathrm{TopCat.sphere},1$, aiming at the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. A singular $1$-simplex is a continuous map $\Delta^1\to S^1$ in the singular simplicial set. The free edge-chain type is the free $\mathbb{Z}$-module on those simplices, so each chain is a finitely supported integer combination of edges.

Support of such a chain is the finite set of basis edges with nonzero coefficient. That set is the natural domain for incidence sums, $\ell^1$ size, and cyclic-peel arguments that shrink support while preserving the balanced-flow (cycle) condition.

One-line definitional wrapper: the support of the free-module element is returned as a Finset of singular $1$-simplices. No further proof obligations.

This is the bookkeeping handle for every support-sensitive lemma in the circle-winding chain development. Downstream it feeds the identity that boundary incidence equals the finite sum over edge support; the $\ell^1$ size of a free edge-chain; the exact $\ell^1$ drop when subtracting an oriented closed walk; positivity of edge contribution at the oriented terminal; and the strict support-cardinality decreases used in one-step cyclic extraction.

Those peels are the combinatorial engine behind writing a balanced $1$-chain as an integer combination of oriented cycles, which (with the kills-boundaries identity for simplex displacement) supplies the generation/extraction half of the winding comparison on $H_1(S^1)$. The module still notes that full surjectivity of the integer comparison map needs a simplicial prism/subdivision operator not yet in Mathlib singular homology; support extraction is the local finite-combinatorial piece already available.