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_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
    @[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
    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_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.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.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
      source
      @[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)
      source
      @[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
      source
      @[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)
      source
      @[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
      source
      @[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)
      source
      @[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 f (CategoryStruct.comp (α.adj.unit.toNatTrans.app Y) h)
      source
      @[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
      source
      @[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 (α.adj.counit.toNatTrans.app X) (CategoryStruct.comp f h)