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.

def TopCat.adj₁ : discrete ⊣ CategoryTheory.forget TopCat

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.adj₁_unit : adj₁.unit = { app := fun (x : Type u) => id, naturality := adj₁.proof_1 }

@[simp]

theorem TopCat.adj₁_counit : adj₁.counit = { app := fun (X : TopCat) => ofHom { toFun := id, continuous_toFun := ⋯ }, naturality := adj₁.proof_3 }

def TopCat.adj₂ : CategoryTheory.forget TopCat ⊣ trivial

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.adj₂_unit : adj₂.unit = { app := fun (X : TopCat) => ofHom { toFun := id, continuous_toFun := ⋯ }, naturality := adj₂.proof_2 }

@[simp]

theorem TopCat.adj₂_counit : adj₂.counit = { app := fun (x : Type u) => id, naturality := adj₂.proof_3 }

instance TopCat.instIsRightAdjointForget : (CategoryTheory.forget TopCat).IsRightAdjoint

instance TopCat.instIsLeftAdjointForget : (CategoryTheory.forget TopCat).IsLeftAdjoint