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

In a real seminormed space and for a radius 0 < r ≤ 1, the rescaled radial retraction r⁻¹ • TauCeti.radialRetraction r maps the closed unit ball into itself 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.

Points of positive norm at most r end at r⁻¹ • y. A vector of seminorm zero instead ends at zero, and at time t its image is (1 - (t : ℝ)) • y.

In a normed space 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_radialPush: its norm is the linear interpolation of the endpoint norms.
• 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} [SeminormedAddCommGroup 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 positive-norm point y of the closed unit ball along its ray, from y towards r⁻¹ • y if ‖y‖ ≤ r and towards ‖y‖⁻¹ • y otherwise. If ‖y‖ = 0, its value is (1 - (t : ℝ)) • y.

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.radialPush_of_norm_eq_zero {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hy : ‖y‖ = 0) (t : ↑unitInterval) : radialPush r t y = (1 - ↑t) • y

On a vector of seminorm zero, the radial push contracts linearly to zero.

@[simp]

theorem TauCeti.radialPush_of_norm_pos_of_norm_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hy0 : 0 < ‖y‖) (hyr : ‖y‖ ≤ r) (t : ↑unitInterval) : radialPush r t y = (1 - ↑t + ↑t * r⁻¹) • y

On a vector of positive norm at most r, the radial push scales by the linear interpolation from 1 to r⁻¹.

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

@[simp]

theorem TauCeti.norm_radialPush {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hr : 0 ≤ r) (t : ↑unitInterval) : ‖radialPush r t y‖ = (1 - ↑t) * ‖y‖ + ↑t * (r⁻¹ * min ‖y‖ r)

The norm along TauCeti.radialPush is the linear interpolation between the initial norm and the norm of the rescaled radial retraction.

theorem TauCeti.norm_le_norm_radialPush {E : Type u_1} [SeminormedAddCommGroup 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} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} {y : E} (hr : 0 ≤ r) (t : ↑unitInterval) (hy : ‖y‖ ≤ 1) : ‖radialPush r t y‖ ≤ 1

For every nonnegative radius, TauCeti.radialPush maps the closed unit ball into itself.

theorem TauCeti.radialPush_of_norm_eq_one {E : Type u_1} [SeminormedAddCommGroup 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} [SeminormedAddCommGroup 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.