English
The left whiskering by a morphism on the domain and the right whiskering by a morphism on the codomain commute; i.e. two different orders of whiskering give the same composite morphism after simplification using associativity and unit constraints.
Русский
Левое усиковое отнесение по области и правое усиковое отнесение по кодоморфизму commute; оба порядка усиков дают одинаковый композиционный морфизм после приведения к каноническому виду через ассоциативность и единичные тензорные ограничения.
LaTeX
$$$ eHomWhiskerLeft\\ V\\ X'\\; g \\; \\circ\\ eHomWhiskerRight\\ V\\ f\\ Y' = eHomWhiskerRight\\ V\\ f\\ Y \\circ eHomWhiskerLeft\\ V\\ X\\ g, $$$
Lean4
@[reassoc]
theorem eHom_whisker_exchange {X X' Y Y' : C} (f : X ⟶ X') (g : Y ⟶ Y') :
eHomWhiskerLeft V X' g ≫ eHomWhiskerRight V f Y' = eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g :=
by
dsimp [eHomWhiskerLeft, eHomWhiskerRight]
rw [assoc, assoc, assoc, assoc, leftUnitor_inv_naturality_assoc, whisker_exchange_assoc, ← e_assoc,
leftUnitor_tensor_inv_assoc, associator_inv_naturality_left_assoc, Iso.hom_inv_id_assoc, ← comp_whiskerRight_assoc,
whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, assoc, Iso.inv_hom_id_assoc, whisker_exchange_assoc,
MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]
