Loop spaces of Hurewicz fibrations

For a Hurewicz fibration p : E → B and a point e : E, the induced map Ω E e → Ω B (p e), γ ↦ p ∘ γ, on the fixed-interval loop spaces Ω X x = Path x x (with the compact-open topology) is again a Hurewicz fibration (TauCeti.IsHurewiczFibration.loopMap), and so is the induced map on double loop spaces (TauCeti.IsHurewiczFibration.loopMap_loopMap). It is the case of loops of the relative lifting property for the open box (TauCeti.IsHurewiczFibration.exists_lift_openBox).

The statement is for the fixed-interval loop space. The analogous statement for Moore loops fails at the loops of length zero, and holds over the Moore loops of positive length; both are in TauCeti.Topology.PathSpace.Moore.LoopFibration.

Main results

• TauCeti.IsHurewiczFibration.loopMap: Ω p is a Hurewicz fibration.
• TauCeti.IsHurewiczFibration.loopMap_loopMap: Ω² p is a Hurewicz fibration.

References

• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapter I.7.

theorem TauCeti.continuous_loopMap {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : Continuous p) (e : E) : Continuous fun (γ : LoopSpace E e) => Path.map γ hp

The map Ω E e → Ω B (p e) induced by a continuous map p is continuous.

theorem TauCeti.IsHurewiczFibration.loopMap {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsHurewiczFibration p) (e : E) : IsHurewiczFibration fun (γ : LoopSpace E e) => Path.map γ ⋯

The loop map of a Hurewicz fibration is a Hurewicz fibration: for a Hurewicz fibration p : E → B and e : E, the induced map Ω E e → Ω B (p e) on fixed-interval loop spaces is a Hurewicz fibration.

theorem TauCeti.IsHurewiczFibration.loopMap_loopMap {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsHurewiczFibration p) (e : E) : IsHurewiczFibration fun (Γ : LoopSpace (LoopSpace E e) (Path.refl e)) => Path.map Γ ⋯

The double loop map of a Hurewicz fibration is a Hurewicz fibration.