English
For M: W→X, N, N' : X→Y, P : Y→Z, the whiskering with M and f yields a left-hand side equal to a composition on the right with associators.
Русский
Для M: W→X, N, N' : X→Y, P : Y→Z, отбивка с M и f приводит к равенству левой и правой частей с использованием ассоциаторов.
LaTeX
$$$$ \\operatorname{whiskerRight}( \\operatorname{whiskerLeft} M f ) P \;=\; \\mathrm{associatorBimod} M N P^{-1} \\circ \\operatorname{whiskerLeft} M ( \\operatorname{whiskerRight} f P ) \\circ \\mathrm{associatorBimod} M' N P $$$$
Lean4
theorem triangle_bimod {X Y Z : Mon C} (M : Bimod X Y) (N : Bimod Y Z) :
(associatorBimod M (regular Y) N).hom ≫ whiskerLeft M (leftUnitorBimod N).hom =
whiskerRight (rightUnitorBimod M).hom N :=
by
dsimp [associatorBimod, leftUnitorBimod, rightUnitorBimod]
ext
apply coequalizer.hom_ext
dsimp
dsimp [AssociatorBimod.hom]
slice_lhs 1 2 => rw [coequalizer.π_desc]
dsimp [AssociatorBimod.homAux]
slice_rhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
dsimp [RightUnitorBimod.hom]
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp [regular]
slice_lhs 1 3 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_lhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
dsimp [LeftUnitorBimod.hom]
slice_lhs 2 3 => rw [← whiskerLeft_comp, coequalizer.π_desc]
slice_rhs 1 2 => rw [← comp_whiskerRight, coequalizer.π_desc]
slice_rhs 1 2 => rw [coequalizer.condition]
simp only [Category.assoc]
