English
For bimodules M: V→W, N: W→X, P: X→Y, Q: Y→Z, a pentagon diagram composed of associators and whiskers commutes.
Русский
Для би-модулей M: V→W, N: W→X, P: X→Y, Q: Y→Z диаграмма с ассоциаторами и отбивками образует правильный пентагон.
LaTeX
$$$$ \\text{(pentagon relation)} \\quad \\text{(explicitly involves } \\mathrm{associatorBimod} \\text{ and whisker operations)} $$$$
Lean4
theorem pentagon_bimod {V W X Y Z : Mon C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y) (Q : Bimod Y Z) :
whiskerRight (associatorBimod M N P).hom Q ≫
(associatorBimod M (N.tensorBimod P) Q).hom ≫ whiskerLeft M (associatorBimod N P Q).hom =
(associatorBimod (M.tensorBimod N) P Q).hom ≫ (associatorBimod M N (P.tensorBimod Q)).hom :=
by
dsimp [associatorBimod]
ext
apply coequalizer.hom_ext
dsimp
dsimp only [AssociatorBimod.hom]
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
slice_lhs 2 3 => rw [coequalizer.π_desc]
slice_rhs 1 2 => rw [coequalizer.π_desc]
dsimp [AssociatorBimod.homAux]
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp
slice_lhs 1 2 => rw [← comp_whiskerRight, coequalizer.π_desc]
slice_rhs 1 3 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_rhs 3 4 => rw [coequalizer.π_desc]
refine (cancel_epi ((tensorRight _ ⋙ tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp
slice_lhs 1 2 =>
rw [← comp_whiskerRight, π_tensor_id_preserves_coequalizer_inv_desc, comp_whiskerRight, comp_whiskerRight]
slice_lhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
dsimp only [TensorBimod.X]
slice_lhs 2 3 => rw [associator_naturality_middle]
slice_lhs 5 6 => rw [ι_colimMap, parallelPairHom_app_one]
slice_lhs 4 5 => rw [← whiskerLeft_comp, coequalizer.π_desc]
slice_lhs 3 4 =>
rw [← whiskerLeft_comp, π_tensor_id_preserves_coequalizer_inv_desc, whiskerLeft_comp, whiskerLeft_comp]
slice_rhs 1 2 => rw [associator_naturality_left]
slice_rhs 2 3 => rw [← whisker_exchange]
slice_rhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_rhs 2 3 => rw [associator_naturality_right]
monoidal
