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