A map of covering spaces with locally connected target is a covering map

Let p : E → X and q : F → X be covering maps and let g : E → F be a continuous map over X, that is, q ∘ g = p. This file proves that g is itself a covering map as soon as F is locally connected.

The proof is the standard sheet comparison. Around a point f₀ of F, choose a connected open neighbourhood in F whose image V lies inside the intersection of evenly covered neighbourhoods for p and q, and trivialize both projections over V. A sheet of p over V is the image of V under v ↦ tp.symm (v, i), so it is connected, and the sheet index of its image under g is a continuous map from V to a discrete space, hence constant. So g carries each sheet of p over V onto a single sheet of q, and injectively, because p = q ∘ g is injective on it. The sheet W of q through f₀ is therefore evenly covered by g, with fibre the set of sheets of p that land in W.

Local connectedness of F produces the connected neighbourhood whose open, connected image is V. It is used exactly once, to make the sheet index locally constant.

Neither total space is assumed connected and g is not assumed surjective. That is consistent because IsCoveringMap allows empty fibres: over a sheet of q missed by g the fibre of g is empty.

Main declarations

• IsCoveringMap.of_comp_eq: a continuous map between covering spaces, with locally connected target and commuting with the projections, is a covering map.

theorem IsCoveringMap.of_comp_eq {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {g : E → F} [LocallyConnectedSpace F] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hg : Continuous g) (hgp : q ∘ g = p) : IsCoveringMap g

A map of covering spaces with locally connected target is a covering map. If p : E → X and q : F → X are covering maps and g : E → F is continuous with q ∘ g = p, then g is a covering map provided F is locally connected.

Neither total space needs to be connected and g need not be surjective; the fibre of g over a point outside its range is empty, which IsCoveringMap permits.