Opposite

📁 Source: Mathlib/CategoryTheory/Monoidal/Opposite.lean

Statistics

Metric	Count
Definitions mop, unmop, MonoidalOpposite, monoidalOppositeCategory, mopEquiv, mopMopEquivalence, mopMopEquivalenceFunctorMonoidal, mopMopEquivalenceInverseMonoidal, tensorIso, tensorLeftIso, tensorLeftMopIso, tensorLeftUnmopIso, tensorRightIso, tensorRightMopIso, tensorRightUnmopIso, unmop, unmopEquiv, «term_ᴹᵒᵖ», instMonoidalOppositeFunctorOpOpEquivalence, instMonoidalOppositeInverseOpOpEquivalence, monoidalCategoryMop, monoidalCategoryOp, monoidalOpOp, monoidalUnopUnop, mopFunctor, unmopFunctor, mop, unmop	28
Theorems instMonoidalOppositeMop, instUnmopOfMonoidalOpposite, hom_ext, mopEquiv_counitIso, mopEquiv_functor, mopEquiv_inverse, mopEquiv_unitIso, mopMopEquivalenceFunctorMonoidal_δ, mopMopEquivalenceFunctorMonoidal_ε, mopMopEquivalenceFunctorMonoidal_η, mopMopEquivalenceFunctorMonoidal_μ, mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, mopMopEquivalenceInverseMonoidal_η_unmop_unmop, mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, mopMopEquivalence_counitIso_hom_app, mopMopEquivalence_counitIso_inv_app, mopMopEquivalence_functor_map, mopMopEquivalence_functor_obj, mopMopEquivalence_inverse_map_unmop_unmop, mopMopEquivalence_inverse_obj_unmop_unmop, mopMopEquivalence_unitIso_hom_app_unmop_unmop, mopMopEquivalence_unitIso_inv_app_unmop_unmop, mop_inj_iff, mop_injective, mop_unmop, tensorIso_hom_app_unmop, tensorIso_inv_app_unmop, tensorLeftIso_hom_app_unmop, tensorLeftIso_inv_app_unmop, tensorLeftMopIso_hom_app_unmop, tensorLeftMopIso_inv_app_unmop, tensorLeftUnmopIso_hom_app, tensorLeftUnmopIso_inv_app, tensorRightIso_hom_app_unmop, tensorRightIso_inv_app_unmop, tensorRightMopIso_hom_app_unmop, tensorRightMopIso_inv_app_unmop, tensorRightUnmopIso_hom_app, tensorRightUnmopIso_inv_app, unmopEquiv_counitIso_hom_app, unmopEquiv_counitIso_inv_app, unmopEquiv_functor_map, unmopEquiv_functor_obj, unmopEquiv_inverse_map_unmop, unmopEquiv_inverse_obj_unmop, unmopEquiv_unitIso_hom_app_unmop, unmopEquiv_unitIso_inv_app_unmop, unmop_inj_iff, unmop_injective, unmop_mop, instIsMonoidalMonoidalOppositeMopMopEquivalence, instIsMonoidalOppositeOpOpEquivalence, monoidalOpOp_δ, monoidalOpOp_ε, monoidalOpOp_η, monoidalOpOp_μ, monoidalUnopUnop_δ, monoidalUnopUnop_ε, monoidalUnopUnop_η, monoidalUnopUnop_μ, mopFunctor_map, mopFunctor_obj, mop_associator, mop_comp, mop_hom_associator, mop_hom_leftUnitor, mop_hom_rightUnitor, mop_id, mop_id_unmop, mop_inv_associator, mop_inv_leftUnitor, mop_inv_rightUnitor, mop_leftUnitor, mop_rightUnitor, mop_tensorHom, mop_tensorObj, mop_tensorUnit, mop_whiskerLeft, mop_whiskerRight, op_associator, op_hom_associator, op_hom_leftUnitor, op_hom_rightUnitor, op_inv_associator, op_inv_leftUnitor, op_inv_rightUnitor, op_leftUnitor, op_rightUnitor, op_tensorHom, op_tensorObj, op_tensorUnit, op_tensor_op, op_whiskerLeft, op_whiskerRight, unmopFunctor_map, unmopFunctor_obj, unmop_associator, unmop_comp, unmop_hom_associator, unmop_hom_leftUnitor, unmop_hom_rightUnitor, unmop_id, unmop_id_mop, unmop_inv_associator, unmop_inv_leftUnitor, unmop_inv_rightUnitor, unmop_leftUnitor, unmop_rightUnitor, unmop_tensorHom, unmop_tensorObj, unmop_tensorUnit, unmop_whiskerLeft, unmop_whiskerRight, unop_associator, unop_hom_associator, unop_hom_leftUnitor, unop_hom_rightUnitor, unop_inv_associator, unop_inv_leftUnitor, unop_inv_rightUnitor, unop_leftUnitor, unop_rightUnitor, unop_tensorHom, unop_tensorObj, unop_tensorUnit, unop_tensor_unop, unop_whiskerLeft, unop_whiskerRight, mop_inj, mop_unmop, unmop_inj, unmop_mop	133
Total	161

CategoryTheory

Definitions

Name	Category	Theorems
MonoidalOpposite 📖	CompData	174 math math: MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft, mop_hom_leftUnitor, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, MonoidalOpposite.unmop_hom_braiding, MonoidalOpposite.unmopFunctor_δ, unmop_hom_rightUnitor, MonoidalOpposite.tensorLeftMopIso_hom_app_unmop, MonoidalOpposite.mopMopEquivalence_functor_obj, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj, unmopFunctor_obj, mop_comp, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft, MonoidalOpposite.mopFunctor_ε, mop_hom_rightUnitor, MonObj.mopEquivCompForgetIso_hom_app_unmop, unmopFunctor_map, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, mop_inv_associator, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom, mopFunctor_map, MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app, MonoidalOpposite.unmopEquiv_inverse_map_unmop, mopFunctor_obj, leftDualFunctor_obj, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft, unmop_hom_associator, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app, mop_associator, MonoidalOpposite.mopMopEquivalence_unitIso_hom_app_unmop_unmop, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop, MonoidalOpposite.tensorLeftUnmopIso_inv_app, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight, MonObj.mop_isMonHom, Quiver.Hom.mop_inj, MonoidalOpposite.unmopEquiv_inverse_obj_unmop, MonObj.mopEquiv_functor_obj_mon_one_unmop, MonObj.unmopMonObj_one, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom, MonoidalOpposite.tensorIso_hom_app_unmop, mop_whiskerLeft, mop_tensorObj, MonoidalOpposite.mopMopEquivalence_inverse_map_unmop_unmop, MonoidalOpposite.mopFunctor_η, unmop_inv_leftUnitor, MonoidalOpposite.mopEquiv_unitIso, unmop_inv_associator, unmop_tensorUnit, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_μ, mop_id, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_ε, unmop_id, MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop, MonoidalOpposite.mop_inv_braiding, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj, MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso, unmop_leftUnitor, unmop_comp, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop, MonObj.mopEquiv_inverse_map_hom, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight, mop_rightUnitor, MonObj.mopEquiv_inverse_obj_X, MonoidalOpposite.tensorRightUnmopIso_inv_app, leftDualFunctor_map, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso, MonoidalOpposite.unmopEquiv_counitIso_hom_app, rightDualFunctor_map, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft, MonObj.mopEquiv_functor_map_hom_unmop, MonoidalOpposite.tensorLeftUnmopIso_hom_app, MonoidalOpposite.mopMopEquivalence_functor_map, MonObj.mopEquivCompForgetIso_inv_app_unmop, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionObj, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso, MonoidalOpposite.mopMopEquivalence_counitIso_inv_app, MonoidalOpposite.tensorRightIso_hom_app_unmop, MonObj.mopEquiv_unitIso_hom_app_hom, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft, MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app, MonoidalOpposite.tensorRightIso_inv_app_unmop, MonObj.mopEquiv_functor_obj_X_unmop, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app, unmop_rightUnitor, MonoidalOpposite.mopFunctor_μ, MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop, MonoidalOpposite.mop_injective, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop, rightDualFunctor_obj, MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_obj, MonoidalOpposite.mopMopEquivalence_unitIso_inv_app_unmop_unmop, unmop_tensorHom, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, mop_inv_leftUnitor, MonoidalOpposite.unmopFunctor_μ, MonoidalOpposite.tensorRightMopIso_inv_app_unmop, MonObj.unmopMonObj_mul, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_δ, mop_inv_rightUnitor, mop_leftUnitor, unmop_inv_rightUnitor, MonObj.mopEquiv_functor_obj_mon_mul_unmop, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_η, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop, MonoidalOpposite.mop_hom_braiding, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomRight, unmop_tensorObj, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, MonoidalOpposite.unmop_inv_braiding, MonObj.mopMonObj_one_unmop, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop, MonoidalOpposite.mopEquiv_inverse, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight, unmop_whiskerRight, MonObj.mopEquiv_inverse_obj_mon_one, MonoidalOpposite.tensorLeftIso_hom_app_unmop, MonoidalOpposite.mop_braiding, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, MonoidalOpposite.unmopEquiv_counitIso_inv_app, unmop_associator, MonoidalOpposite.unmopEquiv_functor_map, MonoidalOpposite.tensorRightMopIso_hom_app_unmop, MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_map, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso, mop_hom_associator, MonoidalOpposite.mopMopEquivalence_inverse_obj_unmop_unmop, instIsMonoidalMonoidalOppositeMopMopEquivalence, MonoidalOpposite.unmopFunctor_η, MonObj.mopEquiv_unitIso_inv_app_hom, MonoidalOpposite.unmopFunctor_ε, Quiver.Hom.unmop_inj, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, unmop_whiskerLeft, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app, MonoidalOpposite.tensorRightUnmopIso_hom_app, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app, MonoidalOpposite.tensorLeftMopIso_inv_app_unmop, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop, unmop_hom_leftUnitor, MonObj.mopMonObj_mul_unmop, MonoidalOpposite.unmop_injective, MonoidalOpposite.mopFunctor_δ, IsIso.instMonoidalOppositeMop, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop, MonoidalOpposite.tensorLeftIso_inv_app_unmop, MonoidalOpposite.tensorIso_inv_app_unmop, MonoidalOpposite.mopMopEquivalence_counitIso_hom_app, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom, MonoidalOpposite.unmop_braiding, mop_whiskerRight, mop_tensorUnit, MonoidalOpposite.mopEquiv_functor, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_η_unmop_unmop, mop_tensorHom, mop_id_unmop, MonoidalOpposite.unmopEquiv_functor_obj, unmop_id_mop, MonoidalOpposite.mopEquiv_counitIso, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso, MonObj.mopEquiv_inverse_obj_mon_mul
instMonoidalOppositeFunctorOpOpEquivalence 📖	CompOp	1 math math: instIsMonoidalOppositeOpOpEquivalence
instMonoidalOppositeInverseOpOpEquivalence 📖	CompOp	1 math math: instIsMonoidalOppositeOpOpEquivalence
monoidalCategoryMop 📖	CompOp	126 math math: mop_hom_leftUnitor, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, MonoidalOpposite.unmop_hom_braiding, MonoidalOpposite.unmopFunctor_δ, unmop_hom_rightUnitor, MonoidalOpposite.tensorLeftMopIso_hom_app_unmop, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft, MonoidalOpposite.mopFunctor_ε, mop_hom_rightUnitor, MonObj.mopEquivCompForgetIso_hom_app_unmop, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, mop_inv_associator, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft, unmop_hom_associator, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app, mop_associator, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop, MonoidalOpposite.tensorLeftUnmopIso_inv_app, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight, MonObj.mop_isMonHom, MonObj.mopEquiv_functor_obj_mon_one_unmop, MonObj.unmopMonObj_one, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom, MonoidalOpposite.tensorIso_hom_app_unmop, mop_whiskerLeft, mop_tensorObj, MonoidalOpposite.mopFunctor_η, unmop_inv_leftUnitor, unmop_inv_associator, unmop_tensorUnit, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_μ, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_ε, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop, MonoidalOpposite.mop_inv_braiding, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso, unmop_leftUnitor, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop, MonObj.mopEquiv_inverse_map_hom, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight, mop_rightUnitor, MonObj.mopEquiv_inverse_obj_X, MonoidalOpposite.tensorRightUnmopIso_inv_app, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft, MonObj.mopEquiv_functor_map_hom_unmop, MonoidalOpposite.tensorLeftUnmopIso_hom_app, MonObj.mopEquivCompForgetIso_inv_app_unmop, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso, MonoidalOpposite.tensorRightIso_hom_app_unmop, MonObj.mopEquiv_unitIso_hom_app_hom, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft, MonoidalOpposite.tensorRightIso_inv_app_unmop, MonObj.mopEquiv_functor_obj_X_unmop, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app, unmop_rightUnitor, MonoidalOpposite.mopFunctor_μ, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop, unmop_tensorHom, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, mop_inv_leftUnitor, MonoidalOpposite.unmopFunctor_μ, MonoidalOpposite.tensorRightMopIso_inv_app_unmop, MonObj.unmopMonObj_mul, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_δ, mop_inv_rightUnitor, mop_leftUnitor, unmop_inv_rightUnitor, MonObj.mopEquiv_functor_obj_mon_mul_unmop, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj, MonoidalOpposite.mopMopEquivalenceFunctorMonoidal_η, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop, MonoidalOpposite.mop_hom_braiding, unmop_tensorObj, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, MonoidalOpposite.unmop_inv_braiding, MonObj.mopMonObj_one_unmop, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight, unmop_whiskerRight, MonObj.mopEquiv_inverse_obj_mon_one, MonoidalOpposite.tensorLeftIso_hom_app_unmop, MonoidalOpposite.mop_braiding, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, unmop_associator, MonoidalOpposite.tensorRightMopIso_hom_app_unmop, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj, MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso, mop_hom_associator, instIsMonoidalMonoidalOppositeMopMopEquivalence, MonoidalOpposite.unmopFunctor_η, MonObj.mopEquiv_unitIso_inv_app_hom, MonoidalOpposite.unmopFunctor_ε, MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, unmop_whiskerLeft, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app, MonoidalOpposite.tensorRightUnmopIso_hom_app, MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight, MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app, MonoidalOpposite.tensorLeftMopIso_inv_app_unmop, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop, unmop_hom_leftUnitor, MonObj.mopMonObj_mul_unmop, MonoidalOpposite.mopFunctor_δ, MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop, MonoidalOpposite.tensorLeftIso_inv_app_unmop, MonoidalOpposite.tensorIso_inv_app_unmop, MonoidalOpposite.unmop_braiding, mop_whiskerRight, mop_tensorUnit, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, MonoidalOpposite.mopMopEquivalenceInverseMonoidal_η_unmop_unmop, mop_tensorHom, MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso, MonObj.mopEquiv_inverse_obj_mon_mul
monoidalCategoryOp 📖	CompOp	132 math math: Comon.tensorObj_comul', MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionRight_unop, op_hom_leftUnitor, op_inv_associator, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomRight, op_tensorHom, Comon.MonOpOpToComon_obj, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso, unop_tensorHom, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionObj, Comon.ComonToMonOpOp_obj, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomRight, op_whiskerRight, unop_inv_associator, Comon.Comon_EquivMon_OpOp_counitIso, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso, Comon.monoidal_rightUnitor_inv_hom, unop_tensor_unop, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomRight, unop_tensorUnit, monoidalOpOp_δ, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, op_tensorUnit, Comon.Comon_EquivMon_OpOp_functor, op_tensorObj, Comon.MonOpOpToComon_map_hom, op_whiskerLeft, BraidedCategory.unop_tensorμ, op_tensor_op, Comon.ComonToMonOpOp_map, op_inv_braiding, Comon.monoidal_whiskerLeft_hom, unop_whiskerRight, op_leftUnitor, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, CommAlgCat.mul_op_of_unop_hom, Comon.monoidal_leftUnitor_hom_hom, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionObj, unop_inv_leftUnitor, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom_unop, monoidalUnopUnop_ε, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionObj, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionUnitIso, monoidalUnopUnop_δ, Comon.MonOpOpToComonObj_comon_comul, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso_unop, Comon.monoidal_whiskerRight_hom, op_braiding, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft_op, monoidalOpOp_μ, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionObj_unop, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionUnitIso, monoidalOpOp_η, Comon.monoidal_associator_hom_hom, op_inv_leftUnitor, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso_op, op_rightUnitor, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft_unop, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionObj, op_hom_braiding, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionRight_op, unop_leftUnitor, unop_braiding, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom_unop, Comon.Comon_EquivMon_OpOp_unitIso, op_hom_associator, op_hom_rightUnitor, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso_unop, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, monoidalOpOp_ε, CommAlgCat.one_op_of_unop_hom, unop_rightUnitor, Comon.monoidal_tensorUnit_comon_comul, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionRight_op, instIsMonoidalOppositeOpOpEquivalence, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom_op, op_inv_rightUnitor, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso, unop_inv_braiding, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionRight_unop, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomRight, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionObj_unop, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom, Comon.monoidal_leftUnitor_inv_hom, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft, monoidalUnopUnop_μ, Comon.MonOpOpToComonObj_X, Comon.monoidal_rightUnitor_hom_hom, Comon.ComonToMonOpOpObj_mon_mul, commBialgCatEquivComonCommAlgCat_inverse_obj, BraidedCategory.op_tensorμ, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso_op, unop_hom_rightUnitor, unop_hom_braiding, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom_op, Comon.monoidal_associator_inv_hom, Comon.Comon_EquivMon_OpOp_inverse, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft_op, Comon.monoidal_tensorUnit_comon_counit, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso, unop_hom_associator, op_associator, unop_tensorObj, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionObj_op, instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, unop_inv_rightUnitor, Comon.monoidal_tensorHom_hom, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, unop_hom_leftUnitor, unop_associator, Comon.MonOpOpToComonObj_comon_counit, monoidalUnopUnop_η, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionObj_op, unop_whiskerLeft, MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionUnitIso, Comon.monoidal_tensorObj_comon_counit, MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft, MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft_unop, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionUnitIso, Comon.ComonToMonOpOpObj_X, Comon.monoidal_tensorObj_comon_comul, Comon.ComonToMonOpOpObj_mon_one
monoidalOpOp 📖	CompOp	4 math math: monoidalOpOp_δ, monoidalOpOp_μ, monoidalOpOp_η, monoidalOpOp_ε
monoidalUnopUnop 📖	CompOp	4 math math: monoidalUnopUnop_ε, monoidalUnopUnop_δ, monoidalUnopUnop_μ, monoidalUnopUnop_η
mopFunctor 📖	CompOp	24 math math: MonoidalOpposite.tensorLeftMopIso_hom_app_unmop, MonoidalOpposite.mopFunctor_ε, mopFunctor_map, mopFunctor_obj, MonoidalOpposite.tensorLeftUnmopIso_inv_app, MonoidalOpposite.tensorIso_hom_app_unmop, MonoidalOpposite.mopFunctor_η, MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop, MonoidalOpposite.tensorRightUnmopIso_inv_app, MonoidalOpposite.tensorLeftUnmopIso_hom_app, MonoidalOpposite.tensorRightIso_hom_app_unmop, MonoidalOpposite.tensorRightIso_inv_app_unmop, MonoidalOpposite.mopFunctor_μ, MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop, MonoidalOpposite.tensorRightMopIso_inv_app_unmop, MonoidalOpposite.tensorLeftIso_hom_app_unmop, MonoidalOpposite.tensorRightMopIso_hom_app_unmop, MonoidalOpposite.tensorRightUnmopIso_hom_app, MonoidalOpposite.tensorLeftMopIso_inv_app_unmop, MonoidalOpposite.mopFunctor_δ, MonoidalOpposite.tensorLeftIso_inv_app_unmop, MonoidalOpposite.tensorIso_inv_app_unmop, MonoidalOpposite.mopEquiv_functor, MonoidalOpposite.mopEquiv_counitIso
unmopFunctor 📖	CompOp	24 math math: MonoidalOpposite.unmopFunctor_δ, MonoidalOpposite.tensorLeftMopIso_hom_app_unmop, unmopFunctor_obj, unmopFunctor_map, MonoidalOpposite.tensorLeftUnmopIso_inv_app, MonoidalOpposite.tensorIso_hom_app_unmop, MonoidalOpposite.unmopEquiv_unitIso_inv_app_unmop, MonoidalOpposite.tensorRightUnmopIso_inv_app, MonoidalOpposite.tensorLeftUnmopIso_hom_app, MonoidalOpposite.tensorRightIso_hom_app_unmop, MonoidalOpposite.tensorRightIso_inv_app_unmop, MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop, MonoidalOpposite.unmopFunctor_μ, MonoidalOpposite.tensorRightMopIso_inv_app_unmop, MonoidalOpposite.mopEquiv_inverse, MonoidalOpposite.tensorLeftIso_hom_app_unmop, MonoidalOpposite.tensorRightMopIso_hom_app_unmop, MonoidalOpposite.unmopFunctor_η, MonoidalOpposite.unmopFunctor_ε, MonoidalOpposite.tensorRightUnmopIso_hom_app, MonoidalOpposite.tensorLeftMopIso_inv_app_unmop, MonoidalOpposite.tensorLeftIso_inv_app_unmop, MonoidalOpposite.tensorIso_inv_app_unmop, MonoidalOpposite.mopEquiv_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMonoidalMonoidalOppositeMopMopEquivalence 📖	mathematical	—	Equivalence.IsMonoidal MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mopMopEquivalence MonoidalOpposite.mopMopEquivalenceFunctorMonoidal MonoidalOpposite.mopMopEquivalenceInverseMonoidal	—	Functor.isoWhiskerRight_trans Iso.trans_assoc Category.comp_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight
instIsMonoidalOppositeOpOpEquivalence 📖	mathematical	—	Equivalence.IsMonoidal Opposite Category.opposite monoidalCategoryOp opOpEquivalence instMonoidalOppositeFunctorOpOpEquivalence instMonoidalOppositeInverseOpOpEquivalence	—	Category.comp_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight
monoidalOpOp_δ 📖	mathematical	—	Functor.OplaxMonoidal.δ Opposite Category.opposite monoidalCategoryOp opOp Functor.Monoidal.toOplaxMonoidal monoidalOpOp CategoryStruct.id CategoryStruct.opposite Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalOpOp_ε 📖	mathematical	—	Functor.LaxMonoidal.ε Opposite Category.opposite monoidalCategoryOp opOp Functor.Monoidal.toLaxMonoidal monoidalOpOp CategoryStruct.id CategoryStruct.opposite Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalOpOp_η 📖	mathematical	—	Functor.OplaxMonoidal.η Opposite Category.opposite monoidalCategoryOp opOp Functor.Monoidal.toOplaxMonoidal monoidalOpOp CategoryStruct.id CategoryStruct.opposite Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalOpOp_μ 📖	mathematical	—	Functor.LaxMonoidal.μ Opposite Category.opposite monoidalCategoryOp opOp Functor.Monoidal.toLaxMonoidal monoidalOpOp CategoryStruct.id CategoryStruct.opposite Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Functor.obj	—	—
monoidalUnopUnop_δ 📖	mathematical	—	Functor.OplaxMonoidal.δ Opposite Category.opposite monoidalCategoryOp unopUnop Functor.Monoidal.toOplaxMonoidal monoidalUnopUnop CategoryStruct.id Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalUnopUnop_ε 📖	mathematical	—	Functor.LaxMonoidal.ε Opposite Category.opposite monoidalCategoryOp unopUnop Functor.Monoidal.toLaxMonoidal monoidalUnopUnop CategoryStruct.id Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalUnopUnop_η 📖	mathematical	—	Functor.OplaxMonoidal.η Opposite Category.opposite monoidalCategoryOp unopUnop Functor.Monoidal.toOplaxMonoidal monoidalUnopUnop CategoryStruct.id Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalUnopUnop_μ 📖	mathematical	—	Functor.LaxMonoidal.μ Opposite Category.opposite monoidalCategoryOp unopUnop Functor.Monoidal.toLaxMonoidal monoidalUnopUnop CategoryStruct.id Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Functor.obj	—	—
mopFunctor_map 📖	mathematical	—	Functor.map MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory mopFunctor Quiver.Hom.mop	—	—
mopFunctor_obj 📖	mathematical	—	Functor.obj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory mopFunctor MonoidalOpposite.mop	—	—
mop_associator 📖	mathematical	—	Iso.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.associator Iso.symm MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
mop_comp 📖	mathematical	—	Quiver.Hom.mop CategoryStruct.comp Category.toCategoryStruct MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalOpposite.mop	—	—
mop_hom_associator 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Iso.hom MonoidalCategoryStruct.associator Iso.inv MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
mop_hom_leftUnitor 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.leftUnitor MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop MonoidalCategoryStruct.rightUnitor	—	—
mop_hom_rightUnitor 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.rightUnitor MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop MonoidalCategoryStruct.leftUnitor	—	—
mop_id 📖	mathematical	—	Quiver.Hom.mop CategoryStruct.id Category.toCategoryStruct MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalOpposite.mop	—	—
mop_id_unmop 📖	mathematical	—	Quiver.Hom.mop MonoidalOpposite.unmop CategoryStruct.id Category.toCategoryStruct MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory	—	—
mop_inv_associator 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Iso.inv MonoidalCategoryStruct.associator Iso.hom MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
mop_inv_leftUnitor 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop MonoidalCategoryStruct.rightUnitor	—	—
mop_inv_rightUnitor 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop MonoidalCategoryStruct.leftUnitor	—	—
mop_leftUnitor 📖	mathematical	—	Iso.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.rightUnitor MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
mop_rightUnitor 📖	mathematical	—	Iso.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.rightUnitor MonoidalCategoryStruct.leftUnitor MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
mop_tensorHom 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorHom MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
mop_tensorObj 📖	mathematical	—	MonoidalOpposite.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop	—	—
mop_tensorUnit 📖	mathematical	—	MonoidalOpposite.mop MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop	—	—
mop_whiskerLeft 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.whiskerLeft MonoidalCategoryStruct.whiskerRight MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
mop_whiskerRight 📖	mathematical	—	Quiver.Hom.mop MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.whiskerRight MonoidalCategoryStruct.whiskerLeft MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory monoidalCategoryMop MonoidalOpposite.mop	—	—
op_associator 📖	mathematical	—	Iso.op MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.associator Iso.symm Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_hom_associator 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Iso.hom MonoidalCategoryStruct.associator Iso.inv Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_hom_leftUnitor 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.leftUnitor Iso.inv Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_hom_rightUnitor 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.rightUnitor Iso.inv Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_inv_associator 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Iso.inv MonoidalCategoryStruct.associator Iso.hom Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_inv_leftUnitor 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor Iso.hom Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_inv_rightUnitor 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor Iso.hom Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_leftUnitor 📖	mathematical	—	Iso.op MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.leftUnitor Iso.symm Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_rightUnitor 📖	mathematical	—	Iso.op MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.rightUnitor Iso.symm Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_tensorHom 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorHom Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_tensorObj 📖	mathematical	—	Opposite.op MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Opposite Category.opposite monoidalCategoryOp	—	—
op_tensorUnit 📖	mathematical	—	Opposite.op MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct Opposite Category.opposite monoidalCategoryOp	—	—
op_tensor_op 📖	mathematical	—	MonoidalCategoryStruct.tensorHom Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj	—	—
op_whiskerLeft 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.whiskerLeft Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
op_whiskerRight 📖	mathematical	—	Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.whiskerRight Opposite Category.opposite monoidalCategoryOp Opposite.op	—	—
unmopFunctor_map 📖	mathematical	—	Functor.map MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory unmopFunctor Quiver.Hom.unmop	—	—
unmopFunctor_obj 📖	mathematical	—	Functor.obj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory unmopFunctor MonoidalOpposite.unmop	—	—
unmop_associator 📖	mathematical	—	Iso.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.associator Iso.symm MonoidalOpposite.unmop	—	—
unmop_comp 📖	mathematical	—	Quiver.Hom.unmop CategoryStruct.comp MonoidalOpposite Category.toCategoryStruct MonoidalOpposite.monoidalOppositeCategory MonoidalOpposite.unmop	—	—
unmop_hom_associator 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop Iso.hom MonoidalCategoryStruct.associator Iso.inv MonoidalOpposite.unmop	—	—
unmop_hom_leftUnitor 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.leftUnitor MonoidalOpposite.unmop MonoidalCategoryStruct.rightUnitor	—	—
unmop_hom_rightUnitor 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.rightUnitor MonoidalOpposite.unmop MonoidalCategoryStruct.leftUnitor	—	—
unmop_id 📖	mathematical	—	Quiver.Hom.unmop CategoryStruct.id MonoidalOpposite Category.toCategoryStruct MonoidalOpposite.monoidalOppositeCategory MonoidalOpposite.unmop	—	—
unmop_id_mop 📖	mathematical	—	Quiver.Hom.unmop MonoidalOpposite.mop CategoryStruct.id MonoidalOpposite Category.toCategoryStruct MonoidalOpposite.monoidalOppositeCategory	—	—
unmop_inv_associator 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop Iso.inv MonoidalCategoryStruct.associator Iso.hom MonoidalOpposite.unmop	—	—
unmop_inv_leftUnitor 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor MonoidalOpposite.unmop MonoidalCategoryStruct.rightUnitor	—	—
unmop_inv_rightUnitor 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor MonoidalOpposite.unmop MonoidalCategoryStruct.leftUnitor	—	—
unmop_leftUnitor 📖	mathematical	—	Iso.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.leftUnitor MonoidalCategoryStruct.rightUnitor MonoidalOpposite.unmop	—	—
unmop_rightUnitor 📖	mathematical	—	Iso.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.rightUnitor MonoidalCategoryStruct.leftUnitor MonoidalOpposite.unmop	—	—
unmop_tensorHom 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.tensorHom MonoidalOpposite.unmop	—	—
unmop_tensorObj 📖	mathematical	—	MonoidalOpposite.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop	—	—
unmop_tensorUnit 📖	mathematical	—	MonoidalOpposite.unmop MonoidalCategoryStruct.tensorUnit MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop	—	—
unmop_whiskerLeft 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.whiskerLeft MonoidalCategoryStruct.whiskerRight MonoidalOpposite.unmop	—	—
unmop_whiskerRight 📖	mathematical	—	Quiver.Hom.unmop MonoidalCategoryStruct.tensorObj MonoidalOpposite MonoidalOpposite.monoidalOppositeCategory MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryMop MonoidalCategoryStruct.whiskerRight MonoidalCategoryStruct.whiskerLeft MonoidalOpposite.unmop	—	—
unop_associator 📖	mathematical	—	Iso.unop MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.associator Iso.symm Opposite.unop	—	—
unop_hom_associator 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp Iso.hom MonoidalCategoryStruct.associator Iso.inv Opposite.unop	—	—
unop_hom_leftUnitor 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.leftUnitor Iso.inv Opposite.unop	—	—
unop_hom_rightUnitor 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.tensorUnit Iso.hom MonoidalCategoryStruct.rightUnitor Iso.inv Opposite.unop	—	—
unop_inv_associator 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp Iso.inv MonoidalCategoryStruct.associator Iso.hom Opposite.unop	—	—
unop_inv_leftUnitor 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.leftUnitor Iso.hom Opposite.unop	—	—
unop_inv_rightUnitor 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.tensorUnit Iso.inv MonoidalCategoryStruct.rightUnitor Iso.hom Opposite.unop	—	—
unop_leftUnitor 📖	mathematical	—	Iso.unop MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.leftUnitor Iso.symm Opposite.unop	—	—
unop_rightUnitor 📖	mathematical	—	Iso.unop MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.tensorUnit MonoidalCategoryStruct.rightUnitor Iso.symm Opposite.unop	—	—
unop_tensorHom 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.tensorHom Opposite.unop	—	—
unop_tensorObj 📖	mathematical	—	Opposite.unop MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp	—	—
unop_tensorUnit 📖	mathematical	—	Opposite.unop MonoidalCategoryStruct.tensorUnit Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp	—	—
unop_tensor_unop 📖	mathematical	—	MonoidalCategoryStruct.tensorHom MonoidalCategory.toMonoidalCategoryStruct Opposite.unop Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite monoidalCategoryOp	—	—
unop_whiskerLeft 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.whiskerLeft Opposite.unop	—	—
unop_whiskerRight 📖	mathematical	—	Quiver.Hom.unop CategoryStruct.toQuiver Category.toCategoryStruct MonoidalCategoryStruct.tensorObj Opposite Category.opposite MonoidalCategory.toMonoidalCategoryStruct monoidalCategoryOp MonoidalCategoryStruct.whiskerRight Opposite.unop	—	—

CategoryTheory.IsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMonoidalOppositeMop 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalOpposite.mop Quiver.Hom.mop	—	CategoryTheory.Functor.map_isIso
instUnmopOfMonoidalOpposite 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.MonoidalOpposite.unmop Quiver.Hom.unmop	—	CategoryTheory.Functor.map_isIso

CategoryTheory.Iso

Definitions

Name	Category	Theorems
mop 📖	CompOp	4 math math: CategoryTheory.mop_associator, CategoryTheory.mop_rightUnitor, CategoryTheory.mop_leftUnitor, CategoryTheory.MonoidalOpposite.mop_braiding
unmop 📖	CompOp	4 math math: CategoryTheory.unmop_leftUnitor, CategoryTheory.unmop_rightUnitor, CategoryTheory.unmop_associator, CategoryTheory.MonoidalOpposite.unmop_braiding

CategoryTheory.MonoidalOpposite

Definitions

Name	Category	Theorems
monoidalOppositeCategory 📖	CompOp	172 math math: CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft, CategoryTheory.mop_hom_leftUnitor, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, unmop_hom_braiding, unmopFunctor_δ, CategoryTheory.unmop_hom_rightUnitor, tensorLeftMopIso_hom_app_unmop, mopMopEquivalence_functor_obj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj, CategoryTheory.unmopFunctor_obj, CategoryTheory.mop_comp, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft, mopFunctor_ε, CategoryTheory.mop_hom_rightUnitor, MonObj.mopEquivCompForgetIso_hom_app_unmop, CategoryTheory.unmopFunctor_map, mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, CategoryTheory.mop_inv_associator, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom, CategoryTheory.mopFunctor_map, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app, unmopEquiv_inverse_map_unmop, CategoryTheory.mopFunctor_obj, CategoryTheory.leftDualFunctor_obj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft, CategoryTheory.unmop_hom_associator, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app, CategoryTheory.mop_associator, mopMopEquivalence_unitIso_hom_app_unmop_unmop, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop, tensorLeftUnmopIso_inv_app, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight, MonObj.mop_isMonHom, Quiver.Hom.mop_inj, unmopEquiv_inverse_obj_unmop, MonObj.mopEquiv_functor_obj_mon_one_unmop, MonObj.unmopMonObj_one, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom, tensorIso_hom_app_unmop, CategoryTheory.mop_whiskerLeft, CategoryTheory.mop_tensorObj, mopMopEquivalence_inverse_map_unmop_unmop, mopFunctor_η, CategoryTheory.unmop_inv_leftUnitor, mopEquiv_unitIso, CategoryTheory.unmop_inv_associator, CategoryTheory.unmop_tensorUnit, mopMopEquivalenceFunctorMonoidal_μ, CategoryTheory.mop_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso, mopMopEquivalenceFunctorMonoidal_ε, CategoryTheory.unmop_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop, mop_inv_braiding, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj, unmopEquiv_unitIso_inv_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso, CategoryTheory.unmop_leftUnitor, CategoryTheory.unmop_comp, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop, MonObj.mopEquiv_inverse_map_hom, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight, CategoryTheory.mop_rightUnitor, MonObj.mopEquiv_inverse_obj_X, tensorRightUnmopIso_inv_app, CategoryTheory.leftDualFunctor_map, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso, unmopEquiv_counitIso_hom_app, CategoryTheory.rightDualFunctor_map, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft, MonObj.mopEquiv_functor_map_hom_unmop, tensorLeftUnmopIso_hom_app, mopMopEquivalence_functor_map, MonObj.mopEquivCompForgetIso_inv_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionObj, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso, mopMopEquivalence_counitIso_inv_app, tensorRightIso_hom_app_unmop, MonObj.mopEquiv_unitIso_hom_app_hom, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app, tensorRightIso_inv_app_unmop, MonObj.mopEquiv_functor_obj_X_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app, CategoryTheory.unmop_rightUnitor, mopFunctor_μ, unmopEquiv_unitIso_hom_app_unmop, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop, CategoryTheory.rightDualFunctor_obj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_obj, mopMopEquivalence_unitIso_inv_app_unmop_unmop, CategoryTheory.unmop_tensorHom, mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, CategoryTheory.mop_inv_leftUnitor, unmopFunctor_μ, tensorRightMopIso_inv_app_unmop, MonObj.unmopMonObj_mul, mopMopEquivalenceFunctorMonoidal_δ, CategoryTheory.mop_inv_rightUnitor, CategoryTheory.mop_leftUnitor, CategoryTheory.unmop_inv_rightUnitor, MonObj.mopEquiv_functor_obj_mon_mul_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj, mopMopEquivalenceFunctorMonoidal_η, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop, mop_hom_braiding, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomRight, CategoryTheory.unmop_tensorObj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, unmop_inv_braiding, MonObj.mopMonObj_one_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop, mopEquiv_inverse, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight, CategoryTheory.unmop_whiskerRight, MonObj.mopEquiv_inverse_obj_mon_one, tensorLeftIso_hom_app_unmop, mop_braiding, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, unmopEquiv_counitIso_inv_app, CategoryTheory.unmop_associator, unmopEquiv_functor_map, tensorRightMopIso_hom_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_map, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso, CategoryTheory.mop_hom_associator, mopMopEquivalence_inverse_obj_unmop_unmop, CategoryTheory.instIsMonoidalMonoidalOppositeMopMopEquivalence, unmopFunctor_η, MonObj.mopEquiv_unitIso_inv_app_hom, unmopFunctor_ε, Quiver.Hom.unmop_inj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, CategoryTheory.unmop_whiskerLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app, tensorRightUnmopIso_hom_app, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app, tensorLeftMopIso_inv_app_unmop, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop, CategoryTheory.unmop_hom_leftUnitor, MonObj.mopMonObj_mul_unmop, mopFunctor_δ, CategoryTheory.IsIso.instMonoidalOppositeMop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop, tensorLeftIso_inv_app_unmop, tensorIso_inv_app_unmop, mopMopEquivalence_counitIso_hom_app, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom, unmop_braiding, CategoryTheory.mop_whiskerRight, CategoryTheory.mop_tensorUnit, mopEquiv_functor, mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, mopMopEquivalenceInverseMonoidal_η_unmop_unmop, CategoryTheory.mop_tensorHom, CategoryTheory.mop_id_unmop, unmopEquiv_functor_obj, CategoryTheory.unmop_id_mop, mopEquiv_counitIso, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso, MonObj.mopEquiv_inverse_obj_mon_mul
mopEquiv 📖	CompOp	10 math math: MonObj.mopEquivCompForgetIso_hom_app_unmop, mopEquiv_unitIso, unmopEquiv_unitIso_inv_app_unmop, unmopEquiv_counitIso_hom_app, MonObj.mopEquivCompForgetIso_inv_app_unmop, unmopEquiv_unitIso_hom_app_unmop, mopEquiv_inverse, unmopEquiv_counitIso_inv_app, mopEquiv_functor, mopEquiv_counitIso
mopMopEquivalence 📖	CompOp	17 math math: mopMopEquivalence_functor_obj, mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, mopMopEquivalence_unitIso_hom_app_unmop_unmop, mopMopEquivalence_inverse_map_unmop_unmop, mopMopEquivalenceFunctorMonoidal_μ, mopMopEquivalenceFunctorMonoidal_ε, mopMopEquivalence_functor_map, mopMopEquivalence_counitIso_inv_app, mopMopEquivalence_unitIso_inv_app_unmop_unmop, mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, mopMopEquivalenceFunctorMonoidal_δ, mopMopEquivalenceFunctorMonoidal_η, mopMopEquivalence_inverse_obj_unmop_unmop, CategoryTheory.instIsMonoidalMonoidalOppositeMopMopEquivalence, mopMopEquivalence_counitIso_hom_app, mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, mopMopEquivalenceInverseMonoidal_η_unmop_unmop
mopMopEquivalenceFunctorMonoidal 📖	CompOp	5 math math: mopMopEquivalenceFunctorMonoidal_μ, mopMopEquivalenceFunctorMonoidal_ε, mopMopEquivalenceFunctorMonoidal_δ, mopMopEquivalenceFunctorMonoidal_η, CategoryTheory.instIsMonoidalMonoidalOppositeMopMopEquivalence
mopMopEquivalenceInverseMonoidal 📖	CompOp	5 math math: mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, CategoryTheory.instIsMonoidalMonoidalOppositeMopMopEquivalence, mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, mopMopEquivalenceInverseMonoidal_η_unmop_unmop
tensorIso 📖	CompOp	2 math math: tensorIso_hom_app_unmop, tensorIso_inv_app_unmop
tensorLeftIso 📖	CompOp	2 math math: tensorLeftIso_hom_app_unmop, tensorLeftIso_inv_app_unmop
tensorLeftMopIso 📖	CompOp	2 math math: tensorLeftMopIso_hom_app_unmop, tensorLeftMopIso_inv_app_unmop
tensorLeftUnmopIso 📖	CompOp	2 math math: tensorLeftUnmopIso_inv_app, tensorLeftUnmopIso_hom_app
tensorRightIso 📖	CompOp	2 math math: tensorRightIso_hom_app_unmop, tensorRightIso_inv_app_unmop
tensorRightMopIso 📖	CompOp	2 math math: tensorRightMopIso_inv_app_unmop, tensorRightMopIso_hom_app_unmop
tensorRightUnmopIso 📖	CompOp	2 math math: tensorRightUnmopIso_inv_app, tensorRightUnmopIso_hom_app
unmop 📖	CompOp	105 math math: CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, unmop_hom_braiding, unmopFunctor_δ, CategoryTheory.unmop_hom_rightUnitor, tensorLeftMopIso_hom_app_unmop, mopMopEquivalence_functor_obj, CategoryTheory.unmopFunctor_obj, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft, MonObj.mopEquivCompForgetIso_hom_app_unmop, mopMopEquivalenceInverseMonoidal_ε_unmop_unmop, mop_unmop, CategoryTheory.IsIso.instUnmopOfMonoidalOpposite, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_hom_app_unmop_app, unmopEquiv_inverse_map_unmop, unmop_inj_iff, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft, CategoryTheory.unmop_hom_associator, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app, mopMopEquivalence_unitIso_hom_app_unmop_unmop, tensorLeftUnmopIso_inv_app, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight, unmopEquiv_inverse_obj_unmop, MonObj.mopEquiv_functor_obj_mon_one_unmop, MonObj.unmopMonObj_one, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom, tensorIso_hom_app_unmop, mopMopEquivalence_inverse_map_unmop_unmop, CategoryTheory.unmop_inv_leftUnitor, CategoryTheory.unmop_inv_associator, CategoryTheory.unmop_tensorUnit, mopMopEquivalenceFunctorMonoidal_μ, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso, CategoryTheory.unmop_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionActionOfMonoidalFunctorToEndofunctorMopIso_inv_app_unmop_app, unmopEquiv_unitIso_inv_app_unmop, CategoryTheory.unmop_leftUnitor, CategoryTheory.unmop_comp, MonObj.mopEquiv_inverse_map_hom, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight, MonObj.mopEquiv_inverse_obj_X, tensorRightUnmopIso_inv_app, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso, MonObj.mopEquiv_functor_map_hom_unmop, tensorLeftUnmopIso_hom_app, mopMopEquivalence_functor_map, MonObj.mopEquivCompForgetIso_inv_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionObj, Quiver.Hom.mop_unmop, tensorRightIso_hom_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app, tensorRightIso_inv_app_unmop, MonObj.mopEquiv_functor_obj_X_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app, CategoryTheory.unmop_rightUnitor, unmopEquiv_unitIso_hom_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_obj, mopMopEquivalence_unitIso_inv_app_unmop_unmop, CategoryTheory.unmop_tensorHom, mopMopEquivalenceInverseMonoidal_δ_unmop_unmop, unmopFunctor_μ, tensorRightMopIso_inv_app_unmop, MonObj.unmopMonObj_mul, mopMopEquivalenceFunctorMonoidal_δ, CategoryTheory.unmop_inv_rightUnitor, MonObj.mopEquiv_functor_obj_mon_mul_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomRight, CategoryTheory.unmop_tensorObj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, unmop_inv_braiding, unmop_mop, MonObj.mopMonObj_one_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, CategoryTheory.unmop_whiskerRight, MonObj.mopEquiv_inverse_obj_mon_one, tensorLeftIso_hom_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, CategoryTheory.unmop_associator, tensorRightMopIso_hom_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_map, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj, mopMopEquivalence_inverse_obj_unmop_unmop, Quiver.Hom.unmop_inj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, CategoryTheory.unmop_whiskerLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app, tensorRightUnmopIso_hom_app, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app, tensorLeftMopIso_inv_app_unmop, CategoryTheory.unmop_hom_leftUnitor, MonObj.mopMonObj_mul_unmop, unmop_injective, tensorLeftIso_inv_app_unmop, tensorIso_inv_app_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom, unmop_braiding, mopMopEquivalenceInverseMonoidal_μ_unmop_unmop, mopMopEquivalenceInverseMonoidal_η_unmop_unmop, CategoryTheory.mop_id_unmop, unmopEquiv_functor_obj, MonObj.unmop_isMonHom, MonObj.mopEquiv_inverse_obj_mon_mul
unmopEquiv 📖	CompOp	13 math math: unmopEquiv_inverse_map_unmop, mopMopEquivalence_unitIso_hom_app_unmop_unmop, unmopEquiv_inverse_obj_unmop, mopMopEquivalence_inverse_map_unmop_unmop, unmopEquiv_unitIso_inv_app_unmop, unmopEquiv_counitIso_hom_app, mopMopEquivalence_counitIso_inv_app, unmopEquiv_unitIso_hom_app_unmop, mopMopEquivalence_unitIso_inv_app_unmop_unmop, unmopEquiv_counitIso_inv_app, unmopEquiv_functor_map, mopMopEquivalence_counitIso_hom_app, unmopEquiv_functor_obj
«term_ᴹᵒᵖ» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	Quiver.Hom.unmop	—	—	—
mopEquiv_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.MonoidalOpposite monoidalOppositeCategory mopEquiv CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.mopFunctor	—	—
mopEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.MonoidalOpposite monoidalOppositeCategory mopEquiv CategoryTheory.mopFunctor	—	—
mopEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalOpposite monoidalOppositeCategory mopEquiv CategoryTheory.unmopFunctor	—	—
mopEquiv_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.MonoidalOpposite monoidalOppositeCategory mopEquiv CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
mopMopEquivalenceFunctorMonoidal_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Equivalence.functor mopMopEquivalence CategoryTheory.Functor.Monoidal.toOplaxMonoidal mopMopEquivalenceFunctorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct unmop	—	—
mopMopEquivalenceFunctorMonoidal_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Equivalence.functor mopMopEquivalence CategoryTheory.Functor.Monoidal.toLaxMonoidal mopMopEquivalenceFunctorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
mopMopEquivalenceFunctorMonoidal_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Equivalence.functor mopMopEquivalence CategoryTheory.Functor.Monoidal.toOplaxMonoidal mopMopEquivalenceFunctorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
mopMopEquivalenceFunctorMonoidal_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Equivalence.functor mopMopEquivalence CategoryTheory.Functor.Monoidal.toLaxMonoidal mopMopEquivalenceFunctorMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct unmop	—	—
mopMopEquivalenceInverseMonoidal_δ_unmop_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite CategoryTheory.Functor.obj monoidalOppositeCategory CategoryTheory.Equivalence.inverse mopMopEquivalence CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.monoidalCategoryMop CategoryTheory.Functor.Monoidal.toOplaxMonoidal mopMopEquivalenceInverseMonoidal CategoryTheory.CategoryStruct.id	—	—
mopMopEquivalenceInverseMonoidal_ε_unmop_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalCategoryStruct.tensorUnit monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Equivalence.inverse mopMopEquivalence CategoryTheory.Functor.Monoidal.toLaxMonoidal mopMopEquivalenceInverseMonoidal CategoryTheory.CategoryStruct.id	—	—
mopMopEquivalenceInverseMonoidal_η_unmop_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite CategoryTheory.Functor.obj monoidalOppositeCategory CategoryTheory.Equivalence.inverse mopMopEquivalence CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.monoidalCategoryMop CategoryTheory.Functor.Monoidal.toOplaxMonoidal mopMopEquivalenceInverseMonoidal CategoryTheory.CategoryStruct.id	—	—
mopMopEquivalenceInverseMonoidal_μ_unmop_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop CategoryTheory.Functor.obj CategoryTheory.Equivalence.inverse mopMopEquivalence CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal mopMopEquivalenceInverseMonoidal CategoryTheory.CategoryStruct.id	—	—
mopMopEquivalence_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.inverse unmopEquiv CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso mopMopEquivalence CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
mopMopEquivalence_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.inverse unmopEquiv CategoryTheory.Equivalence.functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso mopMopEquivalence CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
mopMopEquivalence_functor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.functor mopMopEquivalence Quiver.Hom.unmop unmop	—	—
mopMopEquivalence_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.functor mopMopEquivalence unmop	—	—
mopMopEquivalence_inverse_map_unmop_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.inverse unmopEquiv CategoryTheory.Functor.map mopMopEquivalence	—	—
mopMopEquivalence_inverse_obj_unmop_unmop 📖	mathematical	—	unmop CategoryTheory.MonoidalOpposite CategoryTheory.Functor.obj monoidalOppositeCategory CategoryTheory.Equivalence.inverse mopMopEquivalence	—	—
mopMopEquivalence_unitIso_hom_app_unmop_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite CategoryTheory.Functor.obj monoidalOppositeCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor unmopEquiv CategoryTheory.Equivalence.inverse CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso mopMopEquivalence CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mopMopEquivalence_unitIso_inv_app_unmop_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite CategoryTheory.Functor.obj monoidalOppositeCategory CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor unmopEquiv CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso mopMopEquivalence CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
mop_inj_iff 📖	mathematical	—	mop	—	mop_injective
mop_injective 📖	mathematical	—	CategoryTheory.MonoidalOpposite mop	—	—
mop_unmop 📖	mathematical	—	mop unmop	—	—
tensorIso_hom_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite CategoryTheory.uniformProd monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensor CategoryTheory.monoidalCategoryMop CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.unmopFunctor CategoryTheory.Prod.swap CategoryTheory.mopFunctor tensorIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorIso_inv_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite CategoryTheory.uniformProd monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensor CategoryTheory.monoidalCategoryMop CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.prod' CategoryTheory.Functor.prod CategoryTheory.unmopFunctor CategoryTheory.Prod.swap CategoryTheory.mopFunctor tensorIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorLeftIso_hom_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.monoidalCategoryMop CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.mopFunctor tensorLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorLeftIso_inv_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.monoidalCategoryMop CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.mopFunctor tensorLeftIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorLeftMopIso_hom_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.monoidalCategoryMop mop CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.mopFunctor tensorLeftMopIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorLeftMopIso_inv_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.monoidalCategoryMop mop CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.mopFunctor tensorLeftMopIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorLeftUnmopIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.tensorLeft unmop CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.mopFunctor CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.monoidalCategoryMop CategoryTheory.unmopFunctor tensorLeftUnmopIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorLeftUnmopIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.tensorLeft unmop CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.mopFunctor CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.monoidalCategoryMop CategoryTheory.unmopFunctor tensorLeftUnmopIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorRightIso_hom_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.monoidalCategoryMop CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.mopFunctor tensorRightIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorRightIso_inv_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.monoidalCategoryMop CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.mopFunctor tensorRightIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorRightMopIso_hom_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.monoidalCategoryMop mop CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.mopFunctor tensorRightMopIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorRightMopIso_inv_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.monoidalCategoryMop mop CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.mopFunctor tensorRightMopIso CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorRightUnmopIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.tensorRight unmop CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.mopFunctor CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.monoidalCategoryMop CategoryTheory.unmopFunctor tensorRightUnmopIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorRightUnmopIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategory.tensorRight unmop CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.mopFunctor CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.monoidalCategoryMop CategoryTheory.unmopFunctor tensorRightUnmopIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
unmopEquiv_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.functor mopEquiv CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso unmopEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
unmopEquiv_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.functor mopEquiv CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso unmopEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
unmopEquiv_functor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.functor unmopEquiv Quiver.Hom.unmop	—	—
unmopEquiv_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.functor unmopEquiv unmop	—	—
unmopEquiv_inverse_map_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct mop CategoryTheory.Functor.map CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.inverse unmopEquiv	—	—
unmopEquiv_inverse_obj_unmop 📖	mathematical	—	unmop CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Equivalence.inverse unmopEquiv	—	—
unmopEquiv_unitIso_hom_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.mopFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Equivalence.inverse mopEquiv CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso unmopEquiv CategoryTheory.CategoryStruct.id	—	—
unmopEquiv_unitIso_inv_app_unmop 📖	mathematical	—	unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalOpposite monoidalOppositeCategory CategoryTheory.Functor.comp CategoryTheory.unmopFunctor CategoryTheory.mopFunctor CategoryTheory.NatTrans.app CategoryTheory.Equivalence.inverse mopEquiv CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso unmopEquiv CategoryTheory.CategoryStruct.id	—	—
unmop_inj_iff 📖	mathematical	—	unmop	—	unmop_injective
unmop_injective 📖	mathematical	—	CategoryTheory.MonoidalOpposite unmop	—	—
unmop_mop 📖	mathematical	—	unmop mop	—	—

Quiver.Hom

Definitions

Name	Category	Theorems
mop 📖	CompOp	32 math math: CategoryTheory.mop_hom_leftUnitor, CategoryTheory.mop_comp, CategoryTheory.mop_hom_rightUnitor, CategoryTheory.mop_inv_associator, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom, CategoryTheory.mopFunctor_map, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom, MonObj.mop_isMonHom, mop_inj, CategoryTheory.mop_whiskerLeft, CategoryTheory.mop_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop, CategoryTheory.MonoidalOpposite.mop_inv_braiding, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop, unmop_mop, CategoryTheory.leftDualFunctor_map, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.rightDualFunctor_map, mop_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft, CategoryTheory.mop_inv_leftUnitor, CategoryTheory.mop_inv_rightUnitor, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop, CategoryTheory.MonoidalOpposite.mop_hom_braiding, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight, CategoryTheory.mop_hom_associator, CategoryTheory.IsIso.instMonoidalOppositeMop, CategoryTheory.mop_whiskerRight, CategoryTheory.mop_tensorHom, CategoryTheory.mop_id_unmop
unmop 📖	CompOp	40 math math: CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom, CategoryTheory.MonoidalOpposite.unmop_hom_braiding, CategoryTheory.unmop_hom_rightUnitor, CategoryTheory.unmopFunctor_map, CategoryTheory.IsIso.instUnmopOfMonoidalOpposite, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft, CategoryTheory.unmop_hom_associator, MonObj.unmopMonObj_one, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom, CategoryTheory.unmop_inv_leftUnitor, CategoryTheory.unmop_inv_associator, CategoryTheory.unmop_id, CategoryTheory.unmop_comp, MonObj.mopEquiv_inverse_map_hom, CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight, unmop_mop, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.MonoidalOpposite.mopMopEquivalence_functor_map, mop_unmop, CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app, CategoryTheory.unmop_tensorHom, MonObj.unmopMonObj_mul, CategoryTheory.unmop_inv_rightUnitor, CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, CategoryTheory.MonoidalOpposite.unmop_inv_braiding, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom, CategoryTheory.unmop_whiskerRight, MonObj.mopEquiv_inverse_obj_mon_one, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv, CategoryTheory.MonoidalOpposite.unmopEquiv_functor_map, unmop_inj, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv, CategoryTheory.unmop_whiskerLeft, CategoryTheory.unmop_hom_leftUnitor, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom, CategoryTheory.unmop_id_mop, MonObj.unmop_isMonHom, MonObj.mopEquiv_inverse_obj_mon_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mop_inj 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalOpposite.mop mop	—	—
mop_unmop 📖	mathematical	—	mop CategoryTheory.MonoidalOpposite.unmop unmop	—	—
unmop_inj 📖	mathematical	—	Quiver.Hom CategoryTheory.MonoidalOpposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalOpposite.unmop unmop	—	—
unmop_mop 📖	mathematical	—	unmop CategoryTheory.MonoidalOpposite.mop mop	—	—

---

← Back to Index