The radial push on the Euclidean disk

For 0 ≤ r, the straight-line homotopy TauCeti.radialPush r maps the closed unit ball into itself, so it restricts to a homotopy TauCeti.TopCat.diskRadialPush r of the disk TopCat.disk n. It starts at the identity and, for 0 < r ≤ 1, fixes the boundary sphere at all times and ends by sending the shell r ≤ ‖x‖ into the boundary sphere. Its end map x ↦ x / max r ‖x‖ and the reversed homotopy from it to the identity are how a map defined on the boundary sphere is spread over the outer shell of a disk, as in cell reattachment arguments.

Main declarations

• TauCeti.TopCat.diskRadialPush: the radial push TauCeti.radialPush r on the disk.
• TauCeti.TopCat.diskRadialPush_diskBoundaryInclusion: it fixes the boundary sphere.
• TauCeti.TopCat.norm_diskRadialPush_one: at the end it sends the shell r ≤ ‖x‖ into the boundary sphere.
• TauCeti.TopCat.coe_diskRadialPush_one_of_norm_le, TauCeti.TopCat.coe_diskRadialPush_one_of_le_norm: its end map is x ↦ r⁻¹ • x on the ball of radius r and x ↦ x / ‖x‖ on the shell r ≤ ‖x‖.

noncomputable def TauCeti.TopCat.diskRadialPush {r : ℝ} (n : ℕ) (hr : 0 ≤ r) : C(↑unitInterval × ↑(TopCat.disk n), ↑(TopCat.disk n))

The radial push TauCeti.radialPush r, for 0 ≤ r, as a homotopy of the disk TopCat.disk n: at time t it sends x to (1 - t) • x + t • r⁻¹ • radialRetraction r x.

@[simp]

theorem TauCeti.TopCat.coe_diskRadialPush_apply_down {n : ℕ} {r : ℝ} (hr : 0 ≤ r) (t : ↑unitInterval) (x : ↑(TopCat.disk n)) : ↑((diskRadialPush n hr) (t, x)).down = radialPush r t ↑x.down

@[simp]

theorem TauCeti.TopCat.diskRadialPush_zero {n : ℕ} {r : ℝ} (hr : 0 ≤ r) (x : ↑(TopCat.disk n)) : (diskRadialPush n hr) (0, x) = x

At time 0 the radial push on the disk is the identity.

theorem TauCeti.TopCat.diskRadialPush_diskBoundaryInclusion {n : ℕ} {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) (t : ↑unitInterval) (s : ↑(TopCat.diskBoundary n)) : (diskRadialPush n ⋯) (t, (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion n)) s) = (CategoryTheory.ConcreteCategory.hom (TopCat.diskBoundaryInclusion n)) s

For 0 < r ≤ 1, the radial push on the disk fixes the boundary sphere.

theorem TauCeti.TopCat.norm_diskRadialPush_one {n : ℕ} {r : ℝ} (hr : 0 < r) {x : ↑(TopCat.disk n)} (hx : r ≤ ‖↑x.down‖) : ‖↑((diskRadialPush n ⋯) (1, x)).down‖ = 1

At the end, the radial push on the disk sends the shell r ≤ ‖x‖ into the boundary sphere.

theorem TauCeti.TopCat.coe_diskRadialPush_one_of_norm_le {n : ℕ} {r : ℝ} (hr : 0 ≤ r) {x : ↑(TopCat.disk n)} (hx : ‖↑x.down‖ ≤ r) : ↑((diskRadialPush n hr) (1, x)).down = r⁻¹ • ↑x.down

At the end, the radial push on the disk sends a point x of the ball of radius r to r⁻¹ • x.

theorem TauCeti.TopCat.coe_diskRadialPush_one_of_le_norm {n : ℕ} {r : ℝ} (hr : 0 < r) {x : ↑(TopCat.disk n)} (hx : r ≤ ‖↑x.down‖) : ↑((diskRadialPush n ⋯) (1, x)).down = ‖↑x.down‖⁻¹ • ↑x.down

At the end, the radial push on the disk sends a point x of the shell r ≤ ‖x‖ to x / ‖x‖.