English
The π-tensor-id interaction on the right is given by a commutative relation with actRight; i.e., a coequalizer projection followed by actRight equals a composition with the associator and actLeft.
Русский
Взаимодействие π с TensorId справа выражается в тождественном соотношении с действием справа; то есть сопоставление после сопряжения равно композиции с ассоциатором и actLeft.
LaTeX
$$$ (\mathrm{coequalizer}.π _ _ \; \; ⟶ T.X) ≫ \mathrm{actRight} \, P \, Q = (\alpha_{\!\! _ _ _}).hom ≫ (P.X \; ◁ \; Q.\mathrm{actRight}) ≫ \mathrm{coequalizer}.π _ _ $$$
Lean4
theorem whiskerLeft_π_actLeft :
(R.X ◁ coequalizer.π _ _) ≫ actLeft P Q = (α_ _ _ _).inv ≫ (P.actLeft ▷ Q.X) ≫ coequalizer.π _ _ :=
by
erw [map_π_preserves_coequalizer_inv_colimMap (tensorLeft _)]
simp only [Category.assoc]
