mathlib documentation


Adjunctions regarding the category of topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file shows that the forgetful functor from topological spaces to types has a left and right adjoint, given by Top.discrete, resp. Top.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.

theorem Top.adj₁_unit  :
Top.adj₁.unit = {app := id, naturality' := Top.adj₁._proof_1}
theorem Top.adj₁_counit  :
Top.adj₁.counit = {app := λ (X : Top), {to_fun := id (Top.discrete.obj X), continuous_to_fun := _}, naturality' := Top.adj₁._proof_3}
theorem Top.adj₂_counit  :
Top.adj₂.counit = {app := λ (X : Type u), id, naturality' := Top.adj₂._proof_3}
theorem Top.adj₂_unit  :
Top.adj₂.unit = {app := λ (X : Top), {to_fun := id X, continuous_to_fun := _}, naturality' := Top.adj₂._proof_2}

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