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