Documentation

Mathlib.Topology.Category.TopCat.Adjunctions

Adjunctions regarding the category of topological spaces #

This file shows that the forgetful functor from topological spaces to types has a left and right adjoint, given by TopCat.discrete, resp. TopCat.trivial, the functors which equip a type with the discrete, resp. trivial, topology.

Equipping a type with the discrete topology is left adjoint to the forgetful functor Top ⥤ Type.

Instances For

    Equipping a type with the trivial topology is right adjoint to the forgetful functor Top ⥤ Type.

    Instances For