# 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
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]

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
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.

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
@[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]
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) (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₂
@[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
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
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
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.

@[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]
Equations
@[instance]
@[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₂
@[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]
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 : Type u} [group X] [group Y] (e : X ≃* Y) :

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

Equations

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

@[simp]
@[simp]
@[simp]
theorem mul_equiv.to_Group_iso_hom {X Y : Type u} [group X] [group Y] (e : X ≃* Y) :
@[simp]
theorem mul_equiv.to_Group_iso_inv {X Y : Type u} [group X] [group Y] (e : X ≃* Y) :
@[simp]
theorem add_equiv.to_AddCommGroup_iso_neg {X Y : Type u} (e : X ≃+ Y) :
@[simp]
theorem mul_equiv.to_CommGroup_iso_hom {X Y : Type u} [comm_group X] [comm_group Y] (e : X ≃* Y) :
def mul_equiv.to_CommGroup_iso {X Y : Type u} [comm_group X] [comm_group Y] (e : X ≃* Y) :

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

Equations
def add_equiv.to_AddCommGroup_iso {X Y : Type u} (e : X ≃+ Y) :

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

@[simp]
theorem mul_equiv.to_CommGroup_iso_inv {X Y : Type u} [comm_group X] [comm_group Y] (e : X ≃* Y) :
@[simp]
theorem add_equiv.to_AddCommGroup_iso_hom {X Y : Type u} (e : X ≃+ Y) :
@[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.

@[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.

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) ᾰ
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