mathlib documentation

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] :

(commutator G).normal

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

commutator G = ⁅⊤, ⊤⁆

Instances for commutator

Instances for ↥commutator

theorem commutator_def (G : Type u) [group G] :

commutator G = ⁅⊤, ⊤⁆

theorem commutator_eq_closure (G : Type u) [group G] :

commutator G = subgroup.closure (commutator_set G)

theorem commutator_eq_normal_closure (G : Type u) [group G] :

commutator G = subgroup.normal_closure (commutator_set G)

@[protected, instance]

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

(commutator G).characteristic

@[protected, instance]

def commutator.group.fg (G : Type u) [group G] [finite ↥(commutator_set G)] :

group.fg ↥(commutator G)

theorem rank_commutator_le_card (G : Type u) [group G] [finite ↥(commutator_set G)] :

group.rank ↥(commutator G) ≤ nat.card ↥(commutator_set G)

theorem commutator_centralizer_commutator_le_center (G : Type u) [group G] :

⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ subgroup.center G

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

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

Equations

abelianization G = (G ⧸ commutator G)

Instances for abelianization

@[protected, 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 := _, zpow := group.zpow (quotient_group.quotient.group (commutator G)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

@[protected, instance]

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

inhabited (abelianization G)

Equations

abelianization.inhabited G = {default := 1}

@[protected, instance]

def abelianization.fintype (G : Type u) [group G] [fintype G] [decidable_pred (λ (_x : G), _x ∈ commutator G)] :

fintype (abelianization G)

Equations

abelianization.fintype G = quotient_group.fintype (commutator G)

@[protected, instance]

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

finite (abelianization G)

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' := _}

@[simp]

theorem abelianization.mk_eq_of {G : Type u} [group G] (a : G) :

quot.mk setoid.r a = ⇑abelianization.of a

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

commutator G ≤ f.ker

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 := _}

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

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

@[simp]

theorem abelianization.lift_of {G : Type u} [group G] :

⇑abelianization.lift abelianization.of = monoid_hom.id (abelianization G)

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

def abelianization.map {G : Type u} [group G] {H : Type v} [group H] (f : G →* H) :

abelianization G →* abelianization H

The map operation of the abelianization functor

Equations

abelianization.map f = ⇑abelianization.lift (abelianization.of.comp f)

@[simp]

theorem abelianization.map_of {G : Type u} [group G] {H : Type v} [group H] (f : G →* H) (x : G) :

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

@[simp]

theorem abelianization.map_id {G : Type u} [group G] :

abelianization.map (monoid_hom.id G) = monoid_hom.id (abelianization 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) :

(abelianization.map g).comp (abelianization.map f) = abelianization.map (g.comp f)

@[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} :

⇑(abelianization.map g) (⇑(abelianization.map f) x) = ⇑(abelianization.map (g.comp f)) x

def mul_equiv.abelianization_congr {G : Type u} [group G] {H : Type v} [group H] (e : G ≃* H) :

abelianization G ≃* abelianization H

Equivalent groups have equivalent abelianizations

Equations

e.abelianization_congr = {to_fun := ⇑(abelianization.map e.to_monoid_hom), inv_fun := ⇑(abelianization.map e.symm.to_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}

@[simp]

theorem abelianization_congr_of {G : Type u} [group G] {H : Type v} [group H] (e : G ≃* H) (x : G) :

⇑(e.abelianization_congr) (⇑abelianization.of x) = ⇑abelianization.of (⇑e x)

@[simp]

theorem abelianization_congr_refl {G : Type u} [group G] :

(mul_equiv.refl G).abelianization_congr = mul_equiv.refl (abelianization G)

@[simp]

theorem abelianization_congr_symm {G : Type u} [group G] {H : Type v} [group H] (e : G ≃* H) :

e.abelianization_congr.symm = e.symm.abelianization_congr

@[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) :

e.abelianization_congr.trans e₂.abelianization_congr = (e.trans e₂).abelianization_congr

@[simp]

theorem abelianization.equiv_of_comm_symm_apply {H : Type u_1} [comm_group H] (ᾰ : abelianization H) :

⇑(abelianization.equiv_of_comm.symm) ᾰ = ⇑(⇑abelianization.lift (monoid_hom.id H)) ᾰ

def abelianization.equiv_of_comm {H : Type u_1} [comm_group H] :

H ≃* abelianization H

An Abelian group is equivalent to its own abelianization.

Equations

abelianization.equiv_of_comm = {to_fun := ⇑abelianization.of, inv_fun := ⇑(⇑abelianization.lift (monoid_hom.id H)), left_inv := _, right_inv := _, map_mul' := _}

@[simp]

theorem abelianization.equiv_of_comm_apply {H : Type u_1} [comm_group H] (ᾰ : H) :

⇑abelianization.equiv_of_comm ᾰ = ⇑abelianization.of ᾰ

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

set (G × G)

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

Equations

commutator_representatives G = set.range (λ (g : ↥(commutator_set G)), (Exists.some _, Exists.some _))

Instances for ↥commutator_representatives

commutator_representatives.finite

@[protected, instance]

def commutator_representatives.finite (G : Type u) [group G] [finite ↥(commutator_set G)] :

finite ↥(commutator_representatives G)

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

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

Equations

closure_commutator_representatives G = subgroup.closure (prod.fst '' commutator_representatives G ∪ prod.snd '' commutator_representatives G)

Instances for ↥closure_commutator_representatives

closure_commutator_representatives_fg

@[protected, instance]

def closure_commutator_representatives_fg (G : Type u) [group G] [finite ↥(commutator_set G)] :

group.fg ↥(closure_commutator_representatives G)

theorem rank_closure_commutator_representations_le (G : Type u) [group G] [finite ↥(commutator_set G)] :

group.rank ↥(closure_commutator_representatives G) ≤ 2 * nat.card ↥(commutator_set G)

theorem image_commutator_set_closure_commutator_representatives (G : Type u) [group G] :

⇑((closure_commutator_representatives G).subtype) '' commutator_set ↥(closure_commutator_representatives G) = commutator_set G

theorem card_commutator_set_closure_commutator_representatives (G : Type u) [group G] :

nat.card ↥(commutator_set ↥(closure_commutator_representatives G)) = nat.card ↥(commutator_set G)

theorem card_commutator_closure_commutator_representatives (G : Type u) [group G] :

nat.card ↥(commutator ↥(closure_commutator_representatives G)) = nat.card ↥(commutator G)

@[protected, instance]

def commutator_set.finite (G : Type u) [group G] [finite ↥(commutator_set G)] :

finite ↥(commutator_set ↥(closure_commutator_representatives G))