# 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 `Mathlib/Algebra/Category/GrpCat/Adjunctions.lean`.

## Main definitions #

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

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 = (G ⧸ commutator G)

Instances For

source
instance Abelianization.commGroup (G : Type u) [Group G] :
CommGroup (Abelianization G)
Equations

- Abelianization.commGroup G = { toGroup := QuotientGroup.Quotient.group (commutator G), mul_comm := ⋯ }

source
instance Abelianization.instInhabited (G : Type u) [Group G] :
Inhabited (Abelianization G)
Equations

- Abelianization.instInhabited 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 = { toFun := QuotientGroup.mk, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Abelianization.mk_eq_of {G : Type u} [Group G] (a : G) :
Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a = of a
source
@[simp]
theorem Abelianization.ker_of (G : Type u) [Group G] :
of.ker = commutator G
source
theorem Abelianization.commutator_subset_ker {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) :
commutator G ≤ f.ker
source
def Abelianization.lift {G : Type u} [Group G] {A : Type v} [CommGroup 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

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Abelianization.lift_apply_of {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) (x : G) :
(lift f) (of x) = f x
source
@[deprecated Abelianization.lift_apply_of (since := "2025-07-23")]
theorem Abelianization.lift.of {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) (x : G) :
(lift f) (Abelianization.of x) = f x

Alias of `Abelianization.lift_apply_of`.

source
theorem Abelianization.coe_lift_symm {G : Type u} [Group G] {A : Type v} [CommGroup A] :
⇑lift.symm = fun (x : Abelianization G →* A) => x.comp of
source
@[simp]
theorem Abelianization.lift_symm_apply {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : Abelianization G →* A) :
lift.symm f = f.comp of
source
theorem Abelianization.lift_unique {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) (φ : Abelianization G →* A) (hφ : ∀ (x : G), φ (of x) = f x) {x : Abelianization G} :
φ x = (lift f) x
source
@[deprecated Abelianization.lift_unique (since := "2025-07-23")]
theorem Abelianization.lift.unique {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) (φ : Abelianization G →* A) (hφ : ∀ (x : G), φ (Abelianization.of x) = f x) {x : Abelianization G} :
φ x = (lift f) x

Alias of `Abelianization.lift_unique`.

source
@[simp]
theorem Abelianization.lift_of {G : Type u} [Group G] :
lift of = MonoidHom.id (Abelianization G)
source
theorem Abelianization.hom_ext {G : Type u} [Group G] {A : Type v} [Monoid A] (φ ψ : Abelianization G →* A) (h : φ.comp of = ψ.comp of) :
φ = ψ

See note [partially-applied ext lemmas].

source
theorem Abelianization.hom_ext_iff {G : Type u} [Group G] {A : Type v} [Monoid A] {φ ψ : Abelianization G →* A} :
φ = ψ ↔ φ.comp of = ψ.comp of
source
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)

Instances For

source
@[simp]
theorem Abelianization.lift_of_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) :
lift (of.comp f) = map f

Use `map` as the preferred simp normal form.

source
@[simp]
theorem Abelianization.map_of {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) (x : G) :
(map f) (of x) = of (f x)
source
@[simp]
theorem Abelianization.map_id {G : Type u} [Group G] :
map (MonoidHom.id G) = MonoidHom.id (Abelianization G)
source
@[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) :
(map g).comp (map f) = map (g.comp f)
source
@[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} :
(map g) ((map f) x) = (map (g.comp f)) x
source
def MulEquiv.abelianizationCongr {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) :
Abelianization G ≃* Abelianization H

Equivalent groups have equivalent abelianizations

Equations

- e.abelianizationCongr = { toFun := ⇑(Abelianization.map e.toMonoidHom), invFun := ⇑(Abelianization.map e.symm.toMonoidHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem abelianizationCongr_of {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) (x : G) :
e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)
source
@[simp]
theorem abelianizationCongr_refl {G : Type u} [Group G] :
(MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G)
source
@[simp]
theorem abelianizationCongr_symm {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) :
e.abelianizationCongr.symm = e.symm.abelianizationCongr
source
@[simp]
theorem abelianizationCongr_trans {G : Type u} [Group G] {H : Type v} [Group H] {I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) :
e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr
source
def Abelianization.equivOfComm {H : Type u_1} [CommGroup H] :
H ≃* Abelianization H

An Abelian group is equivalent to its own abelianization.

Equations

- Abelianization.equivOfComm = { toFun := ⇑Abelianization.of, invFun := ⇑(Abelianization.lift (MonoidHom.id H)), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Abelianization.equivOfComm_apply {H : Type u_1} [CommGroup H] (a : H) :
equivOfComm a = of a
source
@[simp]
theorem Abelianization.equivOfComm_symm_apply {H : Type u_1} [CommGroup H] (a : Abelianization H) :
equivOfComm.symm a = (lift (MonoidHom.id H)) a
source
instance instUniqueAbelianization (G : Type u) [Group G] [Unique G] :
Unique (Abelianization G)
Equations

- instUniqueAbelianization G = Quotient.instUniqueQuotient (QuotientGroup.leftRel (commutator G))