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
@[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✝.toPrefunctor.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✝.toPrefunctor.obj X)
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).toPrefunctor.obj F ⊣ (CategoryTheory.whiskeringRight C E D).toPrefunctor.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.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✝.toPrefunctor.map (adj.counit.app X)
    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✝.toPrefunctor.map (adj.unit.app 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).toPrefunctor.obj G ⊣ (CategoryTheory.whiskeringLeft D E C).toPrefunctor.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