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.

@[simp]

theorem GroupCat.toAddGroupCat_map {X : GroupCat} {Y : GroupCat} (a : ↑X →* ↑Y) : GroupCat.toAddGroupCat.toPrefunctor.map a = MonoidHom.toAdditive a

@[simp]

theorem GroupCat.toAddGroupCat_obj (X : GroupCat) : GroupCat.toAddGroupCat.toPrefunctor.obj X = AddGroupCat.of (Additive ↑X)

def GroupCat.toAddGroupCat : CategoryTheory.Functor GroupCat AddGroupCat

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

Equations

• GroupCat.toAddGroupCat = CategoryTheory.Functor.mk { obj := fun (X : GroupCat) => AddGroupCat.of (Additive ↑X), map := fun {X Y : GroupCat} => ⇑MonoidHom.toAdditive }

@[simp]

theorem CommGroupCat.toAddCommGroupCat_obj (X : CommGroupCat) : CommGroupCat.toAddCommGroupCat.toPrefunctor.obj X = AddCommGroupCat.of (Additive ↑X)

@[simp]

theorem CommGroupCat.toAddCommGroupCat_map {X : CommGroupCat} {Y : CommGroupCat} (a : ↑X →* ↑Y) : CommGroupCat.toAddCommGroupCat.toPrefunctor.map a = MonoidHom.toAdditive a

def CommGroupCat.toAddCommGroupCat : CategoryTheory.Functor CommGroupCat AddCommGroupCat

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 AddGroupCat.toGroupCat_obj (X : AddGroupCat) : AddGroupCat.toGroupCat.toPrefunctor.obj X = GroupCat.of (Multiplicative ↑X)

@[simp]

theorem AddGroupCat.toGroupCat_map {X : AddGroupCat} {Y : AddGroupCat} (a : ↑X →+ ↑Y) : AddGroupCat.toGroupCat.toPrefunctor.map a = AddMonoidHom.toMultiplicative a

def AddGroupCat.toGroupCat : CategoryTheory.Functor AddGroupCat GroupCat

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 AddCommGroupCat.toCommGroupCat_map {X : AddCommGroupCat} {Y : AddCommGroupCat} (a : ↑X →+ ↑Y) : AddCommGroupCat.toCommGroupCat.toPrefunctor.map a = AddMonoidHom.toMultiplicative a

@[simp]

theorem AddCommGroupCat.toCommGroupCat_obj (X : AddCommGroupCat) : AddCommGroupCat.toCommGroupCat.toPrefunctor.obj X = CommGroupCat.of (Multiplicative ↑X)

def AddCommGroupCat.toCommGroupCat : CategoryTheory.Functor AddCommGroupCat CommGroupCat

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.

@[simp]

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

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_inv (X : AddGroupCat) (x : Multiplicative ↑X) : x⁻¹ = Additive.ofMul (-Multiplicative.toAdd x)

@[simp]

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

@[simp]

theorem groupAddGroupEquivalence_inverse_map_apply {X : AddGroupCat} {Y : AddGroupCat} (a : ↑X →+ ↑Y) (a : Multiplicative ↑X) : (groupAddGroupEquivalence.inverse.toPrefunctor.map a✝) a = Multiplicative.ofAdd (a✝ (Multiplicative.toAdd a))

@[simp]

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

@[simp]

theorem groupAddGroupEquivalence_functor_obj_α (X : GroupCat) : ↑(groupAddGroupEquivalence.functor.toPrefunctor.obj X) = Additive ↑X

@[simp]

theorem groupAddGroupEquivalence_functor_map_apply {X : GroupCat} {Y : GroupCat} (a : ↑X →* ↑Y) (a : Additive ↑X) : (groupAddGroupEquivalence.functor.toPrefunctor.map a✝) a = Additive.ofMul (a✝ (Additive.toMul a))

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_str_one (X : AddGroupCat) : 1 = 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem groupAddGroupEquivalence_unitIso_hom_app_apply (X : GroupCat) : ∀ (a : ↑((CategoryTheory.Functor.id GroupCat).toPrefunctor.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)

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_neg (X : GroupCat) (x : Additive ↑X) : -x = Multiplicative.ofAdd (Additive.toMul x)⁻¹

@[simp]

theorem groupAddGroupEquivalence_unitIso_inv_app_apply (X : GroupCat) : ∀ (a : ↑((CategoryTheory.Functor.comp GroupCat.toAddGroupCat AddGroupCat.toGroupCat).toPrefunctor.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)

@[simp]

theorem groupAddGroupEquivalence_inverse_obj_α (X : AddGroupCat) : ↑(groupAddGroupEquivalence.inverse.toPrefunctor.obj X) = Multiplicative ↑X

@[simp]

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

@[simp]

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

@[simp]

theorem groupAddGroupEquivalence_functor_obj_str_zero (X : GroupCat) : 0 = 0

@[simp]

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

def groupAddGroupEquivalence : GroupCat ≌ AddGroupCat

The equivalence of categories between Group and AddGroup

Equations

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

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_α (X : CommGroupCat) : ↑(commGroupAddCommGroupEquivalence.functor.toPrefunctor.obj X) = Additive ↑X

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_α (X : AddCommGroupCat) : ↑(commGroupAddCommGroupEquivalence.inverse.toPrefunctor.obj X) = Multiplicative ↑X

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_one (X : AddCommGroupCat) : 1 = 1

@[simp]

theorem commGroupAddCommGroupEquivalence_unitIso_hom_app_apply (X : CommGroupCat) : ∀ (a : ↑((CategoryTheory.Functor.id CommGroupCat).toPrefunctor.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))

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_map_apply {X : AddCommGroupCat} {Y : AddCommGroupCat} (a : ↑X →+ ↑Y) (a : Multiplicative ↑X) : (commGroupAddCommGroupEquivalence.inverse.toPrefunctor.map a✝) a = Multiplicative.ofAdd (a✝ (Multiplicative.toAdd a))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_zero (X : CommGroupCat) : 0 = 0

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_map_apply {X : CommGroupCat} {Y : CommGroupCat} (a : ↑X →* ↑Y) (a : Additive ↑X) : (commGroupAddCommGroupEquivalence.functor.toPrefunctor.map a✝) a = Additive.ofMul (a✝ (Additive.toMul a))

@[simp]

theorem commGroupAddCommGroupEquivalence_unitIso_inv_app_apply (X : CommGroupCat) : ∀ (a : ↑((CategoryTheory.Functor.comp CommGroupCat.toAddCommGroupCat AddCommGroupCat.toCommGroupCat).toPrefunctor.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))

@[simp]

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

@[simp]

theorem commGroupAddCommGroupEquivalence_inverse_obj_str_inv (X : AddCommGroupCat) (x : Multiplicative ↑X) : x⁻¹ = Additive.ofMul (-Multiplicative.toAdd x)

@[simp]

theorem commGroupAddCommGroupEquivalence_functor_obj_str_neg (X : CommGroupCat) (x : Additive ↑X) : -x = Multiplicative.ofAdd (Additive.toMul x)⁻¹

def commGroupAddCommGroupEquivalence : CommGroupCat ≌ AddCommGroupCat

The equivalence of categories between CommGroup and AddCommGroup.

Equations

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