Lifting functions

A lifting function for a continuous map p : E → B is a continuous map Λ : E ×_B C(I, B) → C(I, E) such that Λ (e, γ) starts at e and lies over γ. Its domain is the mapping-path space TauCeti.MappingPathSpace p of pairs (e, γ) with γ 0 = p e, with the compact-open topology on paths.

A lifting function lifts homotopies parametrized by arbitrary spaces, in every universe, so a map with a lifting function is a Hurewicz fibration. Conversely, a Hurewicz fibration lifts the tautological homotopy parametrized by MappingPathSpace p itself, and currying that lift gives a lifting function. Hence a map is a Hurewicz fibration for test spaces in Type (max u v) if and only if it admits a lifting function, and then it is a Hurewicz fibration for test spaces in every universe.

As an application, the endpoint map of any mapping-path replacement MappingPathSpace f → K has an explicit lifting function: the lift of a path δ from (b, γ) at time s is (b, γ') where γ' runs through γ and then through δ on [0, s], at speed 1 + s. So the endpoint map is a Hurewicz fibration for every continuous f, without any hypothesis on its source or target.

Main definitions

• TauCeti.LiftingFunction p: lifting functions for p : C(E, B), with TauCeti.LiftingFunction.lift.
• TauCeti.LiftingFunction.liftFamily: the lifts of a continuous family of paths, as a continuous map, with liftFamily_apply, liftFamily_zero and apply_liftFamily.
• TauCeti.MappingPathSpace.endpointLiftingFunction f: the path-concatenation lifting function of the endpoint map of MappingPathSpace f.

Main results

• TauCeti.LiftingFunction.isHurewiczFibration: a map with a lifting function is a Hurewicz fibration for test spaces in every universe.
• TauCeti.isHurewiczFibration_iff_nonempty_liftingFunction: a map p : C(E, B) is a Hurewicz fibration for test spaces in Type (max u v) if and only if it has a lifting function.
• TauCeti.IsHurewiczFibration.up: a Hurewicz fibration for test spaces in Type (max u v) is one for test spaces in every universe.
• TauCeti.MappingPathSpace.isHurewiczFibration_endpoint: the endpoint map of a mapping-path replacement is a Hurewicz fibration.

References

• W. Hurewicz, On the concept of fiber space, Proc. Nat. Acad. Sci. 41 (1955), 956–961.
• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapter I.7.

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

A lifting function for p : C(E, B): a continuous map Λ : E ×_B C(I, B) → C(I, E) such that Λ (e, γ) starts at e and lies over γ.

• toContinuousMap : C(MappingPathSpace p, C(↑unitInterval, E))

  The lifting function, as a continuous map on the mapping-path space of p.

• apply_zero' (x : MappingPathSpace p) : (self.toContinuousMap x) 0 = (↑x).1

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

• comp_apply' (x : MappingPathSpace p) : p.comp (self.toContinuousMap x) = (↑x).2

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

theorem TauCeti.LiftingFunction.ext {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Λ Λ' : LiftingFunction p} (h : Λ.toContinuousMap = Λ'.toContinuousMap) : Λ = Λ'

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

theorem TauCeti.LiftingFunction.ext_iff {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} {Λ Λ' : LiftingFunction p} : Λ = Λ' ↔ Λ.toContinuousMap = Λ'.toContinuousMap

def TauCeti.LiftingFunction.lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) (e : E) (γ : C(↑unitInterval, B)) (h : γ 0 = p e) : C(↑unitInterval, E)

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

theorem TauCeti.LiftingFunction.lift_def {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) (e : E) (γ : C(↑unitInterval, B)) (h : γ 0 = p e) : Λ.lift e γ h = Λ.toContinuousMap ⟨(e, γ), h⟩

theorem TauCeti.LiftingFunction.lift_congr {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) {e e' : E} (he : e = e') {γ γ' : C(↑unitInterval, B)} (hγ : γ = γ') (h : γ 0 = p e) (h' : γ' 0 = p e') : Λ.lift e γ h = Λ.lift e' γ' h'

@[simp]

theorem TauCeti.LiftingFunction.lift_zero {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) (e : E) (γ : C(↑unitInterval, B)) (h : γ 0 = p e) : (Λ.lift e γ h) 0 = e

@[simp]

theorem TauCeti.LiftingFunction.comp_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) (e : E) (γ : C(↑unitInterval, B)) (h : γ 0 = p e) : p.comp (Λ.lift e γ h) = γ

@[simp]

theorem TauCeti.LiftingFunction.apply_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) (e : E) (γ : C(↑unitInterval, B)) (h : γ 0 = p e) (t : ↑unitInterval) : p ((Λ.lift e γ h) t) = γ t

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

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

def TauCeti.LiftingFunction.liftFamily {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) {Y : Type u_1} [TopologicalSpace Y] (f : C(Y, E)) (γ : C(Y × ↑unitInterval, B)) (h : ∀ (y : Y), γ (y, 0) = p (f y)) : C(Y × ↑unitInterval, E)

The lifts, starting at the points f y, of a family γ of paths in B with γ (y, 0) = p (f y), as a continuous map on Y × I.

theorem TauCeti.LiftingFunction.liftFamily_apply {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) {Y : Type u_1} [TopologicalSpace Y] (f : C(Y, E)) (γ : C(Y × ↑unitInterval, B)) (h : ∀ (y : Y), γ (y, 0) = p (f y)) (y : Y) (t : ↑unitInterval) : (Λ.liftFamily f γ h) (y, t) = (Λ.lift (f y) (γ.curry y) ⋯) t

@[simp]

theorem TauCeti.LiftingFunction.liftFamily_zero {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) {Y : Type u_1} [TopologicalSpace Y] (f : C(Y, E)) (γ : C(Y × ↑unitInterval, B)) (h : ∀ (y : Y), γ (y, 0) = p (f y)) (y : Y) : (Λ.liftFamily f γ h) (y, 0) = f y

@[simp]

theorem TauCeti.LiftingFunction.apply_liftFamily {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (Λ : LiftingFunction p) {Y : Type u_1} [TopologicalSpace Y] (f : C(Y, E)) (γ : C(Y × ↑unitInterval, B)) (h : ∀ (y : Y), γ (y, 0) = p (f y)) (y : Y) (t : ↑unitInterval) : p ((Λ.liftFamily f γ h) (y, t)) = γ (y, t)

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

A map with a lifting function is a Hurewicz fibration, for test spaces in every universe.

theorem TauCeti.IsHurewiczFibration.nonempty_liftingFunction {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} (h : IsHurewiczFibration ⇑p) : Nonempty (LiftingFunction p)

A Hurewicz fibration for test spaces in Type (max u v) has a lifting function: lifting the tautological homotopy parametrized by the mapping-path space and currying gives one.

theorem TauCeti.isHurewiczFibration_iff_nonempty_liftingFunction {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : C(E, B)} : IsHurewiczFibration ⇑p ↔ Nonempty (LiftingFunction p)

A map is a Hurewicz fibration for test spaces in Type (max u v) if and only if it has a lifting function.

theorem TauCeti.IsHurewiczFibration.up {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (h : IsHurewiczFibration p) : IsHurewiczFibration p

A Hurewicz fibration for test spaces in Type (max u v) is a Hurewicz fibration for test spaces in every universe.

The endpoint map of a mapping-path replacement

noncomputable def TauCeti.MappingPathSpace.endpointLiftingFunction {B : Type u'} {K : Type v'} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : LiftingFunction (endpoint f)

The lifting function of the endpoint map of MappingPathSpace f: the lift of a path δ from (b, γ) at time s is b together with γ followed by δ on [0, s], at speed 1 + s.

@[simp]

theorem TauCeti.MappingPathSpace.endpointLiftingFunction_lift_val_fst {B : Type u'} {K : Type v'} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (x : MappingPathSpace f) (δ : C(↑unitInterval, K)) (h : δ 0 = (endpoint f) x) (s : ↑unitInterval) : (↑(((endpointLiftingFunction f).lift x δ h) s)).1 = (↑x).1

The lifts of the endpoint map keep the source point fixed.

theorem TauCeti.MappingPathSpace.endpointLiftingFunction_lift_val_snd {B : Type u'} {K : Type v'} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) (x : MappingPathSpace f) (δ : C(↑unitInterval, K)) (h : δ 0 = (endpoint f) x) (s u : ↑unitInterval) : (↑(((endpointLiftingFunction f).lift x δ h) s)).2 u = if (1 + ↑s) * ↑u ≤ 1 then Set.IccExtend ⋯ (⇑(↑x).2) ((1 + ↑s) * ↑u) else Set.IccExtend ⋯ (⇑δ) ((1 + ↑s) * ↑u - 1)

The path of a lift of the endpoint map: at time s, the original path γ followed by δ on [0, s], at speed 1 + s.

theorem TauCeti.MappingPathSpace.isHurewiczFibration_endpoint {B : Type u'} {K : Type v'} [TopologicalSpace B] [TopologicalSpace K] (f : C(B, K)) : IsHurewiczFibration ⇑(endpoint f)

The endpoint map of a mapping-path replacement is a Hurewicz fibration, for test spaces in every universe.