Specific classes of maps between topological spaces

This file introduces the following properties of a map f : X → Y between topological spaces:

is_open_map f means the image of an open set under f is open.
is_closed_map f means the image of a closed set under f is closed.

(Open and closed maps need not be continuous.)

inducing f means the topology on X is the one induced via f from the topology on Y. These behave like embeddings except they need not be injective. Instead, points of X which are identified by f are also indistinguishable in the topology on X.
embedding f means f is inducing and also injective. Equivalently, f identifies X with a subspace of Y.
open_embedding f means f is an embedding with open image, so it identifies X with an open subspace of Y. Equivalently, f is an embedding and an open map.
closed_embedding f similarly means f is an embedding with closed image, so it identifies X with a closed subspace of Y. Equivalently, f is an embedding and a closed map.
quotient_map f is the dual condition to embedding f: f is surjective and the topology on Y is the one coinduced via f from the topology on X. Equivalently, f identifies Y with a quotient of X. Quotient maps are also sometimes known as identification maps.

References

Tags

open map, closed map, embedding, quotient map, identification map

source

structure inducing {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] (f : α → β) :

Prop

induced : tα = topological_space.induced f tβ

source

theorem inducing_id {α : Type u_1} [topological_space α] :

inducing id

source

theorem inducing.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : inducing g) (hf : inducing f) :

inducing (g ∘ f)

source

theorem inducing_of_inducing_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hf : continuous f) (hg : continuous g) (hgf : inducing (g ∘ f)) :

inducing f

source

theorem inducing_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (hf : inducing f) (h : is_open (set.range f)) (hs : is_open s) :

is_open (f '' s)

source

theorem inducing_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (hf : inducing f) (h : is_closed (set.range f)) (hs : is_closed s) :

is_closed (f '' s)

source

theorem inducing.nhds_eq_comap {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : inducing f) (a : α) :

𝓝 a = filter.comap f (𝓝 (f a))

source

theorem inducing.map_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : inducing f) (a : α) (h : set.range f ∈ 𝓝 (f a)) :

filter.map f (𝓝 a) = 𝓝 (f a)

source

theorem inducing.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] {ι : Type u_1} {f : ι → β} {g : β → γ} {a : filter ι} {b : β} (hg : inducing g) :

filter.tendsto f a (𝓝 b) ↔ filter.tendsto (g ∘ f) a (𝓝 (g b))

source

theorem inducing.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hg : inducing g) :

continuous f ↔ continuous (g ∘ f)

source

theorem inducing.continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : inducing f) :

continuous f

source

structure embedding {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] (f : α → β) :

Prop

to_inducing : inducing f
inj : function.injective f

A function between topological spaces is an embedding if it is injective, and for all s : set α, s is open iff it is the preimage of an open set.

source

theorem embedding.mk' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (inj : function.injective f) (induced : ∀ (a : α), filter.comap f (𝓝 (f a)) = 𝓝 a) :

embedding f

source

theorem embedding_id {α : Type u_1} [topological_space α] :

embedding id

source

theorem embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : embedding g) (hf : embedding f) :

embedding (g ∘ f)

source

theorem embedding_of_embedding_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hf : continuous f) (hg : continuous g) (hgf : embedding (g ∘ f)) :

embedding f

source

theorem embedding_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (hf : embedding f) (h : is_open (set.range f)) (hs : is_open s) :

is_open (f '' s)

source

theorem embedding_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (hf : embedding f) (h : is_closed (set.range f)) (hs : is_closed s) :

is_closed (f '' s)

source

theorem embedding.map_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : embedding f) (a : α) (h : set.range f ∈ 𝓝 (f a)) :

filter.map f (𝓝 a) = 𝓝 (f a)

source

theorem embedding.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] {ι : Type u_1} {f : ι → β} {g : β → γ} {a : filter ι} {b : β} (hg : embedding g) :

filter.tendsto f a (𝓝 b) ↔ filter.tendsto (g ∘ f) a (𝓝 (g b))

source

theorem embedding.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hg : embedding g) :

continuous f ↔ continuous (g ∘ f)

source

theorem embedding.continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : embedding f) :

continuous f

source

theorem embedding.closure_eq_preimage_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {e : α → β} (he : embedding e) (s : set α) :

closure s = e ⁻¹' closure (e '' s)

source

def quotient_map {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] (f : α → β) :

Prop

A function between topological spaces is a quotient map if it is surjective, and for all s : set β, s is open iff its preimage is an open set.

Equations

quotient_map f = (function.surjective f ∧ tβ = topological_space.coinduced f tα)

source

theorem quotient_map.id {α : Type u_1} [topological_space α] :

quotient_map id

source

theorem quotient_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : quotient_map g) (hf : quotient_map f) :

quotient_map (g ∘ f)

source

theorem quotient_map.of_quotient_map_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hf : continuous f) (hg : continuous g) (hgf : quotient_map (g ∘ f)) :

quotient_map g

source

theorem quotient_map.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hf : quotient_map f) :

continuous g ↔ continuous (g ∘ f)

source

theorem quotient_map.continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : quotient_map f) :

continuous f

source

def is_open_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) :

Prop

A map f : α → β is said to be an open map, if the image of any open U : set α is open in β.

Equations

is_open_map f = ∀ (U : set α), is_open U → is_open (f '' U)

source

theorem is_open_map.id {α : Type u_1} [topological_space α] :

is_open_map id

source

theorem is_open_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : is_open_map g) (hf : is_open_map f) :

is_open_map (g ∘ f)

source

theorem is_open_map.is_open_range {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : is_open_map f) :

is_open (set.range f)

source

theorem is_open_map.image_mem_nhds {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : is_open_map f) {x : α} {s : set α} (hx : s ∈ 𝓝 x) :

f '' s ∈ 𝓝 (f x)

source

theorem is_open_map.nhds_le {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : is_open_map f) (a : α) :

𝓝 (f a) ≤ filter.map f (𝓝 a)

source

theorem is_open_map.of_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {f' : β → α} (h : continuous f') (l_inv : function.left_inverse f f') (r_inv : function.right_inverse f f') :

is_open_map f

source

theorem is_open_map.to_quotient_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (open_map : is_open_map f) (cont : continuous f) (surj : function.surjective f) :

quotient_map f

source

theorem is_open_map_iff_nhds_le {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

is_open_map f ↔ ∀ (a : α), 𝓝 (f a) ≤ filter.map f (𝓝 a)

source

def is_closed_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) :

Prop

Equations

is_closed_map f = ∀ (U : set α), is_closed U → is_closed (f '' U)

source

theorem is_closed_map.id {α : Type u_1} [topological_space α] :

is_closed_map id

source

theorem is_closed_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : is_closed_map g) (hf : is_closed_map f) :

is_closed_map (g ∘ f)

source

theorem is_closed_map.of_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {f' : β → α} (h : continuous f') (l_inv : function.left_inverse f f') (r_inv : function.right_inverse f f') :

is_closed_map f

source

theorem is_closed_map.of_nonempty {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h : ∀ (s : set α), is_closed s → s.nonempty → is_closed (f '' s)) :

is_closed_map f

source

structure open_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) :

Prop

to_embedding : embedding f
open_range : is_open (set.range f)

An open embedding is an embedding with open image.

source

theorem open_embedding.open_iff_image_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : open_embedding f) {s : set α} :

is_open s ↔ is_open (f '' s)

source

theorem open_embedding.is_open_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : open_embedding f) :

is_open_map f

source

theorem open_embedding.continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : open_embedding f) :

continuous f

source

theorem open_embedding.open_iff_preimage_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : open_embedding f) {s : set β} (hs : s ⊆ set.range f) :

is_open s ↔ is_open (f ⁻¹' s)

source

theorem open_embedding_of_embedding_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h₁ : embedding f) (h₂ : is_open_map f) :

open_embedding f

source

theorem open_embedding_of_continuous_injective_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h₁ : continuous f) (h₂ : function.injective f) (h₃ : is_open_map f) :

open_embedding f

source

theorem open_embedding_id {α : Type u_1} [topological_space α] :

open_embedding id

source

theorem open_embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : open_embedding g) (hf : open_embedding f) :

open_embedding (g ∘ f)

source

structure closed_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) :

Prop

to_embedding : embedding f
closed_range : is_closed (set.range f)

A closed embedding is an embedding with closed image.

source

theorem closed_embedding.continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : closed_embedding f) :

continuous f

source

theorem closed_embedding.closed_iff_image_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : closed_embedding f) {s : set α} :

is_closed s ↔ is_closed (f '' s)

source

theorem closed_embedding.is_closed_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : closed_embedding f) :

is_closed_map f

source

theorem closed_embedding.closed_iff_preimage_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : closed_embedding f) {s : set β} (hs : s ⊆ set.range f) :

is_closed s ↔ is_closed (f ⁻¹' s)

source

theorem closed_embedding_of_embedding_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h₁ : embedding f) (h₂ : is_closed_map f) :

closed_embedding f

source

theorem closed_embedding_of_continuous_injective_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h₁ : continuous f) (h₂ : function.injective f) (h₃ : is_closed_map f) :

closed_embedding f

source

theorem closed_embedding_id {α : Type u_1} [topological_space α] :

closed_embedding id

source

theorem closed_embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} (hg : closed_embedding g) (hf : closed_embedding f) :

closed_embedding (g ∘ f)