English
A detailed naturality statement for id whiskering on the left in the bimodule setting, expressing that the construction is functorial with respect to morphisms.
Русский
Детальное натурализованное утверждение о левом whiskerLeft с идентичностью в контексте биомодуля; конструкция функциональна по морфизмам.
LaTeX
$$$$ \text{(id whiskerLeft bimod)} \; = \; \text{naturality of left whiskering with identity.} $$$$
Lean4
theorem comp_whiskerLeft_bimod {W X Y Z : Mon C} (M : Bimod W X) (N : Bimod X Y) {P P' : Bimod Y Z} (f : P ⟶ P') :
whiskerLeft (M.tensorBimod N) f =
(associatorBimod M N P).hom ≫ whiskerLeft M (whiskerLeft N f) ≫ (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 [TensorBimod.X, AssociatorBimod.hom]
slice_rhs 1 2 => rw [coequalizer.π_desc]
dsimp [AssociatorBimod.homAux, AssociatorBimod.inv]
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
simp only [Functor.flip_obj_map, curriedTensor_map_app]
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]
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]
slice_rhs 2 3 => rw [associator_inv_naturality_right]
slice_rhs 1 3 => rw [Iso.hom_inv_id_assoc]
slice_lhs 1 2 => rw [← whisker_exchange]
rfl
