Lean4
/-- Right whiskering for morphisms of bimodule objects. -/
@[simps]
noncomputable def whiskerRight {X Y Z : Mon C} {M₁ M₂ : Bimod X Y} (f : M₁ ⟶ M₂) (N : Bimod Y Z) :
M₁.tensorBimod N ⟶ M₂.tensorBimod N
where
hom :=
colimMap
(parallelPairHom _ _ _ _ (f.hom ▷ _ ▷ _) (f.hom ▷ _)
(by rw [← comp_whiskerRight, Hom.right_act_hom, comp_whiskerRight])
(by
slice_lhs 2 3 => rw [whisker_exchange]
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_lhs 2 3 => rw [← comp_whiskerRight, Hom.left_act_hom]
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_middle]
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 [whisker_exchange]
slice_rhs 1 2 => rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one, comp_whiskerRight]
slice_rhs 2 3 => rw [TensorBimod.π_tensor_id_actRight]
simp
