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.
Equations
- Abelianization.of = { toFun := QuotientGroup.mk, map_one' := ⋯, map_mul' := ⋯ }
Instances For
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
The map operation of the Abelianization
functor
Instances For
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 = { 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
Instances For
Subgroup generated by representatives g₁ g₂ : G
of commutators ⁅g₁, g₂⁆ ∈ G
.