Mathlib.Topology.Defs.Induced

Module docstring

{"# 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. "}

TopologicalSpace.induced definition

(f : X → Y) (t : TopologicalSpace Y) : TopologicalSpace X

Full source

/-- 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. -/
def induced (f : X → Y) (t : TopologicalSpace Y) : TopologicalSpace X where
  IsOpen s := ∃ t, IsOpen t ∧ f ⁻¹' t = s
  isOpen_univ := ⟨univ, isOpen_univ, preimage_univ⟩
  isOpen_inter := by
    rintro s₁ s₂ ⟨s'₁, hs₁, rfl⟩ ⟨s'₂, hs₂, rfl⟩
    exact ⟨s'₁ ∩ s'₂, hs₁.inter hs₂, preimage_inter⟩
  isOpen_sUnion S h := by
    choose! g hgo hfg using h
    refine ⟨⋃₀ (g '' S), isOpen_sUnion <| forall_mem_image.2 hgo, ?_⟩
    rw [preimage_sUnion, biUnion_image, sUnion_eq_biUnion]
    exact iUnion₂_congr hfg

Induced Topology

Informal description

Given a function $ f : X \to Y $ and a topological space structure $ t $ on $ Y $, the *induced topology* on $ X $ is the topology where a subset $ s \subseteq X $ is open if and only if it is the preimage $ f^{-1}(t) $ of some open subset $ t \subseteq Y $. This is the coarsest topology on $ X $ that makes $ f $ continuous.

instTopologicalSpaceSubtype instance

{p : X → Prop} [t : TopologicalSpace X] : TopologicalSpace (Subtype p)

Full source

instance _root_.instTopologicalSpaceSubtype {p : X → Prop} [t : TopologicalSpace X] :
    TopologicalSpace (Subtype p) :=
  induced (↑) t

Subtype Topology Inheritance

Informal description

For any topological space $X$ and predicate $p : X \to \text{Prop}$, the subtype $\{x \in X \mid p(x)\}$ inherits a topological space structure from $X$, where a subset is open if and only if it is the intersection of an open set in $X$ with the subtype.

TopologicalSpace.coinduced definition

(f : X → Y) (t : TopologicalSpace X) : TopologicalSpace Y

Full source

/-- 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. -/
def coinduced (f : X → Y) (t : TopologicalSpace X) : TopologicalSpace Y where
  IsOpen s := IsOpen (f ⁻¹' s)
  isOpen_univ := t.isOpen_univ
  isOpen_inter _ _ h₁ h₂ := h₁.inter h₂
  isOpen_sUnion s h := by simpa only [preimage_sUnion] using isOpen_biUnion h

Coinduced topology

Informal description

Given a function $ f : X \to Y $ and a topological space structure $ t $ on $ X $, the *coinduced topology* on $ Y $ is the topology where a subset $ s \subseteq Y $ is open if and only if its preimage $ f^{-1}(s) $ is open in $ X $. This is the finest topology on $ Y $ that makes $ f $ continuous.

Topology.IsCoherentWith structure

(S : Set (Set X))

Full source

/-- 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`.
-/
structure IsCoherentWith (S : Set (Set X)) : Prop where
  isOpen_of_forall_induced (u : Set X) : (∀ s ∈ S, IsOpen ((↑) ⁻¹' u : Set s)) → IsOpen u

Topology generated by a family of subsets

Informal description

A family of subsets $S$ of a topological space $X$ is said to *generate the topology* on $X$ if any of the following equivalent conditions hold: 1. A subset that is relatively open in each $s \in S$ is open in $X$; 2. A subset that is relatively closed in each $s \in S$ is closed in $X$; 3. For any topological space $Y$, a function $f : X \to Y$ is continuous if and only if its restriction to each $s \in S$ is continuous.

Topology.IsInducing structure

(f : X → Y)

Full source

/-- 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`. -/
@[mk_iff]
structure IsInducing (f : X → Y) : Prop where
  /-- The topology on the domain is equal to the induced topology. -/
  eq_induced : tX = tY.induced f

Inducing map between topological spaces

Informal description

A function $ f : X \to Y $ between topological spaces is called *inducing* if the topology on $ X $ is the induced topology from $ Y $ via $ f $. This means that a subset $ s \subseteq X $ is open if and only if there exists an open subset $ t \subseteq Y $ such that $ s = f^{-1}(t) $.

Topology.IsEmbedding structure

(f : X → Y) : Prop extends IsInducing f

Full source

/-- 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. -/
@[mk_iff]
structure IsEmbedding (f : X → Y) : Prop extends IsInducing f where
  /-- A topological embedding is injective. -/
  injective : Function.Injective f

Topological embedding

Informal description

A function $ f : X \to Y $ between topological spaces is called a *topological embedding* if it is injective and the topology on $ X $ is the coarsest topology that makes $ f $ continuous. Equivalently, for any subset $ s \subseteq X $, $ s $ is open in $ X $ if and only if it is the preimage of some open set in $ Y $ under $ f $.

Topology.IsOpenEmbedding structure

(f : X → Y) : Prop extends IsEmbedding f

Full source

/-- An open embedding is an embedding with open range. -/
@[mk_iff]
structure IsOpenEmbedding (f : X → Y) : Prop extends IsEmbedding f where
  /-- The range of an open embedding is an open set. -/
  isOpen_range : IsOpen <| range f

Open Embedding

Informal description

A function $f : X \to Y$ between topological spaces is called an *open embedding* if it is an embedding (i.e., it is injective and the topology on $X$ is induced by $f$) and its range $f(X)$ is an open subset of $Y$. An open embedding is also an open map.

Topology.IsClosedEmbedding structure

(f : X → Y) : Prop extends IsEmbedding f

Full source

/-- A closed embedding is an embedding with closed image. -/
@[mk_iff]
structure IsClosedEmbedding (f : X → Y) : Prop extends IsEmbedding f where
  /-- The range of a closed embedding is a closed set. -/
  isClosed_range : IsClosed <| range f

Closed embedding

Informal description

A closed embedding is an injective continuous map $ f : X \to Y $ between topological spaces where the topology on $ X $ is induced by $ f $ from the topology on $ Y $, and the image of $ f $ is a closed subset of $ Y $.

Topology.IsQuotientMap structure

{X : Type*} {Y : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y)

Full source

/-- 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. -/
@[mk_iff isQuotientMap_iff']
structure IsQuotientMap {X : Type*} {Y : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y]
    (f : X → Y) : Prop where
  surjective : Function.Surjective f
  eq_coinduced : tY = tX.coinduced f

Quotient Map

Informal description

A function $ f : X \to Y $ between topological spaces is called a *quotient map* if it is surjective, and for any subset $ s \subseteq Y $, $ s $ is open in $ Y $ if and only if its preimage $ f^{-1}(s) $ is open in $ X $. This means the topology on $ Y $ is the coinduced topology from $ f $, making $ f $ a quotient map.