# Abelianization of groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.

{-# OPTIONS --lossy-unification #-}

module group-theory.abelianization-groups where

Imports
open import category-theory.adjunctions-large-categories
open import category-theory.functors-large-categories
open import category-theory.functors-large-precategories
open import category-theory.natural-transformations-functors-large-categories
open import category-theory.natural-transformations-functors-large-precategories

open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.set-quotients
open import foundation.sets
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import group-theory.abelian-groups
open import group-theory.category-of-abelian-groups
open import group-theory.category-of-groups
open import group-theory.commutator-subgroups
open import group-theory.commuting-squares-of-group-homomorphisms
open import group-theory.functoriality-quotient-groups
open import group-theory.groups
open import group-theory.homomorphisms-abelian-groups
open import group-theory.homomorphisms-groups
open import group-theory.normal-subgroups
open import group-theory.nullifying-group-homomorphisms
open import group-theory.quotient-groups


## Idea

Consider a group homomorphism f : G → A from a group G into an abelian group A. We say that f is an abelianization of G if the precomposition function

  - ∘ f : hom A B → hom G B


is an equivalence for any abelian group B.

The abelianization Gᵃᵇ of a group G always exists, and can be constructed as the quotient group G/[G,G] of G modulo its commutator subgroup. Therefore we obtain an adjunction

  hom Gᵃᵇ A ≃ hom G A,


i.e., the abelianization is left adjoint to the inclusion functor from the category of abelian groups into the category of groups.

## Definitions

### The predicate of being an abelianization

module _
{l1 l2 : Level} (G : Group l1) (A : Ab l2) (f : hom-Group G (group-Ab A))
where

is-abelianization-Group : UUω
is-abelianization-Group =
{l : Level} (B : Ab l) →
is-equiv (λ h → comp-hom-Group G (group-Ab A) (group-Ab B) h f)


### The abelianization of a group

module _
{l1 : Level} (G : Group l1)
where

group-abelianization-Group : Group l1
group-abelianization-Group =
quotient-Group G (commutator-normal-subgroup-Group G)

hom-abelianization-Group : hom-Group G group-abelianization-Group
hom-abelianization-Group =
quotient-hom-Group G (commutator-normal-subgroup-Group G)

set-abelianization-Group : Set l1
set-abelianization-Group = set-Group group-abelianization-Group

type-abelianization-Group : UU l1
type-abelianization-Group = type-Group group-abelianization-Group

zero-abelianization-Group : type-abelianization-Group
zero-abelianization-Group = unit-Group group-abelianization-Group

(x y : type-abelianization-Group) → type-abelianization-Group

neg-abelianization-Group :
type-abelianization-Group → type-abelianization-Group
neg-abelianization-Group = inv-Group group-abelianization-Group

(x y z : type-abelianization-Group) →
associative-mul-Group group-abelianization-Group

(x : type-abelianization-Group) →
left-unit-law-mul-Group group-abelianization-Group

(x : type-abelianization-Group) →
right-unit-law-mul-Group group-abelianization-Group

(x : type-abelianization-Group) →
zero-abelianization-Group
left-inverse-law-mul-Group group-abelianization-Group

(x : type-abelianization-Group) →
zero-abelianization-Group
right-inverse-law-mul-Group group-abelianization-Group

map-abelianization-Group :
type-Group G → type-abelianization-Group
map-abelianization-Group =
map-hom-Group G group-abelianization-Group hom-abelianization-Group

(x y : type-Group G) →
( map-abelianization-Group x)
( map-abelianization-Group y) ＝
map-abelianization-Group (mul-Group G x y)
compute-mul-quotient-Group G (commutator-normal-subgroup-Group G)

abstract
(x y : type-abelianization-Group) →
double-induction-quotient-Group G G
( commutator-normal-subgroup-Group G)
( commutator-normal-subgroup-Group G)
( λ x y → Id-Prop set-abelianization-Group _ _)
( λ x y →
( apply-effectiveness-map-quotient-hom-Group' G
( commutator-normal-subgroup-Group G)
( sim-left-sim-congruence-Normal-Subgroup G
( commutator-normal-subgroup-Group G)
( mul-Group G x y)
( mul-Group G y x)
( contains-commutator-commutator-subgroup-Group G x y))) ∙

abelianization-Group : Ab l1
pr1 abelianization-Group = group-abelianization-Group


### The abelianization functor

abelianization-hom-Group :
{l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H) →
hom-Ab (abelianization-Group G) (abelianization-Group H)
abelianization-hom-Group G H f =
hom-quotient-Group G H
( commutator-normal-subgroup-Group G)
( commutator-normal-subgroup-Group H)
( f , preserves-commutator-subgroup-hom-Group G H f)

preserves-id-abelianization-functor-Group :
{l1 : Level} (G : Group l1) →
abelianization-hom-Group G G (id-hom-Group G) ＝
id-hom-Ab (abelianization-Group G)
preserves-id-abelianization-functor-Group G =
preserves-id-hom-quotient-Group' G
( commutator-normal-subgroup-Group G)
( preserves-commutator-subgroup-hom-Group G G (id-hom-Group G))

preserves-comp-abelianization-functor-Group :
{l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (K : Group l3)
(g : hom-Group H K) (f : hom-Group G H) →
abelianization-hom-Group G K (comp-hom-Group G H K g f) ＝
comp-hom-Ab
( abelianization-Group G)
( abelianization-Group H)
( abelianization-Group K)
( abelianization-hom-Group H K g)
( abelianization-hom-Group G H f)
preserves-comp-abelianization-functor-Group G H K g f =
preserves-comp-hom-quotient-Group' G H K
( commutator-normal-subgroup-Group G)
( commutator-normal-subgroup-Group H)
( commutator-normal-subgroup-Group K)
( g , preserves-commutator-subgroup-hom-Group H K g)
( f , preserves-commutator-subgroup-hom-Group G H f)
( preserves-commutator-subgroup-hom-Group G K (comp-hom-Group G H K g f))

abelianization-functor-Group :
functor-Large-Category id Group-Large-Category Ab-Large-Category
obj-functor-Large-Precategory
abelianization-functor-Group =
abelianization-Group
hom-functor-Large-Precategory
abelianization-functor-Group {l1} {l2} {G} {H} =
abelianization-hom-Group G H
preserves-comp-functor-Large-Precategory
abelianization-functor-Group {l1} {l2} {l3} {G} {H} {K} =
preserves-comp-abelianization-functor-Group G H K
preserves-id-functor-Large-Precategory
abelianization-functor-Group {l1} {G} =
preserves-id-abelianization-functor-Group G


### The unit of the abelianization adjunction

hom-unit-abelianization-Group :
{l1 : Level} (G : Group l1) → hom-Group G (group-abelianization-Group G)
hom-unit-abelianization-Group G =
quotient-hom-Group G (commutator-normal-subgroup-Group G)

naturality-unit-abelianization-Group :
{l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H) →
coherence-square-hom-Group G H
( group-abelianization-Group G)
( group-abelianization-Group H)
( f)
( hom-unit-abelianization-Group G)
( hom-unit-abelianization-Group H)
( abelianization-hom-Group G H f)
naturality-unit-abelianization-Group G H f =
naturality-hom-quotient-Group G H
( commutator-normal-subgroup-Group G)
( commutator-normal-subgroup-Group H)
( f , preserves-commutator-subgroup-hom-Group G H f)

naturality-unit-abelianization-Group' :
naturality-family-of-morphisms-functor-Large-Category
( Group-Large-Category)
( Group-Large-Category)
( id-functor-Large-Category Group-Large-Category)
( comp-functor-Large-Category
( Group-Large-Category)
( Ab-Large-Category)
( Group-Large-Category)
( forgetful-functor-Ab)
( abelianization-functor-Group))
( hom-unit-abelianization-Group)
naturality-unit-abelianization-Group' {X = G} {H} f =
eq-htpy-hom-Group G
( group-abelianization-Group H)
( naturality-unit-abelianization-Group G H f)

unit-abelianization-Group :
natural-transformation-Large-Category
( Group-Large-Category)
( Group-Large-Category)
( id-functor-Large-Category Group-Large-Category)
( comp-functor-Large-Category
( Group-Large-Category)
( Ab-Large-Category)
( Group-Large-Category)
( forgetful-functor-Ab)
( abelianization-functor-Group))

hom-natural-transformation-Large-Precategory
unit-abelianization-Group =
hom-unit-abelianization-Group
naturality-natural-transformation-Large-Precategory
unit-abelianization-Group =
naturality-unit-abelianization-Group'


### The universal property of abelianization

Proof: Since the abelianization of G is constructed as the quotient group G/[G,G], we immediately obtain that the precomposition function

  hom-Group Gᵃᵇ H → nullifying-hom-Group G H [G,G]


is an equivalence for any group H. That is, any group homomorphism f : G → H of which the kernel contains the commutator subgroup [G,G] extends uniquely to the abelianization.

Since abelian groups have trivial commutator subgroups and since the inclusion f [G,G] ⊆ [H,H] holds for any group homomorphism, it follows that any group homomorphism G → A into an abelian group A extends uniquely to the abelianization Gᵃᵇ. This proves the claim.

module _
{l1 : Level} (G : Group l1)
where

is-quotient-group-abelianization-Group :
universal-property-quotient-Group G
( commutator-normal-subgroup-Group G)
( group-abelianization-Group G)
( nullifying-quotient-hom-Group G (commutator-normal-subgroup-Group G))
is-quotient-group-abelianization-Group =
is-quotient-group-quotient-Group G (commutator-normal-subgroup-Group G)

is-abelianization-abelianization-Group :
is-abelianization-Group G
( abelianization-Group G)
( hom-unit-abelianization-Group G)
is-abelianization-abelianization-Group A =
is-equiv-comp
( hom-nullifying-hom-Group G
( group-Ab A)
( commutator-normal-subgroup-Group G))
( precomp-nullifying-hom-Group G
( commutator-normal-subgroup-Group G)
( group-abelianization-Group G)
( nullifying-quotient-hom-Group G
( commutator-normal-subgroup-Group G))
( group-Ab A))
( is-quotient-group-abelianization-Group (group-Ab A))
( is-equiv-hom-nullifying-hom-group-Ab G A)


equiv-is-adjoint-pair-abelianization-forgetful-functor-Ab :
{l1 l2 : Level} (G : Group l1) (A : Ab l2) →
hom-Ab (abelianization-Group G) A ≃ hom-Group G (group-Ab A)
pr1 (equiv-is-adjoint-pair-abelianization-forgetful-functor-Ab G A) h =
comp-hom-Group G
( group-abelianization-Group G)
( group-Ab A)
( h)
( hom-unit-abelianization-Group G)
is-abelianization-abelianization-Group G A

{l1 l2 l3 l4 : Level}
(G : Group l1) (H : Group l2) (f : hom-Group G H)
(A : Ab l3) (B : Ab l4) (g : hom-Ab A B) →
coherence-square-maps
( λ h →
comp-hom-Ab
( abelianization-Group G)
( abelianization-Group H)
( B)
( comp-hom-Ab (abelianization-Group H) A B g h)
( abelianization-hom-Group G H f))
( λ h →
comp-hom-Group G H
( group-Ab B)
( comp-hom-Group H (group-Ab A) (group-Ab B) g h)
( f))
G H f A B g h =
eq-htpy-hom-Group G
( group-Ab B)
( ( map-hom-Ab A B g ∘ map-hom-Ab (abelianization-Group H) A h) ·l
( naturality-unit-abelianization-Group G H f))

( Group-Large-Category)
( Ab-Large-Category)
( abelianization-functor-Group)
( forgetful-functor-Ab)
{ X1 = G}
{ X2 = H}
{ Y1 = A}
{ Y2 = B}
( f)
( g) =
A B g

( λ l → l)
( λ l → l)
( Group-Large-Category)
( Ab-Large-Category)