# Equivalence between Group and AddGroup#

This file contains two equivalences:

• groupAddGroupEquivalence : the equivalence between GroupCat and AddGroupCat by sending X : GroupCat to Additive X and Y : AddGroupCat to Multiplicative Y.
• commGroupAddCommGroupEquivalence : the equivalence between CommGroupCat and AddCommGroupCat by sending X : CommGroupCat to Additive X and Y : AddCommGroupCat to Multiplicative Y.
@[simp]
theorem GroupCat.toAddGroupCat_map {X : GroupCat} {Y : GroupCat} (a : X →* Y) :

The functor Group ⥤ AddGroup by sending X ↦ additive X and f ↦ f.

Instances For
@[simp]
theorem CommGroupCat.toAddCommGroupCat_map {X : CommGroupCat} {Y : CommGroupCat} (a : X →* Y) :

The functor CommGroup ⥤ AddCommGroup by sending X ↦ additive X and f ↦ f.

Instances For
@[simp]

The functor AddGroup ⥤ Group by sending X ↦ multiplicative Y and f ↦ f.

Instances For
@[simp]

The functor AddCommGroup ⥤ CommGroup by sending X ↦ multiplicative Y and f ↦ f.

Instances For
@[simp]
∀ (a : ), ↑(groupAddGroupEquivalence.counitIso.hom.app X) a = ().toEquiv a
@[simp]
@[simp]
theorem groupAddGroupEquivalence_inverse_obj_str_div (X : AddGroupCat) (x : ) (y : ) :
x / y = x / y
@[simp]
theorem groupAddGroupEquivalence_inverse_map_apply {X : AddGroupCat} {Y : AddGroupCat} (a : X →+ Y) (a : ) :
@[simp]
∀ (a : ) (a_1 : X), = a a_1
@[simp]
theorem groupAddGroupEquivalence_functor_map_apply {X : GroupCat} {Y : GroupCat} (a : X →* Y) (a : Additive X) :
@[simp]
x - y = x - y
@[simp]
∀ (x x_1 : ), x * x_1 = x * x_1
@[simp]
∀ (x x_1 : Additive X), x + x_1 = x + x_1
@[simp]
theorem groupAddGroupEquivalence_functor_obj_str_nsmul (X : GroupCat) :
∀ (a : ) (a_1 : X), a a_1 = a_1 ^ a
@[simp]
theorem groupAddGroupEquivalence_unitIso_hom_app_apply (X : GroupCat) :
@[simp]
@[simp]
theorem groupAddGroupEquivalence_unitIso_inv_app_apply (X : GroupCat) :
@[simp]
∀ (a : ) (a_1 : X), Monoid.npow a a_1 = a a_1
@[simp]
theorem groupAddGroupEquivalence_functor_obj_str_zsmul (X : GroupCat) :
∀ (a : ) (a_1 : X), a a_1 = a_1 ^ a
@[simp]
∀ (a : ↑()), ↑(groupAddGroupEquivalence.counitIso.inv.app X) a = ().toEquiv a

The equivalence of categories between Group and AddGroup

Instances For
@[simp]
@[simp]
theorem commGroupAddCommGroupEquivalence_functor_obj_str_zsmul (X : CommGroupCat) :
∀ (a : ) (a_1 : X), a a_1 = a_1 ^ a
@[simp]
∀ (x x_1 : Additive X), x + x_1 = x + x_1
@[simp]
theorem commGroupAddCommGroupEquivalence_unitIso_hom_app_apply (X : CommGroupCat) :
@[simp]
theorem commGroupAddCommGroupEquivalence_inverse_map_apply {X : AddCommGroupCat} {Y : AddCommGroupCat} (a : X →+ Y) (a : ) :
@[simp]
theorem commGroupAddCommGroupEquivalence_functor_obj_str_nsmul (X : CommGroupCat) :
∀ (a : ) (a_1 : X), a a_1 = a_1 ^ a
@[simp]
∀ (a : ↑()), ↑(commGroupAddCommGroupEquivalence.counitIso.inv.app X) a = ().symm a
@[simp]
@[simp]
∀ (x x_1 : ), x * x_1 = x * x_1
@[simp]
theorem commGroupAddCommGroupEquivalence_functor_map_apply {X : CommGroupCat} {Y : CommGroupCat} (a : X →* Y) (a : Additive X) :
The equivalence of categories between CommGroup and AddCommGroup.