# mathlibdocumentation

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
Instances for Top
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def Top.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
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)  :

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

Equations
@[protected, instance]
def Top.topological_space (X : Top) :
Equations
@[simp]
theorem Top.coe_of (X : Type u)  :
(Top.of X) = X
@[protected, instance]
Equations
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_hom_apply {X Y : Top} (f : X ≃ₜ Y) (ᾰ : X) :
((Top.iso_of_homeo f).hom) = f ᾰ
@[simp]
theorem Top.iso_of_homeo_inv_apply {X Y : Top} (f : X ≃ₜ Y) (ᾰ : Y) :
((Top.iso_of_homeo f).inv) = (f.symm) ᾰ
@[simp]
theorem Top.homeo_of_iso_apply {X Y : Top} (f : X Y) (ᾰ : X) :
= (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]
theorem Top.of_iso_of_homeo {X Y : Top} (f : X ≃ₜ Y) :
@[simp]
theorem Top.of_homeo_of_iso {X Y : Top} (f : X Y) :
@[simp]
theorem Top.open_embedding_iff_comp_is_iso {X Y Z : Top} (f : X Y) (g : Y Z)  :
@[simp]
theorem Top.open_embedding_iff_is_iso_comp {X Y Z : Top} (f : X Y) (g : Y Z)  :