Documentation

Mathlib.Topology.Defs.Induced

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 #

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

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
Equations
def TopologicalSpace.coinduced {X : Type u_1} {Y : Type u_2} (f : XY) (t : TopologicalSpace X) :

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
structure RestrictGenTopology {X : Type u_1} [tX : TopologicalSpace X] (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.
theorem RestrictGenTopology.isOpen_of_forall_induced {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)} (self : RestrictGenTopology S) (u : Set X) :
(∀ sS, IsOpen (Subtype.val ⁻¹' u))IsOpen u
theorem isInducing_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :
structure IsInducing {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (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.

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

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 : XY) :

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
theorem isEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :
structure IsEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) extends IsInducing :

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.

theorem IsEmbedding.inj {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : XY} (self : IsEmbedding 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 : XY) :

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
theorem isOpenEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :
structure IsOpenEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) extends IsEmbedding :

An open embedding is an embedding with open range.

theorem IsOpenEmbedding.isOpen_range {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : XY} (self : IsOpenEmbedding 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 : XY) :

Alias of IsOpenEmbedding.


An open embedding is an embedding with open range.

Equations
theorem isClosedEmbedding_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :
structure IsClosedEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) extends IsEmbedding :

A closed embedding is an embedding with closed image.

theorem IsClosedEmbedding.isClosed_range {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : XY} (self : IsClosedEmbedding 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 : XY) :

Alias of IsClosedEmbedding.


A closed embedding is an embedding with closed image.

Equations
structure IsQuotientMap {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (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.

theorem IsQuotientMap.surjective {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : XY} (self : IsQuotientMap f) :
theorem IsQuotientMap.eq_coinduced {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : XY} (self : IsQuotientMap f) :
@[deprecated IsQuotientMap]
def QuotientMap {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :

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