OrientedSingularEdge
plain-language theorem explainer
Pairs a singular 1-simplex on S¹ with a forward/backward traversal flag so directed walks can be written as free C₁ chains. Algebraic topologists building the winding homomorphism on singular cycles cite it when assembling oriented edge sums. The structure is pure data; orientation flips endpoints and sends the free generator to its negative.
Claim. An oriented singular edge is a pair $(e,\varepsilon)$ where $e$ is a singular $1$-simplex of $S^1$ and $\varepsilon\in\{\mathrm{forward},\mathrm{backward}\}$. Its initial (resp. terminal) vertex is the start or end of $e$ according to $\varepsilon$; its free $C_1$ contribution is $+[e]$ or $-[e]$ accordingly.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1=\mathrm{TopCat.sphere},1$, aiming at the chain-level identity that displacement kills boundaries and hence descends to $H_1(S^1;\mathbb{Z})$.
A singular $1$-simplex is an element of the singular simplicial set of $S^1$ in degree $1$ (a continuous map $\Delta^1\to S^1$). A singular $0$-simplex is the same in degree $0$. Edge orientation is a two-valued flag: forward keeps the raw simplex; backward stands for its formal negative in a directed walk.
This structure packages one occurrence of such an edge inside an oriented walk, so that initial/terminal vertices and the free-module generator can be read off uniformly before forming singular $1$-chains and applying simplex displacement.
proof idea
No proof: it is a structure with two fields (the singular edge and the orientation flag). The companion projections are by cases on orientation: initial/terminal swap the edge's endpoints under backward; the free-chain map sends forward to the free generator on the edge and backward to its additive inverse in the free $C_1$ module on singular $1$-simplices.
why it matters
Directed walks on the singular complex of $S^1$ need a uniform carrier for "edge with sign" before one can form free $1$-chains and evaluate the winding/displacement functional. This type is that carrier: it turns an oriented walk into a sum of $\pm[e]$ terms whose displacement is additive and homotopy-invariant.
Together with simplex displacement and the kills-boundaries identity (alternating face sum of any singular $2$-simplex has displacement zero), oriented edges feed the construction of a winding homomorphism on $1$-cycles that is a left inverse to the fundamental class, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. The module notes that the surjective/generation half still needs a simplicial prism or subdivision operator not yet in Mathlib.
No downstream consumers are wired in the graph yet; the definition sits at the assembly layer between raw singular simplices and free chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.