English
Given W, X, Y, Z monoids and bimodules M, M' : W→X, N : X→Y, P : Y→Z with a morphism f: M→M', the right whiskering distributes over the left and right associators in a precise way.
Русский
Пусть W, X, Y, Z — мономорфные конусы, M, M' : W→X, N : X→Y, P : Y→Z, f: M→M'. Правая отбивка распределяется по отношению к лево- и правоассоциаторам.
LaTeX
$$$$ \\operatorname{whiskerRight} f (N \\otimes_{\\mathrm{Bimod}} P) = (\\mathrm{associatorBimod} M N P)^{-1} \\circ \\operatorname{whiskerRight}( \\operatorname{whiskerRight} f N) P \\circ (\\mathrm{associatorBimod} M' N P)^{\\mathrm{hom}} $$$$
Lean4
theorem whisker_exchange_bimod {X Y Z : Mon C} {M N : Bimod X Y} {P Q : Bimod Y Z} (f : M ⟶ N) (g : P ⟶ Q) :
whiskerLeft M g ≫ whiskerRight f Q = whiskerRight f P ≫ whiskerLeft N g :=
by
ext
apply coequalizer.hom_ext
dsimp
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
slice_lhs 2 3 => rw [ι_colimMap, parallelPairHom_app_one]
slice_lhs 1 2 => rw [whisker_exchange]
simp
