English
For bimod M: W→X, N, N' : X→Y and P : Y→Z, whiskering f: N→N' with M and P yields a natural associativity relation with associatorBimod:
Русский
Для бикмодуля M: W→X, N, N' : X→Y и P : Y→Z, отбивка f: N→N' левым усилием через M и P удовлетворяет натуральному отношению ассоциатора:
LaTeX
$$$$ \\operatorname{whiskerRight} ( \\operatorname{whiskerLeft} M f ) P \;=\; (\\mathrm{associatorBimod} M N P)^{\\mathrm{hom}} \\circ \\operatorname{whiskerLeft} M ( \\operatorname{whiskerRight} f P ) \\circ (\\mathrm{associatorBimod} M N' P)^{-1} $$$$
Lean4
theorem whisker_assoc_bimod {W X Y Z : Mon C} (M : Bimod W X) {N N' : Bimod X Y} (f : N ⟶ N') (P : Bimod Y Z) :
whiskerRight (whiskerLeft M f) P =
(associatorBimod M N P).hom ≫ whiskerLeft M (whiskerRight f P) ≫ (associatorBimod M N' P).inv :=
by
dsimp [tensorHom, tensorBimod, associatorBimod]
ext
apply coequalizer.hom_ext
dsimp
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
dsimp [AssociatorBimod.hom]
slice_rhs 1 2 => rw [coequalizer.π_desc]
dsimp [AssociatorBimod.homAux]
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
simp only [Functor.flip_obj_map, curriedTensor_map_app]
slice_lhs 1 2 => rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one]
slice_rhs 1 3 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_rhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
slice_rhs 2 3 => rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one]
dsimp [AssociatorBimod.inv]
slice_rhs 3 4 => rw [coequalizer.π_desc]
dsimp [AssociatorBimod.invAux]
slice_rhs 2 2 => rw [whiskerLeft_comp]
slice_rhs 3 5 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
simp
