# 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.
• Abelianization.map: lifts a group homomorphism to a homomorphism between the abelianizations
• MulEquiv.abelianizationCongr: Equivalent groups have equivalent abelianizations
def commutator (G : Type u) [] :

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

Equations
Instances For
instance instNormalCommutator (G : Type u) [] :
(commutator G).Normal
Equations
• =
theorem commutator_def (G : Type u) [] :
theorem commutator_eq_closure (G : Type u) [] :
instance commutator_characteristic (G : Type u) [] :
(commutator G).Characteristic
Equations
• =
def Abelianization (G : Type u) [] :

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

Equations
Instances For
instance Abelianization.commGroup (G : Type u) [] :
Equations
• = let __src := ;
instance Abelianization.instInhabited (G : Type u) [] :
Equations
• = { default := 1 }
instance Abelianization.instUnique (G : Type u) [] [] :
Equations
instance Abelianization.instFinite (G : Type u) [] [] :
Equations
• =
def Abelianization.of {G : Type u} [] :

of is the canonical projection from G to its abelianization.

Equations
• Abelianization.of = { toFun := QuotientGroup.mk, map_one' := , map_mul' := }
Instances For
@[simp]
theorem Abelianization.mk_eq_of {G : Type u} [] (a : G) :
Quot.mk Setoid.r a = Abelianization.of a
theorem Abelianization.commutator_subset_ker {G : Type u} [] {A : Type v} [] (f : G →* A) :
f.ker
def Abelianization.lift {G : Type u} [] {A : Type v} [] :
(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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Abelianization.lift.of {G : Type u} [] {A : Type v} [] (f : G →* A) (x : G) :
(Abelianization.lift f) (Abelianization.of x) = f x
theorem Abelianization.lift.unique {G : Type u} [] {A : Type v} [] (f : G →* A) (φ : ) (hφ : ∀ (x : G), φ (Abelianization.of x) = f x) {x : } :
φ x = (Abelianization.lift f) x
@[simp]
theorem Abelianization.lift_of {G : Type u} [] :
Abelianization.lift Abelianization.of =
theorem Abelianization.hom_ext_iff {G : Type u} [] {A : Type v} [] {φ : } {ψ : } :
φ = ψ φ.comp Abelianization.of = ψ.comp Abelianization.of
theorem Abelianization.hom_ext {G : Type u} [] {A : Type v} [] (φ : ) (ψ : ) (h : φ.comp Abelianization.of = ψ.comp Abelianization.of) :
φ = ψ

See note [partially-applied ext lemmas].

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

The map operation of the Abelianization functor

Equations
• = Abelianization.lift (Abelianization.of.comp f)
Instances For
@[simp]
theorem Abelianization.lift_of_comp {G : Type u} [] {H : Type v} [] (f : G →* H) :
Abelianization.lift (Abelianization.of.comp f) =

Use map as the preferred simp normal form.

@[simp]
theorem Abelianization.map_of {G : Type u} [] {H : Type v} [] (f : G →* H) (x : G) :
(Abelianization.of x) = Abelianization.of (f x)
@[simp]
theorem Abelianization.map_id {G : Type u} [] :
@[simp]
theorem Abelianization.map_comp {G : Type u} [] {H : Type v} [] (f : G →* H) {I : Type w} [] (g : H →* I) :
.comp = Abelianization.map (g.comp f)
@[simp]
theorem Abelianization.map_map_apply {G : Type u} [] {H : Type v} [] (f : G →* H) {I : Type w} [] {g : H →* I} {x : } :
( x) = (Abelianization.map (g.comp f)) x
def MulEquiv.abelianizationCongr {G : Type u} [] {H : Type v} [] (e : G ≃* H) :

Equivalent groups have equivalent abelianizations

Equations
Instances For
@[simp]
theorem abelianizationCongr_of {G : Type u} [] {H : Type v} [] (e : G ≃* H) (x : G) :
e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)
@[simp]
theorem abelianizationCongr_refl {G : Type u} [] :
.abelianizationCongr =
@[simp]
theorem abelianizationCongr_symm {G : Type u} [] {H : Type v} [] (e : G ≃* H) :
e.abelianizationCongr.symm = e.symm.abelianizationCongr
@[simp]
theorem abelianizationCongr_trans {G : Type u} [] {H : Type v} [] {I : Type v} [] (e : G ≃* H) (e₂ : H ≃* I) :
e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr
@[simp]
theorem Abelianization.equivOfComm_apply {H : Type u_1} [] (a : H) :
Abelianization.equivOfComm a = Abelianization.of a
@[simp]
theorem Abelianization.equivOfComm_symm_apply {H : Type u_1} [] (a : ) :
Abelianization.equivOfComm.symm a = (Abelianization.lift (MonoidHom.id H)) a
def Abelianization.equivOfComm {H : Type u_1} [] :

An Abelian group is equivalent to its own abelianization.

Equations
• Abelianization.equivOfComm = let __src := Abelianization.of; { toFun := Abelianization.of, invFun := (Abelianization.lift (MonoidHom.id H)), left_inv := , right_inv := , map_mul' := }
Instances For
def commutatorRepresentatives (G : Type u) [] :
Set (G × G)

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

Equations
Instances For

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

Equations
Instances For
instance closureCommutatorRepresentatives_fg (G : Type u) [] [Finite ] :
Equations
• =