isoWhiskerLeft_trans_isoWhiskerRight

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

Похожие утверждения