English
If f: M → M' is a bimodule morphism and N, P are bimodules, then whiskering f by N ⊗ P distributes with the associator in a specified way:
Русский
Если f: M → M' — морфизм би-модуля и N, P — би-модули, то правая отбивка f по N ⊗ P распределяется по отношению к ассоциатору согласно заданному правилу:
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 whiskerRight_comp_bimod {W X Y Z : Mon C} {M M' : Bimod W X} (f : M ⟶ M') (N : Bimod X Y) (P : Bimod Y Z) :
whiskerRight f (N.tensorBimod P) =
(associatorBimod M N P).inv ≫ whiskerRight (whiskerRight f N) P ≫ (associatorBimod M' N P).hom :=
by
dsimp [tensorHom, tensorBimod, associatorBimod]
ext
apply coequalizer.hom_ext
dsimp
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
dsimp [TensorBimod.X, AssociatorBimod.inv]
slice_rhs 1 2 => rw [coequalizer.π_desc]
dsimp [AssociatorBimod.invAux, AssociatorBimod.hom]
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
simp only [curriedTensor_obj_map]
slice_rhs 1 3 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
slice_rhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
slice_rhs 2 3 => rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one]
slice_rhs 3 4 => rw [coequalizer.π_desc]
dsimp [AssociatorBimod.homAux]
slice_rhs 2 2 => rw [comp_whiskerRight]
slice_rhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_rhs 2 3 => rw [associator_naturality_left]
slice_rhs 1 3 => rw [Iso.inv_hom_id_assoc]
slice_lhs 1 2 => rw [whisker_exchange]
rfl
