Adjunctions in Cat

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

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.

@[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

@[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

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.

@[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

@[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

@[simp]

theorem CategoryTheory.Adjunction.toCat_ofCat {C D : Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : Bicategory.Adjunction F G) : (ofCat adj).toCat = adj

@[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

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

@[simp]

theorem CategoryTheory.Bicategory.Adjunction.ofCat_id (C : Cat) : Adjunction.ofCat (id C) = CategoryTheory.Adjunction.id

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')

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

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

@[simp]

theorem CategoryTheory.Bicategory.Adj.left_triangle_components {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) (X : ↑C₁.obj) : CategoryStruct.comp (α.l.toFunctor.map (α.adj.unit.toNatTrans.app X)) (α.adj.counit.toNatTrans.app (α.l.toFunctor.obj X)) = CategoryStruct.id (α.l.toFunctor.obj X)

@[simp]

theorem CategoryTheory.Bicategory.Adj.left_triangle_components_assoc {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) (X : ↑C₁.obj) {Z : ↑C₂.obj} (h : (CategoryStruct.id C₂.obj).toFunctor.obj (α.l.toFunctor.obj X) ⟶ Z) : CategoryStruct.comp (α.l.toFunctor.map (α.adj.unit.toNatTrans.app X)) (CategoryStruct.comp (α.adj.counit.toNatTrans.app (α.l.toFunctor.obj X)) h) = CategoryStruct.comp (CategoryStruct.id (α.l.toFunctor.obj X)) h

@[simp]

theorem CategoryTheory.Bicategory.Adj.right_triangle_components {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) (X : ↑C₂.obj) : CategoryStruct.comp (α.adj.unit.toNatTrans.app (α.r.toFunctor.obj X)) (α.r.toFunctor.map (α.adj.counit.toNatTrans.app X)) = CategoryStruct.id (α.r.toFunctor.obj X)

@[simp]

theorem CategoryTheory.Bicategory.Adj.right_triangle_components_assoc {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) (X : ↑C₂.obj) {Z : ↑C₁.obj} (h : α.r.toFunctor.obj ((CategoryStruct.id C₂.obj).toFunctor.obj X) ⟶ Z) : CategoryStruct.comp (α.adj.unit.toNatTrans.app (α.r.toFunctor.obj X)) (CategoryStruct.comp (α.r.toFunctor.map (α.adj.counit.toNatTrans.app X)) h) = CategoryStruct.comp (CategoryStruct.id (α.r.toFunctor.obj X)) h

@[simp]

theorem CategoryTheory.Bicategory.Adj.unit_naturality {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₁.obj} (f : X ⟶ Y) : CategoryStruct.comp (α.adj.unit.toNatTrans.app X) (α.r.toFunctor.map (α.l.toFunctor.map f)) = CategoryStruct.comp f (α.adj.unit.toNatTrans.app Y)

@[simp]

theorem CategoryTheory.Bicategory.Adj.unit_naturality_assoc {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₁.obj} (f : X ⟶ Y) {Z : ↑C₁.obj} (h : α.r.toFunctor.obj (α.l.toFunctor.obj Y) ⟶ Z) : CategoryStruct.comp (α.adj.unit.toNatTrans.app X) (CategoryStruct.comp (α.r.toFunctor.map (α.l.toFunctor.map f)) h) = CategoryStruct.comp (CategoryStruct.comp f (α.adj.unit.toNatTrans.app Y)) h

@[simp]

theorem CategoryTheory.Bicategory.Adj.counit_naturality {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₂.obj} (f : X ⟶ Y) : CategoryStruct.comp (α.l.toFunctor.map (α.r.toFunctor.map f)) (α.adj.counit.toNatTrans.app Y) = CategoryStruct.comp (α.adj.counit.toNatTrans.app X) f

@[simp]

theorem CategoryTheory.Bicategory.Adj.counit_naturality_assoc {C₁ C₂ : Adj Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₂.obj} (f : X ⟶ Y) {Z : ↑C₂.obj} (h : (CategoryStruct.id C₂.obj).toFunctor.obj Y ⟶ Z) : CategoryStruct.comp (α.l.toFunctor.map (α.r.toFunctor.map f)) (CategoryStruct.comp (α.adj.counit.toNatTrans.app Y) h) = CategoryStruct.comp (CategoryStruct.comp (α.adj.counit.toNatTrans.app X) f) h