Universal cover: covering map, simple connectedness, universal property

Building on the sheet decomposition in TauCeti.AlgebraicTopology.UniversalCover.Basic, this file shows that the endpoint projection UniversalCover.proj is a covering map, and derives path-connectedness, simple connectedness, and the universal lifting property of the universal cover.

This file is adapted from Kim Morrison's mathlib4#38292, file Mathlib/AlgebraicTopology/FundamentalGroupoid/UniversalCover/Covering.lean.

Main results

• UniversalCover.isCoveringMap: the endpoint projection is a covering map.
• UniversalCover.discreteTopology_fiber: fibers of the universal cover are discrete.
• UniversalCover.locallyPathConnectedSpace: the universal cover is locally path-connected.
• UniversalCover.pathConnectedSpace: the universal cover is path-connected.
• UniversalCover.simplyConnectedSpace: the universal cover is simply connected.
• UniversalCover.existsUnique_continuousMap_lifts: the universal lifting property.
• UniversalCover.apply_one_eq_ofBasedPath: a lift of a based path starting at the constant-path point ends at the class of that path.

Implementation notes

UniversalCover.isCoveringMap does not assume X is path-connected. Over a point with no path from x₀ the preimage of a good neighbourhood is empty, hence evenly covered (IsEvenlyCovered.of_preimage_eq_empty); over the path component of x₀ the sheet trivialization applies.

theorem TauCeti.UniversalCover.isCoveringMap {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : IsCoveringMap proj

The endpoint projection proj is a covering map, assuming X is semilocally simply connected and locally path-connected. Fibres over points outside the path component of x₀ are empty.

instance TauCeti.UniversalCover.discreteTopology_fiber {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ x : X) : DiscreteTopology ↑(proj ⁻¹' {x})

Fibers of the universal cover are discrete.

instance TauCeti.UniversalCover.locallyPathConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : LocallyPathConnectedSpace (UniversalCover x₀)

The universal cover of a locally path-connected, semilocally simply connected space is locally path-connected, since its projection is a local homeomorphism.

theorem TauCeti.UniversalCover.joined_basepoint_ofBasedPath {X : Type u_1} [TopologicalSpace X] {x₀ : X} (α : BasedPath x₀) : Joined (ofBasedPath x₀ (BasedPath.refl x₀)) (ofBasedPath x₀ α)

Every point of UniversalCover x₀ is joined to the point represented by the constant path. The connecting path is the family of initial segments t ↦ α |_[0, t].

instance TauCeti.UniversalCover.pathConnectedSpace {X : Type u_1} [TopologicalSpace X] (x₀ : X) : PathConnectedSpace (UniversalCover x₀)

The universal cover is path-connected.

theorem TauCeti.UniversalCover.liftPath_apply_one_eq_ofBasedPath_append {X : Type u_1} [TopologicalSpace X] {x₀ : X} [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] {α : BasedPath x₀} {y : X} (γ : Path α.endpoint y) : (⋯.liftPath (↑γ) (ofBasedPath x₀ α) ⋯) 1 = ofBasedPath x₀ (α.append γ)

The lift through proj of a path γ starting at the class of α ends at the class of the concatenated based path α.append γ.

theorem TauCeti.UniversalCover.apply_one_eq_ofBasedPath {X : Type u_1} [TopologicalSpace X] {x₀ : X} [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] {g : ↑unitInterval → UniversalCover x₀} (hg : Continuous g) (γ : BasedPath x₀) (hγ : ∀ (t : ↑unitInterval), (g t).proj = γ t) (h₀ : g 0 = ofBasedPath x₀ (BasedPath.refl x₀)) : g 1 = ofBasedPath x₀ γ

The endpoint of a lift of a based path. A continuous path in the universal cover that starts at the constant-path point and lies over the based path γ ends at the class of γ: by unique path lifting it agrees with the family of initial segments t ↦ γ |_[0, t].

instance TauCeti.UniversalCover.simplyConnectedSpace {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) : SimplyConnectedSpace (UniversalCover x₀)

The universal cover is simply connected.

theorem TauCeti.UniversalCover.existsUnique_continuousMap_lifts {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [TopologicalSpace A] [SimplyConnectedSpace A] [LocallyPathConnectedSpace A] [LocallyPathConnectedSpace X] [SemilocallySimplyConnectedSpace X] (x₀ : X) (f : C(A, X)) (a₀ : A) (e₀ : UniversalCover x₀) (he : e₀.proj = f a₀) : ∃! F : C(A, UniversalCover x₀), F a₀ = e₀ ∧ proj ∘ ⇑F = ⇑f

Universal property of the universal cover: a continuous map from a simply connected, locally path-connected space lifts uniquely after specifying the image of one point.