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.group (commutator G)), mul_assoc := _, one := group.one (quotient_group.group (commutator G)), one_mul := _, mul_one := _, inv := group.inv (quotient_group.group (commutator G)), 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]
(f : G →* A) :
abelianization G →* A
Equations
- abelianization.lift f = quotient_group.lift (commutator G) f _
@[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
theorem
abelianization.hom_ext
{G : Type u}
[group G]
{A : Type v}
[monoid A]
(φ ψ : abelianization G →* A)
(h : φ.comp abelianization.of = ψ.comp abelianization.of) :
φ = ψ