English
Compatibility of the right action with the hom morphism when whiskering on the right with a regular bimodule and S.X.
Русский
Совместимость правого действия с morphism hom при добавлении к правой стороне регулярного би-модуля и S.X.
LaTeX
$$$$ \big( (\text{regular } S).tensorBimod P \big).actRight \; \circ \; \mathrm{hom} P = (\mathrm{hom} P \; \triangleright\; S.X) \circ P.actRight. $$$$
Lean4
theorem hom_right_act_hom' : (P.tensorBimod (regular S)).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_lhs 2 3 => rw [right_assoc]
slice_rhs 1 2 => rw [← comp_whiskerRight, coequalizer.π_desc]
rw [Iso.hom_inv_id_assoc]
