English
Another formulation of the right associativity for actLeft and μ on P,Q with auxiliary associators.
Русский
Ещё одно выражение правой ассоциативности для actLeft и μ на P,Q с вспомогательными ассоциаторами.
LaTeX
$$$(_ ◁ μ) ≫ actRight P Q = (\alpha_{_ T.X T.X}).hom ≫ (actRight P Q ▷ T.X) ≫ actRight P Q$$$
Lean4
theorem right_assoc' : (_ ◁ μ) ≫ actRight P Q = (α_ _ T.X T.X).inv ≫ (actRight P Q ▷ T.X) ≫ actRight P Q :=
by
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp [X]
slice_lhs 1 2 => rw [← whisker_exchange]
slice_lhs 2 3 => rw [π_tensor_id_actRight]
slice_lhs 1 2 => rw [associator_naturality_right]
slice_lhs 2 3 => rw [← whiskerLeft_comp, right_assoc, whiskerLeft_comp, whiskerLeft_comp]
slice_rhs 1 2 => rw [associator_inv_naturality_left]
slice_rhs 2 3 => rw [← comp_whiskerRight, π_tensor_id_actRight, comp_whiskerRight, comp_whiskerRight]
slice_rhs 4 5 => rw [π_tensor_id_actRight]
simp
