English
Let X, Y, Z be monoidal objects in a category C with suitable limits. For Bimod X Y objects M, N, P and morphisms f: M → N, g: N → P, and any Q: Bimod Y Z, the right whiskering functor distributes over composition:
Русский
Пусть X, Y, Z — монойдальные объекты в категории C с необходимыми пределами. Пусть M, N, P — би-модули X→Y, f: M → N, g: N → P, и Q — би-модуль Y→Z. Тогда правая отбивка f ≫ g по Q равна отбивке f по Q, затем отбивке g по Q:
LaTeX
$$$$ \\operatorname{whiskerRight}(f \\circ g) Q \;=\\; \\operatorname{whiskerRight}(f) Q \\;\\;\\circ\\;\\; \\operatorname{whiskerRight}(g) Q $$$$
Lean4
theorem comp_whiskerRight_bimod {X Y Z : Mon C} {M N P : Bimod X Y} (f : M ⟶ N) (g : N ⟶ P) (Q : Bimod Y Z) :
whiskerRight (f ≫ g) Q = whiskerRight f Q ≫ whiskerRight g Q :=
by
ext
apply Limits.coequalizer.hom_ext
simp
