English
A left action homomorphism commutes with the left adjoint action in the associator context for P,Q,L.
Русский
Гомоморфизм левого действия коммутирует с левым действием активации в контексте ассоциатора для P,Q,L.
LaTeX
$$$((P \otimes Q).tensorBimod L).actLeft \; ≫ \mathrm{hom} P Q L = (R.X \; ◁ \; \mathrm{hom} P Q L) ≫ (P.tensorBimod (Q.tensorBimod L)).actLeft$$$
Lean4
theorem hom_left_act_hom' :
((P.tensorBimod Q).tensorBimod L).actLeft ≫ hom P Q L =
(R.X ◁ hom P Q L) ≫ (P.tensorBimod (Q.tensorBimod L)).actLeft :=
by
dsimp; dsimp [hom, homAux]
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
simp only [curriedTensor_obj_map]
slice_lhs 1 2 => rw [TensorBimod.whiskerLeft_π_actLeft]
slice_lhs 3 4 => rw [coequalizer.π_desc]
slice_rhs 1 2 => rw [← whiskerLeft_comp, coequalizer.π_desc, whiskerLeft_comp]
refine (cancel_epi ((tensorRight _ ⋙ tensorLeft _).map (coequalizer.π _ _))).1 ?_
dsimp; dsimp [TensorBimod.X]
slice_lhs 1 2 => rw [associator_inv_naturality_middle]
slice_lhs 2 3 => rw [← comp_whiskerRight, TensorBimod.whiskerLeft_π_actLeft, comp_whiskerRight, comp_whiskerRight]
slice_lhs 4 6 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_lhs 3 4 => rw [associator_naturality_left]
slice_rhs 1 3 =>
rw [← whiskerLeft_comp, ← whiskerLeft_comp, π_tensor_id_preserves_coequalizer_inv_desc, whiskerLeft_comp,
whiskerLeft_comp]
slice_rhs 3 4 => erw [TensorBimod.whiskerLeft_π_actLeft P (Q.tensorBimod L)]
slice_rhs 2 3 => erw [associator_inv_naturality_right]
slice_rhs 3 4 => erw [whisker_exchange]
monoidal
