whiskerLeft_comp_whiskerRight — Mathlib

English

Horizontal composition of natural transformations equals the interaction between left and right whiskering: α ◫ β = whiskerLeft F β ≫ whiskerRight α K.

Русский

Горизонтальная композиция натуральных преобразований равна взаимодействию левого и правого отбрасываний: α ◫ β = whiskerLeft F β ≫ whiskerRight α K.

LaTeX

$$$\\alpha \\;\\square\\; \\beta = \\mathrm{whiskerLeft}\\,F\\,\\beta \\;\\; ≫ \\; \\mathrm{whiskerRight}\\,\\alpha\\,K.$$$

Lean4

@[reassoc]
theorem whiskerLeft_comp_whiskerRight {F G : C ⥤ D} {H K : D ⥤ E} (α : F ⟶ G) (β : H ⟶ K) :
    whiskerLeft F β ≫ whiskerRight α K = whiskerRight α H ≫ whiskerLeft G β :=
  by
  ext
  simp

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