Pushing a shell of the closed unit ball onto the unit sphere

In a real normed space and for a radius 0 < r ≤ 1, the rescaled radial retraction r⁻¹ • TauCeti.radialRetraction r maps the closed unit ball onto itself: it expands the closed ball of radius r linearly onto the closed unit ball and sends every point of the shell r ≤ ‖y‖ ≤ 1 to the unit sphere along its ray. The straight-line homotopy TauCeti.radialPush r from the identity to it stays inside the closed unit ball, never decreases norms there, and fixes the unit sphere at all times.

This is the deformation which shows that the inclusion of the pair (closed ball, unit sphere) into the pair (closed ball, shell) is a homotopy equivalence of pairs, and similarly, cell by cell, that the skeleta of a CW complex form good pairs.

Main declarations

• TauCeti.radialPush: the straight-line homotopy from the identity to r⁻¹ • TauCeti.radialRetraction r.
• TauCeti.norm_le_norm_radialPush and TauCeti.norm_radialPush_le_one: on the closed unit ball it does not decrease norms and stays in the ball.
• TauCeti.radialPush_of_norm_eq_one: it fixes the unit sphere.
• TauCeti.norm_radialPush_one: at the end it sends the shell r ≤ ‖y‖ to the unit sphere.

References

• A. Hatcher, Algebraic Topology, Section 2.1, the discussion of good pairs before Proposition 2.22.

noncomputable def TauCeti.radialPush {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (t : ↑unitInterval) (y : E) : E

The straight-line homotopy from the identity to the rescaled radial retraction r⁻¹ • TauCeti.radialRetraction r, at time t. For 0 < r ≤ 1 it moves a point y of the closed unit ball along its ray, from y towards r⁻¹ • y if ‖y‖ ≤ r and towards ‖y‖⁻¹ • y otherwise.

Equations

• TauCeti.radialPush r t y = (1 - ↑t) • y + ↑t • r⁻¹ • TauCeti.radialRetraction r y

@[simp]

theorem TauCeti.radialPush_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (y : E) : radialPush r 0 y = y

@[simp]

theorem TauCeti.radialPush_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (r : ℝ) (y : E) : radialPush r 1 y = r⁻¹ • radialRetraction r y

theorem TauCeti.continuous_radialPush {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (hr : 0 ≤ r) : Continuous fun (p : ↑unitInterval × E) => radialPush r p.1 p.2

theorem TauCeti.norm_le_norm_radialPush {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hr : 0 < r) (hr1 : r ≤ 1) (t : ↑unitInterval) (hy : ‖y‖ ≤ 1) : ‖y‖ ≤ ‖radialPush r t y‖

On the closed unit ball, TauCeti.radialPush does not decrease norms.

theorem TauCeti.norm_radialPush_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hr : 0 < r) (hr1 : r ≤ 1) (t : ↑unitInterval) (hy : ‖y‖ ≤ 1) : ‖radialPush r t y‖ ≤ 1

TauCeti.radialPush maps the closed unit ball into itself.

theorem TauCeti.radialPush_of_norm_eq_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hr : 0 < r) (hr1 : r ≤ 1) (t : ↑unitInterval) (hy : ‖y‖ = 1) : radialPush r t y = y

TauCeti.radialPush fixes the unit sphere.

theorem TauCeti.norm_radialPush_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hr : 0 < r) (hy : r ≤ ‖y‖) : ‖radialPush r 1 y‖ = 1

At the end, TauCeti.radialPush r sends the shell r ≤ ‖y‖ to the unit sphere.