Local homeomorphisms that are proper over an open set are coverings there

A local homeomorphism f : E → X need not be a covering map: an open inclusion is a local homeomorphism, and it is not evenly covered at the boundary of its image. What fails there is properness, and the classical remedy is that a proper local homeomorphism between Hausdorff spaces is a covering map. Mathlib records the special case of a compact total space (isLocalHomeomorph_iff_isCoveringMap) and the closed-map form IsClosedMap.isCoveringMapOn_of_isLocalHomeomorphOn.

This file gives the version over an open subset s of a locally compact base: if every compact subset of s has compact preimage, then f is a covering map over s, whatever happens outside s. This is the form a holomorphic map of a domain supplies when it is known to send points near the boundary of the domain close to a closed set C: over the complement s = Cᶜ the map is proper, hence a covering.

Main results

• IsCoveringMapOn.of_isLocalHomeomorph_of_isCompact_preimage -- a local homeomorphism is a covering map over an open set on whose compact subsets it is proper.

References

• O. Forster, Lectures on Riemann Surfaces, Section 4.

theorem IsCoveringMapOn.of_isLocalHomeomorph_of_isCompact_preimage {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {f : E → X} {s : Set X} [T2Space E] [T2Space X] [LocallyCompactSpace X] (hs : IsOpen s) (hf : IsLocalHomeomorphOn f (f ⁻¹' s)) (hK : ∀ K ⊆ s, IsCompact K → IsCompact (f ⁻¹' K)) : IsCoveringMapOn f s

A map locally homeomorphic above an open set is a covering there if it is proper there. If f : E → X is a local homeomorphism on f ⁻¹' s, where the spaces are Hausdorff and X is locally compact, and every compact subset of s has compact preimage, then f is a covering map over s.