pathLift
plain-language theorem explainer
Canonical continuous lift of a path on the unit circle to the real line, starting at a chosen real preimage of the path's initial point. Anyone computing winding or path displacement on S¹ cites this. It is the Mathlib covering-map path-lift applied to the trigonometric covering with the module's fixed start angle.
Claim. For a continuous path $\gamma : I \to S^1$, write $\widetilde{\gamma} : I \to \mathbb{R}$ for the unique continuous lift through the covering $t \mapsto (\cos t, \sin t)$ that starts at a chosen real preimage of $\gamma(0)$.
background
This module builds the local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. The idea is classical: lift the path through the trigonometric covering $\mathbb{R} \to S^1$, $t \mapsto (\cos t, \sin t)$, and read off how far the lift travels in $\mathbb{R}$.
SphereOne is just the carrier of that sphere object. The covering is packaged as isCoveringMap_trig, an IsCoveringMap instance so Mathlib's path-lifting API applies directly. Because a covering lift needs a start height, pathLiftStart picks (via surjectivity of the covering) some real with image $\gamma(0)$, and pathLiftStart_spec records that fiber equation.
The module doc stresses that later results prove displacement is independent of which continuous lift one uses: two lifts starting in the same fiber differ by a constant deck transformation in $2\pi\mathbb{Z}$.
proof idea
One-line definitional wrapper. It feeds the path $\gamma$, the chosen start pathLiftStart γ, and the fiber identity pathLiftStart_spec (symmetrized to match the API's equality direction) into IsCoveringMap.liftPath for isCoveringMap_trig. Existence and continuity of the lift are supplied by Mathlib's covering theory; no extra argument is constructed here.
why it matters
This is the workhorse object behind the whole winding package. pathDisplacement is defined as endpoint difference of this lift; pathDisplacement_eq then shows that difference equals $\Gamma(1)-\Gamma(0)$ for any continuous lift $\Gamma$, which is what makes displacement a usable invariant.
Downstream facts built on it include: closed paths have displacement in $2\pi\mathbb{Z}$; reversing a path negates displacement; zero winding implies the path is homotopic rel endpoints to a constant (via contracting the lift in $\mathbb{R}$ and projecting). In the Recognition foundation layer this supplies the topological winding needed for circle/octave bookkeeping (eight-tick structure, phase on $S^1$) without custom $S^1$ axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.