Mon_

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

Statistics

Metric	Count
Definitions mopEquiv, mopEquivCompForgetIso, mopMonObj, unmopMonObj	4
Theorems mopEquivCompForgetIso_hom_app_unmop, mopEquivCompForgetIso_inv_app_unmop, mopEquiv_counitIso_hom_app_hom_unmop, mopEquiv_counitIso_inv_app_hom_unmop, mopEquiv_functor_map_hom_unmop, mopEquiv_functor_obj_X_unmop, mopEquiv_functor_obj_mon_mul_unmop, mopEquiv_functor_obj_mon_one_unmop, mopEquiv_inverse_map_hom, mopEquiv_inverse_obj_X, mopEquiv_inverse_obj_mon_mul, mopEquiv_inverse_obj_mon_one, mopEquiv_unitIso_hom_app_hom, mopEquiv_unitIso_inv_app_hom, mopMonObj_mul_unmop, mopMonObj_one_unmop, mop_isMonHom, unmopMonObj_mul, unmopMonObj_one, unmop_isMonHom	20
Total	24

MonObj

Definitions

Name	Category	Theorems
mopEquiv 📖	CompOp	14 math math: mopEquivCompForgetIso_hom_app_unmop, mopEquiv_functor_obj_mon_one_unmop, mopEquiv_inverse_map_hom, mopEquiv_inverse_obj_X, mopEquiv_counitIso_hom_app_hom_unmop, mopEquiv_functor_map_hom_unmop, mopEquivCompForgetIso_inv_app_unmop, mopEquiv_unitIso_hom_app_hom, mopEquiv_functor_obj_X_unmop, mopEquiv_functor_obj_mon_mul_unmop, mopEquiv_counitIso_inv_app_hom_unmop, mopEquiv_inverse_obj_mon_one, mopEquiv_unitIso_inv_app_hom, mopEquiv_inverse_obj_mon_mul
mopEquivCompForgetIso 📖	CompOp	2 math math: mopEquivCompForgetIso_hom_app_unmop, mopEquivCompForgetIso_inv_app_unmop
mopMonObj 📖	CompOp	6 math math: mop_isMonHom, mopEquiv_counitIso_hom_app_hom_unmop, mopEquiv_functor_map_hom_unmop, mopEquiv_counitIso_inv_app_hom_unmop, mopMonObj_one_unmop, mopMonObj_mul_unmop
unmopMonObj 📖	CompOp	6 math math: unmopMonObj_one, mopEquiv_inverse_map_hom, mopEquiv_counitIso_hom_app_hom_unmop, unmopMonObj_mul, mopEquiv_counitIso_inv_app_hom_unmop, unmop_isMonHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mopEquivCompForgetIso_hom_app_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.Functor.comp CategoryTheory.monoidalCategoryMop CategoryTheory.Equivalence.functor mopEquiv CategoryTheory.Mon.forget CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalOpposite.mopEquiv mopEquivCompForgetIso CategoryTheory.CategoryStruct.id CategoryTheory.Mon.X	—	—
mopEquivCompForgetIso_inv_app_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.Functor.comp CategoryTheory.monoidalCategoryMop CategoryTheory.Equivalence.functor mopEquiv CategoryTheory.Mon.forget CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.MonoidalOpposite.mopEquiv mopEquivCompForgetIso CategoryTheory.CategoryStruct.id CategoryTheory.Mon.X	—	—
mopEquiv_counitIso_hom_app_hom_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp unmopMonObj CategoryTheory.Mon.mon Quiver.Hom.unmop CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalOpposite.mop mopMonObj Quiver.Hom.mop CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso mopEquiv CategoryTheory.CategoryStruct.id	—	—
mopEquiv_counitIso_inv_app_hom_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp unmopMonObj CategoryTheory.Mon.mon Quiver.Hom.unmop CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalOpposite.mop mopMonObj Quiver.Hom.mop CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso mopEquiv CategoryTheory.CategoryStruct.id	—	—
mopEquiv_functor_map_hom_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite.mop CategoryTheory.Mon.X CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop mopMonObj CategoryTheory.Mon.mon CategoryTheory.Functor.map CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.functor mopEquiv	—	—
mopEquiv_functor_obj_X_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop CategoryTheory.Mon.X CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.functor mopEquiv	—	—
mopEquiv_functor_obj_mon_mul_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X CategoryTheory.MonObj.mul CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Mon.mon CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.functor mopEquiv	—	—
mopEquiv_functor_obj_mon_one_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X CategoryTheory.MonObj.one CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Mon.mon CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.functor mopEquiv	—	—
mopEquiv_inverse_map_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalOpposite.unmop CategoryTheory.Mon.X CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop unmopMonObj CategoryTheory.Mon.mon CategoryTheory.Functor.map CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.inverse mopEquiv Quiver.Hom.unmop	—	—
mopEquiv_inverse_obj_X 📖	mathematical	—	CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.inverse mopEquiv CategoryTheory.MonoidalOpposite.unmop	—	—
mopEquiv_inverse_obj_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.MonoidalOpposite.unmop CategoryTheory.Mon.X CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Mon.mon CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.inverse mopEquiv Quiver.Hom.unmop CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
mopEquiv_inverse_obj_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.MonoidalOpposite.unmop CategoryTheory.Mon.X CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.Mon.mon CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.inverse mopEquiv Quiver.Hom.unmop CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
mopEquiv_unitIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop mopEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
mopEquiv_unitIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop mopEquiv CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
mopMonObj_mul_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop mopMonObj	—	—
mopMonObj_one_unmop 📖	mathematical	—	CategoryTheory.MonoidalOpposite.unmop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalOpposite.mop CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop mopMonObj	—	—
mop_isMonHom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.monoidalCategoryMop CategoryTheory.MonoidalOpposite.mop mopMonObj Quiver.Hom.mop	—	CategoryTheory.Functor.FullyFaithful.map_injective CategoryTheory.IsMonHom.one_hom CategoryTheory.IsMonHom.mul_hom
unmopMonObj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.MonoidalOpposite.unmop unmopMonObj Quiver.Hom.unmop CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop	—	—
unmopMonObj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.MonoidalOpposite.unmop unmopMonObj Quiver.Hom.unmop CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalOpposite CategoryTheory.MonoidalOpposite.monoidalOppositeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryMop	—	—
unmop_isMonHom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalOpposite.unmop unmopMonObj Quiver.Hom.unmop	—	CategoryTheory.Functor.FullyFaithful.map_injective CategoryTheory.IsMonHom.one_hom CategoryTheory.IsMonHom.mul_hom

---

← Back to Index