English
Compatibility of mapWhiskerLeft with the associator on Hom as a long composite of basic map operations.
Русский
Совместимость mapWhiskerLeft с ассоциатором через композицию элементарных отображений.
LaTeX
$$mapWhiskerLeft _ (F.associator G H).hom = (mapCompRight A (F ⋙ G) H).hom ≫ whiskerRight (mapCompRight A F G).hom (mapPair (\\u211d A) H) ≫ ((mapPair (\\u211d A) F).associator (mapPair (\\u211d A) G) (mapPair (\\u211d A) H)).hom ≫ whiskerLeft (mapPair (\\u211d A) F) (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv$$
Lean4
@[reassoc]
theorem mapWhiskerLeft_associator_hom (F : B ⥤ C) (G : C ⥤ D) (H : D ⥤ E) :
mapWhiskerLeft _ (F.associator G H).hom =
(mapCompRight A (F ⋙ G) H).hom ≫
whiskerRight (mapCompRight A F G).hom (mapPair (𝟭 A) H) ≫
((mapPair (𝟭 A) F).associator (mapPair (𝟭 A) G) (mapPair (𝟭 A) H)).hom ≫
whiskerLeft (mapPair (𝟭 A) F) (mapCompRight A G H).inv ≫ (mapCompRight A F (G ⋙ H)).inv :=
by apply natTrans_ext <;> ext <;> simp [mapCompRight]
