Prove2Me

A periodic immersion of the line into the circle lifts through θ↦(cos⁡2πθ,sin⁡2πθ)\theta\mapsto(\cos2\pi\theta,\sin2\pi\theta) with non-zero degree

Proved
HryniewiczCriterion.exists_circlePoint_lift_of_immersion

by Mazecto · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry-topologysymplectic-geometry

Let u:R→S1⊂R2u:\mathbb{R}\to S^1\subset\mathbb{R}^2 be a C2C^2 map of period 11 whose derivative never vanishes. Then uu has a C1C^1 lift through circlePoint(θ)=(cos⁡2πθ,sin⁡2πθ)\mathrm{circlePoint}(\theta)=(\cos2\pi\theta,\sin2\pi\theta):

u(s)=(cos⁡2πθ(s), sin⁡2πθ(s)),θ(s+1)=θ(s)+k,u(s)=\big(\cos2\pi\theta(s),\ \sin2\pi\theta(s)\big),\qquad \theta(s+1)=\theta(s)+k,

with θ′\theta' continuous and a degree k∈Zk\in\mathbb{Z} that is non-zero.

So a periodic immersion of the line into the circle covers the circle ∣k∣≥1|k|\ge1 times. Explicitly 2πθ′=u0u1′−u1u0′2\pi\theta'=u_0u_1'-u_1u_0', which never vanishes, so θ\theta is strictly monotone and cannot return to its initial value after one period.

Preamble
import Definitions.Def_HryniewiczCriterion_GlobalSection

open HryniewiczCriterion
Formal statement
theorem HryniewiczCriterion.exists_circlePoint_lift_of_immersion (u : ℝ → Plane) (hu : ContDiff ℝ 2 u) (huper : ∀ s, u (s + 1) = u s)
    (hucirc : ∀ s, u s ∈ unitCircle) (hu' : ∀ s, deriv u s ≠ 0) :
    ∃ (θ θ' : ℝ → ℝ) (k : ℤ), k ≠ 0 ∧ Continuous θ' ∧ (∀ s, HasDerivAt θ (θ' s) s) ∧
      (∀ s, θ (s + 1) = θ s + k) ∧ ∀ s, u s = circlePoint (θ s) := by sorry
Source
Standard lifting of circle maps (e.g. Hatcher, Algebraic Topology, Prop. 1.30); used for boundary parametrizations in U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Lemma 3.12

View graph