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
🔸 coverage
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
    Instances For
      source
      📐 coverage
      @[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
      📐 coverage
      @[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
      🔸 coverage
      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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          @[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
          📐 coverage
          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
          📐 coverage
          @[simp]
          theorem CategoryTheory.Bicategory.Adjunction.ofCat_id (C : Cat) :
          Adjunction.ofCat (id C) = CategoryTheory.Adjunction.id
          source
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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