Covering maps and clopen sets

A covering map p : E → ↥s onto a subspace of X is also a covering map E → X as soon as s is clopen: over a point of s an evenly covered neighbourhood in ↥s is one in X because s is open, and over a point outside s the open set sᶜ has empty preimage, which IsEvenlyCovered.of_preimage_eq_empty accepts as an evenly covered neighbourhood with empty fibre.

Openness alone is not enough: for s open but not closed, a point of frontier s has every neighbourhood meeting s, so no neighbourhood of it is evenly covered by a surjection onto s. Mathlib's IsCoveringMap allows empty fibres, which is exactly what makes the clopen statement work without assuming p surjective or s = X.

The number of points in a fibre of a covering map is locally constant: an evenly covered neighbourhood identifies the fibres over all of its points. So for any type α, the set of points whose fibre is in bijection with α is clopen.

Main declarations

• IsCoveringMap.subtypeVal_comp: the composite of a covering map onto a clopen subspace with the subspace inclusion is a covering map.
• IsCoveringMap.isClopen_setOf_nonempty_fiber_equiv: the points whose fibre is in bijection with a given type form a clopen set.
• IsCoveringMap.nonempty_fiber_equiv: over a preconnected base all fibres are in bijection, and IsCoveringMap.surjective: a covering map from a nonempty space onto a preconnected space is surjective.

theorem IsCoveringMap.subtypeVal_comp {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {s : Set X} {p : E → ↑s} (hp : IsCoveringMap p) (hs : IsClopen s) : IsCoveringMap (Subtype.val ∘ p)

A covering map onto a clopen subspace is a covering map into the ambient space. Points of s inherit their evenly covered neighbourhoods through the open inclusion, and points outside s are evenly covered by sᶜ with empty fibre.

theorem IsCoveringMap.isClopen_setOf_nonempty_fiber_equiv {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) (α : Type u_3) : IsClopen {x : X | Nonempty (↑(p ⁻¹' {x}) ≃ α)}

The number of points in a fibre of a covering map is locally constant. Over an evenly covered neighbourhood all fibres are in bijection, so both the points whose fibre is in bijection with α and the points whose fibre is not are open.

theorem IsCoveringMap.nonempty_fiber_equiv {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] [PreconnectedSpace X] {p : E → X} (hp : IsCoveringMap p) (x y : X) : Nonempty (↑(p ⁻¹' {x}) ≃ ↑(p ⁻¹' {y}))

Over a preconnected base, all fibres of a covering map are in bijection. The points whose fibre is in bijection with the fibre over y form a clopen set containing y, hence everything.

theorem IsCoveringMap.surjective {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] [PreconnectedSpace X] [Nonempty E] {p : E → X} (hp : IsCoveringMap p) : Function.Surjective p

A covering map from a nonempty space onto a preconnected space is surjective: every fibre is in bijection with the fibre through a given point.