mathlib documentation

topology.category.Top.basic

Category instance for topological spaces #

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.

def Top  :
Type (u+1)

The category of topological spaces and continuous maps.

Equations
@[simp]
theorem Top.id_app (X : Top) (x : X) :
(𝟙 X) x = x
@[simp]
theorem Top.comp_app {X Y Z : Top} (f : X Y) (g : Y Z) (x : X) :
(f g) x = g (f x)
def Top.of (X : Type u) [topological_space X] :

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

Equations
@[instance]
Equations
@[simp]
theorem Top.coe_of (X : Type u) [topological_space X] :
(Top.of X) = X
def Top.discrete  :
Type u Top

The discrete topology on any type.

Equations
def Top.trivial  :
Type u Top

The trivial topology on any type.

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

Any homeomorphisms induces an isomorphism in Top.

Equations
@[simp]
theorem Top.iso_of_homeo_inv_to_fun {X Y : Top} (f : X ≃ₜ Y) (ᾰ : Y) :
((Top.iso_of_homeo f).inv) = (f.symm) ᾰ
@[simp]
theorem Top.iso_of_homeo_hom_to_fun {X Y : Top} (f : X ≃ₜ Y) (ᾰ : X) :
((Top.iso_of_homeo f).hom) = f ᾰ
@[simp]
theorem Top.homeo_of_iso_apply {X Y : Top} (f : X Y) (ᾰ : X) :
(Top.homeo_of_iso f) = (f.hom) ᾰ
def Top.homeo_of_iso {X Y : Top} (f : X Y) :

Any isomorphism in Top induces a homeomorphism.

Equations
@[simp]
theorem Top.homeo_of_iso_symm_apply {X Y : Top} (f : X Y) (ᾰ : Y) :
((Top.homeo_of_iso f).symm) = (f.inv) ᾰ
@[simp]
@[simp]
theorem Top.of_homeo_of_iso {X Y : Top} (f : X Y) :