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