English
In an enriched setting, whiskering an isomorphism on the left and right cancels, reducing a composed whiskered map to the corresponding component with the target isomorphism. More precisely, for any isomorphism α: Y ≅ Y1, a certain equality of enriched morphisms holds, expressing the compatibility of left and right whiskering with the enrichment composition.
Русский
В обобщенной (обогащенной) обстановке, применение левого и правого усиков к изоморфизму отменяет друг друга, приводя к тождественному выражению для соответствующего компонента. Пусть α: Y ≅ Y1, тогда выполняется определенное тождество обогащённых морфизмов, отражающее совместимость левостороннего и правостороннего усиков с композицией обогащения.
LaTeX
$$$ eHomWhiskerLeft\; V\\; X\\; α^{-1} \\triangleright\\ _ \\; \\circ\\ _ \\triangleleft\\; eHomWhiskerRight\\; V\\; α.hom\\; Z \\; \\circ\\; eComp\\; V\\; X\\; Y\\; Z = eComp\\; V\\; X\\; Y_{1}\\; Z, $$$
Lean4
@[reassoc]
theorem eHom_whisker_cancel_inv {X Y Y₁ Z : C} (α : Y ≅ Y₁) :
eHomWhiskerLeft V X α.inv ▷ _ ≫ _ ◁ eHomWhiskerRight V α.hom Z ≫ eComp V X Y Z = eComp V X Y₁ Z :=
eHom_whisker_cancel V α.symm
