EquivalenceGroupAddGroup

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

Statistics

Metric	Count
Definitions toCommGrp, toGrp, toAddCommGrp, toAddGrp, commGroupAddCommGroupEquivalence, groupAddGroupEquivalence	6
Theorems toCommGrp_map, toCommGrp_obj_coe, toGrp_map, toGrp_obj_coe, toAddCommGrp_map, toAddCommGrp_obj_coe, toAddGrp_map, toAddGrp_obj_coe, commGroupAddCommGroupEquivalence_counitIso, commGroupAddCommGroupEquivalence_functor, commGroupAddCommGroupEquivalence_inverse, commGroupAddCommGroupEquivalence_unitIso, groupAddGroupEquivalence_counitIso, groupAddGroupEquivalence_functor, groupAddGroupEquivalence_inverse, groupAddGroupEquivalence_unitIso	16
Total	22

AddCommGrpCat

Definitions

Name	Category	Theorems
toCommGrp 📖	CompOp	4 math math: commGroupAddCommGroupEquivalence_counitIso, toCommGrp_obj_coe, commGroupAddCommGroupEquivalence_inverse, toCommGrp_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCommGrp_map 📖	mathematical	—	CategoryTheory.Functor.map AddCommGrpCat instCategory CommGrpCat CommGrpCat.instCategory toCommGrp CommGrpCat.ofHom Multiplicative carrier Multiplicative.commGroup str DFunLike.coe Equiv AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup MonoidHom MulOneClass.toMulOne Multiplicative.mulOneClass EquivLike.toFunLike Equiv.instEquivLike AddMonoidHom.toMultiplicative Hom.hom	—	—
toCommGrp_obj_coe 📖	mathematical	—	CommGrpCat.carrier CategoryTheory.Functor.obj AddCommGrpCat instCategory CommGrpCat CommGrpCat.instCategory toCommGrp Multiplicative carrier	—	—

AddGrpCat

Definitions

Name	Category	Theorems
toGrp 📖	CompOp	4 math math: toGrp_obj_coe, toGrp_map, groupAddGroupEquivalence_inverse, groupAddGroupEquivalence_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toGrp_map 📖	mathematical	—	CategoryTheory.Functor.map AddGrpCat instCategory GrpCat GrpCat.instCategory toGrp GrpCat.ofHom Multiplicative carrier Multiplicative.group str DFunLike.coe Equiv AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MonoidHom MulOneClass.toMulOne Multiplicative.mulOneClass EquivLike.toFunLike Equiv.instEquivLike AddMonoidHom.toMultiplicative Hom.hom	—	—
toGrp_obj_coe 📖	mathematical	—	GrpCat.carrier CategoryTheory.Functor.obj AddGrpCat instCategory GrpCat GrpCat.instCategory toGrp Multiplicative carrier	—	—

CommGrpCat

Definitions

Name	Category	Theorems
toAddCommGrp 📖	CompOp	4 math math: commGroupAddCommGroupEquivalence_functor, commGroupAddCommGroupEquivalence_counitIso, toAddCommGrp_obj_coe, toAddCommGrp_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddCommGrp_map 📖	mathematical	—	CategoryTheory.Functor.map CommGrpCat instCategory AddCommGrpCat AddCommGrpCat.instCategory toAddCommGrp AddCommGrpCat.ofHom Additive carrier Additive.addCommGroup str DFunLike.coe Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup AddMonoidHom AddZeroClass.toAddZero Additive.addZeroClass EquivLike.toFunLike Equiv.instEquivLike MonoidHom.toAdditive Hom.hom	—	—
toAddCommGrp_obj_coe 📖	mathematical	—	AddCommGrpCat.carrier CategoryTheory.Functor.obj CommGrpCat instCategory AddCommGrpCat AddCommGrpCat.instCategory toAddCommGrp Additive carrier	—	—

GrpCat

Definitions

Name	Category	Theorems
toAddGrp 📖	CompOp	4 math math: toAddGrp_map, groupAddGroupEquivalence_functor, groupAddGroupEquivalence_counitIso, toAddGrp_obj_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddGrp_map 📖	mathematical	—	CategoryTheory.Functor.map GrpCat instCategory AddGrpCat AddGrpCat.instCategory toAddGrp AddGrpCat.ofHom Additive carrier Additive.addGroup str DFunLike.coe Equiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddMonoidHom AddZeroClass.toAddZero Additive.addZeroClass EquivLike.toFunLike Equiv.instEquivLike MonoidHom.toAdditive Hom.hom	—	—
toAddGrp_obj_coe 📖	mathematical	—	AddGrpCat.carrier CategoryTheory.Functor.obj GrpCat instCategory AddGrpCat AddGrpCat.instCategory toAddGrp Additive carrier	—	—

(root)

Definitions

Name	Category	Theorems
commGroupAddCommGroupEquivalence 📖	CompOp	4 math math: commGroupAddCommGroupEquivalence_functor, commGroupAddCommGroupEquivalence_counitIso, commGroupAddCommGroupEquivalence_unitIso, commGroupAddCommGroupEquivalence_inverse
groupAddGroupEquivalence 📖	CompOp	4 math math: groupAddGroupEquivalence_inverse, groupAddGroupEquivalence_functor, groupAddGroupEquivalence_unitIso, groupAddGroupEquivalence_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commGroupAddCommGroupEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CommGrpCat AddCommGrpCat CommGrpCat.instCategory AddCommGrpCat.instCategory commGroupAddCommGroupEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp AddCommGrpCat.toCommGrp CommGrpCat.toAddCommGrp	—	—
commGroupAddCommGroupEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CommGrpCat AddCommGrpCat CommGrpCat.instCategory AddCommGrpCat.instCategory commGroupAddCommGroupEquivalence CommGrpCat.toAddCommGrp	—	—
commGroupAddCommGroupEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CommGrpCat AddCommGrpCat CommGrpCat.instCategory AddCommGrpCat.instCategory commGroupAddCommGroupEquivalence AddCommGrpCat.toCommGrp	—	—
commGroupAddCommGroupEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CommGrpCat AddCommGrpCat CommGrpCat.instCategory AddCommGrpCat.instCategory commGroupAddCommGroupEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
groupAddGroupEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso GrpCat AddGrpCat GrpCat.instCategory AddGrpCat.instCategory groupAddGroupEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp AddGrpCat.toGrp GrpCat.toAddGrp	—	—
groupAddGroupEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor GrpCat AddGrpCat GrpCat.instCategory AddGrpCat.instCategory groupAddGroupEquivalence GrpCat.toAddGrp	—	—
groupAddGroupEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse GrpCat AddGrpCat GrpCat.instCategory AddGrpCat.instCategory groupAddGroupEquivalence AddGrpCat.toGrp	—	—
groupAddGroupEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso GrpCat AddGrpCat GrpCat.instCategory AddGrpCat.instCategory groupAddGroupEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—

---

← Back to Index