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.

@[simp]

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

@[simp]

theorem Grp.toAddGrp_map {X : Grp} {Y : Grp} (a : ↑X →* ↑Y) : Grp.toAddGrp.map a = MonoidHom.toAdditive a

def Grp.toAddGrp : CategoryTheory.Functor Grp AddGrp

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

Equations

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

@[simp]

theorem CommGrp.toAddCommGrp_map {X : CommGrp} {Y : CommGrp} (a : ↑X →* ↑Y) : CommGrp.toAddCommGrp.map a = MonoidHom.toAdditive a

@[simp]

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

def CommGrp.toAddCommGrp : CategoryTheory.Functor CommGrp AddCommGrp

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

Equations

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

@[simp]

theorem AddGrp.toGrp_map {X : AddGrp} {Y : AddGrp} (a : ↑X →+ ↑Y) : AddGrp.toGrp.map a = AddMonoidHom.toMultiplicative a

@[simp]

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

def AddGrp.toGrp : CategoryTheory.Functor AddGrp Grp

The functor AddGroup ⥤ Group 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_obj (X : AddCommGrp) : AddCommGrp.toCommGrp.obj X = CommGrp.of (Multiplicative ↑X)

@[simp]

theorem AddCommGrp.toCommGrp_map {X : AddCommGrp} {Y : AddCommGrp} (a : ↑X →+ ↑Y) : AddCommGrp.toCommGrp.map a = AddMonoidHom.toMultiplicative a

def AddCommGrp.toCommGrp : CategoryTheory.Functor AddCommGrp CommGrp

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

Equations

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

def groupAddGroupEquivalence : Grp ≌ AddGrp

The equivalence of categories between Group and AddGroup

Equations

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

def commGroupAddCommGroupEquivalence : CommGrp ≌ AddCommGrp

The equivalence of categories between CommGroup and AddCommGroup.

Equations

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