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
    Instances For
      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
          Instances For
            structure Topology.IsCoherentWith {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.
            Instances For
              @[deprecated Topology.IsCoherentWith (since := "2025-04-08")]
              def Topology.RestrictGenTopology {X : Type u_1} [tX : TopologicalSpace X] (S : Set (Set X)) :

              Alias of Topology.IsCoherentWith.


              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.
              Equations
                Instances For
                  structure Topology.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.

                  Instances For
                    theorem Topology.isInducing_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :
                    @[deprecated Topology.IsInducing (since := "2024-10-28")]
                    def Topology.Inducing {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :

                    Alias of Topology.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
                      Instances For
                        structure Topology.IsEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) extends Topology.IsInducing f :

                        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
                          @[deprecated Topology.IsEmbedding (since := "2024-10-26")]
                          def Topology.Embedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :

                          Alias of Topology.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
                            Instances For
                              structure Topology.IsOpenEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) extends Topology.IsEmbedding f :

                              An open embedding is an embedding with open range.

                              Instances For
                                structure Topology.IsClosedEmbedding {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) extends Topology.IsEmbedding f :

                                A closed embedding is an embedding with closed image.

                                Instances For
                                  structure Topology.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.

                                  Instances For
                                    @[deprecated Topology.IsQuotientMap (since := "2024-10-22")]
                                    def Topology.QuotientMap {X : Type u_3} {Y : Type u_4} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : XY) :

                                    Alias of Topology.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
                                      Instances For