Local homeomorphisms: local path-connectedness and local inverses

A local homeomorphism p : E → B identifies a neighbourhood of each point of E with an open subset of B, so E inherits any property of B that is local and stable under passing to open subspaces. This file records that for local path-connectedness.

The intended use is a covering map, whose total space is therefore locally path-connected as soon as the base is; this is what lets the covers built over a locally path-connected base be fed back into results that require a locally path-connected source, such as the lifting criterion.

A local inverse L of p composed with p is a local deck transformation of p. Near a point z it agrees with every local deck transformation of p that is continuous at z and sends z into the target of L. This is what identifies the transition maps of charts pushed forward along p with deck transformations.

Main results

• IsLocalHomeomorph.locallyPathConnectedSpace: the domain of a local homeomorphism into a locally path-connected space is locally path-connected.
• IsLocalHomeomorph.localInverseAt_comp_eventuallyEq: near z, a local inverse composed with p agrees with any continuous local deck transformation sending z into the target of that local inverse.

theorem IsLocalHomeomorph.locallyPathConnectedSpace {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] [LocallyPathConnectedSpace B] {p : E → B} (hp : IsLocalHomeomorph p) : LocallyPathConnectedSpace E

A local homeomorphism with locally path-connected codomain has locally path-connected domain. In particular the total space of a covering of a locally path-connected space is locally path-connected.

theorem IsLocalHomeomorph.localInverseAt_comp_eventuallyEq {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsLocalHomeomorph p) {e z : E} {φ : E → E} (hφ : ContinuousAt φ z) (hφz : φ z ∈ (hp.localInverseAt e).target) (hpφ : p ∘ φ =ᶠ[nhds z] p) : ↑(hp.localInverseAt e) ∘ p =ᶠ[nhds z] φ

Let L be a local inverse of a local homeomorphism p at e. If φ is continuous at z, satisfies p ∘ φ = p near z, and sends z into the target of L, then L ∘ p agrees with φ near z.