English
Compatibility of whiskering on the left with composition in bimodules: whiskering a composition equals the composition of whiskerings via associators.
Русский
Совместимость позагащивания слева с композициями в биомодулях: whiskerLeft от композиции равен композиции whiskerLeft через ассоциаторы.
LaTeX
$$$$ \mathrm{whiskerLeft}(M\otimes N)\; f = \big( \mathrm{associatorBimod} M N P \big).\mathrm{hom} \; \circ \; \mathrm{whiskerLeft} M (\mathrm{whiskerLeft} N f) \circ \big( \mathrm{associatorBimod} M N P \big)^{-1}. $$$$
Lean4
theorem whiskerLeft_id_bimod {X Y Z : Mon C} {M : Bimod X Y} {N : Bimod Y Z} :
whiskerLeft M (𝟙 N) = 𝟙 (M.tensorBimod N) := by
ext
apply Limits.coequalizer.hom_ext
dsimp only [tensorBimod_X, whiskerLeft_hom, id_hom']
simp only [whiskerLeft_id, ι_colimMap, parallelPair_obj_one, parallelPairHom_app_one, Category.id_comp]
erw [Category.comp_id]
