rightActionOfMonoidalOppositeLeftAction

Lean4
/-- Define a right action of `C` on `D` from a left action of `Cᴹᵒᵖ` on `D` via
the formula `d ⊙ᵣ c := (mop c) ⊙ₗ d`. -/
@[simps -isSimp]
def rightActionOfMonoidalOppositeLeftAction [MonoidalLeftAction Cᴹᵒᵖ D] : MonoidalRightAction C D
    where
  actionObj d c := mop c ⊙ₗ d
  actionHomLeft {d d'} f c := mop c ⊴ₗ f
  actionHomRight d _ _ f := f.mop ⊵ₗ d
  actionHom {c c'} {d d'} f g := g.mop ⊙ₗₘ 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
      (α_ (mop c₃) (mop c₂) (mop c₁)).inv ⊵ₗ d ≫=
          MonoidalLeftAction.associator_actionHom (mop c₃) (mop c₂) (mop c₁) d |>.symm
Похожие утверждения