Documentation

Mathlib.Topology.Category.TopCat.Adjunctions

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 = { app := fun (X : TopCat) => { toFun := id, continuous_toFun := ⋯ }, naturality := TopCat.adj₁.proof_3 }
source
@[simp]
theorem TopCat.adj₁_unit :
TopCat.adj₁.unit = { app := fun (X : Type u) => id, naturality := TopCat.adj₁.proof_1 }
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TopCat.adj₂_counit :
    TopCat.adj₂.counit = { app := fun (X : Type u) => id, naturality := TopCat.adj₂.proof_3 }
    source
    @[simp]
    theorem TopCat.adj₂_unit :
    TopCat.adj₂.unit = { app := fun (X : TopCat) => { toFun := id, continuous_toFun := ⋯ }, naturality := TopCat.adj₂.proof_2 }
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance TopCat.instIsRightAdjointTypeTypesTopCatInstTopCatLargeCategoryForgetConcreteCategory :
      CategoryTheory.IsRightAdjoint (CategoryTheory.forget TopCat)
      Equations
      source
      instance TopCat.instIsLeftAdjointTopCatInstTopCatLargeCategoryTypeTypesForgetConcreteCategory :
      CategoryTheory.IsLeftAdjoint (CategoryTheory.forget TopCat)
      Equations