English
The left action maps obtained by tensoring with the regular bimodule commute with the hom morphism, reflecting compatibility of left action with the bimod structure.
Русский
Левое действие, полученное тензорованием с регулярным би-модулем, commute с морфизмом hom, отражая совместимость левого действия с би-модулярной структурой.
LaTeX
$$$$ ((\text{regular } R).tensorBimod P).actLeft \; \circ \; \mathrm{hom} P = (R.X \triangleleft \mathrm{hom} P) \circ P.actLeft. $$$$
Lean4
theorem hom_left_act_hom' : ((regular R).tensorBimod P).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 [left_assoc]
slice_rhs 1 2 => rw [← whiskerLeft_comp, coequalizer.π_desc]
rw [Iso.inv_hom_id_assoc]
