Moore loop maps of Hurewicz fibrations

For a Hurewicz fibration p : E → B and e : E, the induced map of fixed-interval loop spaces Ω E e → Ω B (p e) is a Hurewicz fibration (TauCeti.IsHurewiczFibration.loopMap). This file shows that the analogous statement for the Moore loop spaces fails, and that it fails only at the loops of length zero.

The Moore loop map MooreLoopSpace.map p preserves lengths, and the only Moore loop of length zero is the unit (TauCeti.MooreLoopSpace.eq_one_of_length_eq_zero). So the fibre of the Moore loop map over the unit of B is a single point, while over the constant loop of length L > 0 it is the space of Moore loops of length L in the fibre of p, a copy of its loop space. In the simplest case, the map from X to a point, the Moore loop map is the length MooreLoopSpace X x → [0, ∞). If the length has the homotopy lifting property for a single point, lifting the path of lengths from γ.length down to 0 joins every Moore loop γ to the unit, so the Moore loop space is path connected and the fundamental group of X at x is trivial (TauCeti.MooreLoopSpace.subsingleton_fundamentalGroup_of_hasHomotopyLiftingProperty_length). For the circle, the map to a point is a Hurewicz fibration whose Moore loop map is not (TauCeti.MooreLoopSpace.not_forall_isHurewiczFibration_map).

Away from length zero nothing goes wrong. A Moore loop of positive length is determined by its length and its reparametrization to the unit interval (TauCeti.MooreLoopSpace.posLengthHomeomorph), naturally in the space. So over the Moore loops of positive length, the Moore loop map of p is the product of the identity of (0, ∞) with the fixed-interval loop map, and is therefore a Hurewicz fibration (TauCeti.IsHurewiczFibration.restrictPreimage_mooreLoopMap).

Main results

• TauCeti.MooreLoopSpace.subsingleton_fundamentalGroup_of_hasHomotopyLiftingProperty_length: if the length of Moore loops lifts paths, the fundamental group is trivial.
• TauCeti.MooreLoopSpace.not_isHurewiczFibration_length, TauCeti.MooreLoopSpace.not_isHurewiczFibration_map_const: when the fundamental group is nontrivial, neither the length nor the Moore loop map of the map to a point is a Hurewicz fibration.
• TauCeti.MooreLoopSpace.not_forall_isHurewiczFibration_map: the Moore loop map of a Hurewicz fibration need not be a Hurewicz fibration.
• TauCeti.MooreLoopSpace.posLengthHomeomorph: Moore loops of positive length are pairs of a positive length and a loop on the unit interval.
• TauCeti.IsHurewiczFibration.restrictPreimage_mooreLoopMap: over the Moore loops of positive length, the Moore loop map of a Hurewicz fibration is a Hurewicz fibration.

References

• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapters I.7 and III.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, §7.1.

The length of Moore loops is not a fibration

theorem TauCeti.MooreLoopSpace.pathConnectedSpace_of_hasHomotopyLiftingProperty_length {X : Type u} [TopologicalSpace X] {x : X} {A : Type w} [TopologicalSpace A] [Nonempty A] (h : HasHomotopyLiftingProperty length A) : PathConnectedSpace (MooreLoopSpace X x)

If the length of Moore loops at x has the homotopy lifting property with respect to a nonempty space, then every Moore loop at x is joined to the unit: lift the path of lengths from γ.length down to 0, which ends at a loop of length zero.

theorem TauCeti.MooreLoopSpace.subsingleton_fundamentalGroup_of_hasHomotopyLiftingProperty_length {X : Type u} [TopologicalSpace X] {x : X} {A : Type w} [TopologicalSpace A] [Nonempty A] (h : HasHomotopyLiftingProperty length A) : Subsingleton (FundamentalGroup X x)

If the length of Moore loops at x has the homotopy lifting property with respect to a nonempty space, then the fundamental group of X at x is trivial.

theorem TauCeti.MooreLoopSpace.not_isHurewiczFibration_length {X : Type u} [TopologicalSpace X] {x : X} [Nontrivial (FundamentalGroup X x)] : ¬IsHurewiczFibration length

The length of Moore loops is not a Hurewicz fibration when the fundamental group is nontrivial: its fibre over 0 is a single point.

theorem TauCeti.MooreLoopSpace.not_isHurewiczFibration_map_const {X : Type u} [TopologicalSpace X] {x : X} [Nontrivial (FundamentalGroup X x)] : ¬IsHurewiczFibration ⇑(map (ContinuousMap.const X ()) ⋯)

When the fundamental group of X at x is nontrivial, the Moore loop map of the map from X to a point is not a Hurewicz fibration, although the map to a point is one (TauCeti.isHurewiczFibration_of_subsingleton).

theorem TauCeti.MooreLoopSpace.not_forall_isHurewiczFibration_map : ¬∀ (E B : Type) [inst : TopologicalSpace E] [inst_1 : TopologicalSpace B] (p : C(E, B)) (e : E), IsHurewiczFibration ⇑p → IsHurewiczFibration ⇑(map p ⋯)

The Moore loop map of a Hurewicz fibration need not be a Hurewicz fibration. The map from the circle to a point is a Hurewicz fibration, but its Moore loop map is not.

The Moore loop map over positive lengths

theorem TauCeti.IsHurewiczFibration.restrictPreimage_mooreLoopMap {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsHurewiczFibration p) (e : E) : IsHurewiczFibration ((MooreLoopSpace.length ⁻¹' Set.Ioi 0).restrictPreimage ⇑(MooreLoopSpace.map { toFun := p, continuous_toFun := ⋯ } ⋯))

Over the Moore loops of positive length, the Moore loop map of a Hurewicz fibration is a Hurewicz fibration. Under MooreLoopSpace.posLengthHomeomorph it is the product of the identity of (0, ∞) with the fixed-interval loop map, a Hurewicz fibration by TauCeti.IsHurewiczFibration.loopMap. Without the restriction to positive lengths the statement fails (TauCeti.MooreLoopSpace.not_forall_isHurewiczFibration_map).