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

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

- `IsEmbedding`: a map `f : X → Y` is an embedding, if it is a topology inducing map and it is injective.

- `IsOpenEmbedding`: 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.

- `IsClosedEmbedding`: 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.

- `IsQuotientMap`: 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.

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

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

- TopologicalSpace.induced f t = { IsOpen := fun (s : Set X) => ∃ (t_1 : Set Y), IsOpen t_1 ∧ f ⁻¹' t_1 = s, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

Instances For

source
instance instTopologicalSpaceSubtype {X : Type u_1} {p : X → Prop} [t : TopologicalSpace X] :
TopologicalSpace (Subtype p)
Equations

- instTopologicalSpaceSubtype = TopologicalSpace.induced Subtype.val t

source
def TopologicalSpace.coinduced {X : Type u_1} {Y : Type u_2} (f : X → Y) (t : TopologicalSpace X) :
TopologicalSpace Y

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

source
structure Topology.IsCoherentWith {X : Type u_1} [tX : TopologicalSpace X] (S : Set (Set X)) :
Prop

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) : (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u

Instances For

source
structure Topology.IsInducing {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) :
Prop

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

- eq_induced : tX = TopologicalSpace.induced f tY

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

Instances For

source
theorem Topology.isInducing_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) :
IsInducing f ↔ tX = TopologicalSpace.induced f tY
source
structure Topology.IsEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) extends Topology.IsInducing f :
Prop

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.

- eq_induced : tX = TopologicalSpace.induced f tY
- injective : Function.Injective f

  A topological embedding is injective.

Instances For

source
theorem Topology.isEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) :
IsEmbedding f ↔ IsInducing f ∧ Function.Injective f
source
structure Topology.IsOpenEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) extends Topology.IsEmbedding f :
Prop

An open embedding is an embedding with open range.

- eq_induced : tX = TopologicalSpace.induced f tY
- injective : Function.Injective f
- isOpen_range : IsOpen (Set.range f)

  The range of an open embedding is an open set.

Instances For

source
theorem Topology.isOpenEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) :
IsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpen (Set.range f)
source
structure Topology.IsClosedEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) extends Topology.IsEmbedding f :
Prop

A closed embedding is an embedding with closed image.

- eq_induced : tX = TopologicalSpace.induced f tY
- injective : Function.Injective f
- isClosed_range : IsClosed (Set.range f)

  The range of a closed embedding is a closed set.

Instances For

source
theorem Topology.isClosedEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) :
IsClosedEmbedding f ↔ IsEmbedding f ∧ IsClosed (Set.range f)
source
structure Topology.IsQuotientMap {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) :
Prop

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 : Function.Surjective f
- eq_coinduced : tY = TopologicalSpace.coinduced f tX

Instances For

source
theorem Topology.isQuotientMap_iff' {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) :
IsQuotientMap f ↔ Function.Surjective f ∧ tY = TopologicalSpace.coinduced f tX