# 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: 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.

• TopologicalSpace.coinduced: 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.

• Inducing: a map f : X → Y is called inducing, if the topology on the domain is equal to the induced topology.

• Embedding: a map f : X → Y is an embedding, if it is a topology inducing map and it is injective.

• OpenEmbedding: a map f : 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 map f : 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 map f : X → Y is a quotient map, if it is surjective and the topology on the codomain is equal to the coinduced topology.

def TopologicalSpace.induced {X : Type u_1} {Y : Type u_2} (f : XY) (t : ) :

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
• = { IsOpen := fun (s : Set X) => ∃ (t_1 : Set Y), IsOpen t_1 f ⁻¹' t_1 = s, isOpen_univ := , isOpen_inter := , isOpen_sUnion := }
Instances For
instance instTopologicalSpaceSubtype {X : Type u_1} {p : XProp} [t : ] :
Equations
def TopologicalSpace.coinduced {X : Type u_1} {Y : Type u_2} (f : XY) (t : ) :

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
• = { IsOpen := fun (s : Set Y) => IsOpen (f ⁻¹' s), isOpen_univ := , isOpen_inter := , isOpen_sUnion := }
Instances For
structure RestrictGenTopology {X : Type u_1} [tX : ] (S : Set (Set X)) :

We say that restrictions of the topology on X to sets from a family S generates the original topology, if either of the following equivalent conditions hold:

• a set which is relatively open in each s ∈ S is open;
• a set which is relatively closed in each s ∈ S is closed;
• for any topological space Y, a function f : X → Y is continuous provided that it is continuous on each s ∈ S.
• isOpen_of_forall_induced : ∀ (u : Set X), (∀ sS, IsOpen (Subtype.val ⁻¹' u))
Instances For
theorem RestrictGenTopology.isOpen_of_forall_induced {X : Type u_1} [tX : ] {S : Set (Set X)} (self : ) (u : Set X) :
(∀ sS, IsOpen (Subtype.val ⁻¹' u))
theorem inducing_iff {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] (f : XY) :
tX =
structure Inducing {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] (f : XY) :

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 =

The topology on the domain is equal to the induced topology.

Instances For
theorem Inducing.induced {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] {f : XY} (self : ) :
tX =

The topology on the domain is equal to the induced topology.

theorem embedding_iff {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :
structure Embedding {X : Type u_1} {Y : Type u_2} [] [] (f : XY) extends :

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.

Instances For
theorem Embedding.inj {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (self : ) :

A topological embedding is injective.

theorem openEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] (f : XY) :
structure OpenEmbedding {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] (f : XY) extends :

An open embedding is an embedding with open range.

• induced : tX =
• inj :
• isOpen_range : IsOpen (Set.range f)

The range of an open embedding is an open set.

Instances For
theorem OpenEmbedding.isOpen_range {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] {f : XY} (self : ) :

The range of an open embedding is an open set.

theorem closedEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] (f : XY) :
structure ClosedEmbedding {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] (f : XY) extends :

A closed embedding is an embedding with closed image.

• induced : tX =
• inj :
• isClosed_range :

The range of a closed embedding is a closed set.

Instances For
theorem ClosedEmbedding.isClosed_range {X : Type u_1} {Y : Type u_2} [tX : ] [tY : ] {f : XY} (self : ) :

The range of a closed embedding is a closed set.

theorem quotientMap_iff' {X : Type u_3} {Y : Type u_4} [tX : ] [tY : ] (f : XY) :
structure QuotientMap {X : Type u_3} {Y : Type u_4} [tX : ] [tY : ] (f : XY) :

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.

• surjective :
• eq_coinduced : tY =
Instances For
theorem QuotientMap.surjective {X : Type u_3} {Y : Type u_4} [tX : ] [tY : ] {f : XY} (self : ) :
theorem QuotientMap.eq_coinduced {X : Type u_3} {Y : Type u_4} [tX : ] [tY : ] {f : XY} (self : ) :
tY =