isoWhiskerRight_trans — Mathlib

English

Whiskering preserves composition of isomorphisms on the right: isoWhiskerRight (α ≪≫ β) F = isoWhiskerRight α F ≪≫ isoWhiskerRight β F.

Русский

Отбрасывания справа сохраняют композицию изоморфизмов: isoWhiskerRight (α ≪≫ β) F = isoWhiskerRight α F ≪≫ isoWhiskerRight β F.

LaTeX

$$$\\mathrm{isoWhiskerRight}(\\alpha \\otimes \\beta)\\,F = \\mathrm{isoWhiskerRight}\\alpha\\,F \\;\\otimes\\; \\mathrm{isoWhiskerRight}\\beta\\,F.$$$

Lean4

@[simp, reassoc]
theorem isoWhiskerRight_trans {G H K : C ⥤ D} (α : G ≅ H) (β : H ≅ K) (F : D ⥤ E) :
    isoWhiskerRight (α ≪≫ β) F = isoWhiskerRight α F ≪≫ isoWhiskerRight β F :=
  ((whiskeringRight C D E).obj F).mapIso_trans α β

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