Alexander's trick

A homeomorphism f of a real normed space with uniformly bounded displacement is joined to the identity by the ambient isotopy x ↦ t • f (t⁻¹ • x) for t > 0, starting at the identity at t = 0. The displacement at time t is at most t times the original bound, giving joint continuity at time zero. The inverse is the same construction applied to f.symm.

In particular a homeomorphism of the closed unit ball fixing its boundary is isotopic to the identity relative to the boundary. Its identity extension has an isotopy supported in the ball of radius t at time t. This is the disc step in the Alexander method for classifying homeomorphisms of surfaces after fixing a system of cutting curves.

References

• B. Farb, D. Margalit, A Primer on Mapping Class Groups, Section 2.2.1, Lemma 2.1 (the Alexander lemma); Section 2.3 (the Alexander method).

noncomputable def Homeomorph.alexanderIsotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E ≃ₜ E) (C : ℝ) (hC : ∀ (x : E), ‖f x - x‖ ≤ C) : TauCeti.AmbientIsotopy E

Alexander's trick for bounded displacement. Conjugating a homeomorphism by dilations joins it to the identity, provided its displacement is uniformly bounded.

theorem Homeomorph.alexanderIsotopy_apply_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E ≃ₜ E) (C : ℝ) (hC : ∀ (x : E), ‖f x - x‖ ≤ C) {t : ↑unitInterval} (ht : t ≠ 0) (x : E) : (f.alexanderIsotopy C hC).toContinuousMap (t, x) = ↑t • f ((↑t)⁻¹ • x)

At positive times Alexander's isotopy is conjugation by scalar multiplication.

@[simp]

theorem Homeomorph.alexanderIsotopy_final {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E ≃ₜ E) (C : ℝ) (hC : ∀ (x : E), ‖f x - x‖ ≤ C) (x : E) : (f.alexanderIsotopy C hC).final x = f x

The endpoint of Alexander's isotopy is the original homeomorphism.

theorem Homeomorph.alexanderIsotopy_apply_of_le_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E ≃ₜ E) (C : ℝ) (hC : ∀ (x : E), ‖f x - x‖ ≤ C) (hf : ∀ (x : E), 1 ≤ ‖x‖ → f x = x) (t : ↑unitInterval) {x : E} (hx : ↑t ≤ ‖x‖) : (f.alexanderIsotopy C hC).toContinuousMap (t, x) = x

If f fixes the complement of the open unit ball, its Alexander isotopy at time t fixes the complement of the open ball of radius t.

noncomputable def Homeomorph.alexanderIsotopyClosedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ↑(Metric.closedBall 0 1) ≃ₜ ↑(Metric.closedBall 0 1)) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑x‖ = 1 → f x = x) : TauCeti.AmbientIsotopy ↑(Metric.closedBall 0 1)

Alexander's lemma. A homeomorphism of the closed unit ball fixing the unit sphere is joined to the identity through homeomorphisms of the ball fixing the sphere.

@[simp]

theorem Homeomorph.coe_alexanderIsotopyClosedBall_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ↑(Metric.closedBall 0 1) ≃ₜ ↑(Metric.closedBall 0 1)) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑x‖ = 1 → f x = x) (t : ↑unitInterval) (x : ↑(Metric.closedBall 0 1)) : ↑((f.alexanderIsotopyClosedBall hf).toContinuousMap (t, x)) = ((f.extendClosedBall hf).alexanderIsotopy 2 ⋯).toContinuousMap (t, ↑x)

The pointwise formula for the ball isotopy, read in the ambient space.

@[simp]

theorem Homeomorph.alexanderIsotopyClosedBall_final {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ↑(Metric.closedBall 0 1) ≃ₜ ↑(Metric.closedBall 0 1)) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑x‖ = 1 → f x = x) (x : ↑(Metric.closedBall 0 1)) : (f.alexanderIsotopyClosedBall hf).final x = f x

Alexander's ball isotopy ends at the given homeomorphism.

theorem Homeomorph.alexanderIsotopyClosedBall_apply_of_le_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ↑(Metric.closedBall 0 1) ≃ₜ ↑(Metric.closedBall 0 1)) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑x‖ = 1 → f x = x) (t : ↑unitInterval) (x : ↑(Metric.closedBall 0 1)) (hx : ↑t ≤ ‖↑x‖) : (f.alexanderIsotopyClosedBall hf).toContinuousMap (t, x) = x

Alexander's ball isotopy at time t fixes every point of norm at least t. In particular it fixes the unit sphere throughout.

theorem Homeomorph.coe_alexanderIsotopyClosedBall_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ↑(Metric.closedBall 0 1) ≃ₜ ↑(Metric.closedBall 0 1)) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑x‖ = 1 → f x = x) (t : ↑unitInterval) (x : ↑(Metric.closedBall 0 1)) : ↑((f.alexanderIsotopyClosedBall hf).toContinuousMap (t, ⟨↑t • ↑x, ⋯⟩)) = ↑t • ↑(f x)

Inside the shrinking ball, Alexander's isotopy is the given homeomorphism rescaled.

@[simp]

theorem Homeomorph.alexanderIsotopyClosedBall_apply_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ↑(Metric.closedBall 0 1) ≃ₜ ↑(Metric.closedBall 0 1)) (hf : ∀ (x : ↑(Metric.closedBall 0 1)), ‖↑x‖ = 1 → f x = x) (t : ↑unitInterval) (x : ↑(Metric.closedBall 0 1)) (hx : ‖↑x‖ = 1) : (f.alexanderIsotopyClosedBall hf).toContinuousMap (t, x) = x

The unit sphere is fixed throughout Alexander's ball isotopy.