# mathlibdocumentation

algebra.category.Group.basic

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

def Group  :
Type (u+1)

The category of groups and group morphisms.

Equations
@[instance]

Equations

Construct a bundled AddGroup from the underlying type and typeclass.

def Group.of (X : Type u) [group X] :

Construct a bundled Group from the underlying type and typeclass.

Equations
@[instance]
def Group.group (G : Group) :

Equations
@[instance]

@[simp]

@[simp]
theorem Group.coe_of (R : Type u) [group R] :

@[instance]

Equations
@[instance]

@[instance]

@[instance]

Equations
@[instance]
def Group.unique  :

Equations
@[instance]

@[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) :
(∀ (x : G), f₁ x = f₂ x)f₁ = f₂

@[ext]
theorem AddGroup.ext (G H : AddGroup) (f₁ f₂ : G H) :
(∀ (x : G), f₁ x = f₂ x)f₁ = f₂

@[instance]

Equations
@[instance]

Type (u+1)

The category of additive commutative groups and group morphisms.

def CommGroup  :
Type (u+1)

The category of commutative groups and group morphisms.

Equations
def Ab  :
Type (u_1+1)

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

@[instance]

Equations
def AddCommGroup.of (G : Type u)  :

Construct a bundled AddCommGroup from the underlying type and typeclass.

def CommGroup.of (G : Type u) [comm_group G] :

Construct a bundled CommGroup from the underlying type and typeclass.

Equations
@[instance]

Equations
@[instance]

@[simp]
theorem AddCommGroup.coe_of (R : Type u)  :
= R

@[simp]
theorem CommGroup.coe_of (R : Type u) [comm_group R] :

@[instance]

@[instance]

Equations
@[instance]

@[instance]

Equations
@[instance]

@[instance]

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) :
(∀ (x : G), f₁ x = f₂ x)f₁ = f₂

@[ext]
theorem CommGroup.ext (G H : CommGroup) (f₁ f₂ : G H) :
(∀ (x : G), f₁ x = f₂ x)f₁ = f₂

@[instance]

Equations
@[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]
f 1 = g 1f = g

def mul_equiv.to_Group_iso {X Y : Type u} [group X] [group Y] :
X ≃* Y(Group.of X Group.of 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.

def mul_equiv.to_CommGroup_iso {X Y : Type u} [comm_group X] [comm_group Y] :
X ≃* Y

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

Equations
X ≃+ Y

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

Build a mul_equiv from an isomorphism in the category Group.

Equations

Build an add_equiv from an isomorphism in the category AddGroup.

Build an add_equiv from an isomorphism in the category AddCommGroup.

Build a mul_equiv from an isomorphism in the category CommGroup.

Equations
def mul_equiv_iso_Group_iso {X Y : Type u} [group X] [group Y] :
X ≃* Y

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

Equations
X ≃+ Y

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

X ≃+ Y

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

def mul_equiv_iso_CommGroup_iso {X Y : Type u} [comm_group X] [comm_group Y] :
X ≃* Y

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

Equations
def category_theory.Aut.iso_perm {α : Type u} :

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

Equations
def category_theory.Aut.mul_equiv_perm {α : Type u} :

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

Equations
@[instance]

Equations
@[instance]

Equations