# 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

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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

## Equations

- Abelianization G = (G ⧸ commutator G)

## Instances For

## Equations

- Abelianization.commGroup G = let __src := QuotientGroup.Quotient.group (commutator G); CommGroup.mk ⋯

## Equations

- Abelianization.instInhabited G = { default := 1 }

## Equations

## Equations

- ⋯ = ⋯

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

See note [partially-applied ext lemmas].

The map operation of the `Abelianization`

functor

## Equations

- Abelianization.map f = Abelianization.lift (Abelianization.of.comp f)

## Instances For

Use `map`

as the preferred simp normal form.

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

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

Representatives `(g₁, g₂) : G × G`

of commutators `⁅g₁, g₂⁆ ∈ G`

.

## Equations

- commutatorRepresentatives G = Set.range fun (g : ↑(commutatorSet G)) => (Exists.choose ⋯, ⋯.choose)

## Instances For

## Equations

- ⋯ = ⋯

Subgroup generated by representatives `g₁ g₂ : G`

of commutators `⁅g₁, g₂⁆ ∈ G`

.

## Equations

- closureCommutatorRepresentatives G = Subgroup.closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)

## Instances For

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯