English
The right associativity relation for actLeft and μ on P, Q is given by a specific equality with α and associator constraints.
Русский
Правая ассоциативность для actLeft и μ на P, Q задаётся равенством с α и ассоциатором.
LaTeX
$$$(\,\_ ◁ μ \,) ≫ actRight P Q = (\alpha_{_ _ T.X T.X}).hom \; ≫ (actRight P Q \; ▷ \; T.X) \; ≫ actRight P Q$$$
Lean4
theorem left_assoc' : (μ ▷ _) ≫ actLeft P Q = (α_ R.X R.X _).hom ≫ (R.X ◁ actLeft P Q) ≫ actLeft P Q :=
by
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
dsimp [X]
slice_lhs 1 2 => rw [whisker_exchange]
slice_lhs 2 3 => rw [whiskerLeft_π_actLeft]
slice_lhs 1 2 => rw [associator_inv_naturality_left]
slice_lhs 2 3 => rw [← comp_whiskerRight, left_assoc, comp_whiskerRight, comp_whiskerRight]
slice_rhs 1 2 => rw [associator_naturality_right]
slice_rhs 2 3 => rw [← whiskerLeft_comp, whiskerLeft_π_actLeft, whiskerLeft_comp, whiskerLeft_comp]
slice_rhs 4 5 => rw [whiskerLeft_π_actLeft]
slice_rhs 3 4 => rw [associator_inv_naturality_middle]
monoidal
