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.
Equations
- Top.adj₁ = category_theory.adjunction.mk_of_unit_counit {unit := {app := λ (X : Type u), id, naturality' := Top.adj₁._proof_1}, counit := {app := λ (X : Top), {to_fun := id ↥((category_theory.forget Top ⋙ Top.discrete).obj X), continuous_to_fun := _}, naturality' := Top.adj₁._proof_3}, left_triangle' := Top.adj₁._proof_4, right_triangle' := Top.adj₁._proof_5}
@[simp]
@[simp]
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}
@[simp]
@[simp]
Equipping a type with the trivial topology is right adjoint to the forgetful functor
Top ⥤ Type.
Equations
- Top.adj₂ = category_theory.adjunction.mk_of_unit_counit {unit := {app := λ (X : Top), {to_fun := id ↥((𝟭 Top).obj X), continuous_to_fun := _}, naturality' := Top.adj₂._proof_2}, counit := {app := λ (X : Type u), id, naturality' := Top.adj₂._proof_3}, left_triangle' := Top.adj₂._proof_4, right_triangle' := Top.adj₂._proof_5}