# mathlib3documentation

group_theory.abelianization

# The abelianization of a group #

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

This file defines the commutator and the abelianization of a group. It furthermore prepares for the result that the abelianization is left adjoint to the forgetful functor from abelian groups to groups, which can be found in algebra/category/Group/adjunctions.

## Main definitions #

• commutator: defines the commutator of a group G as a subgroup of G.
• abelianization: defines the abelianization of a group G as the quotient of a group by its commutator subgroup.
• abelianization.map: lifts a group homomorphism to a homomorphism between the abelianizations
• mul_equiv.abelianization_congr: Equivalent groups have equivalent abelianizations
@[protected, instance]
def commutator.normal (G : Type u) [group G] :
def commutator (G : Type u) [group G] :

The commutator subgroup of a group G is the normal subgroup generated by the commutators [p,q]=p*q*p⁻¹*q⁻¹.

Equations
Instances for commutator
Instances for ↥commutator
theorem commutator_def (G : Type u) [group G] :
theorem commutator_eq_closure (G : Type u) [group G] :
@[protected, instance]
def commutator_characteristic (G : Type u) [group G] :
@[protected, instance]
def commutator.group.fg (G : Type u) [group G] [finite ] :
theorem rank_commutator_le_card (G : Type u) [group G] [finite ] :
def abelianization (G : Type u) [group G] :

The abelianization of G is the quotient of G by its commutator subgroup.

Equations
Instances for abelianization
@[protected, instance]
def abelianization.comm_group (G : Type u) [group G] :
Equations
@[protected, instance]
def abelianization.inhabited (G : Type u) [group G] :
Equations
@[protected, instance]
def abelianization.fintype (G : Type u) [group G] [fintype G] [decidable_pred (λ (_x : G), _x commutator G)] :
Equations
@[protected, instance]
def abelianization.finite (G : Type u) [group G] [finite G] :
def abelianization.of {G : Type u} [group G] :

of is the canonical projection from G to its abelianization.

Equations
@[simp]
theorem abelianization.mk_eq_of {G : Type u} [group G] (a : G) :
quot.mk setoid.r a =
theorem abelianization.commutator_subset_ker {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) :
f.ker
def abelianization.lift {G : Type u} [group G] {A : Type v} [comm_group A] :
(G →* A) →* A)

If f : G → A is a group homomorphism to an abelian group, then lift f is the unique map from the abelianization of a G to A that factors through f.

Equations
@[simp]
theorem abelianization.lift.of {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) (x : G) :
= f x
theorem abelianization.lift.unique {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) (φ : →* A) (hφ : (x : G), φ = f x) {x : abelianization G} :
φ x =
@[simp]
theorem abelianization.lift_of {G : Type u} [group G] :
@[ext]
theorem abelianization.hom_ext {G : Type u} [group G] {A : Type v} [monoid A] (φ ψ : →* A) (h : = ) :
φ = ψ
def abelianization.map {G : Type u} [group G] {H : Type v} [group H] (f : G →* H) :

The map operation of the abelianization functor

Equations
@[simp]
theorem abelianization.map_of {G : Type u} [group G] {H : Type v} [group H] (f : G →* H) (x : G) :
@[simp]
theorem abelianization.map_id {G : Type u} [group G] :
@[simp]
theorem abelianization.map_comp {G : Type u} [group G] {H : Type v} [group H] (f : G →* H) {I : Type w} [group I] (g : H →* I) :
@[simp]
theorem abelianization.map_map_apply {G : Type u} [group G] {H : Type v} [group H] (f : G →* H) {I : Type w} [group I] {g : H →* I} {x : abelianization G} :
def mul_equiv.abelianization_congr {G : Type u} [group G] {H : Type v} [group H] (e : G ≃* H) :

Equivalent groups have equivalent abelianizations

Equations
@[simp]
theorem abelianization_congr_of {G : Type u} [group G] {H : Type v} [group H] (e : G ≃* H) (x : G) :
@[simp]
theorem abelianization_congr_refl {G : Type u} [group G] :
@[simp]
theorem abelianization_congr_symm {G : Type u} [group G] {H : Type v} [group H] (e : G ≃* H) :
@[simp]
theorem abelianization_congr_trans {G : Type u} [group G] {H : Type v} [group H] (e : G ≃* H) {I : Type v} [group I] (e₂ : H ≃* I) :
@[simp]

An Abelian group is equivalent to its own abelianization.

Equations
@[simp]
theorem abelianization.equiv_of_comm_apply {H : Type u_1} [comm_group H] (ᾰ : H) :
def commutator_representatives (G : Type u) [group G] :
set (G × G)

Representatives (g₁, g₂) : G × G of commutator_set ⁅g₁, g₂⁆ ∈ G.

Equations
Instances for ↥commutator_representatives
@[protected, instance]

Subgroup generated by representatives g₁ g₂ : G of commutators ⁅g₁, g₂⁆ ∈ G.

Equations
Instances for ↥closure_commutator_representatives
@[protected, instance]
@[protected, instance]
def commutator_set.finite (G : Type u) [group G] [finite ] :