Relative homotopy lifting for the open box

A Hurewicz fibration p : E → B lifts homotopies relative to the open box: given a homotopy H : A × I × I → B and a lift g of H on the open box J = I × {0} ∪ ∂I × I (the bottom and the two sides of the square, in coordinates (u, t)), there is a lift of H on the whole square that agrees with g on J (TauCeti.IsHurewiczFibration.exists_lift_openBox). The data on J is passed as a map on the whole square, of which only the values on J are used.

This is the form in which families of paths with prescribed end points are lifted: a homotopy of paths whose end points stay fixed in B lifts to a homotopy of paths whose end points follow prescribed lifts, for instance the constant lifts at a base point for loops (TauCeti.IsHurewiczFibration.loopMap). No cofibration theory is needed.

Main results

• TauCeti.IsHurewiczFibration.exists_lift_openBox: relative homotopy lifting for the pair (A × I × I, A × J).
• TauCeti.IsHurewiczFibration.exists_homotopy_lifts: two lifts of the same family of paths from the same starting points are homotopic through lifts, relative to the starting points.
• TauCeti.IsHurewiczFibration.exists_homotopy_endpoints: two lifts of the same family of paths from the same starting points have homotopic end points, fiberwise over the end points of the paths.

References

• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapter I.7.
• A. Strøm, Note on cofibrations II, Math. Scand. 22 (1968), 130–142.

theorem TauCeti.IsHurewiczFibration.exists_lift_openBox {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {A : Type w} [TopologicalSpace A] (hp : IsHurewiczFibration p) (g : C(A × ↑unitInterval × ↑unitInterval, E)) (H : C(A × ↑unitInterval × ↑unitInterval, B)) (hg : ∀ (a : A) (x : ↑unitInterval × ↑unitInterval), x.2 = 0 ∨ x.1 = 0 ∨ x.1 = 1 → p (g (a, x)) = H (a, x)) : ∃ (G : C(A × ↑unitInterval × ↑unitInterval, E)), p ∘ ⇑G = ⇑H ∧ ∀ (a : A) (x : ↑unitInterval × ↑unitInterval), x.2 = 0 ∨ x.1 = 0 ∨ x.1 = 1 → G (a, x) = g (a, x)

Relative homotopy lifting for the open box. For a Hurewicz fibration p, a homotopy H : A × I × I → B with a lift g on the open box I × {0} ∪ ∂I × I (coordinates (u, t)) lifts to the whole square, agreeing with g on the open box. Only the values of g on the open box matter.

theorem TauCeti.IsHurewiczFibration.exists_homotopy_lifts {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {Y : Type w} [TopologicalSpace Y] (hp : IsHurewiczFibration p) (γ : C(Y × ↑unitInterval, B)) (α α' : C(Y × ↑unitInterval, E)) (hα : ∀ (y : Y) (t : ↑unitInterval), p (α (y, t)) = γ (y, t)) (hα' : ∀ (y : Y) (t : ↑unitInterval), p (α' (y, t)) = γ (y, t)) (h₀ : ∀ (y : Y), α (y, 0) = α' (y, 0)) : ∃ (G : C(Y × ↑unitInterval × ↑unitInterval, E)), (∀ (y : Y) (t : ↑unitInterval), G (y, 0, t) = α (y, t)) ∧ (∀ (y : Y) (t : ↑unitInterval), G (y, 1, t) = α' (y, t)) ∧ (∀ (y : Y) (u : ↑unitInterval), G (y, u, 0) = α (y, 0)) ∧ ∀ (y : Y) (u t : ↑unitInterval), p (G (y, u, t)) = γ (y, t)

Lifts of the same family of paths are vertically homotopic. Let α and α' be two families of paths in E, parametrized by a space Y, with the same starting points and lying over the same family γ of paths in B. Then they are homotopic through lifts of γ, relative to their starting points: there is a family of squares G, in coordinates (u, t), equal to α on the side u = 0, to α' on the side u = 1 and to the common starting point on the bottom t = 0, with p (G (y, (u, t))) = γ (y, t) throughout.

theorem TauCeti.IsHurewiczFibration.exists_homotopy_endpoints {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {Y : Type w} [TopologicalSpace Y] (hp : IsHurewiczFibration p) (γ : C(Y × ↑unitInterval, B)) (α α' : C(Y × ↑unitInterval, E)) (hα : ∀ (y : Y) (t : ↑unitInterval), p (α (y, t)) = γ (y, t)) (hα' : ∀ (y : Y) (t : ↑unitInterval), p (α' (y, t)) = γ (y, t)) (h₀ : ∀ (y : Y), α (y, 0) = α' (y, 0)) : ∃ (K : C(Y × ↑unitInterval, E)), (∀ (y : Y), K (y, 0) = α (y, 1)) ∧ (∀ (y : Y), K (y, 1) = α' (y, 1)) ∧ ∀ (y : Y) (s : ↑unitInterval), p (K (y, s)) = γ (y, 1)

Uniqueness of lifts up to homotopy. Let α and α' be two families of paths in E, parametrized by a space Y, with the same starting points and lying over the same family γ of paths in B. Then their end points are homotopic: there is a homotopy K from α (·, 1) to α' (·, 1) such that, for each y, it stays in the fiber over γ (y, 1), the end point of the path γ (y, ·).