English
For f: M → N between bimodules over X, Y, the right whiskering by the regular Y identifies with the composite through the right unitor isomorphisms:
Русский
Для гомоморфизма f: M → N между би-модулями над X и Y, правая отбивка по регулярному Y совпадает с композицией через правый унитор:
LaTeX
$$$$ \\operatorname{whiskerRight} f (\\mathrm{regular}\, Y) \;=\; (\\mathrm{rightUnitorBimod}\ M)^{\\mathrm{hom}} \\;\\circ\\; f \\;\\circ\\; (\\mathrm{rightUnitorBimod}\\ N)^{\\mathrm{inv}} $$$$
Lean4
theorem whiskerRight_id_bimod {X Y : Mon C} {M N : Bimod X Y} (f : M ⟶ N) :
whiskerRight f (regular Y) = (rightUnitorBimod M).hom ≫ f ≫ (rightUnitorBimod N).inv :=
by
dsimp [tensorHom, regular, rightUnitorBimod]
ext
apply coequalizer.hom_ext
dsimp
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
dsimp [RightUnitorBimod.hom]
slice_rhs 1 2 => rw [coequalizer.π_desc]
dsimp [RightUnitorBimod.inv]
slice_rhs 1 2 => rw [Hom.right_act_hom]
slice_rhs 2 3 => rw [rightUnitor_inv_naturality]
slice_rhs 3 4 => rw [← whisker_exchange]
slice_rhs 4 5 => rw [coequalizer.condition]
slice_rhs 3 4 => rw [associator_naturality_right]
slice_rhs 4 5 => rw [← whiskerLeft_comp, MonObj.mul_one]
simp
