whiskerRight_comp — Mathlib

English

Whiskering respects composition: whiskerRight (α ≫ β) F = whiskerRight α F ≫ whiskerRight β F, for natural transformations α:G⟶H and β:H⟶K and F:D ⥤ E.

Русский

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

LaTeX

$$$\\mathrm{whiskerRight}(\\alpha\\;\\circ\\;\\beta)\\,F = \\mathrm{whiskerRight}\\alpha\\,F \\circ \\mathrm{whiskerRight}\\beta\\,F,$$$

Lean4

@[simp, reassoc]
theorem whiskerRight_comp {G H K : C ⥤ D} (α : G ⟶ H) (β : H ⟶ K) (F : D ⥤ E) :
    whiskerRight (α ≫ β) F = whiskerRight α F ≫ whiskerRight β F :=
  ((whiskeringRight C D E).obj F).map_comp α β

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