orientedEdgeOfCoeff_chain_eq_single
plain-language theorem explainer
The free 1-chain attached to a coefficient-oriented singular edge is exactly the singleton Finsupp generator at that edge with coefficient +1 or −1 according to the sign of the original coefficient. Anyone building oriented cyclic walks or reading off pointwise coefficients of sign-normalized flows on S¹ cites this. The proof is a two-branch case split on the sign, unfolding the orientation and free-module constructors.
Claim. For every free singular $1$-chain $c$ on $S^1$ and every singular $1$-simplex $e$, the free-chain contribution of the edge $e$ oriented by the sign of its coefficient in $c$ equals the singleton generator $\mathrm{single}(e,\,\sigma)$, where $\sigma=+1$ if the coefficient is positive and $\sigma=-1$ otherwise.
background
The module CircleWindingChain lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $\mathrm{TopCat.sphere},1$, aiming at the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Free $1$-chains are the free $\mathbb{Z}$-module on actual singular $1$-simplices; edgeCoeff reads the integer coefficient of a given simplex in such a chain.
An oriented singular edge packages a $1$-simplex with a traversal direction (forward or backward). The helper orientationOfCoeff chooses forward precisely when the coefficient is positive, and orientedEdgeOfCoeff builds that package from a chain and an edge. Each oriented edge carries a free-chain contribution: $+e$ forward, $-e$ backward.
The local goal is bookkeeping: once edges are reoriented by coefficient sign, their chain contributions become unit generators, which is the normal form used when assembling oriented cyclic walks.
proof idea
Case-split on whether edgeCoeff c e is positive.
If yes, unfold orientedEdgeOfCoeff and orientationOfCoeff to obtain the forward-oriented edge; its chain is ModuleCat.freeMk e, which is definitionally Finsupp.single e 1, matching the positive branch of the right-hand side.
If no, the same unfolds yield the backward-oriented edge; its chain is -ModuleCat.freeMk e. Rewrite with Finsupp.single_neg to get Finsupp.single e (-1), matching the negative branch.
No external lemmas beyond the definitions and Finsupp.single_neg are required.
why it matters
This is the unit-coefficient normal form for a single sign-selected edge. Downstream, edgeCoeff_orientedCyclicChain uses it to compute pointwise coefficients of an oriented closed walk: on the walk the coefficient is the sign-unit of the underlying flow, and off the walk it is zero.
That coefficient control is part of the chain-level apparatus supporting the winding homomorphism on $1$-cycles. Together with simplexDisplacement_boundary (winding kills boundaries) and pathWinding_fundamentalLoop (generator maps to $1$), the module establishes the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ with no axioms or sorry. The surjective/generation half remains open, pending a simplicial prism or subdivision operator absent from Mathlib's singular homology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.