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 groupG
as a subgroup ofG
.abelianization
: defines the abelianization of a groupG
as the quotient of a group by its commutator subgroup.
The commutator subgroup of a group G is the normal subgroup
generated by the commutators [p,q]=p*q*p⁻¹*q⁻¹
.
Equations
- commutator G = subgroup.normal_closure {x : G | ∃ (p q : G), ((p * q) * p⁻¹) * q⁻¹ = x}
The abelianization of G is the quotient of G by its commutator subgroup.
Equations
@[instance]
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 := _, mul_left_inv := _, mul_comm := _}
@[instance]
Equations
- abelianization.inhabited G = {default := 1}
of
is the canonical projection from G to its abelianization.
Equations
- abelianization.of = {to_fun := quotient_group.mk (commutator G), map_one' := _, map_mul' := _}
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
@[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) :
φ = ψ