Lifting functions on Moore paths

For a continuous map p : E → B, the space MooreReplacement p consists of the pairs (e, γ) of a point e ∈ E and a Moore path γ in B starting at p e, a subspace of E × P B. It is the domain E ×_B P B of a lifting function, and also the total space of the Moore-path replacement of p (the later file TauCeti.Topology.PathSpace.Moore.Replacement.Basic).

A lifting function for p on Moore paths is a continuous map Φ : E ×_B P B → P E such that Φ (e, γ) starts at e and lies over γ, p ∘ Φ (e, γ) = γ as Moore paths, so in particular of the length of γ. A map with a lifting function has the homotopy lifting property with respect to every space, so it is a Hurewicz fibration (TauCeti.MooreLiftingFunction.isHurewiczFibration).

A lifting function is transitive (TauCeti.MooreLiftingFunction.IsTransitive) when it lifts the constant paths of length zero to constant paths and lifts a concatenation γ · δ to the concatenation of the lift of γ with the lift of δ from the end point of the first lift. A homotopy lifting property alone does not supply a transitive lifting function, and none is constructed from one here; transitive lifting functions are what make the action of the Moore loops on a fibre strict.

Main definitions

• TauCeti.MooreReplacement p: the pairs (e, γ) with γ a Moore path starting at p e.
• TauCeti.MooreLiftingFunction p: lifting functions for p on Moore paths, with TauCeti.MooreLiftingFunction.lift.
• TauCeti.MooreLiftingFunction.IsTransitive: transitivity of a lifting function.
• TauCeti.MooreLiftingFunction.fst: the lifting function of a product projection.

Main results

• TauCeti.MooreLiftingFunction.isHurewiczFibration: a map with a lifting function is a Hurewicz fibration.
• TauCeti.MooreLiftingFunction.isTransitive_fst: the lifting function of a product projection is transitive.

References

• 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 (transitive lifting functions, after Dold and Kamps).
• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapter I.7.

def TauCeti.MooreReplacement {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : Type (max u v)

The pairs (e, γ) of a point e ∈ E and a Moore path γ in B starting at p e, a subspace of E × P B: the domain E ×_B P B of a lifting function, and the total space of the Moore-path replacement of p.

@[instance_reducible]

instance TauCeti.MooreReplacement.instTopologicalSpace {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} : TopologicalSpace (MooreReplacement p)

def TauCeti.MooreReplacement.mk {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e : E) (γ : MoorePath B) (h : γ.source = p e) : MooreReplacement p

The pair (e, γ), for a Moore path γ starting at p e.

def TauCeti.MooreReplacement.point {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) : E

The point of E of a pair (e, γ).

def TauCeti.MooreReplacement.path {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) : MoorePath B

The Moore path of a pair (e, γ).

@[simp]

theorem TauCeti.MooreReplacement.source_path {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) : x.path.source = p x.point

@[simp]

theorem TauCeti.MooreReplacement.point_mk {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e : E) (γ : MoorePath B) (h : γ.source = p e) : (mk e γ h).point = e

@[simp]

theorem TauCeti.MooreReplacement.path_mk {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (e : E) (γ : MoorePath B) (h : γ.source = p e) : (mk e γ h).path = γ

theorem TauCeti.MooreReplacement.ext {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {x y : MooreReplacement p} (h₁ : x.point = y.point) (h₂ : x.path = y.path) : x = y

theorem TauCeti.MooreReplacement.ext_iff {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {x y : MooreReplacement p} : x = y ↔ x.point = y.point ∧ x.path = y.path

@[simp]

theorem TauCeti.MooreReplacement.mk_point_path {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (x : MooreReplacement p) : mk x.point x.path ⋯ = x

theorem TauCeti.MooreReplacement.continuous_point {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} : Continuous point

theorem TauCeti.MooreReplacement.continuous_path {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} : Continuous path

theorem TauCeti.MooreReplacement.continuous_mk {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Y : Type u_1} [TopologicalSpace Y] {f : Y → E} {g : Y → MoorePath B} (hf : Continuous f) (hg : Continuous g) (h : ∀ (y : Y), (g y).source = p (f y)) : Continuous fun (y : Y) => mk (f y) (g y) ⋯

A family of pairs is continuous when its points and its paths are.

structure TauCeti.MooreLiftingFunction {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : C(E, B)) : Type (max u v)

A lifting function for p : E → B on Moore paths: a continuous map Φ : E ×_B P B → P E such that Φ (e, γ) starts at e and lies over γ.

• toContinuousMap : C(MooreReplacement p, MoorePath E)

  The lifting function, as a continuous map.

• source_apply' (x : MooreReplacement p) : (self.toContinuousMap x).source = x.point

  The lift of (e, γ) starts at e.

• map_apply' (x : MooreReplacement p) : MoorePath.map p (self.toContinuousMap x) = x.path

  The lift of (e, γ) lies over γ.

theorem TauCeti.MooreLiftingFunction.ext {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Φ Ψ : MooreLiftingFunction p} (h : Φ.toContinuousMap = Ψ.toContinuousMap) : Φ = Ψ

Two lifting functions are equal when their underlying continuous maps are.

theorem TauCeti.MooreLiftingFunction.ext_iff {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Φ Ψ : MooreLiftingFunction p} : Φ = Ψ ↔ Φ.toContinuousMap = Ψ.toContinuousMap

def TauCeti.MooreLiftingFunction.lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) : MoorePath E

The lift of a Moore path γ starting at p e, from e.

theorem TauCeti.MooreLiftingFunction.lift_def {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) : Φ.lift e γ h = Φ.toContinuousMap (MooreReplacement.mk e γ h)

@[simp]

theorem TauCeti.MooreLiftingFunction.source_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) : (Φ.lift e γ h).source = e

@[simp]

theorem TauCeti.MooreLiftingFunction.map_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) : MoorePath.map p (Φ.lift e γ h) = γ

@[simp]

theorem TauCeti.MooreLiftingFunction.length_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) : (Φ.lift e γ h).length = γ.length

theorem TauCeti.MooreLiftingFunction.lift_eq_refl_of_length_eq_zero {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) (hγ : γ.length = 0) : Φ.lift e γ h = MoorePath.refl e

The lift of a Moore path of length zero is the constant path at its start.

@[simp]

theorem TauCeti.MooreLiftingFunction.apply_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) (t : NNReal) : p ((Φ.lift e γ h).toContinuousMap t) = γ.toContinuousMap t

@[simp]

theorem TauCeti.MooreLiftingFunction.target_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) (e : E) (γ : MoorePath B) (h : γ.source = p e) : p (Φ.lift e γ h).target = γ.target

theorem TauCeti.MooreLiftingFunction.continuous_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) {Y : Type u_1} [TopologicalSpace Y] {f : Y → E} {g : Y → MoorePath B} (hf : Continuous f) (hg : Continuous g) (h : ∀ (y : Y), (g y).source = p (f y)) : Continuous fun (y : Y) => Φ.lift (f y) (g y) ⋯

The lifts form a continuous family in the point and the path.

structure TauCeti.MooreLiftingFunction.IsTransitive {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) : Prop

A lifting function is transitive when it lifts a concatenation γ · δ from e to the lift of γ from e followed by the lift of δ from the end point of the first lift. (Constant paths of length zero lift to constant paths for every lifting function, MooreLiftingFunction.lift_eq_refl_of_length_eq_zero.)

• lift_trans (e : E) (γ δ : MoorePath B) (hγ : γ.source = p e) (h : γ.target = δ.source) : Φ.lift e (γ.trans δ h) ⋯ = (Φ.lift e γ hγ).trans (Φ.lift (Φ.lift e γ hγ).target δ ⋯) ⋯

  A concatenation lifts to the concatenation of the lifts.

A lifting function makes a Hurewicz fibration

theorem TauCeti.MooreLiftingFunction.isHurewiczFibration {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Φ : MooreLiftingFunction p) : IsHurewiczFibration ⇑p

A map with a lifting function on Moore paths is a Hurewicz fibration: it has the homotopy lifting property with respect to every space.

The product projection

def TauCeti.MooreLiftingFunction.fst {B : Type v} [TopologicalSpace B] (F : Type u_1) [TopologicalSpace F] : MooreLiftingFunction ContinuousMap.fst

The lifting function of the projection B × F → B: the lift of γ from (b, f) is γ paired with the constant path at f.

@[simp]

theorem TauCeti.MooreLiftingFunction.fst_lift_apply {B : Type v} [TopologicalSpace B] {F : Type u_1} [TopologicalSpace F] (e : B × F) (γ : MoorePath B) (h : γ.source = ContinuousMap.fst e) (t : NNReal) : ((fst F).lift e γ h).toContinuousMap t = (γ.toContinuousMap t, e.2)

theorem TauCeti.MooreLiftingFunction.isTransitive_fst {B : Type v} [TopologicalSpace B] {F : Type u_1} [TopologicalSpace F] : (fst F).IsTransitive

The lifting function of a product projection is transitive.