Covering maps from local sections of uniform radius

Let p : E → X be a continuous map from a Hausdorff space to a locally connected pseudometric space. Suppose that there is one radius ε > 0 such that every point e : E lies on a continuous local section of p over the ball of radius ε about p e, and that the image of that ball under the section is open. Then p is a covering map.

This is the form in which coverings arise from gluing constructions: the sections are written down by hand, and the uniformity of their radius is the completeness that rules out a local homeomorphism which is not a covering. A typical use is the covering of a homogeneous space by a space glued from translates of a tile, as in Poincaré's polygon theorem.

The sheets over a point x are the images, under the sections through the points of the fibre over x, of a connected open neighbourhood V of x inside the ball of radius ε / 2. Two sections that agree at one point of V agree on all of V, because p is locally injective and E is Hausdorff. Every point e' over V lies on its own section, whose ball contains V, so e' lies on the sheet through the point of the fibre where that section passes.

Main results

• IsCoveringMap.of_forall_exists_section: a continuous map with local sections of uniform radius and open image, from a Hausdorff space to a locally connected pseudometric space, is a covering map.

References

• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3 (covering spaces).

theorem IsCoveringMap.of_forall_exists_section {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [PseudoMetricSpace X] {p : E → X} [T2Space E] [LocallyConnectedSpace X] (hp : Continuous p) {ε : ℝ} (hε : 0 < ε) (h : ∀ (e : E), ∃ (s : X → E), ContinuousOn s (Metric.ball (p e) ε) ∧ IsOpen (s '' Metric.ball (p e) ε) ∧ (∀ x ∈ Metric.ball (p e) ε, p (s x) = x) ∧ s (p e) = e) : IsCoveringMap p

A map with local sections of uniform radius is a covering map. Let p : E → X be a continuous map from a Hausdorff space to a locally connected pseudometric space, and let ε > 0. If every point e is the value at p e of a section of p over the ball of radius ε about p e which is continuous on that ball and maps it to an open set, then p is a covering map.