English
The middle associativity identity for actLeft, actRight, and X in Bimod TensorBimod involves the associator and whiskering.
Русский
Средняя ассоциативность для actLeft, actRight и X в контексте Bimod TensorBimod включает ассоциатор и подшипление.
LaTeX
$$$(actLeft P Q) \; ▷ \; T.X ≫ actRight P Q = (\alpha_{ R.X X T.X}).hom \; ≫ (R.X ◁ actRight P Q) ≫ actLeft P Q$$$
Lean4
theorem middle_assoc' : (actLeft P Q ▷ T.X) ≫ actRight P Q = (α_ R.X _ T.X).hom ≫ (R.X ◁ actRight P Q) ≫ actLeft P Q :=
by
refine (cancel_epi ((tensorLeft _ ⋙ tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp [X]
slice_lhs 1 2 => rw [← comp_whiskerRight, whiskerLeft_π_actLeft, comp_whiskerRight, comp_whiskerRight]
slice_lhs 3 4 => rw [π_tensor_id_actRight]
slice_lhs 2 3 => rw [associator_naturality_left]
slice_rhs 1 2 => rw [associator_naturality_middle]
slice_rhs 2 3 => rw [← whiskerLeft_comp, π_tensor_id_actRight, whiskerLeft_comp, whiskerLeft_comp]
slice_rhs 4 5 => rw [whiskerLeft_π_actLeft]
slice_rhs 3 4 => rw [associator_inv_naturality_right]
slice_rhs 4 5 => rw [whisker_exchange]
simp
