mathlib documentation


def commutator.normal (G : Type u) [group G] :

def commutator (G : Type u) [group G] :

The commutator subgroup of a group G is the normal subgroup generated by the commutators [p,q]=p*q*p⁻¹*q⁻¹

def abelianization (G : Type u) [group G] :
Type u

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


def abelianization.of {G : Type u} [group G] :

of is the canonical projection from G to its abelianization.

theorem abelianization.commutator_subset_ker {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) :

def abelianization.lift {G : Type u} [group G] {A : Type v} [comm_group A] (f : 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.

theorem abelianization.lift.of {G : Type u} [group G] {A : Type v} [comm_group A] (f : G →* A) (x : G) :

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} :

theorem abelianization.hom_ext {G : Type u} [group G] {A : Type v} [monoid A] (φ ψ : abelianization G →* A) (h : φ.comp abelianization.of = ψ.comp abelianization.of) :
φ = ψ

See note [partially-applied ext lemmas].