Relative lifting on parameterized cube cylinders #
Homotopy lifting for A × (I × Iᴺ) gives lifting relative to the bottom and boundary sides
of each cube cylinder, continuously in the parameter space A. The prescribed lift need only
be defined on that subspace. The proof applies zero-set strong-deformation-retract lifting
to the radial deformation, keeping the A coordinate fixed.
References #
- A. Hatcher, Algebraic Topology, Section 4.2, relative homotopy lifting for fibrations.
- A. Strøm, Note on cofibrations II, Math. Scand. 22 (1968), 130–142.
theorem
TauCeti.HasHomotopyLiftingProperty.exists_lift_openBox
{N : Type u_1}
[Finite N]
{A : Type u_2}
[TopologicalSpace A]
{E : Type u_3}
{B : Type u_4}
[TopologicalSpace E]
[TopologicalSpace B]
{p : E → B}
(hp : HasHomotopyLiftingProperty p (A × ↑unitInterval × (N → ↑unitInterval)))
(f : C(↑{y : A × ↑unitInterval × (N → ↑unitInterval) | y.2 ∈ cylinderExtensionDomain (Cube.boundary N)}, E))
(H : C(A × ↑unitInterval × (N → ↑unitInterval), B))
(hf :
∀ (x : ↑{y : A × ↑unitInterval × (N → ↑unitInterval) | y.2 ∈ cylinderExtensionDomain (Cube.boundary N)}),
p (f x) = H ↑x)
:
∃ (G : C(A × ↑unitInterval × (N → ↑unitInterval), E)),
p ∘ ⇑G = ⇑H ∧ ∀ (x : ↑{y : A × ↑unitInterval × (N → ↑unitInterval) | y.2 ∈ cylinderExtensionDomain (Cube.boundary N)}), G ↑x = f x
Homotopy lifting for a parameterized cube cylinder extends compatible lifts on its bottom
and boundary sides, continuously in an arbitrary parameter space A.