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.Abelianization.map
: lifts a group homomorphism to a homomorphism between the abelianizationsMulEquiv.abelianizationCongr
: Equivalent groups have equivalent abelianizations
The commutator subgroup of a group G is the normal subgroup
generated by the commutators [p,q]=p*q*p⁻¹*q⁻¹
.
Instances For
The abelianization of G is the quotient of G by its commutator subgroup.
Instances For
of
is the canonical projection from G to its abelianization.
Instances For
See note [partially-applied ext lemmas].
The map operation of the Abelianization
functor
Instances For
An Abelian group is equivalent to its own abelianization.
Instances For
Subgroup generated by representatives g₁ g₂ : G
of commutators ⁅g₁, g₂⁆ ∈ G
.