Extending boundary-fixing homeomorphisms of a closed ball

A homeomorphism of the closed unit ball that fixes the unit sphere extends by the identity outside the ball. This construction works in every real normed space. It supplies the ambient homeomorphism used in Alexander's trick.

The extension is expressed using the radial retraction, so continuity at the sphere follows without a separate gluing argument.

References

• B. Farb, D. Margalit, A Primer on Mapping Class Groups, Section 2.2.1, Lemma 2.1.

noncomputable def Homeomorph.extendClosedBall {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) : E ≃ₜ E

Extend a homeomorphism of the closed unit ball fixing the unit sphere by the identity outside the ball.

@[simp]

theorem Homeomorph.extendClosedBall_coe {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.extendClosedBall hf) ↑x = ↑(f x)

On the closed ball the extension agrees with the given homeomorphism.

theorem Homeomorph.extendClosedBall_of_one_le {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 : E} (hx : 1 ≤ ‖x‖) : (f.extendClosedBall hf) x = x

The extension fixes the complement of the open unit ball, including its boundary.

@[simp]

theorem Homeomorph.symm_extendClosedBall {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) : (f.extendClosedBall hf).symm = f.symm.extendClosedBall ⋯

Extending the inverse gives the inverse extension.

@[simp]

theorem Homeomorph.norm_extendClosedBall_le_one_iff {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 : E) : ‖(f.extendClosedBall hf) x‖ ≤ 1 ↔ ‖x‖ ≤ 1

The extension and its inverse preserve membership in the closed unit ball.

theorem Homeomorph.norm_extendClosedBall_sub_le {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 : E) : ‖(f.extendClosedBall hf) x - x‖ ≤ 2

The identity extension moves every point by at most twice the unit radius.