# mathlib3documentation

algebra.category.Group.basic

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

We introduce the bundled categories:

• Group
• AddGroup
• CommGroup
• AddCommGroup along with the relevant forgetful functors between them, and to the bundled monoid categories.
Type (u+1)

The category of additive groups and group morphisms

Equations
Instances for AddGroup
def Group  :
Type (u+1)

The category of groups and group morphisms.

Equations
Instances for Group
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
def Group.has_coe_to_sort  :
(Type u_1)
Equations

Construct a bundled AddGroup from the underlying type and typeclass.

Equations
Instances for ↥AddGroup.of
def Group.of (X : Type u) [group X] :

Construct a bundled Group from the underlying type and typeclass.

Equations
Instances for ↥Group.of
def AddGroup.of_hom {X Y : Type u} [add_group X] [add_group Y] (f : X →+ Y) :

Typecheck a add_monoid_hom as a morphism in AddGroup.

Equations
def Group.of_hom {X Y : Type u} [group X] [group Y] (f : X →* Y) :

Typecheck a monoid_hom as a morphism in Group.

Equations
@[simp]
theorem AddGroup.of_hom_apply {X Y : Type u_1} [add_group X] [add_group Y] (f : X →+ Y) (x : X) :
x = f x
@[simp]
theorem Group.of_hom_apply {X Y : Type u_1} [group X] [group Y] (f : X →* Y) (x : X) :
@[protected, instance]
def Group.group (G : Group) :
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem Group.coe_of (R : Type u) [group R] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def AddGroup.of_unique (G : Type u_1) [add_group G] [i : unique G] :
Equations
@[protected, instance]
def Group.of_unique (G : Type u_1) [group G] [i : unique G] :
Equations
@[simp]
0 g = 0
@[simp]
theorem Group.one_apply (G H : Group) (g : G) :
1 g = 1
@[ext]
theorem Group.ext (G H : Group) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂
@[ext]
theorem AddGroup.ext (G H : AddGroup) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
Type (u+1)

The category of additive commutative groups and group morphisms.

Equations
Instances for AddCommGroup
def CommGroup  :
Type (u+1)

The category of commutative groups and group morphisms.

Equations
Instances for CommGroup
@[reducible]
def Ab  :
Type (u_1+1)

Ab is an abbreviation for AddCommGroup, for the sake of mathematicians' sanity.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations

Construct a bundled AddCommGroup from the underlying type and typeclass.

Equations
Instances for ↥AddCommGroup.of
def CommGroup.of (G : Type u) [comm_group G] :

Construct a bundled CommGroup from the underlying type and typeclass.

Equations
Instances for ↥CommGroup.of
def CommGroup.of_hom {X Y : Type u} [comm_group X] [comm_group Y] (f : X →* Y) :

Typecheck a monoid_hom as a morphism in CommGroup.

Equations
def AddCommGroup.of_hom {X Y : Type u} (f : X →+ Y) :

Typecheck a add_monoid_hom as a morphism in AddCommGroup.

Equations
@[simp]
theorem AddCommGroup.of_hom_apply {X Y : Type u_1} (f : X →+ Y) (x : X) :
x = f x
@[simp]
theorem CommGroup.of_hom_apply {X Y : Type u_1} [comm_group X] [comm_group Y] (f : X →* Y) (x : X) :
x = f x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem AddCommGroup.coe_of (R : Type u)  :
= R
@[simp]
theorem CommGroup.coe_of (R : Type u) [comm_group R] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def CommGroup.of_unique (G : Type u_1) [comm_group G] [i : unique G] :
Equations
@[protected, instance]
def AddCommGroup.of_unique (G : Type u_1) [i : unique G] :
Equations
@[simp]
theorem CommGroup.one_apply (G H : CommGroup) (g : G) :
1 g = 1
@[simp]
0 g = 0
@[ext]
theorem AddCommGroup.ext (G H : AddCommGroup) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂
@[ext]
theorem CommGroup.ext (G H : CommGroup) (f₁ f₂ : G H) (w : (x : G), f₁ x = f₂ x) :
f₁ = f₂
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Any element of an abelian group gives a unique morphism from ℤ sending 1 to that element.

Equations
@[simp]
theorem AddCommGroup.as_hom_apply {G : AddCommGroup} (g : G) (i : ) :
i = i g
@[ext]
theorem AddCommGroup.int_hom_ext {G : AddCommGroup} (f g : G) (w : f 1 = g 1) :
f = g
def mul_equiv.to_Group_iso {X Y : Group} (e : X ≃* Y) :
X Y

Build an isomorphism in the category Group from a mul_equiv between groups.

Equations
X Y

Build an isomorphism in the category AddGroup from an add_equiv between add_groups.

Equations
@[simp]
@[simp]
@[simp]
theorem mul_equiv.to_Group_iso_hom {X Y : Group} (e : X ≃* Y) :
@[simp]
theorem mul_equiv.to_Group_iso_inv {X Y : Group} (e : X ≃* Y) :
@[simp]
@[simp]
theorem mul_equiv.to_CommGroup_iso_hom {X Y : CommGroup} (e : X ≃* Y) :
def mul_equiv.to_CommGroup_iso {X Y : CommGroup} (e : X ≃* Y) :
X Y

Build an isomorphism in the category CommGroup from a mul_equiv between comm_groups.

Equations

Build an isomorphism in the category AddCommGroup from a add_equiv between add_comm_groups.

Equations
@[simp]
theorem mul_equiv.to_CommGroup_iso_inv {X Y : CommGroup} (e : X ≃* Y) :
@[simp]
@[simp]
= (i.inv) ᾰ

Build a mul_equiv from an isomorphism in the category Group.

Equations
@[simp]
theorem category_theory.iso.Group_iso_to_mul_equiv_apply {X Y : Group} (i : X Y) (ᾰ : X) :

Build an add_equiv from an isomorphism in the category AddGroup.

Equations
@[simp]
= (i.hom) ᾰ
@[simp]
@[simp]
@[simp]
theorem category_theory.iso.CommGroup_iso_to_mul_equiv_symm_apply {X Y : CommGroup} (i : X Y) (ᾰ : Y) :
= (i.inv) ᾰ

Build an add_equiv from an isomorphism in the category AddCommGroup.

Equations

Build a mul_equiv from an isomorphism in the category CommGroup.

Equations
@[simp]
@[simp]
theorem category_theory.iso.CommGroup_iso_to_mul_equiv_apply {X Y : CommGroup} (i : X Y) (ᾰ : X) :
= (i.hom) ᾰ

multiplicative equivalences between groups are the same as (isomorphic to) isomorphisms in Group

Equations

additive equivalences between add_groups are the same as (isomorphic to) isomorphisms in AddGroup

Equations

additive equivalences between add_comm_groups are the same as (isomorphic to) isomorphisms in AddCommGroup

Equations

multiplicative equivalences between comm_groups are the same as (isomorphic to) isomorphisms in CommGroup

Equations

The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group of permutations.

Equations

The (unbundled) group of automorphisms of a type is mul_equiv to the (unbundled) group of permutations.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]