The homotopy lifting property for covering maps

• IsCoveringMap.exists_path_lifts, IsCoveringMap.liftPath: any path in the base of a covering map lifts uniquely to the covering space (given a lift of the starting point).

• IsCoveringMap.liftHomotopy: any homotopy I × A → X in the base of a covering map E → X can be lifted to a homotopy I × A → E, starting from a given lift of the restriction {0} × A → X.

• IsCoveringMap.existsUnique_continuousMap_lifts: any continuous map from a simply-connected, locally path-connected space lifts uniquely through a covering map (given a lift of an arbitrary point).

theorem IsLocalHomeomorph.exists_lift_nhds {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (homeo : IsLocalHomeomorph p) {f : C(↑unitInterval × A, X)} {g : ↑unitInterval × A → E} (g_lifts : p ∘ g = ⇑f) (cont_0 : Continuous fun (x : A) => g (0, x)) (a : A) (cont_a : Continuous fun (x : ↑unitInterval) => g (x, a)) : ∃ N ∈ nhds a, ∃ (g' : ↑unitInterval × A → E), ContinuousOn g' (Set.univ ×ˢ N) ∧ p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : ↑unitInterval), g' (t, a) = g (t, a)

If p : E → X is a local homeomorphism, and if g : I × A → E is a lift of f : C(I × A, X) continuous on {0} × A ∪ I × {a} for some a : A, then there exists a neighborhood N ∈ 𝓝 a and g' : I × A → E continuous on I × N that agrees with g on {0} × A ∪ I × {a}. The proof follows [hatcher02], Proof of Theorem 1.7, p.30.

Possible TODO: replace I by an arbitrary space assuming A is locally connected and p is a separated map, which guarantees uniqueness and therefore well-definedness on the intersections.

theorem IsLocalHomeomorph.continuous_lift {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (homeo : IsLocalHomeomorph p) (sep : IsSeparatedMap p) (f : C(↑unitInterval × A, X)) {g : ↑unitInterval × A → E} (g_lifts : p ∘ g = ⇑f) (cont_0 : Continuous fun (x : A) => g (0, x)) (cont_A : ∀ (a : A), Continuous fun (x : ↑unitInterval) => g (x, a)) : Continuous g

theorem IsLocalHomeomorph.monodromy_theorem {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (homeo : IsLocalHomeomorph p) (sep : IsSeparatedMap p) {γ₀ γ₁ : C(↑unitInterval, X)} (γ : γ₀.HomotopyRel γ₁ {0, 1}) (Γ : ↑unitInterval → C(↑unitInterval, E)) (Γ_lifts : ∀ (t s : ↑unitInterval), p ((Γ t) s) = γ (t, s)) (Γ_0 : ∀ (t : ↑unitInterval), (Γ t) 0 = (Γ 0) 0) (t : ↑unitInterval) : (Γ t) 1 = (Γ 0) 1

The abstract monodromy theorem: if γ₀ and γ₁ are two paths in a topological space X, γ is a homotopy between them relative to the endpoints, and the path at each time step of the homotopy, γ (t, ·), lifts to a continuous path Γ t through a separated local homeomorphism p : E → X, starting from some point in E independent of t. Then the endpoints of these lifts are also independent of t.

This can be applied to continuation of analytic functions as follows: for a sheaf of analytic functions on an analytic manifold X, we may consider its étale space E (whose points are analytic germs) with the natural projection p : E → X, which is a local homeomorphism and a separated map (because two analytic functions agreeing on a nonempty open set agree on the whole connected component). An analytic continuation of a germ along a path γ (t, ·) : C(I, X) corresponds to a continuous lift of γ (t, ·) to E starting from that germ. If γ is a homotopy and the germ admits continuation along every path γ (t, ·), then the result of the continuations are independent of t. In particular, if X is simply connected and an analytic germ at p : X admits a continuation along every path in X from p to q : X, then the continuation to q is independent of the path chosen.

theorem IsLocalHomeomorph.existsUnique_continuousMap_lifts {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (homeo : IsLocalHomeomorph p) [PathConnectedSpace A] [LocPathConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : E) (he : p e₀ = f a₀) (ex : ∀ (γ : C(↑unitInterval, A)), γ 0 = a₀ → ∃ (Γ : C(↑unitInterval, E)), Γ 0 = e₀ ∧ p ∘ ⇑Γ = ⇑(f.comp γ)) (uniq : ∀ (γ γ' : C(↑unitInterval, A)) (Γ Γ' : C(↑unitInterval, E)), γ 0 = a₀ → γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → p ∘ ⇑Γ = ⇑(f.comp γ) → p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1) : ∃! F : C(A, E), F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

A map f from a path-connected, locally path-connected space A to another space X lifts uniquely through a local homeomorphism p : E → X if for every path γ in A, the composed path f ∘ γ in X lifts to E with endpoint only dependent on the endpoint of γ and independent of the path chosen. In this theorem, we require that a specific point a₀ : A is lifted to a specific point e₀ : E over a₀.

theorem IsCoveringMap.exists_path_lifts {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) (γ : C(↑unitInterval, X)) (e : E) (γ_0 : γ 0 = p e) : ∃ (Γ : C(↑unitInterval, E)), p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

The path lifting property (existence) for covering maps.

noncomputable def IsCoveringMap.liftPath {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) (γ : C(↑unitInterval, X)) (e : E) (γ_0 : γ 0 = p e) : C(↑unitInterval, E)

The lift of a path to a covering space given a lift of the left endpoint.

Equations

• cov.liftPath γ e γ_0 = ⋯.choose

theorem IsCoveringMap.liftPath_lifts {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) (γ : C(↑unitInterval, X)) (e : E) (γ_0 : γ 0 = p e) : p ∘ ⇑(cov.liftPath γ e γ_0) = ⇑γ

theorem IsCoveringMap.liftPath_zero {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) (γ : C(↑unitInterval, X)) (e : E) (γ_0 : γ 0 = p e) : (cov.liftPath γ e γ_0) 0 = e

theorem IsCoveringMap.eq_liftPath_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) {γ : C(↑unitInterval, X)} {e : E} (γ_0 : γ 0 = p e) {Γ : ↑unitInterval → E} : Γ = ⇑(cov.liftPath γ e γ_0) ↔ Continuous Γ ∧ p ∘ Γ = ⇑γ ∧ Γ 0 = e

theorem IsCoveringMap.eq_liftPath_iff' {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) {γ : C(↑unitInterval, X)} {e : E} (γ_0 : γ 0 = p e) {Γ : C(↑unitInterval, E)} : Γ = cov.liftPath γ e γ_0 ↔ p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

Unique characterization of the lifted path.

noncomputable def IsCoveringMap.liftHomotopy {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) (H : C(↑unitInterval × A, X)) (f : C(A, E)) (H_0 : ∀ (a : A), H (0, a) = p (f a)) : C(↑unitInterval × A, E)

The existence of liftHomotopy satisfying liftHomotopy_lifts and liftHomotopy_zero is the homotopy lifting property for covering maps. In other words, a covering map is a Hurewicz fibration.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsCoveringMap.liftHomotopy_apply {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) (H : C(↑unitInterval × A, X)) (f : C(A, E)) (H_0 : ∀ (a : A), H (0, a) = p (f a)) (ta : ↑unitInterval × A) : (cov.liftHomotopy H f H_0) ta = (cov.liftPath (H.comp ((ContinuousMap.id ↑unitInterval).prodMk (ContinuousMap.const (↑unitInterval) ta.2))) (f ta.2) ⋯) ta.1

theorem IsCoveringMap.liftHomotopy_lifts {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) (H : C(↑unitInterval × A, X)) (f : C(A, E)) (H_0 : ∀ (a : A), H (0, a) = p (f a)) : p ∘ ⇑(cov.liftHomotopy H f H_0) = ⇑H

theorem IsCoveringMap.liftHomotopy_zero {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) (H : C(↑unitInterval × A, X)) (f : C(A, E)) (H_0 : ∀ (a : A), H (0, a) = p (f a)) (a : A) : (cov.liftHomotopy H f H_0) (0, a) = f a

theorem IsCoveringMap.eq_liftHomotopy_iff {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) {H : C(↑unitInterval × A, X)} {f : C(A, E)} (H_0 : ∀ (a : A), H (0, a) = p (f a)) (H' : ↑unitInterval × A → E) : H' = ⇑(cov.liftHomotopy H f H_0) ↔ (∀ (a : A), Continuous fun (x : ↑unitInterval) => H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a

theorem IsCoveringMap.eq_liftHomotopy_iff' {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) {H : C(↑unitInterval × A, X)} {f : C(A, E)} (H_0 : ∀ (a : A), H (0, a) = p (f a)) (H' : C(↑unitInterval × A, E)) : H' = cov.liftHomotopy H f H_0 ↔ p ∘ ⇑H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a

noncomputable def IsCoveringMap.liftHomotopyRel {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) {f₀ f₁ : C(A, X)} {S : Set A} (F : f₀.HomotopyRel f₁ S) [PreconnectedSpace A] {f₀' f₁' : C(A, E)} (he : ∃ a ∈ S, f₀' a = f₁' a) (h₀ : p ∘ ⇑f₀' = ⇑f₀) (h₁ : p ∘ ⇑f₁' = ⇑f₁) : f₀'.HomotopyRel f₁' S

The lift to a covering space of a homotopy between two continuous maps relative to a set given compatible lifts of the continuous maps.

Equations

• cov.liftHomotopyRel F he h₀ h₁ = { toContinuousMap := cov.liftHomotopy (↑F) f₀' ⋯, map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ }

theorem IsCoveringMap.homotopicRel_iff_comp {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) [PreconnectedSpace A] {f₀ f₁ : C(A, E)} {S : Set A} (he : ∃ a ∈ S, f₀ a = f₁ a) : f₀.HomotopicRel f₁ S ↔ ({ toFun := p, continuous_toFun := ⋯ }.comp f₀).HomotopicRel ({ toFun := p, continuous_toFun := ⋯ }.comp f₁) S

Two continuous maps from a preconnected space to the total space of a covering map are homotopic relative to a set S if and only if their compositions with the covering map are homotopic relative to S, assuming that they agree at a point in S.

theorem IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) {γ₀ γ₁ : C(↑unitInterval, X)} (h : γ₀.HomotopicRel γ₁ {0, 1}) (e : E) (h₀ : γ₀ 0 = p e) (h₁ : γ₁ 0 = p e) : (cov.liftPath γ₀ e h₀) 1 = (cov.liftPath γ₁ e h₁) 1

Lifting two paths that are homotopic relative to {0,1} starting from the same point also ends up in the same point.

theorem IsCoveringMap.injective_path_homotopic_mapFn {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (cov : IsCoveringMap p) (e₀ e₁ : E) : Function.Injective fun (γ : Path.Homotopic.Quotient e₀ e₁) => γ.mapFn { toFun := p, continuous_toFun := ⋯ }

A covering map induces an injection on all Hom-sets of the fundamental groupoid, in particular on the fundamental group.

theorem IsCoveringMap.existsUnique_continuousMap_lifts {E : Type u_1} {X : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) [SimplyConnectedSpace A] [LocPathConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : E) (he : p e₀ = f a₀) : ∃! F : C(A, E), F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

A map f from a simply-connected, locally path-connected space A to another space X lifts uniquely through a covering map p : E → X, after specifying any lift e₀ : E of any point a₀ : A.