# Local homeomorphisms #

This file defines local homeomorphisms.

## Main definitions #

For a function `f : X → Y` between topological spaces, we say

- `IsLocalHomeomorphOn f s` if `f` is a local homeomorphism around each point of `s`: for each `x : X`, the restriction of `f` to some open neighborhood `U` of `x` gives a homeomorphism between `U` and an open subset of `Y`.
- `IsLocalHomeomorph f`: `f` is a local homeomorphism, i.e. it's a local homeomorphism on `univ`.

Note that `IsLocalHomeomorph` is a global condition. This is in contrast to `OpenPartialHomeomorph`, which is a homeomorphism between specific open subsets.

## Main results #

- local homeomorphisms are locally injective open maps
- more!

source
def IsLocalHomeomorphOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) :
Prop

A function `f : X → Y` satisfies `IsLocalHomeomorphOn f s` if each `x ∈ s` is contained in the source of some `e : OpenPartialHomeomorph X Y` with `f = e`.

Equations

- IsLocalHomeomorphOn f s = ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = ↑e

Instances For

source
theorem isLocalHomeomorphOn_iff_isOpenEmbedding_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) {f : X → Y} :
IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ nhds x, Topology.IsOpenEmbedding (U.restrict f)
source
theorem IsLocalHomeomorphOn.discreteTopology_of_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (h : IsLocalHomeomorphOn f s) [DiscreteTopology ↑(f '' s)] :
DiscreteTopology ↑s
source
theorem IsLocalHomeomorphOn.discreteTopology_image_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (h : IsLocalHomeomorphOn f s) (hs : IsOpen s) :
DiscreteTopology ↑(f '' s) ↔ DiscreteTopology ↑s
source
theorem IsLocalHomeomorphOn.mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) (h : ∀ x ∈ s, ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e) e.source) :
IsLocalHomeomorphOn f s

Proves that `f` satisfies `IsLocalHomeomorphOn f s`. The condition `h` is weaker than the definition of `IsLocalHomeomorphOn f s`, since it only requires `e : OpenPartialHomeomorph X Y` to agree with `f` on its source `e.source`, as opposed to on the whole space `X`.

source
theorem IsLocalHomeomorphOn.OpenPartialHomeomorph.isLocalHomeomorphOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :
IsLocalHomeomorphOn (↑e) e.source

A `OpenPartialHomeomorph` is a local homeomorphism on its source.

source
theorem IsLocalHomeomorphOn.mono {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s t : Set X} (hf : IsLocalHomeomorphOn f t) (hst : s ⊆ t) :
IsLocalHomeomorphOn f s
source
theorem IsLocalHomeomorphOn.of_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} {s : Set X} (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hg : IsLocalHomeomorphOn g (f '' s)) (cont : ∀ x ∈ s, ContinuousAt f x) :
IsLocalHomeomorphOn f s
source
theorem IsLocalHomeomorphOn.of_comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} {s : Set X} (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hf : IsLocalHomeomorphOn f s) :
IsLocalHomeomorphOn g (f '' s)
source
theorem IsLocalHomeomorphOn.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsLocalHomeomorphOn f s) {x : X} (hx : x ∈ s) :
Filter.map f (nhds x) = nhds (f x)
source
theorem IsLocalHomeomorphOn.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsLocalHomeomorphOn f s) {x : X} (hx : x ∈ s) :
ContinuousAt f x
source
theorem IsLocalHomeomorphOn.continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsLocalHomeomorphOn f s) :
ContinuousOn f s
source
theorem IsLocalHomeomorphOn.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} {s : Set X} {t : Set Y} (hg : IsLocalHomeomorphOn g t) (hf : IsLocalHomeomorphOn f s) (h : Set.MapsTo f s t) :
IsLocalHomeomorphOn (g ∘ f) s
source
def IsLocalHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :
Prop

A function `f : X → Y` satisfies `IsLocalHomeomorph f` if each `x : x` is contained in the source of some `e : OpenPartialHomeomorph X Y` with `f = e`.

Equations

- IsLocalHomeomorph f = ∀ (x : X), ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ f = ↑e

Instances For

source
theorem Homeomorph.isLocalHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) :
IsLocalHomeomorph ⇑f
source
theorem isLocalHomeomorph_iff_isLocalHomeomorphOn_univ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :
IsLocalHomeomorph f ↔ IsLocalHomeomorphOn f Set.univ
source
theorem IsLocalHomeomorph.isLocalHomeomorphOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsLocalHomeomorph f) :
IsLocalHomeomorphOn f s
source
theorem isLocalHomeomorph_iff_isOpenEmbedding_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :
IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ nhds x, Topology.IsOpenEmbedding (U.restrict f)
source
theorem Topology.IsOpenEmbedding.isLocalHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) :
IsLocalHomeomorph f
source
theorem IsLocalHomeomorph.comap_discreteTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsLocalHomeomorph f) [DiscreteTopology Y] :
DiscreteTopology X

A space that admits a local homeomorphism to a discrete space is itself discrete.

source
theorem IsLocalHomeomorph.discreteTopology_range_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsLocalHomeomorph f) :
DiscreteTopology ↑(Set.range f) ↔ DiscreteTopology X
source
theorem IsLocalHomeomorph.discreteTopology_iff_of_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsLocalHomeomorph f) (hs : Function.Surjective f) :
DiscreteTopology X ↔ DiscreteTopology Y

If there is a surjective local homeomorphism between two spaces and one of them is discrete, then both spaces are discrete.

source
theorem IsLocalHomeomorph.mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : ∀ (x : X), ∃ (e : OpenPartialHomeomorph X Y), x ∈ e.source ∧ Set.EqOn f (↑e) e.source) :
IsLocalHomeomorph f

Proves that `f` satisfies `IsLocalHomeomorph f`. The condition `h` is weaker than the definition of `IsLocalHomeomorph f`, since it only requires `e : OpenPartialHomeomorph X Y` to agree with `f` on its source `e.source`, as opposed to on the whole space `X`.

source
theorem IsLocalHomeomorph.Homeomorph.isLocalHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) :
IsLocalHomeomorph ⇑h

A homeomorphism is a local homeomorphism.

source
theorem IsLocalHomeomorph.isLocallyInjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) :
IsLocallyInjective f
source
theorem IsLocalHomeomorph.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} (hgf : IsLocalHomeomorph (g ∘ f)) (hg : IsLocalHomeomorph g) (cont : Continuous f) :
IsLocalHomeomorph f
source
theorem IsLocalHomeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) (x : X) :
Filter.map f (nhds x) = nhds (f x)
source
theorem IsLocalHomeomorph.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) :
Continuous f

A local homeomorphism is continuous.

source
theorem IsLocalHomeomorph.isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) :
IsOpenMap f

A local homeomorphism is an open map.

source
theorem IsLocalHomeomorph.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} (hg : IsLocalHomeomorph g) (hf : IsLocalHomeomorph f) :
IsLocalHomeomorph (g ∘ f)

The composition of local homeomorphisms is a local homeomorphism.

source
theorem IsLocalHomeomorph.isOpenEmbedding_of_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) (hi : Function.Injective f) :
Topology.IsOpenEmbedding f

An injective local homeomorphism is an open embedding.

source
noncomputable def IsLocalHomeomorph.toHomeomorph_of_bijective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) (hb : Function.Bijective f) :
X ≃ₜ Y

A bijective local homeomorphism is a homeomorphism.

Equations

- hf.toHomeomorph_of_bijective hb = (Equiv.ofBijective f hb).toHomeomorphOfContinuousOpen ⋯ ⋯

Instances For

source
theorem IsLocalHomeomorph.isOpenEmbedding_of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g : Y → Z} {f : X → Y} (hf : IsLocalHomeomorph g) (hgf : Topology.IsOpenEmbedding (g ∘ f)) (cont : Continuous f) :
Topology.IsOpenEmbedding f

Continuous local sections of a local homeomorphism are open embeddings.

source
theorem IsLocalHomeomorph.isTopologicalBasis {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) :
TopologicalSpace.IsTopologicalBasis {U : Set X | ∃ (V : Set Y), IsOpen V ∧ ∃ (s : C(↑V, X)), f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}

Ranges of continuous local sections of a local homeomorphism form a basis of the source space.