Equivalence between `Group` and `AddGroup` #

This file contains two equivalences:

groupAddGroupEquivalence : the equivalence between GroupCat and AddGroupCat by sending X : GroupCat to Additive X and Y : AddGroupCat to Multiplicative Y.
commGroupAddCommGroupEquivalence : the equivalence between CommGroupCat and AddCommGroupCat by sending X : CommGroupCat to Additive X and Y : AddCommGroupCat to Multiplicative Y.

source

@[simp]

theorem GroupCat.toAddGroupCat_map {X : GroupCat} {Y : GroupCat} (a : ↑X →* ↑Y) :

GroupCat.toAddGroupCat.map a = ↑MonoidHom.toAdditive a

source

@[simp]

theorem GroupCat.toAddGroupCat_obj (X : GroupCat) :

GroupCat.toAddGroupCat.obj X = AddGroupCat.of (Additive ↑X)

source

def GroupCat.toAddGroupCat :

CategoryTheory.Functor GroupCat AddGroupCat

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

Instances For

source

@[simp]

theorem CommGroupCat.toAddCommGroupCat_obj (X : CommGroupCat) :

CommGroupCat.toAddCommGroupCat.obj X = AddCommGroupCat.of (Additive ↑X)

source

@[simp]

theorem CommGroupCat.toAddCommGroupCat_map {X : CommGroupCat} {Y : CommGroupCat} (a : ↑X →* ↑Y) :

CommGroupCat.toAddCommGroupCat.map a = ↑MonoidHom.toAdditive a

source

def CommGroupCat.toAddCommGroupCat :

CategoryTheory.Functor CommGroupCat AddCommGroupCat

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

Instances For

source

@[simp]

theorem AddGroupCat.toGroupCat_obj (X : AddGroupCat) :

AddGroupCat.toGroupCat.obj X = GroupCat.of (Multiplicative ↑X)

source

@[simp]

theorem AddGroupCat.toGroupCat_map {X : AddGroupCat} {Y : AddGroupCat} (a : ↑X →+ ↑Y) :

AddGroupCat.toGroupCat.map a = ↑AddMonoidHom.toMultiplicative a

source

def AddGroupCat.toGroupCat :

CategoryTheory.Functor AddGroupCat GroupCat

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

Instances For

source

@[simp]

theorem AddCommGroupCat.toCommGroupCat_map {X : AddCommGroupCat} {Y : AddCommGroupCat} (a : ↑X →+ ↑Y) :

AddCommGroupCat.toCommGroupCat.map a = ↑AddMonoidHom.toMultiplicative a

source

@[simp]

theorem AddCommGroupCat.toCommGroupCat_obj (X : AddCommGroupCat) :

AddCommGroupCat.toCommGroupCat.obj X = CommGroupCat.of (Multiplicative ↑X)

source

def AddCommGroupCat.toCommGroupCat :

CategoryTheory.Functor AddCommGroupCat CommGroupCat

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

Instances For

source

@[simp]

theorem groupAddGroupEquivalence_counitIso_hom_app_apply (X : AddGroupCat) :

∀ (a : ↑((CategoryTheory.Functor.comp AddGroupCat.toGroupCat GroupCat.toAddGroupCat).obj X)), ↑(groupAddGroupEquivalence.counitIso.hom.app X) a = ↑(AddEquiv.additiveMultiplicative ↑X).toEquiv a

source

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_inv (X : AddGroupCat) (x : Multiplicative ↑X) :

x⁻¹ = ↑Additive.ofMul (-↑Multiplicative.toAdd x)

source

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_div (X : AddGroupCat) (x : Multiplicative ↑X) (y : Multiplicative ↑X) :

x / y = x / y

source

@[simp]

theorem groupAddGroupEquivalence_inverse_map_apply {X : AddGroupCat} {Y : AddGroupCat} (a : ↑X →+ ↑Y) (a : Multiplicative ↑X) :

↑(groupAddGroupEquivalence.inverse.map a) a = ↑Multiplicative.ofAdd (↑a (↑Multiplicative.toAdd a))

source

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_zpow (X : AddGroupCat) :

∀ (a : ℤ) (a_1 : ↑X), DivInvMonoid.zpow a a_1 = a • a_1

source

@[simp]

theorem groupAddGroupEquivalence_functor_obj_α (X : GroupCat) :

↑(groupAddGroupEquivalence.functor.obj X) = Additive ↑X

source

@[simp]

theorem groupAddGroupEquivalence_functor_map_apply {X : GroupCat} {Y : GroupCat} (a : ↑X →* ↑Y) (a : Additive ↑X) :

↑(groupAddGroupEquivalence.functor.map a) a = ↑Additive.ofMul (↑a (↑Additive.toMul a))

source

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_one (X : AddGroupCat) :

1 = 1

source

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_sub (X : GroupCat) (x : Additive ↑X) (y : Additive ↑X) :

x - y = x - y

source

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_mul (X : AddGroupCat) :

∀ (x x_1 : Multiplicative ↑X), x * x_1 = x * x_1

source

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_add (X : GroupCat) :

∀ (x x_1 : Additive ↑X), x + x_1 = x + x_1

source

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_nsmul (X : GroupCat) :

∀ (a : ℕ) (a_1 : ↑X), a • a_1 = a_1 ^ a

source

@[simp]

theorem groupAddGroupEquivalence_unitIso_hom_app_apply (X : GroupCat) :

∀ (a : ↑((CategoryTheory.Functor.id GroupCat).obj X)), ↑(groupAddGroupEquivalence.unitIso.hom.app X) a = ↑(CategoryTheory.CategoryStruct.id (GroupCat.of (Multiplicative (Additive ↑X)))) (↑(CategoryTheory.CategoryStruct.comp (MulEquiv.toMonoidHom (MulEquiv.multiplicativeAdditive ↑X)) (CategoryTheory.CategoryStruct.comp (↑AddMonoidHom.toMultiplicative (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.additiveMultiplicative (Additive ↑X))))) (↑AddMonoidHom.toMultiplicative (↑MonoidHom.toAdditive (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv.multiplicativeAdditive ↑X))))))) a)

source

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_neg (X : GroupCat) (x : Additive ↑X) :

-x = ↑Multiplicative.ofAdd (↑Additive.toMul x)⁻¹

source

@[simp]

theorem groupAddGroupEquivalence_unitIso_inv_app_apply (X : GroupCat) :

∀ (a : ↑((CategoryTheory.Functor.comp GroupCat.toAddGroupCat AddGroupCat.toGroupCat).obj X)), ↑(groupAddGroupEquivalence.unitIso.inv.app X) a = ↑(CategoryTheory.CategoryStruct.comp (↑AddMonoidHom.toMultiplicative (↑MonoidHom.toAdditive (MulEquiv.toMonoidHom (MulEquiv.multiplicativeAdditive ↑X)))) (CategoryTheory.CategoryStruct.comp (↑AddMonoidHom.toMultiplicative (AddEquiv.toAddMonoidHom (AddEquiv.additiveMultiplicative (Additive ↑X)))) (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv.multiplicativeAdditive ↑X))))) (↑(CategoryTheory.CategoryStruct.id (GroupCat.of (Multiplicative (Additive ↑X)))) a)

source

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_α (X : AddGroupCat) :

↑(groupAddGroupEquivalence.inverse.obj X) = Multiplicative ↑X

source

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_npow (X : AddGroupCat) :

∀ (a : ℕ) (a_1 : ↑X), Monoid.npow a a_1 = a • a_1

source

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_zsmul (X : GroupCat) :

∀ (a : ℤ) (a_1 : ↑X), a • a_1 = a_1 ^ a

source

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_zero (X : GroupCat) :

0 = 0

source

@[simp]

theorem groupAddGroupEquivalence_counitIso_inv_app_apply (X : AddGroupCat) :

∀ (a : ↑((CategoryTheory.Functor.id AddGroupCat).obj X)), ↑(groupAddGroupEquivalence.counitIso.inv.app X) a = ↑(AddEquiv.symm (AddEquiv.additiveMultiplicative ↑X)).toEquiv a

source

def groupAddGroupEquivalence :

GroupCat ≌ AddGroupCat

The equivalence of categories between Group and AddGroup

Instances For

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_α (X : CommGroupCat) :

↑(commGroupAddCommGroupEquivalence.functor.obj X) = Additive ↑X

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_α (X : AddCommGroupCat) :

↑(commGroupAddCommGroupEquivalence.inverse.obj X) = Multiplicative ↑X

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_npow (X : AddCommGroupCat) :

∀ (a : ℕ) (a_1 : ↑X), Monoid.npow a a_1 = a • a_1

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_zsmul (X : CommGroupCat) :

∀ (a : ℤ) (a_1 : ↑X), a • a_1 = a_1 ^ a

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_add (X : CommGroupCat) :

∀ (x x_1 : Additive ↑X), x + x_1 = x + x_1

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_one (X : AddCommGroupCat) :

1 = 1

source

@[simp]

theorem commGroupAddCommGroupEquivalence_unitIso_hom_app_apply (X : CommGroupCat) :

∀ (a : ↑((CategoryTheory.Functor.id CommGroupCat).obj X)), ↑(commGroupAddCommGroupEquivalence.unitIso.hom.app X) a = ↑(↑AddMonoidHom.toMultiplicative (↑MonoidHom.toAdditive (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv.multiplicativeAdditive ↑X))))) (↑(↑AddMonoidHom.toMultiplicative (AddEquiv.toAddMonoidHom (AddEquiv.symm (AddEquiv.additiveMultiplicative ↑(AddCommGroupCat.of (Additive ↑X)))))) (↑(MulEquiv.multiplicativeAdditive ↑X) a))

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_map_apply {X : AddCommGroupCat} {Y : AddCommGroupCat} (a : ↑X →+ ↑Y) (a : Multiplicative ↑X) :

↑(commGroupAddCommGroupEquivalence.inverse.map a) a = ↑Multiplicative.ofAdd (↑a (↑Multiplicative.toAdd a))

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_nsmul (X : CommGroupCat) :

∀ (a : ℕ) (a_1 : ↑X), a • a_1 = a_1 ^ a

source

@[simp]

theorem commGroupAddCommGroupEquivalence_counitIso_inv_app_apply (X : AddCommGroupCat) :

∀ (a : ↑((CategoryTheory.Functor.id AddCommGroupCat).obj X)), ↑(commGroupAddCommGroupEquivalence.counitIso.inv.app X) a = ↑(↑(AddEquiv.additiveMultiplicative ↑X)).symm a

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_div (X : AddCommGroupCat) (x : Multiplicative ↑X) (y : Multiplicative ↑X) :

x / y = x / y

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_sub (X : CommGroupCat) (x : Additive ↑X) (y : Additive ↑X) :

x - y = x - y

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_zpow (X : AddCommGroupCat) :

∀ (a : ℤ) (a_1 : ↑X), DivInvMonoid.zpow a a_1 = a • a_1

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_mul (X : AddCommGroupCat) :

∀ (x x_1 : Multiplicative ↑X), x * x_1 = x * x_1

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_zero (X : CommGroupCat) :

0 = 0

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_map_apply {X : CommGroupCat} {Y : CommGroupCat} (a : ↑X →* ↑Y) (a : Additive ↑X) :

↑(commGroupAddCommGroupEquivalence.functor.map a) a = ↑Additive.ofMul (↑a (↑Additive.toMul a))

source

@[simp]

theorem commGroupAddCommGroupEquivalence_unitIso_inv_app_apply (X : CommGroupCat) :

∀ (a : ↑((CategoryTheory.Functor.comp CommGroupCat.toAddCommGroupCat AddCommGroupCat.toCommGroupCat).obj X)), ↑(commGroupAddCommGroupEquivalence.unitIso.inv.app X) a = ↑(MulEquiv.symm (MulEquiv.multiplicativeAdditive ↑X)) (↑(↑AddMonoidHom.toMultiplicative (AddEquiv.toAddMonoidHom (AddEquiv.additiveMultiplicative ↑(AddCommGroupCat.of (Additive ↑X))))) (↑(↑AddMonoidHom.toMultiplicative (↑MonoidHom.toAdditive (MulEquiv.toMonoidHom (MulEquiv.multiplicativeAdditive ↑X)))) a))

source

@[simp]

theorem commGroupAddCommGroupEquivalence_counitIso_hom_app_apply (X : AddCommGroupCat) :

∀ (a : ↑((CategoryTheory.Functor.comp AddCommGroupCat.toCommGroupCat CommGroupCat.toAddCommGroupCat).obj X)), ↑(commGroupAddCommGroupEquivalence.counitIso.hom.app X) a = ↑↑(AddEquiv.additiveMultiplicative ↑X) a

source

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_inv (X : AddCommGroupCat) (x : Multiplicative ↑X) :

x⁻¹ = ↑Additive.ofMul (-↑Multiplicative.toAdd x)

source

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_neg (X : CommGroupCat) (x : Additive ↑X) :

-x = ↑Multiplicative.ofAdd (↑Additive.toMul x)⁻¹

source

def commGroupAddCommGroupEquivalence :

CommGroupCat ≌ AddCommGroupCat

The equivalence of categories between CommGroup and AddCommGroup.

Instances For

Equivalence between Group and AddGroup #

Equivalence between `Group` and `AddGroup` #