Opposites

📁 Source: Mathlib/CategoryTheory/Monoidal/Action/Opposites.lean

Statistics

Metric	Count
Definitions leftActionOfMonoidalOppositeRightAction, leftActionOfOppositeLeftAction, monoidalOppositeLeftAction, oppositeLeftAction, monoidalOppositeRightAction, oppositeRightAction, rightActionOfMonoidalOppositeLeftAction, rightActionOfOppositeRightAction	8
Theorems leftActionOfMonoidalOppositeRightAction_actionAssocIso, leftActionOfMonoidalOppositeRightAction_actionHom, leftActionOfMonoidalOppositeRightAction_actionHomLeft, leftActionOfMonoidalOppositeRightAction_actionHomRight, leftActionOfMonoidalOppositeRightAction_actionObj, leftActionOfMonoidalOppositeRightAction_actionUnitIso, leftActionOfOppositeLeftAction_actionAssocIso, leftActionOfOppositeLeftAction_actionAssocIso_unop, leftActionOfOppositeLeftAction_actionHom, leftActionOfOppositeLeftAction_actionHomLeft, leftActionOfOppositeLeftAction_actionHomLeft_unop, leftActionOfOppositeLeftAction_actionHomRight, leftActionOfOppositeLeftAction_actionHom_unop, leftActionOfOppositeLeftAction_actionObj, leftActionOfOppositeLeftAction_actionObj_unop, leftActionOfOppositeLeftAction_actionRight_unop, leftActionOfOppositeLeftAction_actionUnitIso, monoidalOppositeLeftAction_actionAssocIso, monoidalOppositeLeftAction_actionAssocIso_mop_mop, monoidalOppositeLeftAction_actionHom, monoidalOppositeLeftAction_actionHomLeft, monoidalOppositeLeftAction_actionHomLeft_mop, monoidalOppositeLeftAction_actionHomRight, monoidalOppositeLeftAction_actionHom_mop_mop, monoidalOppositeLeftAction_actionObj, monoidalOppositeLeftAction_actionObj_mop, monoidalOppositeLeftAction_actionRight_mop, monoidalOppositeLeftAction_actionUnitIso, oppositeLeftAction_actionAssocIso, oppositeLeftAction_actionAssocIso_op, oppositeLeftAction_actionHom, oppositeLeftAction_actionHomLeft, oppositeLeftAction_actionHomLeft_op, oppositeLeftAction_actionHomRight, oppositeLeftAction_actionHom_op, oppositeLeftAction_actionObj, oppositeLeftAction_actionObj_op, oppositeLeftAction_actionRight_op, oppositeLeftAction_actionUnitIso, monoidalOppositeRightAction_actionAssocIso, monoidalOppositeRightAction_actionAssocIso_mop_mop, monoidalOppositeRightAction_actionHom, monoidalOppositeRightAction_actionHomLeft, monoidalOppositeRightAction_actionHomRight, monoidalOppositeRightAction_actionHomRight_mop, monoidalOppositeRightAction_actionHom_mop_mop, monoidalOppositeRightAction_actionObj, monoidalOppositeRightAction_actionObj_mop, monoidalOppositeRightAction_actionRight_mop, monoidalOppositeRightAction_actionUnitIso, oppositeRightAction_actionAssocIso, oppositeRightAction_actionAssocIso_op, oppositeRightAction_actionHom, oppositeRightAction_actionHomLeft, oppositeRightAction_actionHomLeft_op, oppositeRightAction_actionHomRight, oppositeRightAction_actionHom_op, oppositeRightAction_actionObj, oppositeRightAction_actionObj_op, oppositeRightAction_actionRight_op, oppositeRightAction_actionUnitIso, rightActionOfMonoidalOppositeLeftAction_actionAssocIso, rightActionOfMonoidalOppositeLeftAction_actionHom, rightActionOfMonoidalOppositeLeftAction_actionHomLeft, rightActionOfMonoidalOppositeLeftAction_actionHomRight, rightActionOfMonoidalOppositeLeftAction_actionObj, rightActionOfMonoidalOppositeLeftAction_actionUnitIso, rightActionOfOppositeRightAction_actionAssocIso, rightActionOfOppositeRightAction_actionAssocIso_unop, rightActionOfOppositeRightAction_actionHom, rightActionOfOppositeRightAction_actionHomLeft, rightActionOfOppositeRightAction_actionHomLeft_unop, rightActionOfOppositeRightAction_actionHomRight, rightActionOfOppositeRightAction_actionHom_unop, rightActionOfOppositeRightAction_actionObj, rightActionOfOppositeRightAction_actionObj_unop, rightActionOfOppositeRightAction_actionRight_unop, rightActionOfOppositeRightAction_actionUnitIso	78
Total	86

CategoryTheory.MonoidalCategory.MonoidalLeftAction

Definitions

Name	Category	Theorems
leftActionOfMonoidalOppositeRightAction 📖	CompOp	6 math math: leftActionOfMonoidalOppositeRightAction_actionObj, leftActionOfMonoidalOppositeRightAction_actionHom, leftActionOfMonoidalOppositeRightAction_actionAssocIso, leftActionOfMonoidalOppositeRightAction_actionUnitIso, leftActionOfMonoidalOppositeRightAction_actionHomLeft, leftActionOfMonoidalOppositeRightAction_actionHomRight
leftActionOfOppositeLeftAction 📖	CompOp	11 math math: leftActionOfOppositeLeftAction_actionHomRight, leftActionOfOppositeLeftAction_actionAssocIso, leftActionOfOppositeLeftAction_actionObj, leftActionOfOppositeLeftAction_actionHom_unop, leftActionOfOppositeLeftAction_actionUnitIso, leftActionOfOppositeLeftAction_actionHomLeft_unop, leftActionOfOppositeLeftAction_actionAssocIso_unop, leftActionOfOppositeLeftAction_actionRight_unop, leftActionOfOppositeLeftAction_actionObj_unop, leftActionOfOppositeLeftAction_actionHom, leftActionOfOppositeLeftAction_actionHomLeft
monoidalOppositeLeftAction 📖	CompOp	11 math math: monoidalOppositeLeftAction_actionHomLeft, monoidalOppositeLeftAction_actionHomRight, monoidalOppositeLeftAction_actionHomLeft_mop, monoidalOppositeLeftAction_actionUnitIso, monoidalOppositeLeftAction_actionHom_mop_mop, monoidalOppositeLeftAction_actionAssocIso, monoidalOppositeLeftAction_actionObj, monoidalOppositeLeftAction_actionObj_mop, monoidalOppositeLeftAction_actionHom, monoidalOppositeLeftAction_actionRight_mop, monoidalOppositeLeftAction_actionAssocIso_mop_mop
oppositeLeftAction 📖	CompOp	11 math math: oppositeLeftAction_actionHomRight, oppositeLeftAction_actionAssocIso, oppositeLeftAction_actionHomLeft_op, oppositeLeftAction_actionObj, oppositeLeftAction_actionRight_op, oppositeLeftAction_actionHom_op, oppositeLeftAction_actionHom, oppositeLeftAction_actionAssocIso_op, oppositeLeftAction_actionHomLeft, oppositeLeftAction_actionObj_op, oppositeLeftAction_actionUnitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftActionOfMonoidalOppositeRightAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfMonoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.mop	—	—
leftActionOfMonoidalOppositeRightAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfMonoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop	—	—
leftActionOfMonoidalOppositeRightAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfMonoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop	—	—
leftActionOfMonoidalOppositeRightAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfMonoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.mop	—	—
leftActionOfMonoidalOppositeRightAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfMonoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.mop	—	—
leftActionOfMonoidalOppositeRightAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfMonoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct	—	—
leftActionOfOppositeLeftAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction CategoryTheory.Iso.unop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Opposite.unop CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
leftActionOfOppositeLeftAction_actionAssocIso_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Opposite.unop CategoryTheory.Iso.unop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
leftActionOfOppositeLeftAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Quiver.Hom.op	—	—
leftActionOfOppositeLeftAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Quiver.Hom.op	—	—
leftActionOfOppositeLeftAction_actionHomLeft_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
leftActionOfOppositeLeftAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Quiver.Hom.op	—	—
leftActionOfOppositeLeftAction_actionHom_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
leftActionOfOppositeLeftAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op	—	—
leftActionOfOppositeLeftAction_actionObj_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
leftActionOfOppositeLeftAction_actionRight_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
leftActionOfOppositeLeftAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalLeftActionStruct leftActionOfOppositeLeftAction CategoryTheory.Iso.unop Opposite.op CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.symm	—	—
monoidalOppositeLeftAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.unmop	—	—
monoidalOppositeLeftAction_actionAssocIso_mop_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct	—	—
monoidalOppositeLeftAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.unmop Quiver.Hom.unmop	—	—
monoidalOppositeLeftAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.unmop Quiver.Hom.unmop	—	—
monoidalOppositeLeftAction_actionHomLeft_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct	—	—
monoidalOppositeLeftAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.unmop	—	—
monoidalOppositeLeftAction_actionHom_mop_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct	—	—
monoidalOppositeLeftAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct CategoryTheory.MonoidalOpposite.unmop	—	—
monoidalOppositeLeftAction_actionObj_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct	—	—
monoidalOppositeLeftAction_actionRight_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct	—	—
monoidalOppositeLeftAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalLeftActionStruct monoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct	—	—
oppositeLeftAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction CategoryTheory.Iso.op CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite.unop Opposite.op CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
oppositeLeftAction_actionAssocIso_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Opposite.op CategoryTheory.Iso.op CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
oppositeLeftAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite.unop Quiver.Hom.unop	—	—
oppositeLeftAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite.unop Quiver.Hom.unop	—	—
oppositeLeftAction_actionHomLeft_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj	—	—
oppositeLeftAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite.unop Quiver.Hom.unop	—	—
oppositeLeftAction_actionHom_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj	—	—
oppositeLeftAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Opposite.op Opposite.unop	—	—
oppositeLeftAction_actionObj_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Opposite.op	—	—
oppositeLeftAction_actionRight_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj	—	—
oppositeLeftAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalLeftActionStruct oppositeLeftAction CategoryTheory.Iso.op Opposite.unop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.symm	—	—

CategoryTheory.MonoidalCategory.MonoidalRightAction

Definitions

Name	Category	Theorems
monoidalOppositeRightAction 📖	CompOp	11 math math: monoidalOppositeRightAction_actionHomLeft, monoidalOppositeRightAction_actionAssocIso_mop_mop, monoidalOppositeRightAction_actionHom, monoidalOppositeRightAction_actionHomRight_mop, monoidalOppositeRightAction_actionAssocIso, monoidalOppositeRightAction_actionHomRight, monoidalOppositeRightAction_actionObj_mop, monoidalOppositeRightAction_actionHom_mop_mop, monoidalOppositeRightAction_actionObj, monoidalOppositeRightAction_actionRight_mop, monoidalOppositeRightAction_actionUnitIso
oppositeRightAction 📖	CompOp	11 math math: oppositeRightAction_actionObj, oppositeRightAction_actionHomRight, oppositeRightAction_actionAssocIso_op, oppositeRightAction_actionRight_op, oppositeRightAction_actionHomLeft, oppositeRightAction_actionHom_op, oppositeRightAction_actionHom, oppositeRightAction_actionHomLeft_op, oppositeRightAction_actionAssocIso, oppositeRightAction_actionObj_op, oppositeRightAction_actionUnitIso
rightActionOfMonoidalOppositeLeftAction 📖	CompOp	6 math math: rightActionOfMonoidalOppositeLeftAction_actionHom, rightActionOfMonoidalOppositeLeftAction_actionObj, rightActionOfMonoidalOppositeLeftAction_actionHomLeft, rightActionOfMonoidalOppositeLeftAction_actionUnitIso, rightActionOfMonoidalOppositeLeftAction_actionHomRight, rightActionOfMonoidalOppositeLeftAction_actionAssocIso
rightActionOfOppositeRightAction 📖	CompOp	11 math math: rightActionOfOppositeRightAction_actionRight_unop, rightActionOfOppositeRightAction_actionHom, rightActionOfOppositeRightAction_actionObj, rightActionOfOppositeRightAction_actionUnitIso, rightActionOfOppositeRightAction_actionAssocIso_unop, rightActionOfOppositeRightAction_actionObj_unop, rightActionOfOppositeRightAction_actionHom_unop, rightActionOfOppositeRightAction_actionAssocIso, rightActionOfOppositeRightAction_actionHomRight, rightActionOfOppositeRightAction_actionHomLeft, rightActionOfOppositeRightAction_actionHomLeft_unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monoidalOppositeRightAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.unmop	—	—
monoidalOppositeRightAction_actionAssocIso_mop_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct	—	—
monoidalOppositeRightAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.unmop Quiver.Hom.unmop	—	—
monoidalOppositeRightAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.unmop	—	—
monoidalOppositeRightAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.unmop Quiver.Hom.unmop	—	—
monoidalOppositeRightAction_actionHomRight_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct	—	—
monoidalOppositeRightAction_actionHom_mop_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct	—	—
monoidalOppositeRightAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.unmop	—	—
monoidalOppositeRightAction_actionObj_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct	—	—
monoidalOppositeRightAction_actionRight_mop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct	—	—
monoidalOppositeRightAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop toMonoidalRightActionStruct monoidalOppositeRightAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct	—	—
oppositeRightAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction CategoryTheory.Iso.op CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite.unop Opposite.op CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
oppositeRightAction_actionAssocIso_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Opposite.op CategoryTheory.Iso.op CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
oppositeRightAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite.unop Quiver.Hom.unop	—	—
oppositeRightAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite.unop Quiver.Hom.unop	—	—
oppositeRightAction_actionHomLeft_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj	—	—
oppositeRightAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite.unop Quiver.Hom.unop	—	—
oppositeRightAction_actionHom_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj	—	—
oppositeRightAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Opposite.op Opposite.unop	—	—
oppositeRightAction_actionObj_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Opposite.op	—	—
oppositeRightAction_actionRight_op 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj	—	—
oppositeRightAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso Opposite CategoryTheory.Category.opposite CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp toMonoidalRightActionStruct oppositeRightAction CategoryTheory.Iso.op Opposite.unop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.symm	—	—
rightActionOfMonoidalOppositeLeftAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfMonoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.mop	—	—
rightActionOfMonoidalOppositeLeftAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfMonoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop	—	—
rightActionOfMonoidalOppositeLeftAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfMonoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.mop	—	—
rightActionOfMonoidalOppositeLeftAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfMonoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop	—	—
rightActionOfMonoidalOppositeLeftAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfMonoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct CategoryTheory.MonoidalOpposite.mop	—	—
rightActionOfMonoidalOppositeLeftAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfMonoidalOppositeLeftAction CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct	—	—
rightActionOfOppositeRightAction_actionAssocIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction CategoryTheory.Iso.unop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Opposite.unop CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
rightActionOfOppositeRightAction_actionAssocIso_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Opposite.unop CategoryTheory.Iso.unop CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.symm	—	—
rightActionOfOppositeRightAction_actionHom 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Quiver.Hom.op	—	—
rightActionOfOppositeRightAction_actionHomLeft 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Quiver.Hom.op	—	—
rightActionOfOppositeRightAction_actionHomLeft_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
rightActionOfOppositeRightAction_actionHomRight 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op Quiver.Hom.op	—	—
rightActionOfOppositeRightAction_actionHom_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
rightActionOfOppositeRightAction_actionObj 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op	—	—
rightActionOfOppositeRightAction_actionObj_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
rightActionOfOppositeRightAction_actionRight_unop 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
rightActionOfOppositeRightAction_actionUnitIso 📖	mathematical	—	CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct toMonoidalRightActionStruct rightActionOfOppositeRightAction CategoryTheory.Iso.unop Opposite.op CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.symm	—	—

---

← Back to Index