The abelianization of a group #

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.

source

@[instance]

def commutator.normal (G : Type u) [group G] :

(commutator G).normal

source

def commutator (G : Type u) [group G] :

subgroup G

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

Equations

commutator G = subgroup.normal_closure {x : G | ∃ (p q : G), ((p * q) * p⁻¹) * q⁻¹ = x}

source

def abelianization (G : Type u) [group G] :

Type u

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

Equations

abelianization G = quotient_group.quotient (commutator G)

source

@[instance]

def abelianization.comm_group (G : Type u) [group G] :

comm_group (abelianization G)

Equations

abelianization.comm_group G = {mul := group.mul (quotient_group.quotient.group (commutator G)), mul_assoc := _, one := group.one (quotient_group.quotient.group (commutator G)), one_mul := _, mul_one := _, npow := group.npow (quotient_group.quotient.group (commutator G)), npow_zero' := _, npow_succ' := _, inv := group.inv (quotient_group.quotient.group (commutator G)), div := group.div (quotient_group.quotient.group (commutator G)), div_eq_mul_inv := _, gpow := group.gpow (quotient_group.quotient.group (commutator G)), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

@[instance]

def abelianization.inhabited (G : Type u) [group G] :

inhabited (abelianization G)

Equations

abelianization.inhabited G = {default := 1}

source

def abelianization.of {G : Type u} [group G] :

G →* abelianization G

of is the canonical projection from G to its abelianization.

Equations

abelianization.of = {to_fun := quotient_group.mk (commutator G), map_one' := _, map_mul' := _}

source

theorem abelianization.commutator_subset_ker {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) :

commutator G ≤ f.ker

source

def abelianization.lift {G : Type u} [group G] {A : Type v} [comm_group A] :

(G →* A) ≃ (abelianization G →* 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

abelianization.lift = {to_fun := λ (f : G →* A), quotient_group.lift (commutator G) f _, inv_fun := λ (F : abelianization G →* A), F.comp abelianization.of, left_inv := _, right_inv := _}

source

@[simp]

theorem abelianization.lift.of {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) (x : G) :

⇑(⇑abelianization.lift f) (⇑abelianization.of x) = ⇑f x

source

theorem abelianization.lift.unique {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) (φ : abelianization G →* A) (hφ : ∀ (x : G), ⇑φ (⇑abelianization.of x) = ⇑f x) {x : abelianization G} :

⇑φ x = ⇑(⇑abelianization.lift f) x

source

@[ext]

theorem abelianization.hom_ext {G : Type u} [group G] {A : Type v} [monoid A] (φ ψ : abelianization G →* A) (h : φ.comp abelianization.of = ψ.comp abelianization.of) :

φ = ψ

See note [partially-applied ext lemmas].