windingChainMap_freeToChain_orientedChain
plain-language theorem explainer
For a single oriented singular edge on S¹, the winding chain map applied to its raw free-to-chain image equals that edge's oriented winding (negated if traversed backward). Anyone building the integer comparison H₁(S¹;ℤ) → ℝ or summing windings along walks cites this. The proof cases on orientation and reduces to the free-generator evaluation lemma, using linearity of the chain map under negation.
Claim. Let $o$ be a singular $1$-simplex on $S^1$ equipped with a traversal orientation. Applying the winding chain map $W:C_1(S^1;\mathbb{Z})\to\mathbb{R}$ to the image of $o$'s underlying free generator under the free-to-singular chain map yields the oriented winding of $o$: the ordinary singular winding if the orientation is forward, and its negative if backward.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1$ and proves that winding kills boundaries, the key identity making winding a homology invariant. Together with the fact that the once-around generator has winding $1$, this supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
An oriented singular edge pairs a singular $1$-simplex with a forward or backward traversal. Its oriented winding is the singular winding number, negated on backward edges. The winding chain map $W:C_1(S^1;\mathbb{Z})\to\mathbb{R}$ sends the free generator indexed by a singular $1$-simplex $s$ to $n\mapsto n\cdot\mathrm{winding}(s)$. The free-to-chain map embeds the free $\mathbb{Z}$-module on singular $1$-simplices into the singular chain group by sending each free generator to the matching coproduct summand.
The upstream free-generator lemma already states that $W$ on the free-to-chain image of a bare generator recovers ordinary singular winding. This declaration extends that identity from unoriented generators to oriented edge occurrences.
proof idea
Destructure the oriented edge into its underlying singular simplex $e$ and orientation. Case on orientation.
Forward: after unfolding oriented winding and the chain of a forward edge, the claim is exactly the free-generator evaluation lemma windingChainMap_singularOneChainFreeToChain_freeMk applied to $e$.
Backward: the chain is the negation of the free generator. Unfold, apply map_neg twice (once for each module homomorphism), then finish again by the free-generator lemma. The two minuses produce the sign flip that defines backward oriented winding.
why it matters
This is the single-edge stepping stone to windingChainMap_freeToChain_orientedChain_sum, which states that $W$ on the free-to-chain image of a finite sum of oriented edges equals the total oriented winding of the walk. That sum form is the natural evaluation of the winding homomorphism on the raw chain of an oriented path, and feeds the chain-level comparison that realizes winding as a left inverse to the fundamental class.
In the module's program, the kills-boundaries identity (simplexDisplacement_boundary) already shows $W$ vanishes on boundaries. The generator evaluation (this lemma and its sum extension) plus pathWinding_fundamentalLoop give injectivity of the integer comparison. Surjectivity (every $1$-cycle homologous to an integer multiple of the fundamental cycle) still needs a simplicial prism/subdivision operator that Mathlib's singular homology does not yet supply. No Recognition-Science forcing-chain landmarks (T5–T8, RCL, $\varphi$) are invoked here; the result is pure singular homology of the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.