Documentation

Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup

Equivalence between Group and AddGroup #

This file contains two equivalences:

source
def Grp.toAddGrp :
CategoryTheory.Functor Grp AddGrp

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Grp.toAddGrp_map {x✝ x✝¹ : Grp} (f : x✝ ⟶ x✝¹) :
toAddGrp.map f = AddGrp.ofHom (MonoidHom.toAdditive (Hom.hom f))
source
@[simp]
theorem Grp.toAddGrp_obj_coe (X : Grp) :
↑(toAddGrp.obj X) = Additive ↑X
source
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.
source
@[simp]
theorem CommGrp.toAddCommGrp_map {x✝ x✝¹ : CommGrp} (f : x✝ ⟶ x✝¹) :
toAddCommGrp.map f = AddCommGrp.ofHom (MonoidHom.toAdditive (Hom.hom f))
source
@[simp]
theorem CommGrp.toAddCommGrp_obj_coe (X : CommGrp) :
↑(toAddCommGrp.obj X) = Additive ↑X
source
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.
source
@[simp]
theorem AddGrp.toGrp_obj_coe (X : AddGrp) :
↑(toGrp.obj X) = Multiplicative ↑X
source
@[simp]
theorem AddGrp.toGrp_map {x✝ x✝¹ : AddGrp} (f : x✝ ⟶ x✝¹) :
toGrp.map f = Grp.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))
source
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.
source
@[simp]
theorem AddCommGrp.toCommGrp_map {x✝ x✝¹ : AddCommGrp} (f : x✝ ⟶ x✝¹) :
toCommGrp.map f = CommGrp.ofHom (AddMonoidHom.toMultiplicative (Hom.hom f))
source
@[simp]
theorem AddCommGrp.toCommGrp_obj_coe (X : AddCommGrp) :
↑(toCommGrp.obj X) = Multiplicative ↑X
source
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.
source
@[simp]
theorem groupAddGroupEquivalence_functor :
groupAddGroupEquivalence.functor = Grp.toAddGrp
source
@[simp]
theorem groupAddGroupEquivalence_inverse :
groupAddGroupEquivalence.inverse = AddGrp.toGrp
source
@[simp]
theorem groupAddGroupEquivalence_unitIso :
groupAddGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Grp)
source
@[simp]
theorem groupAddGroupEquivalence_counitIso :
groupAddGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddGrp.toGrp.comp Grp.toAddGrp)
source
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.
source
@[simp]
theorem commGroupAddCommGroupEquivalence_inverse :
commGroupAddCommGroupEquivalence.inverse = AddCommGrp.toCommGrp
source
@[simp]
theorem commGroupAddCommGroupEquivalence_unitIso :
commGroupAddCommGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id CommGrp)
source
@[simp]
theorem commGroupAddCommGroupEquivalence_counitIso :
commGroupAddCommGroupEquivalence.counitIso = CategoryTheory.Iso.refl (AddCommGrp.toCommGrp.comp CommGrp.toAddCommGrp)
source
@[simp]
theorem commGroupAddCommGroupEquivalence_functor :
commGroupAddCommGroupEquivalence.functor = CommGrp.toAddCommGrp