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