CommGrp_

📁 Source: Mathlib/CategoryTheory/Preadditive/CommGrp_.lean

Statistics

Metric	Count
Definitions CommGrp_, commGrpEquivalence, commGrpEquivalenceAux, instGrpObj, toCommGrp	5
Theorems commGrpEquivalenceAux_hom_app_hom_hom_hom, commGrpEquivalenceAux_inv_app_hom_hom_hom, commGrpEquivalence_counitIso_hom_app_hom_hom_hom, commGrpEquivalence_counitIso_inv_app_hom_hom_hom, commGrpEquivalence_functor_map_hom_hom_hom, commGrpEquivalence_functor_obj_X, commGrpEquivalence_functor_obj_grp_inv, commGrpEquivalence_functor_obj_grp_mul, commGrpEquivalence_functor_obj_grp_one, commGrpEquivalence_inverse_map, commGrpEquivalence_inverse_obj, commGrpEquivalence_unitIso_hom_app, commGrpEquivalence_unitIso_inv_app, instIsCommMonObj, inv_def, mul_def, one_def, toCommGrp_map, toCommGrp_obj_X, toCommGrp_obj_grp	20
Total	25

CategoryTheory

Definitions

Name	Category	Theorems
CommGrp_ 📖	CompOp	—

CategoryTheory.Preadditive

Definitions

Name	Category	Theorems
commGrpEquivalence 📖	CompOp	11 math math: commGrpEquivalence_functor_obj_grp_one, commGrpEquivalence_unitIso_inv_app, commGrpEquivalence_unitIso_hom_app, commGrpEquivalence_functor_obj_grp_mul, commGrpEquivalence_functor_obj_grp_inv, commGrpEquivalence_functor_obj_X, commGrpEquivalence_counitIso_inv_app_hom_hom_hom, commGrpEquivalence_counitIso_hom_app_hom_hom_hom, commGrpEquivalence_inverse_map, commGrpEquivalence_functor_map_hom_hom_hom, commGrpEquivalence_inverse_obj
commGrpEquivalenceAux 📖	CompOp	2 math math: commGrpEquivalenceAux_hom_app_hom_hom_hom, commGrpEquivalenceAux_inv_app_hom_hom_hom
instGrpObj 📖	CompOp	7 math math: toCommGrp_map, instIsCommMonObj, toCommGrp_obj_grp, inv_def, mul_def, one_def, commGrpEquivalence_functor_map_hom_hom_hom
toCommGrp 📖	CompOp	7 math math: toCommGrp_map, commGrpEquivalenceAux_hom_app_hom_hom_hom, commGrpEquivalenceAux_inv_app_hom_hom_hom, toCommGrp_obj_grp, commGrpEquivalence_counitIso_inv_app_hom_hom_hom, commGrpEquivalence_counitIso_hom_app_hom_hom_hom, toCommGrp_obj_X

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commGrpEquivalenceAux_hom_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.comp CategoryTheory.CommGrp.forget toCommGrp CategoryTheory.CommGrp.grp CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category commGrpEquivalenceAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
commGrpEquivalenceAux_inv_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.id CategoryTheory.CommGrp.grp CategoryTheory.Functor.comp CategoryTheory.CommGrp.forget toCommGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category commGrpEquivalenceAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
commGrpEquivalence_counitIso_hom_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.comp CategoryTheory.CommGrp.forget toCommGrp CategoryTheory.CommGrp.grp CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso commGrpEquivalence CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
commGrpEquivalence_counitIso_inv_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.id CategoryTheory.CommGrp.grp CategoryTheory.Functor.comp CategoryTheory.CommGrp.forget toCommGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso commGrpEquivalence CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
commGrpEquivalence_functor_map_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.CommGrp.toGrp instGrpObj instIsCommMonObj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp CategoryTheory.Grp.instCategory CategoryTheory.Functor.map CategoryTheory.CommGrp.instCategory CategoryTheory.Equivalence.functor commGrpEquivalence	—	instIsCommMonObj
commGrpEquivalence_functor_obj_X 📖	mathematical	—	CategoryTheory.CommGrp.X CategoryTheory.Functor.obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Equivalence.functor commGrpEquivalence	—	—
commGrpEquivalence_functor_obj_grp_inv 📖	mathematical	—	CategoryTheory.GrpObj.inv CategoryTheory.CommGrp.grp CategoryTheory.Functor.obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Equivalence.functor commGrpEquivalence Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup CategoryTheory.CategoryStruct.id	—	—
commGrpEquivalence_functor_obj_grp_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.Functor.obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Equivalence.functor commGrpEquivalence Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid homGroup CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
commGrpEquivalence_functor_obj_grp_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.Functor.obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Equivalence.functor commGrpEquivalence Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	—
commGrpEquivalence_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Equivalence.inverse commGrpEquivalence CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.CommGrp.forget₂Grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp.toGrp	—	—
commGrpEquivalence_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Equivalence.inverse commGrpEquivalence CategoryTheory.CommGrp.X	—	—
commGrpEquivalence_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory commGrpEquivalence CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
commGrpEquivalence_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory commGrpEquivalence CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
instIsCommMonObj 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj instGrpObj	—	comp_add CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd add_comm
inv_def 📖	mathematical	—	CategoryTheory.GrpObj.inv instGrpObj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup CategoryTheory.CategoryStruct.id	—	—
mul_def 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj instGrpObj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid homGroup CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.SemiCartesianMonoidalCategory.snd	—	—
one_def 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj instGrpObj Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	—
toCommGrp_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory toCommGrp CategoryTheory.InducedCategory.homMk CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.CommGrp.toGrp instGrpObj instIsCommMonObj CategoryTheory.Grp.homMk''	—	instIsCommMonObj
toCommGrp_obj_X 📖	mathematical	—	CategoryTheory.CommGrp.X CategoryTheory.Functor.obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory toCommGrp	—	—
toCommGrp_obj_grp 📖	mathematical	—	CategoryTheory.CommGrp.grp CategoryTheory.Functor.obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory toCommGrp instGrpObj	—	—

---

← Back to Index