Equivalence between Group and AddGroup

This file contains two equivalences:

• groupAddGroupEquivalence : the equivalence between Grp and AddGrp by sending X : Grp to Additive X and Y : AddGrp to Multiplicative Y.
• commGroupAddCommGroupEquivalence : the equivalence between CommGrp and AddCommGrp by sending X : CommGrp to Additive X and Y : AddCommGrp to Multiplicative Y.

def Grp.toAddGrp : CategoryTheory.Functor Grp AddGrp

The functor Grp ⥤ AddGrp by sending X ↦ Additive X and f ↦ f.

Equations

• Grp.toAddGrp = { obj := fun (X : Grp) => AddGrp.of (Additive ↑X), map := fun {x x_1 : Grp} => ⇑MonoidHom.toAdditive, map_id := Grp.toAddGrp.proof_1, map_comp := @Grp.toAddGrp.proof_2 }

@[simp]

theorem Grp.toAddGrp_obj (X : Grp) : Grp.toAddGrp.obj X = AddGrp.of (Additive ↑X)

@[simp]

theorem Grp.toAddGrp_map : ∀ {x x_1 : Grp} (a : ↑x →* ↑x_1), Grp.toAddGrp.map a = MonoidHom.toAdditive a

def CommGrp.toAddCommGrp : CategoryTheory.Functor CommGrp AddCommGrp

The functor CommGrp ⥤ AddCommGrp by sending X ↦ Additive X and f ↦ f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommGrp.toAddCommGrp_map : ∀ {x x_1 : CommGrp} (a : ↑x →* ↑x_1), CommGrp.toAddCommGrp.map a = MonoidHom.toAdditive a

@[simp]

theorem CommGrp.toAddCommGrp_obj (X : CommGrp) : CommGrp.toAddCommGrp.obj X = AddCommGrp.of (Additive ↑X)

def AddGrp.toGrp : CategoryTheory.Functor AddGrp Grp

The functor AddGrp ⥤ Grp by sending X ↦ Multiplicative Y and f ↦ f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddGrp.toGrp_map : ∀ {x x_1 : AddGrp} (a : ↑x →+ ↑x_1), AddGrp.toGrp.map a = AddMonoidHom.toMultiplicative a

@[simp]

theorem AddGrp.toGrp_obj (X : AddGrp) : AddGrp.toGrp.obj X = Grp.of (Multiplicative ↑X)

def AddCommGrp.toCommGrp : CategoryTheory.Functor AddCommGrp CommGrp

The functor AddCommGrp ⥤ CommGrp by sending X ↦ Multiplicative Y and f ↦ f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddCommGrp.toCommGrp_map : ∀ {x x_1 : AddCommGrp} (a : ↑x →+ ↑x_1), AddCommGrp.toCommGrp.map a = AddMonoidHom.toMultiplicative a

@[simp]

theorem AddCommGrp.toCommGrp_obj (X : AddCommGrp) : AddCommGrp.toCommGrp.obj X = CommGrp.of (Multiplicative ↑X)

def groupAddGroupEquivalence : Grp ≌ AddGrp

The equivalence of categories between Grp and AddGrp

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem groupAddGroupEquivalence_counitIso : groupAddGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddGrp.toGrp.comp Grp.toAddGrp)

@[simp]

theorem groupAddGroupEquivalence_functor : groupAddGroupEquivalence.functor = Grp.toAddGrp

@[simp]

theorem groupAddGroupEquivalence_inverse : groupAddGroupEquivalence.inverse = AddGrp.toGrp

def commGroupAddCommGroupEquivalence : CommGrp ≌ AddCommGrp

The equivalence of categories between CommGrp and AddCommGrp.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem commGroupAddCommGroupEquivalence_functor : commGroupAddCommGroupEquivalence.functor = CommGrp.toAddCommGrp

@[simp]

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

@[simp]

theorem commGroupAddCommGroupEquivalence_counitIso : commGroupAddCommGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddCommGrp.toCommGrp.comp CommGrp.toAddCommGrp)

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse : commGroupAddCommGroupEquivalence.inverse = AddCommGrp.toCommGrp