English
For F: B ⥤ C, G,H: C ⥤ D and K: D ⥤ E, the whiskering-right of the left whiskerex identity is an equality involving associators: isoWhiskerRight (isoWhiskerLeft F α) K = associator F α K ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫ (associator)^(-1).
Русский
Для F: B ⥤ C, G,H: C ⥤ D и K: D ⥤ E, правая отбрасывание от левого изоморфизма образует равенство через ассоциаторы: isoWhiskerRight (isoWhiskerLeft F α) K = ассоциатор F α K ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫ (ассоциатор)^(-1).
LaTeX
$$$\\mathrm{isoWhiskerRight}(\\mathrm{isoWhiskerLeft}\\,F\\;α)\\;K = \\mathrm{Functor.associator}\\,\\_\\_\\_ \\; ≪≫ \\; \\mathrm{isoWhiskerLeft}\\,F\\,(\\mathrm{isoWhiskerRight}\\,α\\,K) \\;≪≫ (\\mathrm{Functor.associator}\\,\\_\\_\\_).symm$$$
Lean4
@[reassoc]
theorem isoWhiskerRight_left (F : B ⥤ C) {G H : C ⥤ D} (α : G ≅ H) (K : D ⥤ E) :
isoWhiskerRight (isoWhiskerLeft F α) K =
Functor.associator _ _ _ ≪≫ isoWhiskerLeft F (isoWhiskerRight α K) ≪≫ (Functor.associator _ _ _).symm :=
by cat_disch
