Lifts of circle diffeomorphisms

Every C^n diffeomorphism φ of the circle AddCircle T, n ≠ 0, has a C^n lift F : ℝ → ℝ, φ x = F x, with either F (x + T) = F x + T and F' > 0 (the orientation-preserving case) or F (x + T) = F x - T and F' < 0 (the orientation-reversing case). A continuous lift exists by AddCircle.exists_continuous_lift, and it is C^n by AddCircle.contDiff_of_comp_coe_eq. A lift G of φ⁻¹ satisfies G ∘ F = id + c (Homeomorph.exists_addCircle_lift_symm_comp_eq_add), so G' (F x) F' x = 1 and F' never vanishes, while the lift of a homeomorphism is monotone of degree one or antitone of degree -1 (AddCircle.strictMono_or_strictAnti_of_lift).

Main declarations

• AddCircle.deriv_pos_or_deriv_neg_of_lift: a continuous lift of a C^n diffeomorphism of the circle, n ≠ 0, has degree one and positive derivative, or degree -1 and negative derivative.
• Diffeomorph.exists_addCircle_lift: every C^n diffeomorphism of the circle, n ≠ 0, has a C^n lift of one of these two kinds.

References

• B. Farb, D. Margalit, A Primer on Mapping Class Groups, Section 2.1, for lifts of circle homeomorphisms.

theorem AddCircle.deriv_pos_or_deriv_neg_of_lift {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {F : ℝ → ℝ} {φ : Diffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (AddCircle T) (AddCircle T) n} (hn : n ≠ 0) (hF : Continuous F) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : ((∀ (x : ℝ), F (x + T) = F x + T) ∧ ∀ (x : ℝ), 0 < deriv F x) ∨ (∀ (x : ℝ), F (x + T) = F x - T) ∧ ∀ (x : ℝ), deriv F x < 0

Lifts of circle diffeomorphisms. A continuous lift F of a C^n diffeomorphism φ of AddCircle T, n ≠ 0, either satisfies F (x + T) = F x + T and has positive derivative (the orientation-preserving case), or satisfies F (x + T) = F x - T and has negative derivative (the orientation-reversing case). Such a lift is C^n by AddCircle.contDiff_of_comp_coe_eq.

theorem Diffeomorph.exists_addCircle_lift {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} (φ : Diffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (AddCircle T) (AddCircle T) n) (hn : n ≠ 0) : ∃ (F : ℝ → ℝ), ContDiff ℝ n F ∧ (∀ (x : ℝ), φ ↑x = ↑(F x)) ∧ (((∀ (x : ℝ), F (x + T) = F x + T) ∧ ∀ (x : ℝ), 0 < deriv F x) ∨ (∀ (x : ℝ), F (x + T) = F x - T) ∧ ∀ (x : ℝ), deriv F x < 0)

Every circle diffeomorphism has a lift. A C^n diffeomorphism φ of AddCircle T, n ≠ 0, has a C^n lift F, φ x = F x, which either satisfies F (x + T) = F x + T and has positive derivative, or satisfies F (x + T) = F x - T and has negative derivative.