# Equivalence between Group and AddGroup#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains two equivalences:

• Group_AddGroup_equivalence : the equivalence between Group and AddGroup by sending X : Group to additive X and Y : AddGroup to multiplicative Y.
• CommGroup_AddCommGroup_equivalence : the equivalence between CommGroup and AddCommGroup by sending X : CommGroup to additive X and Y : AddCommGroup to multiplicative Y.
@[simp]
theorem Group.to_AddGroup_map (X Y : Group) (ᾰ : X →* Y) :

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

Equations
@[simp]
theorem Group.to_AddGroup_obj (X : Group) :
@[simp]
theorem CommGroup.to_AddCommGroup_map (X Y : CommGroup) (ᾰ : X →* Y) :

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

Equations
@[simp]
theorem AddGroup.to_Group_map (X Y : AddGroup) (ᾰ : X →+ Y) :
@[simp]

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

Equations

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

Equations
@[simp]
@[simp]
theorem AddCommGroup.to_CommGroup_map (X Y : AddCommGroup) (ᾰ : X →+ Y) :
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_zpow (X : AddGroup) (ᾰ : ) (ᾰ_1 : multiplicative X) :
ᾰ_1 = ᾰ_1 ^
@[simp]
+ ᾰ_1 = ᾰ_1
@[simp]
@[simp]
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_npow (X : AddGroup) (ᾰ : ) (ᾰ_1 : multiplicative X) :
ᾰ_1 = ᾰ_1
@[simp]
@[simp]
@[simp]
* ᾰ_1 = ᾰ_1

The equivalence of categories between Group and AddGroup

Equations
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_zsmul (X : Group) (ᾰ : ) (ᾰ_1 : additive X) :
ᾰ_1 = ᾰ_1
@[simp]
- ᾰ_1 = ᾰ_1
@[simp]
/ ᾰ_1 = ᾰ_1
@[simp]
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_nsmul (X : Group) (ᾰ : ) (ᾰ_1 : additive X) :
ᾰ_1 = ᾰ_1
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_nsmul (X : CommGroup) (ᾰ : ) (ᾰ_1 : additive X) :
ᾰ_1 = ᾰ_1

The equivalence of categories between CommGroup and AddCommGroup.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]