English
The right whiskering of a composition equals the composition of whiskerings on each factor, with Y fixed.
Русский
Правое взятие whiskerRight от композиции равняется композиции whiskerRight по каждому фактору.
LaTeX
$$$eHomWhiskerRight\,V\,(f)\times(f') Y = eHomWhiskerRight\,V\,f'Y \circ eHomWhiskerRight\,V\,fY.$$$
Lean4
@[simp, reassoc]
theorem eHomWhiskerRight_comp {X X' X'' : C} (f : X ⟶ X') (f' : X' ⟶ X'') (Y : C) :
eHomWhiskerRight V (f ≫ f') Y = eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y :=
by
dsimp [eHomWhiskerRight]
rw [assoc, assoc, eHomEquiv_comp, comp_whiskerRight_assoc, comp_whiskerRight_assoc, ← e_assoc', tensorHom_def',
comp_whiskerRight_assoc, id_whiskerLeft, comp_whiskerRight_assoc, ← comp_whiskerRight_assoc, Iso.inv_hom_id,
id_whiskerRight_assoc, comp_whiskerRight_assoc, leftUnitor_inv_whiskerRight_assoc, ←
associator_inv_naturality_left_assoc, Iso.inv_hom_id_assoc, ← whisker_exchange_assoc, id_whiskerLeft_assoc,
Iso.inv_hom_id_assoc]
