parallelTwoEdgeFlow
plain-language theorem explainer
Defines the integer 1-chain e − f on two singular 1-simplices of S¹: coefficient +1 on the first edge and −1 on the second. Anyone proving that parallel edges with matching endpoints form a cycle, or classifying large-support 1-chains in the winding argument for H₁(S¹;ℤ), cites this shape. The body is the free-module difference of the two basis vectors.
Claim. For singular $1$-simplices $e,f$ of $S^1$, the parallel two-edge flow is the free $\mathbb{Z}$-chain $[e]-[f]$ in $C_1^{\mathrm{sing}}(S^1;\mathbb{Z})$.
background
This module lifts path winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ 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 a continuous map $\Delta^1\to S^1$ in the singular simplicial set; the free module on those simplices is the singular $1$-chain group used here.
The parallel-flow shape is the elementary two-term chain with opposite unit coefficients. Downstream lemmas show that when $e$ and $f$ share initial and terminal vertices, this chain is a cycle (boundary zero), is nonzero when $e\neq f$, and has support exactly ${e,f}$. That package is the obstruction pattern for distinct parallel edges in the large-support branch of the homology argument.
Upstream, the free-module constructor and the singular-simplex type are the only ingredients; the winding/displacement calculus sits one layer above and is not invoked in the definition itself.
proof idea
One-line definition: take the free $\mathbb{Z}$-basis vectors of $e$ and $f$ in the free module on singular $1$-simplices and subtract. No lemmas, no tactics; the algebraic difference is the entire body.
why it matters
This is the named obstruction shape for the parallel-edge case in the circle winding chain. It feeds seven local lemmas: boundary vanishes when endpoints match; left and right coefficients are $+1$ and $-1$; the chain is nonzero and has support card $2$ when the edges are distinct; and the large-support branch applies.
Those facts sit inside the module's program: simplex displacement kills $2$-boundaries, and together with the fundamental loop winding to $1$ this yields a left inverse to the fundamental class (injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Surjectivity (generation by the fundamental cycle) remains open and needs a prism/subdivision operator Mathlib does not yet supply. The definition itself is pure scaffolding for that injectivity bookkeeping, not a physics constant or forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.