Lifting maps out of convex sets through covering maps

A nonempty convex subset of a real topological vector space is contractible (Convex.contractibleSpace), hence simply connected, and it is locally path-connected (Convex.locallyPathConnectedSpace'). By the lifting criterion (IsCoveringMap.existsUnique_continuousMap_lifts), every continuous map out of such a set lifts uniquely through a covering map once the lift of one point is prescribed (IsCoveringMap.existsUnique_continuousMap_lifts_of_convex). This applies, for instance, to the closed unit balls carrying the characteristic maps of CW complexes.

References

• A. Hatcher, Algebraic Topology, Section 1.3, Proposition 1.33 (the lifting criterion) and Proposition 1.34 (unique lifting).

theorem IsCoveringMap.existsUnique_continuousMap_lifts_of_convex {E : Type u_1} {X : Type u_2} {V : Type u_3} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] {s : Set V} (hp : IsCoveringMap p) (hs : Convex ℝ s) (f : C(↑s, X)) (x : ↑s) (e : E) (he : p e = f x) : ∃! F : C(↑s, E), F x = e ∧ p ∘ ⇑F = ⇑f

A continuous map out of a convex subset of a real topological vector space lifts uniquely through a covering map once the lift of one point is prescribed: the set is contractible and locally path-connected.