The homotopy lifting property

A map p : E → B has the homotopy lifting property with respect to a space A when every homotopy H : I × A → B whose initial map lifts along p to f : A → E lifts along p to a homotopy G : I × A → E starting at f. The property is stated for maps between topological spaces in arbitrary universes. Covering maps have it for every space (IsCoveringMap.hasHomotopyLiftingProperty), as do product projections (TauCeti.hasHomotopyLiftingProperty_fst), maps to a subsingleton (TauCeti.hasHomotopyLiftingProperty_of_subsingleton) and homeomorphisms (Homeomorph.hasHomotopyLiftingProperty); it is closed under composition (TauCeti.HasHomotopyLiftingProperty.comp), products (TauCeti.HasHomotopyLiftingProperty.prodMap), base change (TauCeti.HasHomotopyLiftingProperty.pullback), restriction over a subset of the base (TauCeti.HasHomotopyLiftingProperty.restrictPreimage) and restriction to a subset of the total space closed under joining by paths (TauCeti.HasHomotopyLiftingProperty.comp_subtypeVal), and homotopy lifting of U.restrictPreimage p lifts homotopies valued in U (TauCeti.HasHomotopyLiftingProperty.exists_lift_of_mem); it depends on the space only up to homeomorphism (Homeomorph.hasHomotopyLiftingProperty_iff), passes from open subsets along open embeddings (TauCeti.HasHomotopyLiftingProperty.of_isOpenEmbedding), and a map with it lifts paths (TauCeti.HasHomotopyLiftingProperty.exists_path_lift).

Serre fibrations, the maps with the homotopy lifting property with respect to every disk, are in TauCeti.Topology.Homotopy.SerreFibration.Basic.

References

• A. Hatcher, Algebraic Topology, Section 4.2, the homotopy lifting property.

def TauCeti.HasHomotopyLiftingProperty {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (p : E → B) (A : Type w) [TopologicalSpace A] : Prop

A map p : E → B has the homotopy lifting property with respect to a space A when every homotopy H : I × A → B whose initial map lifts along p to some f : A → E lifts along p to a homotopy G : I × A → E starting at f.

theorem TauCeti.HasHomotopyLiftingProperty.exists_path_lift {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} [Nonempty A] (h : HasHomotopyLiftingProperty p A) {e : E} {b : B} (γ : Path (p e) b) : ∃ (Γ : C(↑unitInterval, E)), Γ 0 = e ∧ p ∘ ⇑Γ = ⇑γ

A map with the homotopy lifting property with respect to a nonempty space lifts paths: a path in B starting at p e lifts to a path in E starting at e.

theorem TauCeti.HasHomotopyLiftingProperty.surjective {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} [Nonempty A] [Nonempty E] [PathConnectedSpace B] (h : HasHomotopyLiftingProperty p A) : Function.Surjective p

A map with the homotopy lifting property with respect to a nonempty space, from a nonempty space onto a path-connected space, is surjective.

theorem TauCeti.hasHomotopyLiftingProperty_fst {B : Type v} [TopologicalSpace B] (F : Type u_1) [TopologicalSpace F] (A : Type w) [TopologicalSpace A] : HasHomotopyLiftingProperty Prod.fst A

The projection B × F → B has the homotopy lifting property with respect to every space: a homotopy lifts by keeping the F-coordinate of the initial lift fixed.

theorem TauCeti.hasHomotopyLiftingProperty_of_subsingleton {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [Subsingleton B] (A : Type w) [TopologicalSpace A] : HasHomotopyLiftingProperty p A

A map to a subsingleton space has the homotopy lifting property with respect to every space: a homotopy lifts as the constant homotopy of the initial lift.

theorem TauCeti.HasHomotopyLiftingProperty.prodMap {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} {E' : Type u_1} {B' : Type u_2} [TopologicalSpace E'] [TopologicalSpace B'] {q : E' → B'} (hp : HasHomotopyLiftingProperty p A) (hq : HasHomotopyLiftingProperty q A) : HasHomotopyLiftingProperty (Prod.map p q) A

The product of two maps with the homotopy lifting property with respect to A has it as well: a homotopy lifts coordinatewise.

theorem Homeomorph.hasHomotopyLiftingProperty {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] (e : E ≃ₜ B) (A : Type w) [TopologicalSpace A] : TauCeti.HasHomotopyLiftingProperty (⇑e) A

A homeomorphism has the homotopy lifting property with respect to every space.

theorem TauCeti.HasHomotopyLiftingProperty.comp {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} {C : Type u_1} [TopologicalSpace C] {q : B → C} (hq : HasHomotopyLiftingProperty q A) (hp : HasHomotopyLiftingProperty p A) (hpc : Continuous p) : HasHomotopyLiftingProperty (q ∘ p) A

The homotopy lifting property is closed under composition.

theorem TauCeti.HasHomotopyLiftingProperty.pullback {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} {B' : Type u_1} [TopologicalSpace B'] (hp : HasHomotopyLiftingProperty p A) (g : C(B', B)) : HasHomotopyLiftingProperty (fun (x : { x : B' × E // g x.1 = p x.2 }) => (↑x).1) A

The homotopy lifting property passes to the base change {(b', e) | g b' = p e} → B' along any continuous map g : B' → B.

theorem TauCeti.HasHomotopyLiftingProperty.restrictPreimage {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} (hp : HasHomotopyLiftingProperty p A) (t : Set B) : HasHomotopyLiftingProperty (t.restrictPreimage p) A

The homotopy lifting property passes to the restriction p⁻¹(t) → t of p over any subset t of the base: a lift of a homotopy in t lies over t.

theorem TauCeti.HasHomotopyLiftingProperty.comp_subtypeVal {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} (hp : HasHomotopyLiftingProperty p A) {S : Set E} (hS : ∀ ⦃e e' : E⦄, e ∈ S → Joined e e' → e' ∈ S) : HasHomotopyLiftingProperty (p ∘ Subtype.val) A

The homotopy lifting property passes to the restriction S → B of p to a subset S of the total space that is closed under joining by paths, for instance a union of path components: each value of a lift is joined to the starting point of its track.

theorem TauCeti.HasHomotopyLiftingProperty.exists_lift_of_mem {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {p : E → B} {U : Set B} (h : HasHomotopyLiftingProperty (U.restrictPreimage p) A) (f : C(A, E)) (H : C(↑unitInterval × A, B)) (hHU : ∀ (z : ↑unitInterval × A), H z ∈ U) (hH : ∀ (a : A), H (0, a) = p (f a)) : ∃ (G : C(↑unitInterval × A, E)), p ∘ ⇑G = ⇑H ∧ ∀ (a : A), G (0, a) = f a

If the restriction U.restrictPreimage p : p ⁻¹' U → U over U : Set B has the homotopy lifting property with respect to A, then every homotopy H : C(I × A, B) valued in U whose initial map lifts along p to f : C(A, E) lifts along p to a homotopy G : C(I × A, E) starting at f.

theorem TauCeti.HasHomotopyLiftingProperty.of_homeomorph {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {A' : Type w'} [TopologicalSpace A'] {p : E → B} (h : HasHomotopyLiftingProperty p A') (e : A ≃ₜ A') : HasHomotopyLiftingProperty p A

The homotopy lifting property with respect to a space passes to every space homeomorphic to it.

theorem TauCeti.HasHomotopyLiftingProperty.of_isOpenEmbedding {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {A' : Type w'} [TopologicalSpace A'] {p : E → B} (h : ∀ (W : Set A'), IsOpen W → HasHomotopyLiftingProperty p ↑W) {e : A → A'} (he : Topology.IsOpenEmbedding e) : HasHomotopyLiftingProperty p A

If p has the homotopy lifting property with respect to every open subset of A', then it has the homotopy lifting property with respect to every space admitting an open embedding into A'.

theorem Homeomorph.hasHomotopyLiftingProperty_iff {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {A : Type w} [TopologicalSpace A] {A' : Type w'} [TopologicalSpace A'] {p : E → B} (e : A ≃ₜ A') : TauCeti.HasHomotopyLiftingProperty p A ↔ TauCeti.HasHomotopyLiftingProperty p A'

The homotopy lifting property with respect to a space depends on the space only up to homeomorphism.

theorem IsCoveringMap.hasHomotopyLiftingProperty {E : Type u} {B : Type v} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsCoveringMap p) (A : Type w) [TopologicalSpace A] : TauCeti.HasHomotopyLiftingProperty p A

A covering map has the homotopy lifting property with respect to every space.