Induced and coinduced topologies #
In this file we define the induced and coinduced topologies, as well as topology inducing maps, topological embeddings, and quotient maps.
Main definitions #

TopologicalSpace.induced
: givenf : X → Y
and a topology onY
, the induced topology onX
is the collection of sets that are preimages of some open set inY
. This is the coarsest topology that makesf
continuous. 
TopologicalSpace.coinduced
: givenf : X → Y
and a topology onX
, the coinduced topology onY
is defined such thats : Set Y
is open if the preimage ofs
is open. This is the finest topology that makesf
continuous. 
Inducing
: a mapf : X → Y
is called inducing, if the topology on the domain is equal to the induced topology. 
Embedding
: a mapf : X → Y
is an embedding, if it is a topology inducing map and it is injective. 
OpenEmbedding
: a mapf : X → Y
is an open embedding, if it is an embedding and its range is open. An open embedding is an open map. 
ClosedEmbedding
: a mapf : X → Y
is an open embedding, if it is an embedding and its range is open. An open embedding is an open map. 
QuotientMap
: a mapf : X → Y
is a quotient map, if it is surjective and the topology on the codomain is equal to the coinduced topology.
Given f : X → Y
and a topology on Y
,
the induced topology on X
is the collection of sets
that are preimages of some open set in Y
.
This is the coarsest topology that makes f
continuous.
Equations
Instances For
Given f : X → Y
and a topology on X
,
the coinduced topology on Y
is defined such that
s : Set Y
is open if the preimage of s
is open.
This is the finest topology that makes f
continuous.
Equations
 TopologicalSpace.coinduced f t = { IsOpen := fun (s : Set Y) => IsOpen (f ⁻¹' s), isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }
Instances For
A function f : X → Y
between topological spaces is inducing if the topology on X
is induced
by the topology on Y
through f
, meaning that a set s : Set X
is open iff it is the preimage
under f
of some open set t : Set Y
.
 induced : tX = TopologicalSpace.induced f tY
The topology on the domain is equal to the induced topology.
Instances For
A function between topological spaces is an embedding if it is injective,
and for all s : Set X
, s
is open iff it is the preimage of an open set.
 induced : inst✝¹ = TopologicalSpace.induced f inst✝
 inj : Function.Injective f
A topological embedding is injective.
Instances For
An open embedding is an embedding with open range.
 induced : tX = TopologicalSpace.induced f tY
 inj : Function.Injective f
The range of an open embedding is an open set.
Instances For
A closed embedding is an embedding with closed image.
 induced : tX = TopologicalSpace.induced f tY
 inj : Function.Injective f
The range of a closed embedding is a closed set.
Instances For
A function between topological spaces is a quotient map if it is surjective,
and for all s : Set Y
, s
is open iff its preimage is an open set.
Equations
 QuotientMap f = (Function.Surjective f ∧ tY = TopologicalSpace.coinduced f tX)