CartesianMonoidal

📁 Source: Mathlib/Algebra/Category/Grp/CartesianMonoidal.lean

Statistics

Metric	Count
Definitions cartesianMonoidalCategory, cartesianMonoidalCategoryAddCommGrp, instBraidedCategory, instBraidedForgetAddMonoidHomCarrier, binaryProductLimitCone, cartesianMonoidalCategoryAddGrp, instBraidedCategory, instBraidedForgetAddMonoidHomCarrier, binaryProductLimitCone, cartesianMonoidalCategory, instBraidedCategory, instBraidedForgetMonoidHomCarrier, binaryProductLimitCone, cartesianMonoidalCategoryGrp, instBraidedCategory, instBraidedForgetMonoidHomCarrier	16
Theorems tensorObj_eq, μ_forget_apply, binaryProductLimitCone_cone_pt, binaryProductLimitCone_isLimit_lift, tensorObj_eq, μ_forget_apply, binaryProductLimitCone_cone_pt, binaryProductLimitCone_isLimit_lift, tensorObj_eq, μ_forget_apply, binaryProductLimitCone_cone_pt, binaryProductLimitCone_isLimit_lift, tensorObj_eq, μ_forget_apply	14
Total	30

AddCommGrpCat

Definitions

Name	Category	Theorems
cartesianMonoidalCategory 📖	CompOp	2 math math: μ_forget_apply, tensorObj_eq
cartesianMonoidalCategoryAddCommGrp 📖	CompOp	—
instBraidedCategory 📖	CompOp	1 math math: μ_forget_apply
instBraidedForgetAddMonoidHomCarrier 📖	CompOp	1 math math: μ_forget_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorObj_eq 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj AddCommGrpCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory of carrier Prod.instAddCommGroup str	—	—
μ_forget_apply 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ AddCommGrpCat instCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.types CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.LaxBraided.toLaxMonoidal instBraidedCategory CategoryTheory.instBraidedCategoryType CategoryTheory.Functor.Braided.toLaxBraided instBraidedForgetAddMonoidHomCarrier CategoryTheory.Functor.obj	—	CategoryTheory.Functor.Monoidal.μ_fst CategoryTheory.Functor.Monoidal.μ_snd

AddGrpCat

Definitions

Name	Category	Theorems
binaryProductLimitCone 📖	CompOp	2 math math: binaryProductLimitCone_isLimit_lift, binaryProductLimitCone_cone_pt
cartesianMonoidalCategoryAddGrp 📖	CompOp	2 math math: tensorObj_eq, μ_forget_apply
instBraidedCategory 📖	CompOp	1 math math: μ_forget_apply
instBraidedForgetAddMonoidHomCarrier 📖	CompOp	1 math math: μ_forget_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binaryProductLimitCone_cone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory AddGrpCat instCategory CategoryTheory.Limits.pair CategoryTheory.Limits.LimitCone.cone binaryProductLimitCone of carrier Prod.instAddGroup str	—	—
binaryProductLimitCone_isLimit_lift 📖	mathematical	—	CategoryTheory.Limits.IsLimit.lift CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory AddGrpCat instCategory CategoryTheory.Limits.pair of carrier Prod.instAddGroup str ofHom AddMonoidHom.fst AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.snd CategoryTheory.Limits.LimitCone.isLimit binaryProductLimitCone CategoryTheory.Limits.Cone.pt AddMonoidHom.prod Hom.hom CategoryTheory.Limits.BinaryFan.fst CategoryTheory.Limits.BinaryFan.snd	—	—
tensorObj_eq 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj AddGrpCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategoryAddGrp of carrier Prod.instAddGroup str	—	—
μ_forget_apply 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ AddGrpCat instCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategoryAddGrp CategoryTheory.types CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.LaxBraided.toLaxMonoidal instBraidedCategory CategoryTheory.instBraidedCategoryType CategoryTheory.Functor.Braided.toLaxBraided instBraidedForgetAddMonoidHomCarrier CategoryTheory.Functor.obj	—	CategoryTheory.Functor.Monoidal.μ_fst CategoryTheory.Functor.Monoidal.μ_snd

CommGrpCat

Definitions

Name	Category	Theorems
binaryProductLimitCone 📖	CompOp	2 math math: binaryProductLimitCone_cone_pt, binaryProductLimitCone_isLimit_lift
cartesianMonoidalCategory 📖	CompOp	2 math math: μ_forget_apply, tensorObj_eq
instBraidedCategory 📖	CompOp	1 math math: μ_forget_apply
instBraidedForgetMonoidHomCarrier 📖	CompOp	1 math math: μ_forget_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binaryProductLimitCone_cone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CommGrpCat instCategory CategoryTheory.Limits.pair CategoryTheory.Limits.LimitCone.cone binaryProductLimitCone of carrier Prod.instCommGroup str	—	—
binaryProductLimitCone_isLimit_lift 📖	mathematical	—	CategoryTheory.Limits.IsLimit.lift CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CommGrpCat instCategory CategoryTheory.Limits.pair of carrier Prod.instCommGroup str ofHom MonoidHom.fst Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MonoidHom.snd CategoryTheory.Limits.LimitCone.isLimit binaryProductLimitCone CategoryTheory.Limits.Cone.pt MonoidHom.prod Hom.hom CategoryTheory.Limits.BinaryFan.fst CategoryTheory.Limits.BinaryFan.snd	—	—
tensorObj_eq 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CommGrpCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory of carrier Prod.instCommGroup str	—	—
μ_forget_apply 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CommGrpCat instCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.types CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CategoryTheory.Functor.LaxBraided.toLaxMonoidal instBraidedCategory CategoryTheory.instBraidedCategoryType CategoryTheory.Functor.Braided.toLaxBraided instBraidedForgetMonoidHomCarrier CategoryTheory.Functor.obj	—	CategoryTheory.Functor.Monoidal.μ_fst CategoryTheory.Functor.Monoidal.μ_snd

GrpCat

Definitions

Name	Category	Theorems
binaryProductLimitCone 📖	CompOp	2 math math: binaryProductLimitCone_cone_pt, binaryProductLimitCone_isLimit_lift
cartesianMonoidalCategoryGrp 📖	CompOp	2 math math: tensorObj_eq, μ_forget_apply
instBraidedCategory 📖	CompOp	1 math math: μ_forget_apply
instBraidedForgetMonoidHomCarrier 📖	CompOp	1 math math: μ_forget_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binaryProductLimitCone_cone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory GrpCat instCategory CategoryTheory.Limits.pair CategoryTheory.Limits.LimitCone.cone binaryProductLimitCone of carrier Prod.instGroup str	—	—
binaryProductLimitCone_isLimit_lift 📖	mathematical	—	CategoryTheory.Limits.IsLimit.lift CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory GrpCat instCategory CategoryTheory.Limits.pair of carrier Prod.instGroup str ofHom MonoidHom.fst Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.snd CategoryTheory.Limits.LimitCone.isLimit binaryProductLimitCone CategoryTheory.Limits.Cone.pt MonoidHom.prod Hom.hom CategoryTheory.Limits.BinaryFan.fst CategoryTheory.Limits.BinaryFan.snd	—	—
tensorObj_eq 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj GrpCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategoryGrp of carrier Prod.instGroup str	—	—
μ_forget_apply 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ GrpCat instCategory CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategoryGrp CategoryTheory.types CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CategoryTheory.Functor.LaxBraided.toLaxMonoidal instBraidedCategory CategoryTheory.instBraidedCategoryType CategoryTheory.Functor.Braided.toLaxBraided instBraidedForgetMonoidHomCarrier CategoryTheory.Functor.obj	—	CategoryTheory.Functor.Monoidal.μ_fst CategoryTheory.Functor.Monoidal.μ_snd

---

← Back to Index