orientedEdgePath
plain-language theorem explainer
An oriented singular edge on S¹ is turned into a continuous path I → S¹: the edge path itself when forward, its reverse when backward. Anyone assembling signed closed walks or path-base corrections in the singular chain complex cites this. The body is a two-branch match on the orientation flag.
Claim. Given an oriented singular edge $o$ (a singular $1$-simplex of $S^1$ together with a forward/backward traversal flag), return the continuous path $I \to S^1$ that traces $o$: the standard unit-interval reparameterisation of the edge when the flag is forward, and the time-reversed path $t \mapsto \gamma(1-t)$ when the flag is backward.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
An oriented singular edge pairs a singular $1$-simplex with an EdgeOrientation (forward or backward). The unoriented bridge is singularEdgePath: read the simplex as a path $I \to S^1$ via the standard $\Delta^1 \simeq I$ reparameterisation. Path reversal is the CircleWinding map $\gamma \mapsto \gamma \circ (t \mapsto 1-t)$.
SphereOne is the carrier of Mathlib's TopCat.sphere 1. Downstream, finite lists of these oriented edges with matching terminal/initial vertices form oriented cyclic families (closed signed walks in the singular $1$-skeleton).
proof idea
Definition by cases on the orientation field. Forward returns singularEdgePath of the underlying edge. Backward returns CircleWinding.reversePath applied to that same edge path. No further lemmas; the match is the entire construction.
why it matters
This is the path-level reading of a signed edge occurrence. It feeds OrientedCyclicFamilyTerm (finite oriented closed walks) and the path-base correction package: forward edges have definitional equality of path-base chain to the signed free generator, while backward edges leave a residual bounded by the backtrack prism plus a constant $2$-simplex.
Those corrections assemble into the terminal-side correction for oriented cyclic families, part of showing that winding on singular $1$-cycles is a homology invariant and a left inverse to the fundamental class. That is the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ in the module's programme; the generation/surjectivity half still needs a simplicial prism operator Mathlib does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.