The unit sphere is a closed cofibration in the closed unit ball

The unit sphere of a real seminormed space has the homotopy extension property inside the closed unit ball. Concretely, the cylinder I × D over the closed unit ball D retracts onto {0} × D ∪ I × S, where S is the unit sphere, by radial projection away from the point of the cylinder axis at height 2: the ray from that point through (t, x) leaves the cylinder either through its bottom face or through its side, and the retraction sends (t, x) to that exit point.

This is the basic example of a closed cofibration. It is the geometric input for the homotopy extension property of the inclusion of a skeleton of a CW complex into the next one, whose cells are attached along maps defined on such spheres.

As a consequence, a map out of the unit sphere is null-homotopic exactly when it extends over the closed unit ball: a null-homotopy is extended from the sphere to the ball, starting at a constant map, and conversely the closed ball is contractible. This is the criterion for extending a map over a cell attached along a sphere.

The retraction also compresses maps of pairs. If a map g of the closed unit ball sending the sphere into B is homotopic, through such maps, to a map into B, then g is homotopic relative to the sphere to a map into B. This is how vanishing relative homotopy groups give the hypothesis of the compression lemma for CW complexes.

Main declarations

• TauCeti.ballRadialDen, TauCeti.ballRadialProjection: the shared radial denominator and projection in ambient coordinates, also used for the bottom-and-sides deformation of cubes.
• TauCeti.ballRadialProjection_spec, TauCeti.ballRadialProjection_eq_self: the projection lands on the bottom and sides and fixes that subspace.
• TauCeti.hasHomotopyExtensionProperty_sphere_closedBall: the unit sphere has the homotopy extension property inside the closed unit ball.
• ContinuousMap.nullhomotopic_iff_exists_extension_closedBall: a map out of the unit sphere is null-homotopic exactly when it extends over the closed unit ball.
• ContinuousMap.HomotopicWith.exists_homotopicRel_range_subset: a map of pairs homotopic through maps of pairs to a map into B is homotopic relative to the sphere to a map into B.

References

• A. Hatcher, Algebraic Topology, Chapter 0, proof of Proposition 0.16, which retracts Dⁿ × I onto Dⁿ × {0} ∪ ∂Dⁿ × I by radial projection from the point (0, 2); Section 4.1, the compression criterion preceding Theorem 4.3, for compressing maps of pairs.

def TauCeti.ballRadialDen {E : Type u} [SeminormedAddCommGroup E] (p : ↑unitInterval × ↑(Metric.closedBall 0 1)) : ℝ

The denominator for radial projection from height two onto the bottom and sides of the unit-ball cylinder. It is shared with the radial deformation of finite cubes.

theorem TauCeti.ballRadialDen_def {E : Type u} [SeminormedAddCommGroup E] (p : ↑unitInterval × ↑(Metric.closedBall 0 1)) : ballRadialDen p = max (2 - ↑p.1) (2 * ‖↑p.2‖)

noncomputable def TauCeti.ballRadialProjection {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑unitInterval × ↑(Metric.closedBall 0 1)) : ℝ × E

Radial projection of the cylinder over the closed unit ball away from the point at height 2 on its axis, written in the ambient coordinates ℝ × E. The scale factor is the smaller of the factors needed to reach the bottom face and the side of the cylinder. Taking the maximum in the denominator gives a single continuous formula, including at the cylinder axis.

theorem TauCeti.ballRadialProjection_def {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑unitInterval × ↑(Metric.closedBall 0 1)) : ballRadialProjection p = (2 - 2 * (2 - ↑p.1) / ballRadialDen p, (2 / ballRadialDen p) • ↑p.2)

theorem TauCeti.continuous_ballRadialProjection {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : Continuous ballRadialProjection

theorem TauCeti.ballRadialProjection_spec {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑unitInterval × ↑(Metric.closedBall 0 1)) : (ballRadialProjection p).1 ∈ unitInterval ∧ (ballRadialProjection p).2 ∈ Metric.closedBall 0 1 ∧ ((ballRadialProjection p).1 = 0 ∨ (ballRadialProjection p).2 ∈ Metric.sphere 0 1)

The radial projection lands in the cylinder, and in the union of its bottom face with the part of the cylinder lying over the sphere.

@[simp]

theorem TauCeti.ballRadialProjection_eq_self {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑unitInterval × ↑(Metric.closedBall 0 1)) (hp : p ∈ cylinderExtensionDomain (Subtype.val ⁻¹' Metric.sphere 0 1)) : ballRadialProjection p = (↑p.1, ↑p.2)

The radial projection fixes the bottom face of the cylinder and the part of the cylinder lying over the sphere.

theorem TauCeti.hasHomotopyExtensionProperty_sphere_closedBall {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : HasHomotopyExtensionProperty (Subtype.val ⁻¹' Metric.sphere 0 1)

The unit sphere of a real seminormed space has the homotopy extension property inside the closed unit ball: the inclusion of the unit sphere is a closed cofibration.

theorem ContinuousMap.nullhomotopic_iff_exists_extension_closedBall {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {Y : Type u_2} [TopologicalSpace Y] (g : C(↑(Metric.sphere 0 1), Y)) : g.Nullhomotopic ↔ ∃ (G : C(↑(Metric.closedBall 0 1), Y)), ∀ (y : ↑(Metric.sphere 0 1)), G ⟨↑y, ⋯⟩ = g y

A map out of the unit sphere is null-homotopic exactly when it extends over the closed unit ball.

theorem ContinuousMap.HomotopicWith.exists_homotopicRel_range_subset {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {Y : Type u_2} [TopologicalSpace Y] {B : Set Y} {g g₁ : C(↑(Metric.closedBall 0 1), Y)} (h : g.HomotopicWith g₁ fun (f : C(↑(Metric.closedBall 0 1), Y)) => Set.MapsTo ⇑f {x : ↑(Metric.closedBall 0 1) | ↑x ∈ Metric.sphere 0 1} B) (h₁ : Set.range ⇑g₁ ⊆ B) : ∃ (g' : C(↑(Metric.closedBall 0 1), Y)), g.HomotopicRel g' {x : ↑(Metric.closedBall 0 1) | ↑x ∈ Metric.sphere 0 1} ∧ Set.range ⇑g' ⊆ B

Compressing a map of pairs relative to the sphere. Let g map the closed unit ball of a real seminormed space into Y, and let B ⊆ Y. If g is homotopic, through maps sending the unit sphere into B, to a map with values in B, then g is homotopic relative to the unit sphere to a map with values in B.