leftActionOfMonoidalOppositeRightAction

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