English
The left/right actions commute with the hom morphism under the right unitor, reflecting the naturality of actions with respect to right unitor operations.
Русский
Правое униторное действие совместимо с морфизмом hom через правое действие, выражая натуральность действий по отношению к правому унитору.
LaTeX
$$$$ \big( (\text{regular } R).tensorBimod P \big).actRight \circ \mathrm{hom} P = (\mathrm{hom} P \; \triangleright\; S.X) \circ P.actRight. $$$$
Lean4
theorem hom_left_act_hom' : (P.tensorBimod (regular S)).actLeft ≫ hom P = (R.X ◁ hom P) ≫ P.actLeft :=
by
dsimp; dsimp [hom, TensorBimod.actLeft, regular]
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
dsimp
slice_lhs 1 4 => rw [id_tensor_π_preserves_coequalizer_inv_colimMap_desc]
slice_lhs 2 3 => rw [middle_assoc]
slice_rhs 1 2 => rw [← whiskerLeft_comp, coequalizer.π_desc]
rw [Iso.inv_hom_id_assoc]
