Lean4
/-- Construct an isomorphism of bimodules by giving an isomorphism between the underlying objects
and checking compatibility with left and right actions only in the forward direction.
-/
@[simps]
def isoOfIso {X Y : Mon C} {P Q : Bimod X Y} (f : P.X ≅ Q.X)
(f_left_act_hom : P.actLeft ≫ f.hom = (X.X ◁ f.hom) ≫ Q.actLeft)
(f_right_act_hom : P.actRight ≫ f.hom = (f.hom ▷ Y.X) ≫ Q.actRight) : P ≅ Q
where
hom := { hom := f.hom }
inv :=
{ hom := f.inv
left_act_hom := by
rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id, f_left_act_hom, ←
Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id, whiskerLeft_id, Category.id_comp]
right_act_hom := by
rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id, f_right_act_hom, ←
Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id, id_whiskerRight, Category.id_comp] }
hom_inv_id := by ext; dsimp; rw [Iso.hom_inv_id]
inv_hom_id := by ext; dsimp; rw [Iso.inv_hom_id]
