THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[simp]
theorem
category_theory.adjunction.whisker_right_unit_app_app
(C : Type u_1)
{D : Type u_2}
{E : Type u_3}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
(adj : F ⊣ G)
(X : C ⥤ D)
(X_1 : C) :
@[simp]
theorem
category_theory.adjunction.whisker_right_counit_app_app
(C : Type u_1)
{D : Type u_2}
{E : Type u_3}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
(adj : F ⊣ G)
(X : C ⥤ E)
(X_1 : C) :
@[protected]
def
category_theory.adjunction.whisker_right
(C : Type u_1)
{D : Type u_2}
{E : Type u_3}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
(adj : F ⊣ G) :
(category_theory.whiskering_right C D E).obj F ⊣ (category_theory.whiskering_right C E D).obj G
Given an adjunction F ⊣ G, this provides the natural adjunction
(whiskering_right C _ _).obj F ⊣ (whiskering_right C _ _).obj G.
Equations
- category_theory.adjunction.whisker_right C adj = category_theory.adjunction.mk_of_unit_counit {unit := {app := λ (X : C ⥤ D), ((𝟭 (C ⥤ D)).obj X).right_unitor.inv ≫ category_theory.whisker_left X adj.unit ≫ (((𝟭 (C ⥤ D)).obj X).associator F G).inv, naturality' := _}, counit := {app := λ (X : C ⥤ E), (X.associator G F).hom ≫ category_theory.whisker_left X adj.counit ≫ X.right_unitor.hom, naturality' := _}, left_triangle' := _, right_triangle' := _}
@[simp]
theorem
category_theory.adjunction.whisker_left_counit_app_app
(C : Type u_1)
{D : Type u_2}
{E : Type u_3}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
(adj : F ⊣ G)
(X : E ⥤ C)
(X_1 : E) :
@[simp]
theorem
category_theory.adjunction.whisker_left_unit_app_app
(C : Type u_1)
{D : Type u_2}
{E : Type u_3}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
(adj : F ⊣ G)
(X : D ⥤ C)
(X_1 : D) :
@[protected]
def
category_theory.adjunction.whisker_left
(C : Type u_1)
{D : Type u_2}
{E : Type u_3}
[category_theory.category C]
[category_theory.category D]
[category_theory.category E]
{F : D ⥤ E}
{G : E ⥤ D}
(adj : F ⊣ G) :
(category_theory.whiskering_left E D C).obj G ⊣ (category_theory.whiskering_left D E C).obj F
Given an adjunction F ⊣ G, this provides the natural adjunction
(whiskering_left _ _ C).obj G ⊣ (whiskering_left _ _ C).obj F.
Equations
- category_theory.adjunction.whisker_left C adj = category_theory.adjunction.mk_of_unit_counit {unit := {app := λ (X : D ⥤ C), ((𝟭 (D ⥤ C)).obj X).left_unitor.inv ≫ category_theory.whisker_right adj.unit X ≫ (F.associator G ((𝟭 (D ⥤ C)).obj X)).hom, naturality' := _}, counit := {app := λ (X : E ⥤ C), (G.associator F X).inv ≫ category_theory.whisker_right adj.counit X ≫ X.left_unitor.hom, naturality' := _}, left_triangle' := _, right_triangle' := _}