Equivalence between Group and AddGroup

This file contains two equivalences:

• groupAddGroupEquivalence : the equivalence between GrpCat and AddGrpCat by sending X : GrpCat to Additive X and Y : AddGrpCat to Multiplicative Y.
• commGroupAddCommGroupEquivalence : the equivalence between CommGrpCat and AddCommGrpCat by sending X : CommGrpCat to Additive X and Y : AddCommGrpCat to Multiplicative Y.

def GrpCat.toAddGrp : CategoryTheory.Functor GrpCat AddGrpCat

The functor GrpCat ⥤ AddGrpCat by sending X ↦ Additive X and f ↦ f.

@[simp]

theorem GrpCat.toAddGrp_map {x✝ x✝¹ : GrpCat} (f : x✝ ⟶ x✝¹) : toAddGrp.map f = AddGrpCat.ofHom (MonoidHom.toAdditive (Hom.hom f))

@[simp]

theorem GrpCat.toAddGrp_obj_coe (X : GrpCat) : ↑(toAddGrp.obj X) = Additive ↑X

def CommGrpCat.toAddCommGrp : CategoryTheory.Functor CommGrpCat AddCommGrpCat

The functor CommGrpCat ⥤ AddCommGrpCat by sending X ↦ Additive X and f ↦ f.

@[simp]

theorem CommGrpCat.toAddCommGrp_map {x✝ x✝¹ : CommGrpCat} (f : x✝ ⟶ x✝¹) : toAddCommGrp.map f = AddCommGrpCat.ofHom (MonoidHom.toAdditive (Hom.hom f))

@[simp]

theorem CommGrpCat.toAddCommGrp_obj_coe (X : CommGrpCat) : ↑(toAddCommGrp.obj X) = Additive ↑X

def AddGrpCat.toGrp : CategoryTheory.Functor AddGrpCat GrpCat

The functor AddGrpCat ⥤ GrpCat by sending X ↦ Multiplicative X and f ↦ f.

@[simp]

theorem AddGrpCat.toGrp_map {x✝ x✝¹ : AddGrpCat} (f : x✝ ⟶ x✝¹) : toGrp.map f = GrpCat.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))

@[simp]

theorem AddGrpCat.toGrp_obj_coe (X : AddGrpCat) : ↑(toGrp.obj X) = Multiplicative ↑X

def AddCommGrpCat.toCommGrp : CategoryTheory.Functor AddCommGrpCat CommGrpCat

The functor AddCommGrpCat ⥤ CommGrpCat by sending X ↦ Multiplicative X and f ↦ f.

@[simp]

theorem AddCommGrpCat.toCommGrp_map {x✝ x✝¹ : AddCommGrpCat} (f : x✝ ⟶ x✝¹) : toCommGrp.map f = CommGrpCat.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))

@[simp]

theorem AddCommGrpCat.toCommGrp_obj_coe (X : AddCommGrpCat) : ↑(toCommGrp.obj X) = Multiplicative ↑X

def groupAddGroupEquivalence : GrpCat ≌ AddGrpCat

The equivalence of categories between GrpCat and AddGrpCat

@[simp]

theorem groupAddGroupEquivalence_unitIso : groupAddGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id GrpCat)

@[simp]

theorem groupAddGroupEquivalence_functor : groupAddGroupEquivalence.functor = GrpCat.toAddGrp

@[simp]

theorem groupAddGroupEquivalence_inverse : groupAddGroupEquivalence.inverse = AddGrpCat.toGrp

@[simp]

theorem groupAddGroupEquivalence_counitIso : groupAddGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddGrpCat.toGrp.comp GrpCat.toAddGrp)

def commGroupAddCommGroupEquivalence : CommGrpCat ≌ AddCommGrpCat

The equivalence of categories between CommGrpCat and AddCommGrpCat.

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse : commGroupAddCommGroupEquivalence.inverse = AddCommGrpCat.toCommGrp

@[simp]

theorem commGroupAddCommGroupEquivalence_functor : commGroupAddCommGroupEquivalence.functor = CommGrpCat.toAddCommGrp

@[simp]

theorem commGroupAddCommGroupEquivalence_counitIso : commGroupAddCommGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddCommGrpCat.toCommGrp.comp CommGrpCat.toAddCommGrp)

@[simp]

theorem commGroupAddCommGroupEquivalence_unitIso : commGroupAddCommGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CommGrpCat)