whiskerLeft — Mathlib

Lean4
/-- Given an adjunction `F ⊣ G`, this provides the natural adjunction
  `(whiskeringLeft _ _ C).obj G ⊣ (whiskeringLeft _ _ C).obj F`. -/
@[simps! unit_app_app counit_app_app]
protected def whiskerLeft (adj : F ⊣ G) : (whiskeringLeft E D C).obj G ⊣ (whiskeringLeft D E C).obj F
    where
  unit := { app := fun X => (leftUnitor _).inv ≫ whiskerRight adj.unit X ≫ (associator _ _ _).hom }
  counit := { app := fun X => (associator _ _ _).inv ≫ whiskerRight adj.counit X ≫ (leftUnitor _).hom }
  left_triangle_components X := by ext; simp [← X.map_comp]
  right_triangle_components X := by ext; simp [← X.map_comp]
Похожие утверждения