# mathlibdocumentation

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} {F : D E} {G : E D} (adj : F G) (X : C D) (X_1 : C) :
X).app X_1 = adj.unit.app (X.obj X_1)
@[simp]
theorem category_theory.adjunction.whisker_right_counit_app_app (C : Type u_1) {D : Type u_2} {E : Type u_3} {F : D E} {G : E D} (adj : F G) (X : C E) (X_1 : C) :
X).app X_1 = adj.counit.app (X.obj X_1)
@[protected]
def category_theory.adjunction.whisker_right (C : Type u_1) {D : Type u_2} {E : Type u_3} {F : D E} {G : E D} (adj : F G) :
.obj F .obj G

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} {F : D E} {G : E D} (adj : F G) (X : E C) (X_1 : E) :
X).app X_1 = X.map (adj.counit.app X_1)
@[simp]
theorem category_theory.adjunction.whisker_left_unit_app_app (C : Type u_1) {D : Type u_2} {E : Type u_3} {F : D E} {G : E D} (adj : F G) (X : D C) (X_1 : D) :
X).app X_1 = X.map (adj.unit.app X_1)
@[protected]
def category_theory.adjunction.whisker_left (C : Type u_1) {D : Type u_2} {E : Type u_3} {F : D E} {G : E D} (adj : F G) :
.obj G .obj F

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

Equations