Lean4
/-- Left whiskering for morphisms of bimodule objects. -/
@[simps]
noncomputable def whiskerLeft {X Y Z : Mon C} (M : Bimod X Y) {N₁ N₂ : Bimod Y Z} (f : N₁ ⟶ N₂) :
M.tensorBimod N₁ ⟶ M.tensorBimod N₂
where
hom :=
colimMap
(parallelPairHom _ _ _ _ (_ ◁ f.hom) (_ ◁ f.hom) (by rw [whisker_exchange])
(by
simp only [Category.assoc, tensor_whiskerLeft, Iso.inv_hom_id_assoc, Iso.cancel_iso_hom_left]
slice_lhs 1 2 => rw [← whiskerLeft_comp, Hom.left_act_hom]
simp))
left_act_hom := by
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
dsimp
slice_lhs 1 2 => rw [TensorBimod.whiskerLeft_π_actLeft]
slice_lhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
slice_rhs 1 2 => rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one, whiskerLeft_comp]
slice_rhs 2 3 => rw [TensorBimod.whiskerLeft_π_actLeft]
slice_rhs 1 2 => rw [associator_inv_naturality_right]
slice_rhs 2 3 => rw [whisker_exchange]
simp
right_act_hom := by
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp
slice_lhs 1 2 => rw [TensorBimod.π_tensor_id_actRight]
slice_lhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
slice_lhs 2 3 => rw [← whiskerLeft_comp, Hom.right_act_hom]
slice_rhs 1 2 => rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one, comp_whiskerRight]
slice_rhs 2 3 => rw [TensorBimod.π_tensor_id_actRight]
simp
