Documentation

Mathlib.CategoryTheory.Bicategory.Adjunction.Cat

Adjunctions in Cat #

We show that adjunctions in the bicategory Cat correspond to adjunctions between functors in the usual categorical sense.

source
def CategoryTheory.Adjunction.toCat {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
Bicategory.Adjunction F.toCatHom G.toCatHom

The adjunction in the bicategorical sense attached to an adjunction between functors.

Equations
  • adj.toCat = { unit := { toNatTrans := adj.unit }, counit := { toNatTrans := adj.counit }, left_triangle := ⋯, right_triangle := ⋯ }
Instances For
    source
    @[simp]
    theorem CategoryTheory.Adjunction.toCat_unit_toNatTrans {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
    adj.toCat.unit.toNatTrans = adj.unit
    source
    @[simp]
    theorem CategoryTheory.Adjunction.toCat_counit_toNatTrans {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
    adj.toCat.counit.toNatTrans = adj.counit
    source
    def CategoryTheory.Adjunction.ofCat {C D : Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : Bicategory.Adjunction F G) :
    F.toFunctor ⊣ G.toFunctor

    The adjunction of functors corresponding to an adjunction in the bicategory Cat.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Adjunction.ofCat_unit {C D : Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : Bicategory.Adjunction F G) :
      (ofCat adj).unit = adj.unit.toNatTrans
      source
      @[simp]
      theorem CategoryTheory.Adjunction.ofCat_counit {C D : Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : Bicategory.Adjunction F G) :
      (ofCat adj).counit = adj.counit.toNatTrans
      source
      @[simp]
      theorem CategoryTheory.Adjunction.toCat_ofCat {C D : Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : Bicategory.Adjunction F G) :
      (ofCat adj).toCat = adj
      source
      @[simp]
      theorem CategoryTheory.Adjunction.ofCat_toCat {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
      ofCat adj.toCat = adj
      source
      theorem CategoryTheory.Adjunction.toCat_comp_toCat {C D E : Type u} [Category.{v, u} C] [Category.{v, u} D] [Category.{v, u} E] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {F' : Functor D E} {G' : Functor E D} (adj' : F' ⊣ G') :
      adj.toCat.comp adj'.toCat = (adj.comp adj').toCat
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Adjunction.ofCat_id (C : Cat) :
      Adjunction.ofCat (id C) = CategoryTheory.Adjunction.id
      source
      theorem CategoryTheory.Bicategory.Adjunction.ofCat_comp {C D E : Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : Adjunction F G) {F' : D ⟶ E} {G' : E ⟶ D} (adj' : Adjunction F' G') :
      Adjunction.ofCat (adj.comp adj') = (Adjunction.ofCat adj).comp (Adjunction.ofCat adj')
      source
      theorem CategoryTheory.Bicategory.toNatTrans_mateEquiv {C D E F : Cat} {G : C ⟶ E} {H : D ⟶ F} {L₁ : C ⟶ D} {R₁ : D ⟶ C} {L₂ : E ⟶ F} {R₂ : F ⟶ E} (adj₁ : Adjunction L₁ R₁) (adj₂ : Adjunction L₂ R₂) (f : CategoryStruct.comp G L₂ ⟶ CategoryStruct.comp L₁ H) :
      ((mateEquiv adj₁ adj₂) f).toNatTrans = (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans
      source
      theorem CategoryTheory.Bicategory.toNatTrans_conjugateEquiv {C D : Cat} {L₁ L₂ : C ⟶ D} {R₁ R₂ : D ⟶ C} (adj₁ : Adjunction L₁ R₁) (adj₂ : Adjunction L₂ R₂) (f : L₂ ⟶ L₁) :
      ((conjugateEquiv adj₁ adj₂) f).toNatTrans = (CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂)) f.toNatTrans