Equipping a type with the discrete topology is left adjoint to the forgetful functor Top ⥤ Type.
Equations
- Top.adj₁ = {hom_equiv := λ (X : Type u) (Y : Top), {to_fun := λ (f : Top.discrete.obj X ⟶ Y), ⇑f, inv_fun := λ (f : X ⟶ (category_theory.forget Top).obj Y), {to_fun := f, continuous_to_fun := _}, left_inv := _, right_inv := _}, unit := {app := λ (X : Type u), id, naturality' := Top.adj₁._proof_4}, counit := {app := λ (X : Top), {to_fun := id ↥((category_theory.forget Top ⋙ Top.discrete).obj X), continuous_to_fun := _}, naturality' := Top.adj₁._proof_6}, hom_equiv_unit' := Top.adj₁._proof_7, hom_equiv_counit' := Top.adj₁._proof_8}
Equipping a type with the trivial topology is right adjoint to the forgetful functor Top ⥤ Type.
Equations
- Top.adj₂ = {hom_equiv := λ (X : Top) (Y : Type u), {to_fun := λ (f : (category_theory.forget Top).obj X ⟶ Y), {to_fun := f, continuous_to_fun := _}, inv_fun := λ (f : X ⟶ Top.trivial.obj Y), ⇑f, left_inv := _, right_inv := _}, unit := {app := λ (X : Top), {to_fun := id ↥((𝟭 Top).obj X), continuous_to_fun := _}, naturality' := Top.adj₂._proof_5}, counit := {app := λ (X : Type u), id, naturality' := Top.adj₂._proof_6}, hom_equiv_unit' := Top.adj₂._proof_7, hom_equiv_counit' := Top.adj₂._proof_8}