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 PartialHomeomorph, which is a homeomorphism between specific open subsets.

Main results

• local homeomorphisms are locally injective open maps
• more!

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 : PartialHomeomorph X Y with f = e.

Equations

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

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)

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

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

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 : PartialHomeomorph 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 : PartialHomeomorph X Y to agree with f on its source e.source, as opposed to on the whole space X.

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

A PartialHomeomorph is a local homeomorphism on its 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

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

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)

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)

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

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

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

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 : PartialHomeomorph X Y with f = e.

Equations

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

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

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

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

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)

theorem Topology.IsOpenEmbedding.isLocalHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) : IsLocalHomeomorph f

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.

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

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.

theorem IsLocalHomeomorph.mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : ∀ (x : X), ∃ (e : PartialHomeomorph 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 : PartialHomeomorph X Y to agree with f on its source e.source, as opposed to on the whole space X.

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.

theorem IsLocalHomeomorph.isLocallyInjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) : IsLocallyInjective f

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

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)

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.

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.

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.

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.

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 ⋯ ⋯

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.

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.