parallelTwoEdgeFlow_support
plain-language theorem explainer
For two distinct singular 1-simplices e and f on S¹, the free chain e − f has support exactly {e, f}. Anyone tracking two-edge parallel-flow obstructions in the singular chain complex cites this. The proof is a pointwise coefficient case split using the free-generator and difference formulas for edge coefficients.
Claim. Let $e$ and $f$ be distinct singular $1$-simplices of $S^1$. The free singular $1$-chain $e - f$ (coefficient $+1$ on $e$ and $-1$ on $f$) has support equal to the two-element set $\{e, f\}$.
background
This module lifts the path-level winding/displacement invariant on $S^1$ to singular simplices and proves that displacement kills boundaries, giving 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 $\mathrm{TopCat.sphere},1$ in degree $1$. Free edge-chains are finitely supported integer combinations of those simplices. The support of a free chain is the finite set of simplices with nonzero coefficient; membership is equivalent to a nonzero edge coefficient.
The two-edge parallel flow is the free chain $\mathrm{freeMk}(e)-\mathrm{freeMk}(f)$: coefficient $+1$ on one edge and $-1$ on another. Upstream, the coefficient of a single generator is the indicator value at that generator, and coefficients of differences subtract pointwise.
proof idea
Prove set equality by extensionality on an arbitrary singular edge $x$. Rewrite membership via the support-membership criterion (nonzero coefficient). Unfold the parallel flow to a difference of free generators, apply the difference formula for coefficients, then the single-generator coefficient formula on each summand. Case-split on whether $x$ equals $e$ and whether $x$ equals $f$: the double-equal case contradicts distinctness; each single-equal case simplifies to a nonzero coefficient; the neither case yields coefficient zero. All steps are algebraic on Finsupp coefficients.
why it matters
Feeds the immediate parent parallelTwoEdgeFlow_supportCard, which upgrades this identity to the statement that a distinct two-edge parallel flow has support cardinality exactly two. That cardinality fact is the bookkeeping step for treating $e-f$ as a genuine two-edge obstruction shape in the free singular chain complex of $S^1$.
In the module's program, such shapes sit under the winding/displacement invariant that kills boundaries and splits the fundamental class, establishing injectivity of the comparison map $H_1(S^1;\mathbb{Z})\to\mathbb{Z}$. The generation/surjectivity half remains open (needs a simplicial prism or subdivision operator Mathlib does not yet supply). This lemma is pure support algebra; it does not itself compute winding, but it keeps the obstruction chains well-formed for those later arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.