mathlib3 documentation

topology.category.Top.basic

Category instance for topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce the bundled category Top of topological spaces together with the functors discrete and trivial from the category of types to Top which equip a type with the corresponding discrete, resp. trivial, topology. For a proof that these functors are left, resp. right adjoint to the forgetful functor, see topology.category.Top.adjunctions.

source
def Top  :
Type (u+1)

The category of topological spaces and continuous maps.

Equations
Instances for Top
source
@[protected, instance]
def Top.bundled_hom  :
category_theory.bundled_hom continuous_map
Equations
source
@[protected, instance]
def Top.concrete_category  :
category_theory.concrete_category Top
source
@[protected, instance]
def Top.large_category  :
category_theory.large_category Top
source
@[protected, instance]
def Top.has_coe_to_sort  :
has_coe_to_sort Top (Type u_1)
Equations
source
@[protected, instance]
def Top.topological_space_unbundled (x : Top) :
topological_space ↥x
Equations
source
@[simp]
theorem Top.id_app (X : Top) (x : ↥X) :
⇑(𝟙 X) x = x
source
@[simp]
theorem Top.comp_app {X Y Z : Top} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) :
⇑(f ≫ g) x = ⇑g (⇑f x)
source
def Top.of (X : Type u) [topological_space X] :
Top

Construct a bundled Top from the underlying type and the typeclass.

Equations
Instances for ↥Top.of
source
@[protected, instance]
def Top.topological_space (X : Top) :
topological_space ↥X
Equations
source
@[simp]
theorem Top.coe_of (X : Type u) [topological_space X] :
↥(Top.of X) = X
source
@[protected, instance]
def Top.inhabited  :
inhabited Top
Equations
source
def Top.discrete  :
Type u ⥤ Top

The discrete topology on any type.

Equations
source
@[protected, instance]
def Top.obj.discrete_topology {X : Type u} :
discrete_topology ↥(Top.discrete.obj X)
source
def Top.trivial  :
Type u ⥤ Top

The trivial topology on any type.

Equations
source
def Top.iso_of_homeo {X Y : Top} (f : ↥X ≃ₜ ↥Y) :
X ≅ Y

Any homeomorphisms induces an isomorphism in Top.

Equations
source
@[simp]
theorem Top.iso_of_homeo_hom_apply {X Y : Top} (f : ↥X ≃ₜ ↥Y) (ᾰ : ↥X) :
⇑((Top.iso_of_homeo f).hom) ᾰ = ⇑f ᾰ
source
@[simp]
theorem Top.iso_of_homeo_inv_apply {X Y : Top} (f : ↥X ≃ₜ ↥Y) (ᾰ : ↥Y) :
⇑((Top.iso_of_homeo f).inv) ᾰ = ⇑(f.symm) ᾰ
source
@[simp]
theorem Top.homeo_of_iso_apply {X Y : Top} (f : X ≅ Y) (ᾰ : ↥X) :
⇑(Top.homeo_of_iso f) ᾰ = ⇑(f.hom) ᾰ
source
def Top.homeo_of_iso {X Y : Top} (f : X ≅ Y) :
↥X ≃ₜ ↥Y

Any isomorphism in Top induces a homeomorphism.

Equations
source
@[simp]
theorem Top.homeo_of_iso_symm_apply {X Y : Top} (f : X ≅ Y) (ᾰ : ↥Y) :
⇑((Top.homeo_of_iso f).symm) ᾰ = ⇑(f.inv) ᾰ
source
@[simp]
theorem Top.of_iso_of_homeo {X Y : Top} (f : ↥X ≃ₜ ↥Y) :
Top.homeo_of_iso (Top.iso_of_homeo f) = f
source
@[simp]
theorem Top.of_homeo_of_iso {X Y : Top} (f : X ≅ Y) :
Top.iso_of_homeo (Top.homeo_of_iso f) = f
source
@[simp]
theorem Top.open_embedding_iff_comp_is_iso {X Y Z : Top} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso g] :
open_embedding ⇑(f ≫ g) ↔ open_embedding ⇑f
source
@[simp]
theorem Top.open_embedding_iff_is_iso_comp {X Y Z : Top} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.is_iso f] :
open_embedding ⇑(f ≫ g) ↔ open_embedding ⇑g