English
For isomorphisms α: F ≅ G and β: H ≅ K, whiskering left and whiskering right interact: isoWhiskerLeft F β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ isoWhiskerLeft G β.
Русский
Для изоморфизмов α: F ≅ G и β: H ≅ K взаимодействие левого и правого отбрасываний: isoWhiskerLeft F β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ isoWhiskerLeft G β.
LaTeX
$$$\\mathrm{isoWhiskerLeft}\,F\\,\\beta \\;\\; ≪≫ \\; \\mathrm{isoWhiskerRight}\\,α\\,K = \\mathrm{isoWhiskerRight}\\,α\\,H \\;≪≫\\; \\mathrm{isoWhiskerLeft}\\,G\\,β.$$$
Lean4
@[reassoc]
theorem isoWhiskerLeft_trans_isoWhiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α : F ≅ G) (β : H ≅ K) :
isoWhiskerLeft F β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ isoWhiskerLeft G β :=
by
ext
simp