Maps of the circle given by a lift

A map φ : AddCircle T → AddCircle T of degree one is described by a lift F : ℝ → ℝ with F (x + T) = F x + T and φ x = F x for every real x. This file records the basic properties of such maps used to work with diffeomorphisms of the circle through their lifts.

A continuous lift makes φ continuous, and a continuous strictly monotone lift makes φ a homeomorphism, AddCircle.homeomorphOfLift: such a lift maps each fundamental interval (t, t + T] onto the fundamental interval (F t, F t + T]. Derivatives of lifts are treated in TauCeti.Analysis.Calculus.Deriv.AddCircle.

Conversely, every continuous circle map has a continuous lift, by the lifting property of the universal covering ℝ → AddCircle T, and two continuous lifts of the same map differ by a constant. So a continuous lift F of any continuous circle map has a degree, an integer d with F (x + T) = F x + d * T. For a homeomorphism φ the degree is ±1: a lift G of φ⁻¹ gives G ∘ F = id + c, so F is injective and the degrees multiply to 1. A continuous injective map of ℝ is strictly monotone or strictly antitone, so every continuous lift of a homeomorphism of the circle is either strictly monotone of degree one or strictly antitone of degree -1.

Main declarations

• AddCircle.bijective_of_lift: a circle map with a continuous strictly monotone lift is bijective, and AddCircle.homeomorphOfLift is the resulting homeomorphism.
• AddCircle.exists_continuous_lift: every continuous circle map has a continuous lift.
• AddCircle.exists_forall_eq_add_of_lift: two continuous lifts of the same circle map differ by a constant.
• AddCircle.exists_int_forall_add_period_eq_of_lift: a continuous lift has an integer degree d, and then shifts integer multiples of the period by multiples of d * T (AddCircle.lift_add_int_mul_of_degree, stated for any real increment per period).
• AddCircle.add_mul_sub_add_period: for any weight c, the interpolation x ↦ x + c * (F x - x) between the identity and a lift F is again a lift.
• AddCircle.periodic_sub_of_lift: the displacement x ↦ F x - x of a lift is periodic.
• Homeomorph.exists_addCircle_lift_symm_comp_eq_add: for a homeomorphism φ of the circle, a continuous lift of φ⁻¹ composed with a continuous lift of φ is a translation.
• AddCircle.strictMono_or_strictAnti_of_lift: a continuous lift of a homeomorphism of the circle is strictly monotone of degree one or strictly antitone of degree -1.

References

• A. Hatcher, Algebraic Topology, Proposition 1.33 (the lifting criterion).
• B. Farb, D. Margalit, A Primer on Mapping Class Groups, Section 2.1 (homeomorphisms of the circle and their lifts).

theorem AddCircle.lift_add_int_mul_of_degree {T : ℝ} {F : ℝ → ℝ} {a : ℝ} (hper : ∀ (x : ℝ), F (x + T) = F x + a) (x : ℝ) (k : ℤ) : F (x + ↑k * T) = F x + ↑k * a

A map F that increases by a over each period, F (x + T) = F x + a, increases by k * a over k periods: F (x + k * T) = F x + k * a. For a lift of degree d, a = d * T.

theorem AddCircle.lift_add_int_mul {T : ℝ} {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + T) = F x + T) (x : ℝ) (k : ℤ) : F (x + ↑k * T) = F x + ↑k * T

A lift F with F (x + T) = F x + T shifts integer multiples of the period.

theorem AddCircle.add_mul_sub_add_period {T : ℝ} {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + T) = F x + T) (c x : ℝ) : x + T + c * (F (x + T) - (x + T)) = x + c * (F x - x) + T

Interpolating between the identity and a lift F with a weight c gives again a lift: x ↦ x + c * (F x - x) shifts x + T to the image of x plus T.

theorem AddCircle.periodic_sub_of_lift {T : ℝ} {F : ℝ → ℝ} (hper : ∀ (x : ℝ), F (x + T) = F x + T) : Function.Periodic (fun (x : ℝ) => F x - x) T

The displacement x ↦ F x - x of a lift F is periodic.

theorem AddCircle.image_Ioc_subset_of_lift {T : ℝ} {F : ℝ → ℝ} (hF : StrictMono F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) : F '' Set.Ioc 0 T ⊆ Set.Ioc (F 0) (F 0 + T)

A strictly monotone lift F maps the fundamental interval (0, T] into (F 0, F 0 + T].

theorem AddCircle.continuous_of_lift {T : ℝ} {φ : AddCircle T → AddCircle T} {F : ℝ → ℝ} (hF : Continuous F) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : Continuous φ

A circle map with a continuous lift is continuous.

theorem AddCircle.exists_continuous_lift {T : ℝ} {φ : AddCircle T → AddCircle T} (hφ : Continuous φ) : ∃ (F : ℝ → ℝ), Continuous F ∧ ∀ (x : ℝ), φ ↑x = ↑(F x)

Lifting circle maps. Every continuous map φ of the circle AddCircle T has a continuous lift: a continuous F : ℝ → ℝ with φ x = F x for every real x. This is the lifting property of the universal covering ℝ → AddCircle T.

theorem AddCircle.exists_forall_eq_add_of_lift {T : ℝ} {F₁ F₂ : ℝ → ℝ} (h₁ : Continuous F₁) (h₂ : Continuous F₂) (h : ∀ (x : ℝ), ↑(F₁ x) = ↑(F₂ x)) : ∃ (c : ℝ), ∀ (x : ℝ), F₁ x = F₂ x + c

Two continuous lifts of the same circle map differ by a constant: if F₁ x and F₂ x have the same image in AddCircle T for every x, then F₁ = F₂ + c.

theorem AddCircle.exists_int_forall_add_period_eq_of_lift {T : ℝ} {φ : AddCircle T → AddCircle T} {F : ℝ → ℝ} (hF : Continuous F) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : ∃ (d : ℤ), ∀ (x : ℝ), F (x + T) = F x + ↑d * T

The degree of a circle map. A continuous lift F of a circle map changes by an integer multiple of the period over each period: F (x + T) = F x + d * T for some integer d.

theorem Homeomorph.exists_addCircle_lift_symm_comp_eq_add {T : ℝ} {F : ℝ → ℝ} (φ : AddCircle T ≃ₜ AddCircle T) (hF : Continuous F) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : ∃ (G : ℝ → ℝ) (c : ℝ), Continuous G ∧ (∀ (x : ℝ), φ.symm ↑x = ↑(G x)) ∧ ∀ (x : ℝ), G (F x) = x + c

A continuous lift G of the inverse of a homeomorphism φ of the circle, composed with a continuous lift F of φ, lifts the identity, so it is a translation: G (F x) = x + c.

theorem AddCircle.image_Ioc_of_lift {T : ℝ} {F : ℝ → ℝ} [hT : Fact (0 < T)] (hF : StrictMono F) (hFc : Continuous F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) : F '' Set.Ioc 0 T = Set.Ioc (F 0) (F 0 + T)

A continuous strictly monotone lift F maps the fundamental interval (0, T] onto (F 0, F 0 + T].

theorem AddCircle.bijective_of_lift {T : ℝ} {φ : AddCircle T → AddCircle T} {F : ℝ → ℝ} [hT : Fact (0 < T)] (hF : StrictMono F) (hFc : Continuous F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : Function.Bijective φ

A circle map with a continuous strictly monotone lift is bijective.

noncomputable def AddCircle.homeomorphOfLift {T : ℝ} {F : ℝ → ℝ} [hT : Fact (0 < T)] (φ : AddCircle T → AddCircle T) (hF : StrictMono F) (hFc : Continuous F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : AddCircle T ≃ₜ AddCircle T

The homeomorphism of the circle given by a continuous strictly monotone lift F with F (x + T) = F x + T.

@[simp]

theorem AddCircle.coe_homeomorphOfLift {T : ℝ} {φ : AddCircle T → AddCircle T} {F : ℝ → ℝ} [hT : Fact (0 < T)] (hF : StrictMono F) (hFc : Continuous F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : ⇑(homeomorphOfLift φ hF hFc hper hφ) = φ

@[simp]

theorem AddCircle.homeomorphOfLift_symm_apply_apply {T : ℝ} {φ : AddCircle T → AddCircle T} {F : ℝ → ℝ} [hT : Fact (0 < T)] (hF : StrictMono F) (hFc : Continuous F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) (x : AddCircle T) : (homeomorphOfLift φ hF hFc hper hφ).symm (φ x) = x

theorem AddCircle.apply_homeomorphOfLift_symm_apply {T : ℝ} {φ : AddCircle T → AddCircle T} {F : ℝ → ℝ} [hT : Fact (0 < T)] (hF : StrictMono F) (hFc : Continuous F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) (x : AddCircle T) : φ ((homeomorphOfLift φ hF hFc hper hφ).symm x) = x

@[simp]

theorem AddCircle.comp_homeomorphOfLift_symm {T : ℝ} {φ : AddCircle T → AddCircle T} {F : ℝ → ℝ} [hT : Fact (0 < T)] (hF : StrictMono F) (hFc : Continuous F) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : φ ∘ ⇑(homeomorphOfLift φ hF hFc hper hφ).symm = id

The composition form of apply_homeomorphOfLift_symm_apply, usable by simp: the applied form cannot be a simp lemma, because its left-hand side has the variable φ as head symbol.

theorem AddCircle.strictMono_or_strictAnti_of_lift {T : ℝ} {F : ℝ → ℝ} [hT : Fact (0 < T)] {φ : AddCircle T ≃ₜ AddCircle T} (hF : Continuous F) (hφ : ∀ (x : ℝ), φ ↑x = ↑(F x)) : (StrictMono F ∧ ∀ (x : ℝ), F (x + T) = F x + T) ∨ StrictAnti F ∧ ∀ (x : ℝ), F (x + T) = F x - T

Lifts of homeomorphisms of the circle. A continuous lift F of a homeomorphism φ of AddCircle T is either strictly monotone with F (x + T) = F x + T (the orientation-preserving case) or strictly antitone with F (x + T) = F x - T (the orientation-reversing case).