mathlib3 documentation

algebra.category.Group.equivalence_Group_AddGroup

Equivalence between Group and AddGroup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains two equivalences:

source
@[simp]
theorem Group.to_AddGroup_map (X Y : Group) (ᾰ : ↥X →* ↥Y) :
Group.to_AddGroup.map ᾰ = ⇑monoid_hom.to_additive ᾰ
source
def Group.to_AddGroup  :
Group ⥤ AddGroup

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

Equations
source
@[simp]
theorem Group.to_AddGroup_obj (X : Group) :
Group.to_AddGroup.obj X = AddGroup.of (additive ↥X)
source
@[simp]
theorem CommGroup.to_AddCommGroup_map (X Y : CommGroup) (ᾰ : ↥X →* ↥Y) :
CommGroup.to_AddCommGroup.map ᾰ = ⇑monoid_hom.to_additive ᾰ
source
def CommGroup.to_AddCommGroup  :
CommGroup ⥤ AddCommGroup

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

Equations
source
@[simp]
theorem CommGroup.to_AddCommGroup_obj (X : CommGroup) :
CommGroup.to_AddCommGroup.obj X = AddCommGroup.of (additive ↥X)
source
@[simp]
theorem AddGroup.to_Group_map (X Y : AddGroup) (ᾰ : ↥X →+ ↥Y) :
AddGroup.to_Group.map ᾰ = ⇑add_monoid_hom.to_multiplicative ᾰ
source
@[simp]
theorem AddGroup.to_Group_obj (X : AddGroup) :
AddGroup.to_Group.obj X = Group.of (multiplicative ↥X)
source
def AddGroup.to_Group  :
AddGroup ⥤ Group

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

Equations
source
def AddCommGroup.to_CommGroup  :
AddCommGroup ⥤ CommGroup

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

Equations
source
@[simp]
theorem AddCommGroup.to_CommGroup_obj (X : AddCommGroup) :
AddCommGroup.to_CommGroup.obj X = CommGroup.of (multiplicative ↥X)
source
@[simp]
theorem AddCommGroup.to_CommGroup_map (X Y : AddCommGroup) (ᾰ : ↥X →+ ↥Y) :
AddCommGroup.to_CommGroup.map ᾰ = ⇑add_monoid_hom.to_multiplicative ᾰ
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_zpow (X : AddGroup) (ᾰ : ℤ) (ᾰ_1 : multiplicative ↥X) :
group.zpow ᾰ ᾰ_1 = ᾰ_1 ^ ᾰ
source
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_add (X : Group) (ᾰ ᾰ_1 : additive ↥X) :
ᾰ + ᾰ_1 = sub_neg_monoid.add ᾰ ᾰ_1
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_α (X : AddGroup) :
↥(Group_AddGroup_equivalence.inverse.obj X) = multiplicative ↥X
source
@[simp]
theorem Group_AddGroup_equivalence_counit_iso_inv_app_apply (X : AddGroup) (ᾰ : ↥((𝟭 AddGroup).obj X)) :
⇑(Group_AddGroup_equivalence.counit_iso.inv.app X) ᾰ = ⇑((add_equiv.additive_multiplicative ↥X).symm) ᾰ
source
@[simp]
theorem Group_AddGroup_equivalence_counit_iso_hom_app_apply (X : AddGroup) (ᾰ : ↥((AddGroup.to_Group ⋙ Group.to_AddGroup).obj X)) :
⇑(Group_AddGroup_equivalence.counit_iso.hom.app X) ᾰ = ⇑(add_equiv.additive_multiplicative ↥X) ᾰ
source
@[simp]
theorem Group_AddGroup_equivalence_functor_map_apply (X Y : Group) (ᾰ : ↥X →* ↥Y) (a : additive ↥X) :
⇑(Group_AddGroup_equivalence.functor.map ᾰ) a = ⇑additive.of_mul (⇑ᾰ (⇑additive.to_mul a))
source
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_neg (X : Group) (ᾰ : additive ↥X) :
-ᾰ = sub_neg_monoid.neg ᾰ
source
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_α (X : Group) :
↥(Group_AddGroup_equivalence.functor.obj X) = additive ↥X
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_npow (X : AddGroup) (ᾰ : ℕ) (ᾰ_1 : multiplicative ↥X) :
group.npow ᾰ ᾰ_1 = div_inv_monoid.npow ᾰ ᾰ_1
source
@[simp]
theorem Group_AddGroup_equivalence_unit_iso_inv_app_apply (X : Group) (ᾰ : ↥((Group.to_AddGroup ⋙ AddGroup.to_Group).obj X)) :
⇑(Group_AddGroup_equivalence.unit_iso.inv.app X) ᾰ = ⇑((mul_equiv.multiplicative_additive ↥X).symm) (⇑multiplicative.of_add (⇑(add_equiv.additive_multiplicative (additive ↥X)) (⇑additive.of_mul (⇑(mul_equiv.multiplicative_additive ↥X) (⇑additive.to_mul (⇑multiplicative.to_add ᾰ))))))
source
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_zero (X : Group) :
0 = sub_neg_monoid.zero
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_mul (X : AddGroup) (ᾰ ᾰ_1 : multiplicative ↥X) :
ᾰ * ᾰ_1 = div_inv_monoid.mul ᾰ ᾰ_1
source
@[simp]
theorem Group_AddGroup_equivalence_unit_iso_hom_app_apply (X : Group) (ᾰ : ↥((𝟭 Group).obj X)) :
⇑(Group_AddGroup_equivalence.unit_iso.hom.app X) ᾰ = ⇑multiplicative.of_add (⇑additive.of_mul (⇑((mul_equiv.multiplicative_additive ↥X).symm) (⇑additive.to_mul (⇑((add_equiv.additive_multiplicative (additive ↥X)).symm) (⇑multiplicative.to_add (⇑(mul_equiv.multiplicative_additive ↥X) ᾰ))))))
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_map_apply (X Y : AddGroup) (ᾰ : ↥X →+ ↥Y) (a : multiplicative ↥X) :
⇑(Group_AddGroup_equivalence.inverse.map ᾰ) a = ⇑multiplicative.of_add (⇑ᾰ (⇑multiplicative.to_add a))
source
def Group_AddGroup_equivalence  :
Group ≌ AddGroup

The equivalence of categories between Group and AddGroup

Equations
source
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_zsmul (X : Group) (ᾰ : ℤ) (ᾰ_1 : additive ↥X) :
add_group.zsmul ᾰ ᾰ_1 = ᾰ • ᾰ_1
source
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_sub (X : Group) (ᾰ ᾰ_1 : additive ↥X) :
ᾰ - ᾰ_1 = sub_neg_monoid.sub ᾰ ᾰ_1
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_div (X : AddGroup) (ᾰ ᾰ_1 : multiplicative ↥X) :
ᾰ / ᾰ_1 = div_inv_monoid.div ᾰ ᾰ_1
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_one (X : AddGroup) :
1 = div_inv_monoid.one
source
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_nsmul (X : Group) (ᾰ : ℕ) (ᾰ_1 : additive ↥X) :
add_group.nsmul ᾰ ᾰ_1 = sub_neg_monoid.nsmul ᾰ ᾰ_1
source
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_inv (X : AddGroup) (ᾰ : multiplicative ↥X) :
ᾰ⁻¹ = div_inv_monoid.inv ᾰ
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_nsmul (X : CommGroup) (ᾰ : ℕ) (ᾰ_1 : additive ↥X) :
add_comm_group.nsmul ᾰ ᾰ_1 = add_group.nsmul ᾰ ᾰ_1
source
def CommGroup_AddCommGroup_equivalence  :
CommGroup ≌ AddCommGroup

The equivalence of categories between CommGroup and AddCommGroup.

Equations
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_map_apply (X Y : AddCommGroup) (ᾰ : ↥X →+ ↥Y) (a : multiplicative ↥X) :
⇑(CommGroup_AddCommGroup_equivalence.inverse.map ᾰ) a = ⇑multiplicative.of_add (⇑ᾰ (⇑multiplicative.to_add a))
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_zero (X : CommGroup) :
0 = add_group.zero
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_obj_str_one (X : AddCommGroup) :
1 = group.one
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_obj_str_div (X : AddCommGroup) (ᾰ ᾰ_1 : multiplicative ↥X) :
ᾰ / ᾰ_1 = group.div ᾰ ᾰ_1
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_counit_iso_hom_app_apply (X : AddCommGroup) (ᾰ : ↥((AddCommGroup.to_CommGroup ⋙ CommGroup.to_AddCommGroup).obj X)) :
⇑(CommGroup_AddCommGroup_equivalence.counit_iso.hom.app X) ᾰ = ⇑(add_equiv.additive_multiplicative ↥X) ᾰ
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_counit_iso_inv_app_apply (X : AddCommGroup) (ᾰ : ↥((𝟭 AddCommGroup).obj X)) :
⇑(CommGroup_AddCommGroup_equivalence.counit_iso.inv.app X) ᾰ = ⇑((add_equiv.additive_multiplicative ↥X).symm) ᾰ
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_α (X : CommGroup) :
↥(CommGroup_AddCommGroup_equivalence.functor.obj X) = additive ↥X
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_add (X : CommGroup) (ᾰ ᾰ_1 : additive ↥X) :
ᾰ + ᾰ_1 = add_group.add ᾰ ᾰ_1
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_obj_str_npow (X : AddCommGroup) (ᾰ : ℕ) (ᾰ_1 : multiplicative ↥X) :
comm_group.npow ᾰ ᾰ_1 = group.npow ᾰ ᾰ_1
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_obj_α (X : AddCommGroup) :
↥(CommGroup_AddCommGroup_equivalence.inverse.obj X) = multiplicative ↥X
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_sub (X : CommGroup) (ᾰ ᾰ_1 : additive ↥X) :
ᾰ - ᾰ_1 = add_group.sub ᾰ ᾰ_1
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_map_apply (X Y : CommGroup) (ᾰ : ↥X →* ↥Y) (a : additive ↥X) :
⇑(CommGroup_AddCommGroup_equivalence.functor.map ᾰ) a = ⇑additive.of_mul (⇑ᾰ (⇑additive.to_mul a))
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_neg (X : CommGroup) (ᾰ : additive ↥X) :
-ᾰ = add_group.neg ᾰ
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_zsmul (X : CommGroup) (ᾰ : ℤ) (ᾰ_1 : additive ↥X) :
add_comm_group.zsmul ᾰ ᾰ_1 = add_group.zsmul ᾰ ᾰ_1
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_obj_str_inv (X : AddCommGroup) (ᾰ : multiplicative ↥X) :
ᾰ⁻¹ = group.inv ᾰ
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_unit_iso_inv_app_apply (X : CommGroup) (ᾰ : ↥((CommGroup.to_AddCommGroup ⋙ AddCommGroup.to_CommGroup).obj X)) :
⇑(CommGroup_AddCommGroup_equivalence.unit_iso.inv.app X) ᾰ = ⇑((mul_equiv.multiplicative_additive ↥X).symm) (⇑multiplicative.of_add (⇑(add_equiv.additive_multiplicative (additive ↥X)) (⇑additive.of_mul (⇑(mul_equiv.multiplicative_additive ↥X) (⇑additive.to_mul (⇑multiplicative.to_add ᾰ))))))
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_obj_str_mul (X : AddCommGroup) (ᾰ ᾰ_1 : multiplicative ↥X) :
ᾰ * ᾰ_1 = group.mul ᾰ ᾰ_1
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_inverse_obj_str_zpow (X : AddCommGroup) (ᾰ : ℤ) (ᾰ_1 : multiplicative ↥X) :
comm_group.zpow ᾰ ᾰ_1 = group.zpow ᾰ ᾰ_1
source
@[simp]
theorem CommGroup_AddCommGroup_equivalence_unit_iso_hom_app_apply (X : CommGroup) (ᾰ : ↥((𝟭 CommGroup).obj X)) :
⇑(CommGroup_AddCommGroup_equivalence.unit_iso.hom.app X) ᾰ = ⇑multiplicative.of_add (⇑additive.of_mul (⇑((mul_equiv.multiplicative_additive ↥X).symm) (⇑additive.to_mul (⇑((add_equiv.additive_multiplicative (additive ↥X)).symm) (⇑multiplicative.to_add (⇑(mul_equiv.multiplicative_additive ↥X) ᾰ))))))