Commit 2025-07-05 12:52 aff540ef
View on Github →feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites (#25860)
Given a monoidal category C and a category D, we prove that a left (resp. right) Cᴹᵒᵖ-action on D gives a right (resp. left) C-action on D. Conversely, we show that left/right C-actions gives right/left Cᴹᵒᵖ-actions.
Estimated changes
added def CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction
added theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop
added theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop