mathlib documentation

topology.maps

Specific classes of maps between topological spaces

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

(Open and closed maps need not be continuous.)

References

Tags

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

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

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

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

theorem inducing_of_inducing_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} :
continuous fcontinuous ginducing (g f)inducing f

theorem inducing_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
inducing fis_open (set.range f)is_open sis_open (f '' s)

theorem inducing_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
inducing fis_closed (set.range f)is_closed sis_closed (f '' s)

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

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

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

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

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

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

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.

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

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

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

theorem embedding_of_embedding_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} :
continuous fcontinuous gembedding (g f)embedding f

theorem embedding_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
embedding fis_open (set.range f)is_open sis_open (f '' s)

theorem embedding_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :

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

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

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

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

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

def quotient_map {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] :
(α → β) → 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
theorem quotient_map.id {α : Type u_1} [topological_space α] :

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

theorem quotient_map.of_quotient_map_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} :

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

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

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

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

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

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

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

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 α} :
s 𝓝 xf '' s 𝓝 (f x)

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)

theorem is_open_map.of_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {f' : β → α} :

theorem is_open_map.to_quotient_map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

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)

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

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

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

theorem is_closed_map.of_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {f' : β → α} :

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

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

An open embedding is an embedding with open image.

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

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

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

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

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

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

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

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

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

A closed embedding is an embedding with closed image.

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

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

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

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

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

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

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