Mon_

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

Statistics

Metric	Count
Definitions homMulEquiv, homMonoidHom, commMonoid, monoid, mulEquivCongrRight, instCartesianMonoidalCategory, instMonObjOfIsCommMonObjX, ofRepresentableBy, ofRepresentableBy, Mon_ClassOfRepresentableBy, yonedaMon, yonedaMonFullyFaithful, yonedaMonObj, yonedaMonObjIsoOfRepresentableBy, yonedaMonObjRepresentableBy	15
Theorems homMulEquiv_apply, homMulEquiv_symm_apply, homMonoidHom_apply, map_mul, map_one, mulEquivCongrRight_apply, mulEquivCongrRight_symm_apply, mul_def, one_def, hom_mul, hom_one, hom_pow, fst_hom, hom_mul, hom_one, instIsCommMonObj, lift_hom, snd_hom, comp_mul, comp_mul_assoc, comp_one, comp_one_assoc, comp_pow, comp_pow_assoc, instIsMonHomFst, instIsMonHomLift, instIsMonHomMulOfIsCommMonObj, instIsMonHomOne, instIsMonHomSnd, instIsMonHomToUnit, lift_comp_one_left, lift_comp_one_left_assoc, lift_comp_one_right, lift_comp_one_right_assoc, lift_lift_assoc, mul_comp, mul_comp_assoc, mul_eq_mul, ofRepresentableBy_mul, ofRepresentableBy_one, ofRepresentableBy_yonedaMonObjRepresentableBy, one_comp, one_comp_assoc, one_eq_one, pow_comp, pow_comp_assoc, comp_mul, comp_one, comp_pow, mul_comp, mul_eq_mul, ofRepresentableBy_yonedaMonObjRepresentableBy, one_comp, one_eq_one, pow_comp, Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy, essImage_yonedaMon, instFaithfulMonFunctorOppositeMonCatYonedaMon, instFullMonFunctorOppositeMonCatYonedaMon, isCommMonObj_iff_isMulCommutative, yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, yonedaMonObj_map, yonedaMonObj_obj_coe, yonedaMon_map_app, yonedaMon_naturality, yonedaMon_naturality_assoc, yonedaMon_obj	68
Total	83

CategoryTheory

Definitions

Name	Category	Theorems
Mon_ClassOfRepresentableBy 📖	CompOp	—
yonedaMon 📖	CompOp	6 math math: instFullMonFunctorOppositeMonCatYonedaMon, essImage_yonedaMon, instFaithfulMonFunctorOppositeMonCatYonedaMon, yonedaMon_map_app, yonedaGrp_map_app, yonedaMon_obj
yonedaMonFullyFaithful 📖	CompOp	—
yonedaMonObj 📖	CompOp	12 math math: yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, yonedaMon_naturality_assoc, yonedaMonObj_map, yonedaMon_naturality, yonedaMonObj_obj_coe, Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy, yonedaMon_map_app, yonedaGrpObj_map, MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy, yonedaMon_obj, Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy
yonedaMonObjIsoOfRepresentableBy 📖	CompOp	2 math math: yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply
yonedaMonObjRepresentableBy 📖	CompOp	3 math math: Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy, MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy, Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy 📖	mathematical	—	MonObj.ofRepresentableBy yonedaMonObj yonedaMonObjRepresentableBy	—	MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy
essImage_yonedaMon 📖	mathematical	—	Functor.essImage Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Functor Opposite Category.opposite MonCat MonCat.instCategory Mon.instCategory Functor.category yonedaMon Set.preimage types Functor.comp forget MonoidHom MonCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier setOf Functor.IsRepresentable	—	—
instFaithfulMonFunctorOppositeMonCatYonedaMon 📖	mathematical	—	Functor.Faithful Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Opposite Category.opposite MonCat MonCat.instCategory Functor.category yonedaMon	—	Functor.FullyFaithful.faithful
instFullMonFunctorOppositeMonCatYonedaMon 📖	mathematical	—	Functor.Full Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Opposite Category.opposite MonCat MonCat.instCategory Functor.category yonedaMon	—	Functor.FullyFaithful.full
isCommMonObj_iff_isMulCommutative 📖	mathematical	—	IsCommMonObj SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory IsMulCommutative Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Hom.monoid	—	mul_comm MonObj.mul_eq_mul MonObj.comp_mul CartesianMonoidalCategory.braiding_hom_fst CartesianMonoidalCategory.braiding_hom_snd
yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop MonCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass Hom.monoid MonObj.ofRepresentableBy MonCat.str MonoidHom.instFunLike MonCat.Hom.hom Functor.obj Opposite Category.opposite MonCat MonCat.instCategory yonedaMonObj NatTrans.app Iso.hom Functor Functor.category yonedaMonObjIsoOfRepresentableBy Equiv EquivLike.toFunLike Equiv.instEquivLike Functor.RepresentableBy.homEquiv Functor.comp types forget MonCat.instConcreteCategoryMonoidHomCarrier	—	—
yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply 📖	mathematical	—	DFunLike.coe MonoidHom MonCat.carrier Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str Hom.monoid MonObj.ofRepresentableBy MonoidHom.instFunLike MonCat.Hom.hom Functor.obj Opposite Category.opposite MonCat MonCat.instCategory yonedaMonObj NatTrans.app Iso.inv Functor Functor.category yonedaMonObjIsoOfRepresentableBy Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Functor.RepresentableBy.homEquiv Functor.comp types forget MonCat.instConcreteCategoryMonoidHomCarrier	—	—
yonedaMonObj_map 📖	mathematical	—	Functor.map Opposite Category.opposite MonCat MonCat.instCategory yonedaMonObj MonCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Hom.monoid MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne CategoryStruct.comp Quiver.Hom.unop	—	—
yonedaMonObj_obj_coe 📖	mathematical	—	MonCat.carrier Functor.obj Opposite Category.opposite MonCat MonCat.instCategory yonedaMonObj Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—
yonedaMon_map_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite MonCat MonCat.instCategory yonedaMonObj Mon.X SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.mon Functor.map Mon Mon.instCategory Functor Functor.category yonedaMon MonCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Hom.monoid MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne CategoryStruct.comp Mon.Hom.hom	—	—
yonedaMon_naturality 📖	mathematical	—	DFunLike.coe Functor.obj Opposite Category.opposite MonCat MonCat.instCategory yonedaMonObj Opposite.op MonCat.carrier ConcreteCategory.hom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier NatTrans.app CategoryStruct.comp Category.toCategoryStruct Opposite.unop	—	NatTrans.naturality
yonedaMon_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct DFunLike.coe MonoidHom MonCat.carrier Functor.obj Opposite Category.opposite MonCat MonCat.instCategory yonedaMonObj Opposite.op MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike ConcreteCategory.hom MonCat.instConcreteCategoryMonoidHomCarrier NatTrans.app	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' yonedaMon_naturality
yonedaMon_obj 📖	mathematical	—	Functor.obj Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Opposite Category.opposite MonCat MonCat.instCategory Functor.category yonedaMon yonedaMonObj Mon.X Mon.mon	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
homMonoidHom 📖	CompOp	1 math math: homMonoidHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homMonoidHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid monObjObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Monoidal.toLaxMonoidal MonoidHom.instFunLike homMonoidHom map	—	—
map_mul 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid obj monObjObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Monoidal.toLaxMonoidal	—	map_comp Monoidal.instIsIsoμ CategoryTheory.IsIso.comp_inv_eq CategoryTheory.CartesianMonoidalCategory.hom_ext Monoidal.inv_μ OplaxMonoidal.lift_δ CategoryTheory.CartesianMonoidalCategory.lift_fst CategoryTheory.CartesianMonoidalCategory.lift_snd
map_one 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid obj monObjObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Monoidal.toLaxMonoidal	—	map_comp Monoidal.toUnit_ε_assoc

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
homMulEquiv 📖	CompOp	2 math math: homMulEquiv_apply, homMulEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homMulEquiv_apply 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.Functor.monObjObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.Monoidal.toLaxMonoidal EquivLike.toFunLike MulEquiv.instEquivLike homMulEquiv CategoryTheory.Functor.map	—	—
homMulEquiv_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.Functor.monObjObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.Monoidal.toLaxMonoidal EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm homMulEquiv preimage	—	—

CategoryTheory.Hom

Definitions

Name	Category	Theorems
commMonoid 📖	CompOp	—
monoid 📖	CompOp	44 math math: CategoryTheory.Mon_Class.mul_comp, CategoryTheory.Mon_Class.comp_mul, CategoryTheory.Functor.map_mul, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, CategoryTheory.MonObj.comp_mul_assoc, CategoryTheory.MonObj.comp_one, CategoryTheory.MonObj.one_comp_assoc, CategoryTheory.yonedaMonObj_map, CategoryTheory.MonObj.mul_comp, mul_def, CategoryTheory.Mon_Class.mul_eq_mul, CategoryTheory.yonedaMon_map_app, CategoryTheory.MonObj.one_comp, CategoryTheory.MonObj.comp_pow, CategoryTheory.Mon_Class.one_eq_one, CategoryTheory.Grp.Hom.hom_pow, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv, mulEquivCongrRight_symm_apply, CategoryTheory.MonObj.mul_comp_assoc, CategoryTheory.isCommMonObj_iff_isMulCommutative, CategoryTheory.Mon.Hom.hom_mul, CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply, CategoryTheory.Mon_Class.comp_pow, CategoryTheory.MonObj.pow_comp_assoc, CategoryTheory.Grp.Hom.hom_mul, CategoryTheory.Mon.Hom.hom_pow, CategoryTheory.MonObj.comp_mul, CategoryTheory.Mon_Class.pow_comp, CategoryTheory.MonObj.comp_one_assoc, CategoryTheory.Mon_Class.comp_one, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc, CategoryTheory.MonObj.pow_comp, CategoryTheory.Mon_Class.one_comp, one_def, CategoryTheory.Functor.homMonoidHom_apply, CategoryTheory.MonObj.one_eq_one, mulEquivCongrRight_apply, CategoryTheory.Grp.Hom.hom_one, CategoryTheory.MonObj.comp_pow_assoc, CategoryTheory.Functor.map_one, CategoryTheory.MonObj.mul_eq_mul, CategoryTheory.Mon.Hom.hom_one
mulEquivCongrRight 📖	CompOp	2 math math: mulEquivCongrRight_symm_apply, mulEquivCongrRight_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulEquivCongrRight_apply 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass monoid EquivLike.toFunLike MulEquiv.instEquivLike mulEquivCongrRight CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom	—	—
mulEquivCongrRight_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass monoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm mulEquivCongrRight CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv	—	—
mul_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass monoid CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.MonObj.mul	—	—
one_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass monoid CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	—

CategoryTheory.Mon

Definitions

Name	Category	Theorems
instCartesianMonoidalCategory 📖	CompOp	10 math math: CategoryTheory.Grp.lift_hom, lift_hom, fst_hom, CategoryTheory.Grp.Hom.hom_pow, Hom.hom_mul, CategoryTheory.Grp.Hom.hom_mul, Hom.hom_pow, CategoryTheory.Grp.Hom.hom_one, snd_hom, Hom.hom_one
instMonObjOfIsCommMonObjX 📖	CompOp	9 math math: CategoryTheory.Grp.Hom.hom_pow, instIsCommMonObj, Hom.hom_mul, CategoryTheory.Grp.Hom.hom_mul, Hom.hom_pow, hom_mul, CategoryTheory.Grp.Hom.hom_one, hom_one, Hom.hom_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_hom 📖	mathematical	—	Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst X	—	—
hom_mul 📖	mathematical	—	Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monMonoidal CategoryTheory.MonObj.mul instMonObjOfIsCommMonObjX X mon	—	—
hom_one 📖	mathematical	—	Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monMonoidal CategoryTheory.MonObj.one instMonObjOfIsCommMonObjX X mon	—	—
instIsCommMonObj 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCategory monMonoidal CategoryTheory.SymmetricCategory.toBraidedCategory instSymmetricCategory CategoryTheory.CartesianMonoidalCategory.toSymmetricCategory instMonObjOfIsCommMonObjX	—	Hom.ext' CategoryTheory.IsCommMonObj.mul_comm
lift_hom 📖	mathematical	—	Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift X	—	—
snd_hom 📖	mathematical	—	Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.snd X	—	—

CategoryTheory.Mon.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_mul 📖	mathematical	—	hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Quiver.Hom CategoryTheory.Mon CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.instCategory MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.Mon.instCartesianMonoidalCategory CategoryTheory.Mon.instMonObjOfIsCommMonObjX CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
hom_one 📖	mathematical	—	hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Quiver.Hom CategoryTheory.Mon CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.instCategory MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.Mon.instCartesianMonoidalCategory CategoryTheory.Mon.instMonObjOfIsCommMonObjX CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
hom_pow 📖	mathematical	—	hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Quiver.Hom CategoryTheory.Mon CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.instCategory Monoid.toNatPow CategoryTheory.Hom.monoid CategoryTheory.Mon.instCartesianMonoidalCategory CategoryTheory.Mon.instMonObjOfIsCommMonObjX CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	pow_zero pow_succ

CategoryTheory.MonObj

Definitions

Name	Category	Theorems
ofRepresentableBy 📖	CompOp	9 math math: CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, ofRepresentableBy_one, CategoryTheory.IsCommMonObj.ofRepresentableBy, CategoryTheory.IsCommMon.ofRepresentableBy, CategoryTheory.Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy, ofRepresentableBy_yonedaMonObjRepresentableBy, ofRepresentableBy_mul, CategoryTheory.Mon_Class.ofRepresentableBy_yonedaMonObjRepresentableBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	MonoidHom.map_mul
comp_mul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_mul
comp_one 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	MonoidHom.map_one
comp_one_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_one
comp_pow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Monoid.toNatPow CategoryTheory.Hom.monoid	—	pow_zero comp_one pow_succ comp_mul
comp_pow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Monoid.toNatPow CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_pow
instIsMonHomFst 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.instMonObjTensorObj CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc CategoryTheory.CartesianMonoidalCategory.tensorHom_fst CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst_assoc CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit CategoryTheory.Category.id_comp CategoryTheory.CartesianMonoidalCategory.tensorμ_fst_assoc
instIsMonHomLift 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.instMonObjTensorObj CategoryTheory.CartesianMonoidalCategory.lift	—	CategoryTheory.CartesianMonoidalCategory.comp_lift CategoryTheory.IsMonHom.one_hom CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.CartesianMonoidalCategory.lift_fst CategoryTheory.Category.assoc CategoryTheory.CartesianMonoidalCategory.tensorHom_fst CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst_assoc CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit CategoryTheory.Category.id_comp CategoryTheory.CartesianMonoidalCategory.lift_snd CategoryTheory.CartesianMonoidalCategory.tensorHom_snd CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd_assoc CategoryTheory.IsMonHom.mul_hom CategoryTheory.CartesianMonoidalCategory.tensorμ_fst_assoc CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc CategoryTheory.CartesianMonoidalCategory.tensorμ_snd_assoc
instIsMonHomMulOfIsCommMonObj 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.instMonObjTensorObj mul	—	CategoryTheory.Category.assoc mul_one_hom CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique CategoryTheory.Iso.inv_hom_id_assoc mul_mul_mul_comm
instIsMonHomOne 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instTensorUnit one	—	CategoryTheory.Category.id_comp mul_one_hom CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
instIsMonHomSnd 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.instMonObjTensorObj CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.Category.assoc CategoryTheory.CartesianMonoidalCategory.tensorHom_snd CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd_assoc CategoryTheory.CartesianMonoidalCategory.tensorμ_snd_assoc
instIsMonHomToUnit 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instTensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit Unique.instSubsingleton
lift_comp_one_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.MonoidalCategoryStruct.tensorUnit one mul	—	CategoryTheory.whisker_eq one_mul CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc
lift_comp_one_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.MonoidalCategoryStruct.tensorUnit one mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_one_left
lift_comp_one_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.MonoidalCategoryStruct.tensorUnit one mul	—	CategoryTheory.whisker_eq mul_one CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc
lift_comp_one_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.MonoidalCategoryStruct.tensorUnit one mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_one_right
lift_lift_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift mul	—	CategoryTheory.whisker_eq mul_assoc CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc
mul_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc CategoryTheory.IsMonHom.mul_hom CategoryTheory.CartesianMonoidalCategory.lift_map_assoc
mul_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_comp
mul_eq_mul 📖	mathematical	—	mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.CartesianMonoidalCategory.lift_fst_snd CategoryTheory.Category.id_comp
ofRepresentableBy_mul 📖	mathematical	—	mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory ofRepresentableBy DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.comp MonCat MonCat.instCategory CategoryTheory.forget MonoidHom MonCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier Opposite.op CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Functor.RepresentableBy.homEquiv MulOne.toMul MonCat.monoidObj CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
ofRepresentableBy_one 📖	mathematical	—	one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory ofRepresentableBy DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.comp MonCat MonCat.instCategory CategoryTheory.forget MonoidHom MonCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier Opposite.op CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Functor.RepresentableBy.homEquiv MulOne.toOne MonCat.monoidObj	—	—
ofRepresentableBy_yonedaMonObjRepresentableBy 📖	mathematical	—	ofRepresentableBy CategoryTheory.yonedaMonObj CategoryTheory.yonedaMonObjRepresentableBy	—	ext CategoryTheory.CartesianMonoidalCategory.lift_fst_snd CategoryTheory.Category.id_comp
one_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc CategoryTheory.IsMonHom.one_hom
one_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_comp
one_eq_one 📖	mathematical	—	one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique CategoryTheory.Category.id_comp
pow_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Monoid.toNatPow CategoryTheory.Hom.monoid	—	pow_zero one_comp pow_succ mul_comp
pow_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Monoid.toNatPow CategoryTheory.Hom.monoid	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pow_comp

CategoryTheory.Mon_Class

Definitions

Name	Category	Theorems
ofRepresentableBy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.MonObj.comp_mul
comp_one 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.MonObj.comp_one
comp_pow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Monoid.toNatPow CategoryTheory.Hom.monoid	—	CategoryTheory.MonObj.comp_pow
mul_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.MonObj.mul_comp
mul_eq_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	CategoryTheory.MonObj.mul_eq_mul
ofRepresentableBy_yonedaMonObjRepresentableBy 📖	mathematical	—	CategoryTheory.MonObj.ofRepresentableBy CategoryTheory.yonedaMonObj CategoryTheory.yonedaMonObjRepresentableBy	—	CategoryTheory.MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy
one_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.MonObj.one_comp
one_eq_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid	—	CategoryTheory.MonObj.one_eq_one
pow_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Monoid.toNatPow CategoryTheory.Hom.monoid	—	CategoryTheory.MonObj.pow_comp

---

← Back to Index