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.

source

@[simp]

theorem TopCat.adj₁_counit :

TopCat.adj₁.counit = CategoryTheory.NatTrans.mk fun X => ContinuousMap.mk id

source

@[simp]

theorem TopCat.adj₁_unit :

TopCat.adj₁.unit = CategoryTheory.NatTrans.mk fun X => id

source

def TopCat.adj₁ :

TopCat.discrete ⊣ CategoryTheory.forget TopCat

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

Instances For

source

@[simp]

theorem TopCat.adj₂_counit :

TopCat.adj₂.counit = CategoryTheory.NatTrans.mk fun X => id

source

@[simp]

theorem TopCat.adj₂_unit :

TopCat.adj₂.unit = CategoryTheory.NatTrans.mk fun X => ContinuousMap.mk id

source

def TopCat.adj₂ :

CategoryTheory.forget TopCat ⊣ TopCat.trivial

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

Instances For

source

instance TopCat.instIsRightAdjointTypeTypesTopCatInstTopCatLargeCategoryForgetConcreteCategory :

CategoryTheory.IsRightAdjoint (CategoryTheory.forget TopCat)

source

instance TopCat.instIsLeftAdjointTopCatInstTopCatLargeCategoryTypeTypesForgetConcreteCategory :

CategoryTheory.IsLeftAdjoint (CategoryTheory.forget TopCat)