monoidalOppositeRightAction — Mathlib

Lean4
/-- Define a right action of `Cᴹᵒᵖ` on `D` from a left action of `C` on `D` via
the formula `d ⊙ᵣ mop c = c ⊙ₗ d`. -/
@[simps -isSimp]
def monoidalOppositeRightAction [MonoidalLeftAction C D] : MonoidalRightAction Cᴹᵒᵖ D
    where
  actionObj d c := unmop c ⊙ₗ d
  actionHomLeft {d d'} f c := unmop c ⊴ₗ f
  actionHomRight d _ _ f := f.unmop ⊵ₗ d
  actionHom {c c'} {d d'} f g := g.unmop ⊙ₗₘ f
  actionAssocIso _ _ _ := αₗ _ _ _
  actionUnitIso _ := λₗ _
  actionHom_def _ _ := MonoidalLeftAction.actionHom_def' _ _
  actionAssocIso_hom_naturality _ _ _ := MonoidalLeftAction.actionAssocIso_hom_naturality _ _ _
  actionUnitIso_hom_naturality _ := MonoidalLeftAction.actionUnitIso_hom_naturality _
  actionHom_associator c₁ c₂ c₃
    d := by
    simpa only [mop_tensorObj, mop_hom_associator, MonoidalLeftAction.inv_hom_actionHomLeft_assoc] using
      (α_ (unmop c₃) (unmop c₂) (unmop c₁)).inv ⊵ₗ d ≫=
          MonoidalLeftAction.associator_actionHom (unmop c₃) (unmop c₂) (unmop c₁) d |>.symm
Похожие утверждения