Interpolating circle diffeomorphisms to the identity

An orientation-preserving diffeomorphism φ of the circle AddCircle T is presented by a lift F : ℝ → ℝ with F (x + T) = F x + T and F' > 0. For a weight w ∈ [0, 1] the map x ↦ x + w (F x - x) is again such a lift: its derivative (1 - w) + w F' is positive. So the lifts interpolate between the identity and F through circle diffeomorphisms. This file makes the interpolation smooth in all variables at once, including the inverses, and uses it to extend φ across a product collar N × AddCircle T with a smooth real depth function: equal to φ on one side of the collar and to the identity on the other. This extends a boundary-circle diffeomorphism of a surface into a collar of that boundary circle.

The general construction is AddCircle.prodDiffeomorphOfLift. Let L : ℝ × ℝ → ℝ be a C^n family of lifts, L (s, x + T) = L (s, x) + T, with positive derivative in x, and let κ : N → ℝ be a C^n function on a manifold N, possibly with boundary or corners. Then (a, [x]) ↦ (a, [L (κ a, x)]) is a C^n diffeomorphism of N × AddCircle T. The forward map is smooth because the quotient map ℝ → AddCircle T is a local diffeomorphism. For the inverse, the map (s, x) ↦ (s, L (s, x)) of the plane is a bijection whose derivative is invertible everywhere, so it is an open map, hence a homeomorphism, and its inverse is C^n by the inverse function theorem; the inverse is again a family of lifts and descends to the circle.

Every C^n diffeomorphism φ of the circle, n ≠ 0, has such a presentation, or the mirror one: by Diffeomorph.exists_addCircle_lift it has a C^n lift with either F (x + T) = F x + T and F' > 0 or F (x + T) = F x - T and F' < 0. Hence every diffeomorphism of the circle is the final map of a diffeotopy, or is so after composing with the reflection θ ↦ -θ.

Main definitions

• AddCircle.prodDiffeomorphOfLift: the level-preserving diffeomorphism (a, [x]) ↦ (a, [L (κ a, x)]) of N × AddCircle T.
• AddCircle.diffeotopyOfLift: the diffeotopy of AddCircle T which at time t is the circle map with lift x ↦ x + sin (π t / 2) ^ 2 (F x - x), from the identity to the map with lift F.
• AddCircle.collarDiffeomorphOfLift: the level-preserving diffeomorphism of N × AddCircle T with lift x ↦ x + smoothTransition (1 - depth r) (F x - x) at parameter r.
• AddCircle.halfCylinderDiffeotopyOfLift: a motion on an inward half-cylinder, fixed beyond depth two and agreeing with the prescribed circle map through depth one at the final time.

Main results

• AddCircle.diffeotopyOfLift_final_apply_coe: every orientation-preserving C^n diffeomorphism of the circle, n ≠ 0, presented by a lift, is the final map of a diffeotopy.
• Diffeomorph.exists_diffeotopy_final_eq_or_final_eq_comp_neg: every C^n diffeomorphism φ of the circle, n ≠ 0, is the final map of a diffeotopy, or φ ∘ (θ ↦ -θ) is.
• AddCircle.collarDiffeomorphOfLift_apply_coe_of_nonpos and AddCircle.collarDiffeomorphOfLift_apply_of_one_le: the collar diffeomorphism is (r, θ) ↦ (r, φ θ) at depths at most zero and the identity at depths at least one; likewise for its inverse (AddCircle.collarDiffeomorphOfLift_symm_apply_coe_of_nonpos, AddCircle.collarDiffeomorphOfLift_symm_apply_of_one_le).

References

• M. W. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §§1–2, for diffeotopies and their extension across collars.
• B. Farb, D. Margalit, A Primer on Mapping Class Groups, Section 2.1, for lifts of circle homeomorphisms and the two isotopy classes of homeomorphisms of the circle.

Families of lifts on the plane

Families of circle diffeomorphisms

noncomputable def AddCircle.prodDiffeomorphOfLift {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {L : ℝ × ℝ → ℝ} {N : Type u_1} {E' : Type u_2} {H' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] (hL : ContDiff ℝ n L) (hn : n ≠ 0) (hper : ∀ (s x : ℝ), L (s, x + T) = L (s, x) + T) (hpos : ∀ (s x : ℝ), 0 < deriv (fun (y : ℝ) => L (s, y)) x) (κ : N → ℝ) (hκ : ContMDiff I' (modelWithCornersSelf ℝ ℝ) n κ) : Diffeomorph (I'.prod (modelWithCornersSelf ℝ ℝ)) (I'.prod (modelWithCornersSelf ℝ ℝ)) (N × AddCircle T) (N × AddCircle T) n

A smooth family of circle diffeomorphisms. For a C^n family L of lifts, L (s, x + T) = L (s, x) + T, with positive derivative in x, and a C^n function κ on a manifold N, the map (a, [x]) ↦ (a, [L (κ a, x)]) is a level-preserving C^n diffeomorphism of N × AddCircle T. Its slice at a is the orientation-preserving circle diffeomorphism with lift L (κ a, ·).

@[simp]

theorem AddCircle.prodDiffeomorphOfLift_apply_coe {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {L : ℝ × ℝ → ℝ} {N : Type u_1} {E' : Type u_2} {H' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] (hL : ContDiff ℝ n L) (hn : n ≠ 0) (hper : ∀ (s x : ℝ), L (s, x + T) = L (s, x) + T) (hpos : ∀ (s x : ℝ), 0 < deriv (fun (y : ℝ) => L (s, y)) x) (κ : N → ℝ) (hκ : ContMDiff I' (modelWithCornersSelf ℝ ℝ) n κ) (a : N) (x : ℝ) : (prodDiffeomorphOfLift hL hn hper hpos κ hκ) (a, ↑x) = (a, ↑(L (κ a, x)))

@[simp]

theorem AddCircle.fst_prodDiffeomorphOfLift {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {L : ℝ × ℝ → ℝ} {N : Type u_1} {E' : Type u_2} {H' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] (hL : ContDiff ℝ n L) (hn : n ≠ 0) (hper : ∀ (s x : ℝ), L (s, x + T) = L (s, x) + T) (hpos : ∀ (s x : ℝ), 0 < deriv (fun (y : ℝ) => L (s, y)) x) (κ : N → ℝ) (hκ : ContMDiff I' (modelWithCornersSelf ℝ ℝ) n κ) (p : N × AddCircle T) : ((prodDiffeomorphOfLift hL hn hper hpos κ hκ) p).1 = p.1

@[simp]

theorem AddCircle.fst_prodDiffeomorphOfLift_symm {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {L : ℝ × ℝ → ℝ} {N : Type u_1} {E' : Type u_2} {H' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] (hL : ContDiff ℝ n L) (hn : n ≠ 0) (hper : ∀ (s x : ℝ), L (s, x + T) = L (s, x) + T) (hpos : ∀ (s x : ℝ), 0 < deriv (fun (y : ℝ) => L (s, y)) x) (κ : N → ℝ) (hκ : ContMDiff I' (modelWithCornersSelf ℝ ℝ) n κ) (p : N × AddCircle T) : ((prodDiffeomorphOfLift hL hn hper hpos κ hκ).symm p).1 = p.1

@[simp]

theorem AddCircle.prodDiffeomorphOfLift_symm_apply_coe {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {L : ℝ × ℝ → ℝ} {N : Type u_1} {E' : Type u_2} {H' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace N] [ChartedSpace H' N] (hL : ContDiff ℝ n L) (hn : n ≠ 0) (hper : ∀ (s x : ℝ), L (s, x + T) = L (s, x) + T) (hpos : ∀ (s x : ℝ), 0 < deriv (fun (y : ℝ) => L (s, y)) x) (κ : N → ℝ) (hκ : ContMDiff I' (modelWithCornersSelf ℝ ℝ) n κ) (a : N) (x : ℝ) : (prodDiffeomorphOfLift hL hn hper hpos κ hκ).symm (a, ↑(L (κ a, x))) = (a, ↑x)

The inverse of prodDiffeomorphOfLift undoes the lift L (κ a, ·) on the slice at a.

Interpolating a lift to the identity

noncomputable def AddCircle.diffeotopyOfLift {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {F : ℝ → ℝ} (hF : ContDiff ℝ n F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) : TauCeti.Diffeotopy (modelWithCornersSelf ℝ ℝ) n (AddCircle T)

Orientation-preserving circle diffeomorphisms are diffeotopic to the identity. For a C^n lift F, n ≠ 0, with F (x + T) = F x + T and F' > 0, the diffeotopy of AddCircle T which at time t is the circle diffeomorphism with lift x ↦ x + sin (π t / 2) ^ 2 (F x - x). It starts at the identity and ends at the diffeomorphism with lift F.

@[simp]

theorem AddCircle.diffeotopyOfLift_apply_coe {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {F : ℝ → ℝ} (hF : ContDiff ℝ n F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (t : ↑unitInterval) (x : ℝ) : (fun (p : ↑unitInterval × AddCircle T) => ((diffeotopyOfLift hF hn hper hpos).toDiffeomorph p).2) (t, ↑x) = ↑(x + Real.sin (Real.pi * ↑t / 2) ^ 2 * (F x - x))

At time t the diffeotopy diffeotopyOfLift is the circle map with lift x ↦ x + sin (π t / 2) ^ 2 (F x - x).

theorem AddCircle.diffeotopyOfLift_final_apply_coe {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} {F : ℝ → ℝ} (hF : ContDiff ℝ n F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (x : ℝ) : (diffeotopyOfLift hF hn hper hpos).final ↑x = ↑(F x)

The diffeotopy diffeotopyOfLift ends at the circle diffeomorphism with lift F.

Extension across a product collar

noncomputable def AddCircle.collarDiffeomorphOfLift {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) : Diffeomorph (J.prod (modelWithCornersSelf ℝ ℝ)) (J.prod (modelWithCornersSelf ℝ ℝ)) (N × AddCircle T) (N × AddCircle T) ↑n

Extension of a circle diffeomorphism across a product collar. For a C^n lift F, n ≠ 0, with F (x + T) = F x + T and F' > 0, and a smooth depth function on N, this is (r, [x]) ↦ (r, [x + smoothTransition (1 - depth r) (F x - x)]). It is the circle diffeomorphism with lift F at depths at most zero and the identity at depths at least one. The parameter manifold may have boundary, allowing inward half-collars.

@[simp]

theorem AddCircle.collarDiffeomorphOfLift_apply_coe {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) (r : N) (x : ℝ) : (collarDiffeomorphOfLift hF hn hper hpos depth hdepth) (r, ↑x) = (r, ↑(x + (1 - depth r).smoothTransition * (F x - x)))

@[simp]

theorem AddCircle.fst_collarDiffeomorphOfLift {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) (p : N × AddCircle T) : ((collarDiffeomorphOfLift hF hn hper hpos depth hdepth) p).1 = p.1

@[simp]

theorem AddCircle.fst_collarDiffeomorphOfLift_symm {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) (p : N × AddCircle T) : ((collarDiffeomorphOfLift hF hn hper hpos depth hdepth).symm p).1 = p.1

theorem AddCircle.collarDiffeomorphOfLift_apply_coe_of_nonpos {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) {r : N} (hr : depth r ≤ 0) (x : ℝ) : (collarDiffeomorphOfLift hF hn hper hpos depth hdepth) (r, ↑x) = (r, ↑(F x))

At nonpositive depth, the collar map is the circle diffeomorphism with lift F.

theorem AddCircle.collarDiffeomorphOfLift_apply_of_one_le {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) {r : N} (hr : 1 ≤ depth r) (θ : AddCircle T) : (collarDiffeomorphOfLift hF hn hper hpos depth hdepth) (r, θ) = (r, θ)

At depth at least one, the collar map is the identity.

theorem AddCircle.collarDiffeomorphOfLift_symm_apply_coe_of_nonpos {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) {r : N} (hr : depth r ≤ 0) (x : ℝ) : (collarDiffeomorphOfLift hF hn hper hpos depth hdepth).symm (r, ↑(F x)) = (r, ↑x)

At nonpositive depth, the inverse collar map undoes the lift F.

theorem AddCircle.collarDiffeomorphOfLift_symm_apply_of_one_le {T : ℝ} [Fact (0 < T)] {N : Type u_1} {E : Type u_2} {H : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {J : ModelWithCorners ℝ E H} [TopologicalSpace N] [ChartedSpace H N] {F : ℝ → ℝ} {n : ℕ∞} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (depth : N → ℝ) (hdepth : ContMDiff J (modelWithCornersSelf ℝ ℝ) (↑n) depth) {r : N} (hr : 1 ≤ depth r) (θ : AddCircle T) : (collarDiffeomorphOfLift hF hn hper hpos depth hdepth).symm (r, θ) = (r, θ)

At depth at least one, the inverse collar map is the identity.

Motion on an inward half-cylinder

noncomputable def AddCircle.halfCylinderDiffeotopyOfLift {T : ℝ} [Fact (0 < T)] {n : ℕ∞} {F : ℝ → ℝ} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) : TauCeti.Diffeotopy ((modelWithCornersEuclideanHalfSpace 1).prod (modelWithCornersSelf ℝ ℝ)) (↑n) (EuclideanHalfSpace 1 × AddCircle T)

A circle lift interpolated on an inward half-cylinder, stationary beyond depth two. At time one it agrees with the prescribed circle map through depth one.

@[simp]

theorem AddCircle.halfCylinderDiffeotopyOfLift_apply_coe {T : ℝ} [Fact (0 < T)] {n : ℕ∞} {F : ℝ → ℝ} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (t : ↑unitInterval) (r : EuclideanHalfSpace 1) (x : ℝ) : (fun (p : ↑unitInterval × EuclideanHalfSpace 1 × AddCircle T) => ((halfCylinderDiffeotopyOfLift hF hn hper hpos).toDiffeomorph p).2) (t, r, ↑x) = (r, ↑(x + (↑t * (2 - (↑r).ofLp 0).smoothTransition).smoothTransition * (F x - x)))

The half-cylinder motion in lifted circle coordinates.

theorem AddCircle.halfCylinderDiffeotopyOfLift_apply_of_two_le {T : ℝ} [Fact (0 < T)] {n : ℕ∞} {F : ℝ → ℝ} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) (t : ↑unitInterval) {r : EuclideanHalfSpace 1} (hr : 2 ≤ (↑r).ofLp 0) (θ : AddCircle T) : (fun (p : ↑unitInterval × EuclideanHalfSpace 1 × AddCircle T) => ((halfCylinderDiffeotopyOfLift hF hn hper hpos).toDiffeomorph p).2) (t, r, θ) = (r, θ)

The half-cylinder motion fixes every point at depth at least two, at every time.

theorem AddCircle.halfCylinderDiffeotopyOfLift_final_apply_coe_of_le_one {T : ℝ} [Fact (0 < T)] {n : ℕ∞} {F : ℝ → ℝ} (hF : ContDiff ℝ (↑n) F) (hn : n ≠ 0) (hper : ∀ (x : ℝ), F (x + T) = F x + T) (hpos : ∀ (x : ℝ), 0 < deriv F x) {r : EuclideanHalfSpace 1} (hr : (↑r).ofLp 0 ≤ 1) (x : ℝ) : (halfCylinderDiffeotopyOfLift hF hn hper hpos).final (r, ↑x) = (r, ↑(F x))

Through depth one, the final half-cylinder map is the product map of the prescribed lift.

theorem Diffeomorph.exists_diffeotopy_final_eq_or_final_eq_comp_neg {T : ℝ} [Fact (0 < T)] {n : WithTop ℕ∞} (φ : Diffeomorph (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) (AddCircle T) (AddCircle T) n) (hn : n ≠ 0) : ∃ (Ψ : TauCeti.Diffeotopy (modelWithCornersSelf ℝ ℝ) n (AddCircle T)), ⇑Ψ.final = ⇑φ ∨ ⇑Ψ.final = ⇑φ ∘ Neg.neg

Diffeotopy classes of circle diffeomorphisms. A C^n diffeomorphism φ of AddCircle T, n ≠ 0, is the final map of a diffeotopy starting at the identity, or its composite θ ↦ φ (-θ) with the reflection is.