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