English
A right action homomorphism commutes with the right action in the associator context for P,Q,L.
Русский
Гомоморфизм правого действия совместим с правым действием в контексте ассоциатора для P,Q,L.
LaTeX
$$$((P.tensorBimod Q).tensorBimod L).actRight \; ≫ \mathrm{hom} P Q L = (\mathrm{hom} P Q L \; ▷ \; U.X) ≫ (P.tensorBimod (Q.tensorBimod L)).actRight$$$
Lean4
theorem hom_right_act_hom' :
((P.tensorBimod Q).tensorBimod L).actRight ≫ hom P Q L =
(hom P Q L ▷ U.X) ≫ (P.tensorBimod (Q.tensorBimod L)).actRight :=
by
dsimp; dsimp [hom, homAux]
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
simp only [Functor.flip_obj_map, curriedTensor_map_app]
slice_lhs 1 2 => rw [TensorBimod.π_tensor_id_actRight]
slice_lhs 3 4 => rw [coequalizer.π_desc]
slice_rhs 1 2 => rw [← comp_whiskerRight, coequalizer.π_desc, comp_whiskerRight]
refine (cancel_epi ((tensorRight _ ⋙ tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp; dsimp [TensorBimod.X]
slice_lhs 1 2 => rw [associator_naturality_left]
slice_lhs 2 3 => rw [← whisker_exchange]
slice_lhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_lhs 2 3 => rw [associator_naturality_right]
slice_rhs 1 3 =>
rw [← comp_whiskerRight, ← comp_whiskerRight, π_tensor_id_preserves_coequalizer_inv_desc, comp_whiskerRight,
comp_whiskerRight]
slice_rhs 3 4 => erw [TensorBimod.π_tensor_id_actRight P (Q.tensorBimod L)]
slice_rhs 2 3 => erw [associator_naturality_middle]
dsimp
slice_rhs 3 4 => rw [← whiskerLeft_comp, TensorBimod.π_tensor_id_actRight, whiskerLeft_comp, whiskerLeft_comp]
monoidal
