Radial deformation onto the bottom and sides of a cube cylinder

Projection from height two above the cube's centre gives a deformation cubeLiftDeform from the bottom-and-sides subspace to each point of the cylinder, reaching that point at cubeLiftTime. This time vanishes exactly on cylinderExtensionDomain (Cube.boundary N). The construction includes the zero-dimensional cube. It is the geometric input for relative homotopy lifting along the bottom-and-sides inclusion of I × Iᴺ; the square (N = Unit) is the open-box case. Its denominator and initial projection reuse the unit-ball radial projection from TauCeti.Topology.Homotopy.Extension.Ball through cubeHomeomorphClosedBall.

References

• A. Strøm, Note on cofibrations II, Math. Scand. 22 (1968), 130–142.

noncomputable def TauCeti.cubeLiftDen {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : ℝ

The radial denominator for the bottom-and-sides projection.

theorem TauCeti.cubeLiftDen_def {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftDen x = max (2 - ↑x.1) (2 * cubeRadius x.2)

theorem TauCeti.one_le_cubeLiftDen {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : 1 ≤ cubeLiftDen x

theorem TauCeti.cubeLiftDen_le_two {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftDen x ≤ 2

noncomputable def TauCeti.cubeLiftTime {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : ℝ

Time at which the radial deformation reaches x.

theorem TauCeti.cubeLiftTime_def {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftTime x = 2 / cubeLiftDen x - 1

theorem TauCeti.cubeLiftTime_mem {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftTime x ∈ unitInterval

theorem TauCeti.continuous_cubeLiftTime {N : Type u_1} [Fintype N] : Continuous cubeLiftTime

@[simp]

theorem TauCeti.cubeLiftTime_eq_zero {N : Type u_1} [Fintype N] {x : ↑unitInterval × (N → ↑unitInterval)} (hx : x ∈ cylinderExtensionDomain (Cube.boundary N)) : cubeLiftTime x = 0

noncomputable def TauCeti.cubeLiftDeform {N : Type u_1} [Fintype N] (s : ↑unitInterval) (x : ↑unitInterval × (N → ↑unitInterval)) : ↑unitInterval × (N → ↑unitInterval)

Run the radial segment from the bottom and sides, stopping when it reaches x.

theorem TauCeti.cubeLiftDeform_def {N : Type u_1} [Fintype N] (s : ↑unitInterval) (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftDeform s x = have a := cubeLiftTime x - min (cubeLiftTime x) ↑s; (Set.projIcc 0 1 ⋯ (↑x.1 + a * (↑x.1 - 2)), cubeScale (1 + a) x.2)

theorem TauCeti.continuous_cubeLiftDeform {N : Type u_1} [Fintype N] : Continuous fun (y : ↑unitInterval × ↑unitInterval × (N → ↑unitInterval)) => cubeLiftDeform y.1 y.2

@[simp]

theorem TauCeti.cubeLiftDeform_one {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftDeform 1 x = x

@[simp]

theorem TauCeti.cubeLiftDeform_of_mem {N : Type u_1} [Fintype N] (s : ↑unitInterval) {x : ↑unitInterval × (N → ↑unitInterval)} (hx : x ∈ cylinderExtensionDomain (Cube.boundary N)) : cubeLiftDeform s x = x

@[simp]

theorem TauCeti.cubeLiftDeform_time {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftDeform ⟨cubeLiftTime x, ⋯⟩ x = x

theorem TauCeti.cubeLiftDeform_zero_mem {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftDeform 0 x ∈ cylinderExtensionDomain (Cube.boundary N)

theorem TauCeti.cubeLiftTime_eq_zero_iff {N : Type u_1} [Fintype N] (x : ↑unitInterval × (N → ↑unitInterval)) : cubeLiftTime x = 0 ↔ x ∈ cylinderExtensionDomain (Cube.boundary N)

theorem TauCeti.cubeLiftDeform_zero_one {N : Type u_1} [Fintype N] (z : N → ↑unitInterval) : cubeLiftDeform 0 (1, z) = if cubeRadius z ≤ 1 / 2 then (0, cubeScale 2 z) else (Set.projIcc 0 1 ⋯ (2 - 1 / cubeRadius z), cubeScale (1 / cubeRadius z) z)

The initial radial projection of the top face lands on the bottom for radius at most 1 / 2, and otherwise rescales by the reciprocal radius.

theorem TauCeti.cubeLiftDeform_zero_one_snd_mem_boundary {N : Type u_1} [Fintype N] {z : N → ↑unitInterval} (hz : 1 / 2 < cubeRadius z) : (cubeLiftDeform 0 (1, z)).2 ∈ Cube.boundary N

Above radius 1 / 2, the initial projection of the top face lies on a boundary side.

theorem TauCeti.eq_zero_or_eq_one_or_mem_boundary_of_mem_cylinderExtensionDomain {N : Type u_1} {x : ↑unitInterval × (Option N → ↑unitInterval)} (hx : x ∈ cylinderExtensionDomain (Cube.boundary (Option N))) : (x.2 none = 0 ∨ x.2 none = 1) ∨ (piOptionEquivProdHomeomorph fun (x : Option N) => ↑unitInterval).symm (x.1, fun (i : N) => x.2 (some i)) ∈ Cube.boundary (Option N)

For x in {0} × I^(Option N) ∪ I × ∂I^(Option N), either x.2 none ∈ {0, 1}, or the point obtained from x.2 by replacing its none coordinate with x.1 (via piOptionEquivProdHomeomorph, after dropping x.2 none) lies in ∂I^(Option N).