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.

• Embedding: 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.

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 := ⋯ }

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

Equations

• instTopologicalSpaceSubtype = TopologicalSpace.induced Subtype.val t

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 := ⋯ }

structure RestrictGenTopology {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

theorem RestrictGenTopology.isOpen_of_forall_induced {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)} (self : RestrictGenTopology S) (u : Set X) : (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u

theorem 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

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

theorem IsInducing.eq_induced {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : IsInducing f) : tX = TopologicalSpace.induced f tY

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

@[deprecated IsInducing]

def Inducing {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop

Alias of IsInducing.

---

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.

Equations

• @Inducing = @IsInducing

theorem 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

structure IsEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) extends IsInducing : 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
• inj : Function.Injective f

  A topological embedding is injective.

theorem IsEmbedding.inj {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : IsEmbedding f) : Function.Injective f

A topological embedding is injective.

@[deprecated IsEmbedding]

def Embedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop

Alias of IsEmbedding.

---

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.

Equations

• @Embedding = @IsEmbedding

theorem 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)

structure IsOpenEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) extends IsEmbedding : Prop

An open embedding is an embedding with open range.

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

  The range of an open embedding is an open set.

theorem IsOpenEmbedding.isOpen_range {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : IsOpenEmbedding f) : IsOpen (Set.range f)

The range of an open embedding is an open set.

@[deprecated IsOpenEmbedding]

def OpenEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop

Alias of IsOpenEmbedding.

---

An open embedding is an embedding with open range.

Equations

• @OpenEmbedding = @IsOpenEmbedding

theorem 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)

structure IsClosedEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) extends IsEmbedding : Prop

A closed embedding is an embedding with closed image.

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

  The range of a closed embedding is a closed set.

theorem IsClosedEmbedding.isClosed_range {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : IsClosedEmbedding f) : IsClosed (Set.range f)

The range of a closed embedding is a closed set.

@[deprecated IsClosedEmbedding]

def ClosedEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop

Alias of IsClosedEmbedding.

---

A closed embedding is an embedding with closed image.

Equations

• @ClosedEmbedding = @IsClosedEmbedding

theorem 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

structure 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

theorem IsQuotientMap.surjective {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : IsQuotientMap f) : Function.Surjective f

theorem IsQuotientMap.eq_coinduced {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : IsQuotientMap f) : tY = TopologicalSpace.coinduced f tX

@[deprecated IsQuotientMap]

def QuotientMap {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop

Alias of IsQuotientMap.

---

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 = @IsQuotientMap