Equivalence between Group
and AddGroup
#
This file contains two equivalences:
groupAddGroupEquivalence
: the equivalence betweenGrp
andAddGrp
by sendingX : Grp
toAdditive X
andY : AddGrp
toMultiplicative Y
.commGroupAddCommGroupEquivalence
: the equivalence betweenCommGrp
andAddCommGrp
by sendingX : CommGrp
toAdditive X
andY : AddCommGrp
toMultiplicative Y
.
@[simp]
theorem
Grp.toAddGrp_map
{X : Grp}
{Y : Grp}
(a : ↑X →* ↑Y)
:
Grp.toAddGrp.map a = MonoidHom.toAdditive a
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 Y : Grp} => ⇑MonoidHom.toAdditive, map_id := Grp.toAddGrp.proof_1, map_comp := @Grp.toAddGrp.proof_2 }
Instances For
@[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)
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.
Instances For
@[simp]
theorem
AddGrp.toGrp_map
{X : AddGrp}
{Y : AddGrp}
(a : ↑X →+ ↑Y)
:
AddGrp.toGrp.map a = AddMonoidHom.toMultiplicative a
@[simp]
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.
Instances For
@[simp]
theorem
AddCommGrp.toCommGrp_map
{X : AddCommGrp}
{Y : AddCommGrp}
(a : ↑X →+ ↑Y)
:
AddCommGrp.toCommGrp.map a = AddMonoidHom.toMultiplicative a
@[simp]
theorem
AddCommGrp.toCommGrp_obj
(X : AddCommGrp)
:
AddCommGrp.toCommGrp.obj X = CommGrp.of (Multiplicative ↑X)
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.
Instances For
@[simp]
@[simp]
theorem
groupAddGroupEquivalence_counitIso :
groupAddGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddGrp.toGrp.comp Grp.toAddGrp)
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
The equivalence of categories between CommGrp
and AddCommGrp
.
Equations
- One or more equations did not get rendered due to their size.