CommGrp_

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

Statistics

Metric	Count
Definitions CommGrpObj, ofRepresentableBy, toGrpObj, CommGrp_Class, ofRepresentableBy, yonedaCommGrpGrp, yonedaCommGrpGrpObj	7
Theorems toIsCommMonObj, yonedaCommGrpGrpObj_map, yonedaCommGrpGrpObj_obj_coe, yonedaCommGrpGrp_map_app, yonedaCommGrpGrp_obj	5
Total	12

CategoryTheory

Definitions

Name	Category	Theorems
CommGrpObj 📖	CompData	—
CommGrp_Class 📖	CompOp	—
yonedaCommGrpGrp 📖	CompOp	2 math math: yonedaCommGrpGrp_obj, yonedaCommGrpGrp_map_app
yonedaCommGrpGrpObj 📖	CompOp	4 math math: yonedaCommGrpGrpObj_map, yonedaCommGrpGrp_obj, yonedaCommGrpGrpObj_obj_coe, yonedaCommGrpGrp_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
yonedaCommGrpGrpObj_map 📖	mathematical	—	Functor.map Opposite Grp Category.opposite Grp.instCategory CommGrpCat CommGrpCat.instCategory yonedaCommGrpGrpObj CommGrpCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop CommGrp.toGrp Hom.commGroup Grp.instCartesianMonoidalCategory Grp.instGrpObj CommGrp.comm Grp.instBraidedCategory MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulOne.toOne CategoryStruct.comp Quiver.Hom.unop	—	CommGrp.comm
yonedaCommGrpGrpObj_obj_coe 📖	mathematical	—	CommGrpCat.carrier Functor.obj Opposite Grp Category.opposite Grp.instCategory CommGrpCat CommGrpCat.instCategory yonedaCommGrpGrpObj Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop CommGrp.toGrp	—	—
yonedaCommGrpGrp_map_app 📖	mathematical	—	NatTrans.app Opposite Grp Category.opposite Grp.instCategory CommGrpCat CommGrpCat.instCategory yonedaCommGrpGrpObj Functor.map CommGrp CommGrp.instCategory Functor Functor.category yonedaCommGrpGrp CommGrpCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop CommGrp.toGrp Hom.commGroup Grp.instCartesianMonoidalCategory Grp.instGrpObj CommGrp.comm Grp.instBraidedCategory MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup MulOne.toOne CategoryStruct.comp InducedCategory.Hom.hom	—	CommGrp.comm
yonedaCommGrpGrp_obj 📖	mathematical	—	Functor.obj CommGrp CommGrp.instCategory Functor Opposite Grp Category.opposite Grp.instCategory CommGrpCat CommGrpCat.instCategory Functor.category yonedaCommGrpGrp yonedaCommGrpGrpObj	—	—

CategoryTheory.CommGrpObj

Definitions

Name	Category	Theorems
ofRepresentableBy 📖	CompOp	—
toGrpObj 📖	CompOp	1 math math: toIsCommMonObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsCommMonObj 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj toGrpObj	—	—

CategoryTheory.CommGrp_Class

Definitions

Name	Category	Theorems
ofRepresentableBy 📖	CompOp	—

---

← Back to Index