English
The right action maps from tensoring with the regular bimodule commute with the hom morphism, expressing compatibility of right action with bimodule morphisms.
Русский
Правое действие совместимо с морфизмом hom через тензорирование с регулярным би-модулем.
LaTeX
$$$$ ((\text{regular } R).tensorBimod P).actRight \; \circ \; \mathrm{hom} P = (\mathrm{hom} P \; \triangleright\; S.X) \circ P.actRight. $$$$
Lean4
theorem hom_right_act_hom' : ((regular R).tensorBimod P).actRight ≫ hom P = (hom P ▷ S.X) ≫ P.actRight :=
by
dsimp; dsimp [hom, TensorBimod.actRight, regular]
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp
slice_lhs 1 4 => rw [π_tensor_id_preserves_coequalizer_inv_colimMap_desc]
slice_rhs 1 2 => rw [← comp_whiskerRight, coequalizer.π_desc]
slice_rhs 1 2 => rw [middle_assoc]
simp only [Category.assoc]
