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 group G as a subgroup of G.
• Abelianization: defines the abelianization of a group G as the quotient of a group by its commutator subgroup.
• Abelianization.map: lifts a group homomorphism to a homomorphism between the abelianizations
• MulEquiv.abelianizationCongr: Equivalent groups have equivalent abelianizations

def commutator (G : Type u) [Group G] : Subgroup G

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

Equations

• commutator G = ⁅⊤, ⊤⁆

instance instNormalCommutator (G : Type u) [Group G] : Subgroup.Normal (commutator G)

Equations

• (_ : Subgroup.Normal (commutator G)) = (_ : Subgroup.Normal ⁅⊤, ⊤⁆)

theorem commutator_def (G : Type u) [Group G] : commutator G = ⁅⊤, ⊤⁆

theorem commutator_eq_closure (G : Type u) [Group G] : commutator G = Subgroup.closure (commutatorSet G)

theorem commutator_eq_normalClosure (G : Type u) [Group G] : commutator G = Subgroup.normalClosure (commutatorSet G)

instance commutator_characteristic (G : Type u) [Group G] : Subgroup.Characteristic (commutator G)

Equations

• (_ : Subgroup.Characteristic (commutator G)) = (_ : Subgroup.Characteristic ⁅⊤, ⊤⁆)

instance instFGSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupCommutatorToGroup (G : Type u) [Group G] [Finite ↑(commutatorSet G)] : Group.FG ↥(commutator G)

Equations

• (_ : Group.FG ↥(commutator G)) = (_ : Group.FG ↥(commutator G))

theorem rank_commutator_le_card (G : Type u) [Group G] [Finite ↑(commutatorSet G)] : Group.rank ↥(commutator G) ≤ Nat.card ↑(commutatorSet G)

theorem commutator_centralizer_commutator_le_center (G : Type u) [Group G] : ⁅Subgroup.centralizer ↑(commutator G), Subgroup.centralizer ↑(commutator G)⁆ ≤ Subgroup.center G

def Abelianization (G : Type u) [Group G] : Type u

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

Equations

• Abelianization G = (G ⧸ commutator G)

instance Abelianization.commGroup (G : Type u) [Group G] : CommGroup (Abelianization G)

Equations

• Abelianization.commGroup G = let src := QuotientGroup.Quotient.group (commutator G); CommGroup.mk (_ : ∀ (x y : Abelianization G), x * y = y * x)

instance Abelianization.instInhabitedAbelianization (G : Type u) [Group G] : Inhabited (Abelianization G)

Equations

• Abelianization.instInhabitedAbelianization G = { default := 1 }

instance Abelianization.instUniqueAbelianization (G : Type u) [Group G] [Unique G] : Unique (Abelianization G)

Equations

• Abelianization.instUniqueAbelianization G = Quotient.instUniqueQuotient (QuotientGroup.leftRel (commutator G))

instance Abelianization.instFintypeAbelianization (G : Type u) [Group G] [Fintype G] [DecidablePred fun (x : G) => x ∈ commutator G] : Fintype (Abelianization G)

Equations

• Abelianization.instFintypeAbelianization G = QuotientGroup.fintype (commutator G)

instance Abelianization.instFiniteAbelianization (G : Type u) [Group G] [Finite G] : Finite (Abelianization G)

Equations

• (_ : Finite (Abelianization G)) = (_ : Finite (Quotient (QuotientGroup.leftRel (commutator G))))

def Abelianization.of {G : Type u} [Group G] : G →* Abelianization G

of is the canonical projection from G to its abelianization.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Abelianization.mk_eq_of {G : Type u} [Group G] (a : G) : Quot.mk Setoid.r a = Abelianization.of a

theorem Abelianization.commutator_subset_ker {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) : commutator G ≤ MonoidHom.ker f

def Abelianization.lift {G : Type u} [Group G] {A : Type v} [CommGroup 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Abelianization.lift.of {G : Type u} [Group G] {A : Type v} [CommGroup 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} [CommGroup A] (f : G →* A) (φ : Abelianization G →* A) (hφ : ∀ (x : G), φ (Abelianization.of x) = f x) {x : Abelianization G} : φ x = (Abelianization.lift f) x

@[simp]

theorem Abelianization.lift_of {G : Type u} [Group G] : Abelianization.lift Abelianization.of = MonoidHom.id (Abelianization G)

theorem Abelianization.hom_ext {G : Type u} [Group G] {A : Type v} [Monoid A] (φ : Abelianization G →* A) (ψ : Abelianization G →* A) (h : MonoidHom.comp φ Abelianization.of = MonoidHom.comp ψ Abelianization.of) : φ = ψ

See note [partially-applied ext lemmas].

def Abelianization.map {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) : Abelianization G →* Abelianization H

The map operation of the Abelianization functor

Equations

• Abelianization.map f = Abelianization.lift (MonoidHom.comp Abelianization.of f)

@[simp]

theorem Abelianization.map_of {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) (x : G) : (Abelianization.map f) (Abelianization.of x) = Abelianization.of (f x)

@[simp]

theorem Abelianization.map_id {G : Type u} [Group G] : Abelianization.map (MonoidHom.id G) = MonoidHom.id (Abelianization G)

@[simp]

theorem Abelianization.map_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] (g : H →* I) : MonoidHom.comp (Abelianization.map g) (Abelianization.map f) = Abelianization.map (MonoidHom.comp g f)

@[simp]

theorem Abelianization.map_map_apply {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] {g : H →* I} {x : Abelianization G} : (Abelianization.map g) ((Abelianization.map f) x) = (Abelianization.map (MonoidHom.comp g f)) x

def MulEquiv.abelianizationCongr {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) : Abelianization G ≃* Abelianization H

Equivalent groups have equivalent abelianizations

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem abelianizationCongr_of {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) (x : G) : (MulEquiv.abelianizationCongr e) (Abelianization.of x) = Abelianization.of (e x)

@[simp]

theorem abelianizationCongr_refl {G : Type u} [Group G] : MulEquiv.abelianizationCongr (MulEquiv.refl G) = MulEquiv.refl (Abelianization G)

@[simp]

theorem abelianizationCongr_symm {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) : MulEquiv.symm (MulEquiv.abelianizationCongr e) = MulEquiv.abelianizationCongr (MulEquiv.symm e)

@[simp]

theorem abelianizationCongr_trans {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) {I : Type v} [Group I] (e₂ : H ≃* I) : MulEquiv.trans (MulEquiv.abelianizationCongr e) (MulEquiv.abelianizationCongr e₂) = MulEquiv.abelianizationCongr (MulEquiv.trans e e₂)

@[simp]

theorem Abelianization.equivOfComm_symm_apply {H : Type u_1} [CommGroup H] (a : Abelianization H) : (MulEquiv.symm Abelianization.equivOfComm) a = (Abelianization.lift (MonoidHom.id H)) a

@[simp]

theorem Abelianization.equivOfComm_apply {H : Type u_1} [CommGroup H] (a : H) : Abelianization.equivOfComm a = Abelianization.of a

def Abelianization.equivOfComm {H : Type u_1} [CommGroup H] : H ≃* Abelianization H

An Abelian group is equivalent to its own abelianization.

Equations

• One or more equations did not get rendered due to their size.

def commutatorRepresentatives (G : Type u) [Group G] : Set (G × G)

Representatives (g₁, g₂) : G × G of commutators ⁅g₁, g₂⁆ ∈ G.

Equations

• One or more equations did not get rendered due to their size.

instance instFiniteElemProdCommutatorRepresentatives (G : Type u) [Group G] [Finite ↑(commutatorSet G)] : Finite ↑(commutatorRepresentatives G)

Equations

• (_ : Finite ↑(commutatorRepresentatives G)) = (_ : Finite ↑(commutatorRepresentatives G))

def closureCommutatorRepresentatives (G : Type u) [Group G] : Subgroup G

Subgroup generated by representatives g₁ g₂ : G of commutators ⁅g₁, g₂⁆ ∈ G.

Equations

• closureCommutatorRepresentatives G = Subgroup.closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)

instance closureCommutatorRepresentatives_fg (G : Type u) [Group G] [Finite ↑(commutatorSet G)] : Group.FG ↥(closureCommutatorRepresentatives G)

Equations

• (_ : Group.FG ↥(closureCommutatorRepresentatives G)) = (_ : Group.FG ↥(Subgroup.closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)))

theorem rank_closureCommutatorRepresentatives_le (G : Type u) [Group G] [Finite ↑(commutatorSet G)] : Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)

theorem image_commutatorSet_closureCommutatorRepresentatives (G : Type u) [Group G] : ⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G

theorem card_commutatorSet_closureCommutatorRepresentatives (G : Type u) [Group G] : Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) = Nat.card ↑(commutatorSet G)

theorem card_commutator_closureCommutatorRepresentatives (G : Type u) [Group G] : Nat.card ↥(commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(commutator G)

instance instFiniteElemSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupClosureCommutatorRepresentativesCommutatorSetToGroup (G : Type u) [Group G] [Finite ↑(commutatorSet G)] : Finite ↑(commutatorSet ↥(closureCommutatorRepresentatives G))

Equations

• (_ : Finite ↑(commutatorSet ↥(closureCommutatorRepresentatives G))) = (_ : Finite ↑(commutatorSet ↥(closureCommutatorRepresentatives G)))