Lean4
/-- Define a left action of `Cᴹᵒᵖ` on `D` from a right action of `C` on `D` via
the formula `mop c ⊙ₗ d = d ⊙ᵣ c`. -/
@[simps -isSimp]
def monoidalOppositeLeftAction [MonoidalRightAction C D] : MonoidalLeftAction Cᴹᵒᵖ D
where
actionObj c d := d ⊙ᵣ unmop c
actionHomLeft {c c'} f d := d ⊴ᵣ f.unmop
actionHomRight c {d d'} f := f ⊵ᵣ unmop c
actionHom {c c'} {d d} f g := g ⊙ᵣₘ f.unmop
actionAssocIso _ _ _ := αᵣ _ _ _
actionUnitIso _ := ρᵣ _
actionHom_def _ _ := MonoidalRightAction.actionHom_def' _ _
actionAssocIso_hom_naturality _ _ _ := MonoidalRightAction.actionAssocIso_hom_naturality _ _ _
actionUnitIso_hom_naturality _ := MonoidalRightAction.actionUnitIso_hom_naturality _
rightUnitor_actionHom c d := MonoidalRightAction.actionHom_leftUnitor _ _
associator_actionHom c₁ c₂ c₃
d := by
simpa only [mop_tensorObj, mop_hom_associator, MonoidalRightAction.actionHomRight_inv_hom_assoc] using
(d ⊴ᵣ (α_ (unmop c₃) (unmop c₂) (unmop c₁)).inv) ≫=
MonoidalRightAction.actionHom_associator (unmop c₃) (unmop c₂) (unmop c₁) d |>.symm
