mathlib documentation

category_theory.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.

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

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

Equations
@[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) :

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

Equations