Documentation

Mathlib.CategoryTheory.Adjunction.Whiskering

Given categories C D E, functors F : D ⥤ E and G : E ⥤ D with an adjunction F ⊣ G, we provide the induced adjunction between the functor categories C ⥤ D and C ⥤ E, and the functor categories E ⥤ C and D ⥤ C.

source
def CategoryTheory.Adjunction.whiskerRight (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) :
(CategoryTheory.whiskeringRight C D E).obj F ⊣ (CategoryTheory.whiskeringRight C E D).obj G

Given an adjunction F ⊣ G, this provides the natural adjunction (whiskeringRight C _ _).obj F ⊣ (whiskeringRight C _ _).obj G.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Adjunction.whiskerRight_counit_app_app (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor C E) (X✝ : C) :
    ((CategoryTheory.Adjunction.whiskerRight C adj).counit.app X).app X✝ = adj.counit.app (X.obj X✝)
    source
    @[simp]
    theorem CategoryTheory.Adjunction.whiskerRight_unit_app_app (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor C D) (X✝ : C) :
    ((CategoryTheory.Adjunction.whiskerRight C adj).unit.app X).app X✝ = adj.unit.app (X.obj X✝)
    source
    def CategoryTheory.Adjunction.whiskerLeft (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) :
    (CategoryTheory.whiskeringLeft E D C).obj G ⊣ (CategoryTheory.whiskeringLeft D E C).obj F

    Given an adjunction F ⊣ G, this provides the natural adjunction (whiskeringLeft _ _ C).obj G ⊣ (whiskeringLeft _ _ C).obj F.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Adjunction.whiskerLeft_unit_app_app (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor D C) (X✝ : D) :
      ((CategoryTheory.Adjunction.whiskerLeft C adj).unit.app X).app X✝ = X.map (adj.unit.app X✝)
      source
      @[simp]
      theorem CategoryTheory.Adjunction.whiskerLeft_counit_app_app (C : Type u_1) {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} (adj : F ⊣ G) (X : CategoryTheory.Functor E C) (X✝ : E) :
      ((CategoryTheory.Adjunction.whiskerLeft C adj).counit.app X).app X✝ = X.map (adj.counit.app X✝)