pathLift_lifts
plain-language theorem explainer
The canonical continuous lift of a path on $S^1$ projects back to the original path under the trigonometric covering $\mathbb{R}\to S^1$. Anyone computing winding or path displacement via lifts cites this identity. The proof is a one-line wrapper of the covering-map path-lifting API applied at the chosen real start angle.
Claim. For every continuous path $\gamma:I\to S^1$, if $\widetilde{\gamma}:I\to\mathbb{R}$ denotes the canonical continuous lift of $\gamma$ starting at a chosen real preimage of $\gamma(0)$, then $\mathrm{trig}\circ\widetilde{\gamma}=\gamma$, where $\mathrm{trig}:\mathbb{R}\to S^1$ is the once-around trigonometric covering.
background
The module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. The carrier is abbreviated $S^1$. The covering is the continuous map $\mathrm{trig}:\mathbb{R}\to S^1$ sending an angle to the corresponding point on the unit circle; it is packaged as an IsCoveringMap so Mathlib's path-lifting API applies directly.
For a path $\gamma:I\to S^1$, a real start angle is chosen by surjectivity of $\mathrm{trig}$ at $\gamma(0)$. The canonical lift $\widetilde{\gamma}:I\to\mathbb{R}$ is the unique continuous lift of $\gamma$ with that start value, obtained from the covering's liftPath construction. The module's central later result is that displacement computed from this lift agrees with the endpoint difference of any continuous lift, via a deck-transformation argument with period $2\pi\mathbb{Z}$.
proof idea
One-line wrapper. Apply the general covering fact IsCoveringMap.liftPath_lifts to isCoveringMap_trig, the path $\gamma$, the chosen start angle pathLiftStart γ, and the fiber identity pathLiftStart_spec (symmetrized so the start of the lift maps to $\gamma(0)$). The definition of pathLift is exactly that same liftPath call, so the composition identity is immediate.
why it matters
This is the basic projection identity for the canonical lift. Downstream, pathDisplacement_eq uses it to prove lift-independence of displacement: any continuous lift has the same endpoint difference as the canonical one. Closed-path integrality (pathDisplacement_loop_intMul) evaluates the identity at the endpoints to place lift ends in the same fiber. Reversal and zero-winding homotopy both need the lift to project back to $\gamma$. In the chain module, cone face-map identities cite it pointwise (e.g. at $t=0$ or along a 1-simplex) so the cone on a path restricts correctly on faces. It sits under the foundation layer that makes winding a usable invariant on exact $S^1$, with no local circle replacements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.