topology.maps

# Specific classes of maps between topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 inseparable 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.

## Tags #

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

structure inducing {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] (f : α β) :
Prop
• induced : =

A function f : α → β between topological spaces is inducing if the topology on α is induced by the topology on β through f, meaning that a set s : set α is open iff it is the preimage under f of some open set t : set β.

theorem inducing_iff {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] (f : α β) :
=
theorem inducing_id {α : Type u_1}  :
@[protected]
theorem inducing.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : inducing g) (hf : inducing f) :
theorem inducing_of_inducing_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} (hf : continuous f) (hg : continuous g) (hgf : inducing (g f)) :
theorem inducing_iff_nhds {α : Type u_1} {β : Type u_2} {f : α β} :
(a : α), nhds a = (nhds (f a))
theorem inducing.nhds_eq_comap {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) (a : α) :
nhds a = (nhds (f a))
theorem inducing.nhds_set_eq_comap {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) (s : set α) :
= (nhds_set (f '' s))
theorem inducing.map_nhds_eq {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) (a : α) :
(nhds a) = nhds_within (f a) (set.range f)
theorem inducing.map_nhds_of_mem {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) (a : α) (h : nhds (f a)) :
(nhds a) = nhds (f a)
theorem inducing.image_mem_nhds_within {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) {a : α} {s : set α} (hs : s nhds a) :
f '' s nhds_within (f a) (set.range f)
theorem inducing.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} {ι : Type u_1} {f : ι β} {g : β γ} {a : filter ι} {b : β} (hg : inducing g) :
(nhds b) filter.tendsto (g f) a (nhds (g b))
theorem inducing.continuous_at_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} (hg : inducing g) {x : α} :
theorem inducing.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} (hg : inducing g) :
theorem inducing.continuous_at_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} (hf : inducing f) {x : α} (h : nhds (f x)) :
continuous_at (g f) x (f x)
@[protected]
theorem inducing.continuous {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) :
@[protected]
theorem inducing.inducing_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} (hg : inducing g) :
theorem inducing.closure_eq_preimage_closure_image {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) (s : set α) :
= f ⁻¹' closure (f '' s)
theorem inducing.is_closed_iff {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) {s : set α} :
(t : set β), f ⁻¹' t = s
theorem inducing.is_closed_iff' {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) {s : set α} :
(x : α), f x closure (f '' s) x s
theorem inducing.is_closed_preimage {α : Type u_1} {β : Type u_2} {f : α β} (h : inducing f) (s : set β) (hs : is_closed s) :
theorem inducing.is_open_iff {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) {s : set α} :
(t : set β), f ⁻¹' t = s
theorem inducing.dense_iff {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) {s : set α} :
(x : α), f x closure (f '' s)
structure embedding {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] (f : α β) :
Prop
• to_inducing :
• inj :

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_iff {α : Type u_1} {β : Type u_2} [tα : topological_space α] [tβ : topological_space β] (f : α β) :
theorem function.injective.embedding_induced {α : Type u_1} {β : Type u_2} [t : topological_space β] {f : α β} (hf : function.injective f) :
theorem embedding.mk' {α : Type u_1} {β : Type u_2} (f : α β) (inj : function.injective f) (induced : (a : α), (nhds (f a)) = nhds a) :
theorem embedding_id {α : Type u_1}  :
theorem embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : embedding g) (hf : embedding f) :
theorem embedding_of_embedding_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} (hf : continuous f) (hg : continuous g) (hgf : embedding (g f)) :
@[protected]
theorem function.left_inverse.embedding {α : Type u_1} {β : Type u_2} {f : α β} {g : β α} (h : g) (hf : continuous f) (hg : continuous g) :
theorem embedding.map_nhds_eq {α : Type u_1} {β : Type u_2} {f : α β} (hf : embedding f) (a : α) :
(nhds a) = nhds_within (f a) (set.range f)
theorem embedding.map_nhds_of_mem {α : Type u_1} {β : Type u_2} {f : α β} (hf : embedding f) (a : α) (h : nhds (f a)) :
(nhds a) = nhds (f a)
theorem embedding.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} {ι : Type u_1} {f : ι β} {g : β γ} {a : filter ι} {b : β} (hg : embedding g) :
(nhds b) filter.tendsto (g f) a (nhds (g b))
theorem embedding.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : β γ} (hg : embedding g) :
theorem embedding.continuous {α : Type u_1} {β : Type u_2} {f : α β} (hf : embedding f) :
theorem embedding.closure_eq_preimage_closure_image {α : Type u_1} {β : Type u_2} {e : α β} (he : embedding e) (s : set α) :
= e ⁻¹' closure (e '' s)
theorem embedding.discrete_topology {X : Type u_1} {Y : Type u_2} [tY : topological_space Y] {f : X Y} (hf : embedding f) :

The topology induced under an inclusion f : X → Y from the discrete topological space Y is the discrete topology on X.

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
theorem quotient_map_iff {α : Type u_1} {β : Type u_2} {f : α β} :
(s : set β), is_open (f ⁻¹' s)
theorem quotient_map_iff_closed {α : Type u_1} {β : Type u_2} {f : α β} :
(s : set β), is_closed (f ⁻¹' s)
@[protected]
theorem quotient_map.id {α : Type u_1}  :
@[protected]
theorem quotient_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : quotient_map g) (hf : quotient_map f) :
@[protected]
theorem quotient_map.of_quotient_map_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hf : continuous f) (hg : continuous g) (hgf : quotient_map (g f)) :
theorem quotient_map.of_inverse {α : Type u_1} {β : Type u_2} {f : α β} {g : β α} (hf : continuous f) (hg : continuous g) (h : f) :
@[protected]
theorem quotient_map.continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hf : quotient_map f) :
@[protected]
theorem quotient_map.continuous {α : Type u_1} {β : Type u_2} {f : α β} (hf : quotient_map f) :
@[protected]
theorem quotient_map.surjective {α : Type u_1} {β : Type u_2} {f : α β} (hf : quotient_map f) :
@[protected]
theorem quotient_map.is_open_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : quotient_map f) {s : set β} :
@[protected]
theorem quotient_map.is_closed_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : quotient_map f) {s : set β} :
def is_open_map {α : Type u_1} {β : Type u_2} (f : α β) :
Prop

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

Equations
@[protected]
theorem is_open_map.id {α : Type u_1}  :
@[protected]
theorem is_open_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : is_open_map g) (hf : is_open_map f) :
theorem is_open_map.is_open_range {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) :
theorem is_open_map.image_mem_nhds {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) {x : α} {s : set α} (hx : s nhds x) :
f '' s nhds (f x)
theorem is_open_map.range_mem_nhds {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) (x : α) :
nhds (f x)
theorem is_open_map.maps_to_interior {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) {s : set α} {t : set β} (h : s t) :
theorem is_open_map.image_interior_subset {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) (s : set α) :
f '' interior (f '' s)
theorem is_open_map.nhds_le {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) (a : α) :
nhds (f a) (nhds a)
theorem is_open_map.of_nhds_le {α : Type u_1} {β : Type u_2} {f : α β} (hf : (a : α), nhds (f a) (nhds a)) :
theorem is_open_map.of_sections {α : Type u_1} {β : Type u_2} {f : α β} (h : (x : α), (g : β α), (f x) g (f x) = x ) :
theorem is_open_map.of_inverse {α : Type u_1} {β : Type u_2} {f : α β} {f' : β α} (h : continuous f') (l_inv : f') (r_inv : f') :
theorem is_open_map.to_quotient_map {α : Type u_1} {β : Type u_2} {f : α β} (open_map : is_open_map f) (cont : continuous f) (surj : function.surjective f) :

A continuous surjective open map is a quotient map.

theorem is_open_map.interior_preimage_subset_preimage_interior {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) {s : set β} :
theorem is_open_map.preimage_interior_eq_interior_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf₁ : is_open_map f) (hf₂ : continuous f) (s : set β) :
theorem is_open_map.preimage_closure_subset_closure_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) {s : set β} :
theorem is_open_map.preimage_closure_eq_closure_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) (hfc : continuous f) (s : set β) :
theorem is_open_map.preimage_frontier_subset_frontier_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) {s : set β} :
theorem is_open_map.preimage_frontier_eq_frontier_preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_open_map f) (hfc : continuous f) (s : set β) :
theorem is_open_map_iff_nhds_le {α : Type u_1} {β : Type u_2} {f : α β} :
(a : α), nhds (f a) (nhds a)
theorem is_open_map_iff_interior {α : Type u_1} {β : Type u_2} {f : α β} :
(s : set α), f '' interior (f '' s)
@[protected]
theorem inducing.is_open_map {α : Type u_1} {β : Type u_2} {f : α β} (hi : inducing f) (ho : is_open (set.range f)) :

An inducing map with an open range is an open map.

def is_closed_map {α : Type u_1} {β : Type u_2} (f : α β) :
Prop

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

Equations
@[protected]
theorem is_closed_map.id {α : Type u_1}  :
@[protected]
theorem is_closed_map.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : is_closed_map g) (hf : is_closed_map f) :
theorem is_closed_map.closure_image_subset {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_closed_map f) (s : set α) :
closure (f '' s) f ''
theorem is_closed_map.of_inverse {α : Type u_1} {β : Type u_2} {f : α β} {f' : β α} (h : continuous f') (l_inv : f') (r_inv : f') :
theorem is_closed_map.of_nonempty {α : Type u_1} {β : Type u_2} {f : α β} (h : (s : set α), s.nonempty is_closed (f '' s)) :
theorem is_closed_map.closed_range {α : Type u_1} {β : Type u_2} {f : α β} (hf : is_closed_map f) :
theorem is_closed_map.to_quotient_map {α : Type u_1} {β : Type u_2} {f : α β} (hcl : is_closed_map f) (hcont : continuous f) (hsurj : function.surjective f) :
theorem inducing.is_closed_map {α : Type u_1} {β : Type u_2} {f : α β} (hf : inducing f) (h : is_closed (set.range f)) :
theorem is_closed_map_iff_closure_image {α : Type u_1} {β : Type u_2} {f : α β} :
(s : set α), closure (f '' s) f ''
theorem open_embedding_iff {α : Type u_1} {β : Type u_2} (f : α β) :
structure open_embedding {α : Type u_1} {β : Type u_2} (f : α β) :
Prop

An open embedding is an embedding with open image.

theorem open_embedding.is_open_map {α : Type u_1} {β : Type u_2} {f : α β} (hf : open_embedding f) :
theorem open_embedding.map_nhds_eq {α : Type u_1} {β : Type u_2} {f : α β} (hf : open_embedding f) (a : α) :
(nhds a) = nhds (f a)
theorem open_embedding.open_iff_image_open {α : Type u_1} {β : Type u_2} {f : α β} (hf : open_embedding f) {s : set α} :
is_open (f '' s)
theorem open_embedding.tendsto_nhds_iff {β : Type u_2} {γ : Type u_3} {ι : Type u_1} {f : ι β} {g : β γ} {a : filter ι} {b : β} (hg : open_embedding g) :
(nhds b) filter.tendsto (g f) a (nhds (g b))
theorem open_embedding.continuous {α : Type u_1} {β : Type u_2} {f : α β} (hf : open_embedding f) :
theorem open_embedding.open_iff_preimage_open {α : Type u_1} {β : Type u_2} {f : α β} (hf : open_embedding f) {s : set β} (hs : s ) :
theorem open_embedding_of_embedding_open {α : Type u_1} {β : Type u_2} {f : α β} (h₁ : embedding f) (h₂ : is_open_map f) :
theorem open_embedding_iff_embedding_open {α : Type u_1} {β : Type u_2} {f : α β} :
theorem open_embedding_of_continuous_injective_open {α : Type u_1} {β : Type u_2} {f : α β} (h₁ : continuous f) (h₂ : function.injective f) (h₃ : is_open_map f) :
theorem open_embedding_iff_continuous_injective_open {α : Type u_1} {β : Type u_2} {f : α β} :
theorem open_embedding_id {α : Type u_1}  :
theorem open_embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : open_embedding g) (hf : open_embedding f) :
theorem open_embedding.is_open_map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : open_embedding g) :
theorem open_embedding.of_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) {g : β γ} (hg : open_embedding g) :
theorem open_embedding.of_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) {g : β γ} (hg : open_embedding g) (h : open_embedding (g f)) :
structure closed_embedding {α : Type u_1} {β : Type u_2} (f : α β) :
Prop
• to_embedding :
• closed_range :

A closed embedding is an embedding with closed image.

theorem closed_embedding_iff {α : Type u_1} {β : Type u_2} (f : α β) :
theorem closed_embedding.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} {f : α β} {ι : Type u_3} {g : ι α} {a : filter ι} {b : α} (hf : closed_embedding f) :
(nhds b) filter.tendsto (f g) a (nhds (f b))
theorem closed_embedding.continuous {α : Type u_1} {β : Type u_2} {f : α β} (hf : closed_embedding f) :
theorem closed_embedding.is_closed_map {α : Type u_1} {β : Type u_2} {f : α β} (hf : closed_embedding f) :
theorem closed_embedding.closed_iff_image_closed {α : Type u_1} {β : Type u_2} {f : α β} (hf : closed_embedding f) {s : set α} :
theorem closed_embedding.closed_iff_preimage_closed {α : Type u_1} {β : Type u_2} {f : α β} (hf : closed_embedding f) {s : set β} (hs : s ) :
theorem closed_embedding_of_embedding_closed {α : Type u_1} {β : Type u_2} {f : α β} (h₁ : embedding f) (h₂ : is_closed_map f) :
theorem closed_embedding_of_continuous_injective_closed {α : Type u_1} {β : Type u_2} {f : α β} (h₁ : continuous f) (h₂ : function.injective f) (h₃ : is_closed_map f) :
theorem closed_embedding_id {α : Type u_1}  :
theorem closed_embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : closed_embedding g) (hf : closed_embedding f) :
theorem closed_embedding.closure_image_eq {α : Type u_1} {β : Type u_2} {f : α β} (hf : closed_embedding f) (s : set α) :
closure (f '' s) = f ''