Lean4
/-- Define a right action of `Cᵒᵖ` on `Dᵒᵖ` from a right action of `C` on `D` via
the formula `(op d) ⊙ᵣ (op c) = op (d ⊙ᵣ c)`. -/
@[simps -isSimp]
def oppositeRightAction [MonoidalRightAction C D] : MonoidalRightAction Cᵒᵖ Dᵒᵖ
where
actionObj c d := op <| c.unop ⊙ᵣ d.unop
actionHomLeft {c c'} f d := (f.unop ⊵ᵣ unop d).op
actionHomRight c {d d'} f := (unop c ⊴ᵣ f.unop).op
actionHom {c c'} {d d'} f g := (f.unop ⊙ᵣₘ g.unop).op
actionAssocIso _ _ _ := Iso.op <| (αᵣ _ _ _).symm
actionUnitIso _ := Iso.op <| (ρᵣ _).symm
actionHom_def
| op f, op g => by
apply Quiver.Hom.unop_inj
simpa [MonoidalRightAction.action_exchange] using MonoidalRightAction.actionHom_def f g
actionAssocIso_hom_naturality
| op f, op g, op h => by
apply Quiver.Hom.unop_inj
haveI := (αᵣ (unop _) (unop _) (unop _)).inv ≫= MonoidalRightAction.actionAssocIso_hom_naturality f g h
simp only [Iso.inv_hom_id_assoc] at this
simp [← this]
actionUnitIso_hom_naturality
_ := by
apply Quiver.Hom.unop_inj
simp
whiskerRight_actionHomLeft _ _ _ _
_ := by
apply Quiver.Hom.unop_inj
simp
actionHom_associator _ _ _
_ := by
apply Quiver.Hom.unop_inj
apply IsIso.inv_eq_inv.mp
simp
actionHom_leftUnitor _
_ := by
apply Quiver.Hom.unop_inj
apply IsIso.inv_eq_inv.mp
simp
actionHom_rightUnitor _
_ := by
apply Quiver.Hom.unop_inj
apply IsIso.inv_eq_inv.mp
simp
