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 fmeans the image of an open set underfis open.is_closed_map fmeans the image of a closed set underfis closed.
(Open and closed maps need not be continuous.)
inducing fmeans the topology onXis the one induced viaffrom the topology onY. These behave like embeddings except they need not be injective. Instead, points ofXwhich are identified byfare also indistinguishable in the topology onX.embedding fmeansfis inducing and also injective. Equivalently,fidentifiesXwith a subspace ofY.open_embedding fmeansfis an embedding with open image, so it identifiesXwith an open subspace ofY. Equivalently,fis an embedding and an open map.closed_embedding fsimilarly meansfis an embedding with closed image, so it identifiesXwith a closed subspace ofY. Equivalently,fis an embedding and a closed map.quotient_map fis the dual condition toembedding f:fis surjective and the topology onYis the one coinduced viaffrom the topology onX. Equivalently,fidentifiesYwith a quotient ofX. Quotient maps are also sometimes known as identification maps.
References
- https://en.wikipedia.org/wiki/Open_and_closed_maps
- https://en.wikipedia.org/wiki/Embedding#General_topology
- https://en.wikipedia.org/wiki/Quotient_space_(topology)#Quotient_map
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
- induced : tα = topological_space.induced f tβ
theorem
inducing.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{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 f → continuous g → inducing (g ∘ f) → inducing f
theorem
inducing_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
theorem
inducing_is_closed
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
theorem
inducing.nhds_eq_comap
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : inducing f)
(a : α) :
nhds a = filter.comap f (nhds (f a))
theorem
inducing.map_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : inducing 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 (nhds b) ↔ filter.tendsto (g ∘ f) a (nhds (g b)))
theorem
inducing.continuous_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β}
{g : β → γ} :
inducing g → (continuous f ↔ continuous (g ∘ f))
theorem
inducing.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
inducing f → continuous f
structure
embedding
{α : Type u_1}
{β : Type u_2}
[tα : topological_space α]
[tβ : topological_space β] :
(α → β) → 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.
theorem
embedding.mk'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β) :
function.injective f → (∀ (a : α), filter.comap f (nhds (f a)) = nhds a) → embedding f
theorem
embedding.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{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 f → continuous g → embedding (g ∘ f) → embedding f
theorem
embedding_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
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 : α) :
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 (nhds b) ↔ filter.tendsto (g ∘ f) a (nhds (g b)))
theorem
embedding.continuous_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β}
{g : β → γ} :
embedding g → (continuous f ↔ continuous (g ∘ f))
theorem
embedding.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
embedding f → continuous 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
- quotient_map f = (function.surjective f ∧ tβ = topological_space.coinduced f tα)
theorem
quotient_map.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : β → γ}
{f : α → β} :
quotient_map g → quotient_map f → quotient_map (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 : β → γ} :
continuous f → continuous g → quotient_map (g ∘ f) → quotient_map g
theorem
quotient_map.continuous_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β}
{g : β → γ} :
quotient_map f → (continuous g ↔ continuous (g ∘ f))
theorem
quotient_map.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
quotient_map f → continuous 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 β.
theorem
is_open_map.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : β → γ}
{f : α → β} :
is_open_map g → is_open_map f → is_open_map (g ∘ f)
theorem
is_open_map.is_open_range
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
is_open_map f → is_open (set.range 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 α} :
theorem
is_open_map.nhds_le
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : is_open_map f)
(a : α) :
nhds (f a) ≤ filter.map f (nhds a)
theorem
is_open_map.of_inverse
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{f' : β → α} :
continuous f' → function.left_inverse f f' → function.right_inverse f f' → is_open_map f
theorem
is_open_map.to_quotient_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
is_open_map f → continuous f → function.surjective f → quotient_map f
theorem
is_open_map_iff_nhds_le
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
is_open_map f ↔ ∀ (a : α), nhds (f a) ≤ filter.map f (nhds a)
def
is_closed_map
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
(α → β) → Prop
theorem
is_closed_map.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : β → γ}
{f : α → β} :
is_closed_map g → is_closed_map f → is_closed_map (g ∘ f)
theorem
is_closed_map.of_inverse
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{f' : β → α} :
continuous f' → function.left_inverse f f' → function.right_inverse f f' → 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 : α → β} :
open_embedding f → is_open_map f
theorem
open_embedding.continuous
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
open_embedding f → continuous 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 : α → β} :
embedding f → is_open_map f → open_embedding f
theorem
open_embedding_of_continuous_injective_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
continuous f → function.injective f → is_open_map f → open_embedding f
theorem
open_embedding.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : β → γ}
{f : α → β} :
open_embedding g → open_embedding f → open_embedding (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 : α → β} :
closed_embedding f → continuous 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 : α → β} :
embedding f → is_closed_map f → closed_embedding f
theorem
closed_embedding_of_continuous_injective_closed
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β} :
continuous f → function.injective f → is_closed_map f → closed_embedding f
theorem
closed_embedding.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : β → γ}
{f : α → β} :
closed_embedding g → closed_embedding f → closed_embedding (g ∘ f)