Perfect groups

A group G is perfect if it equals its commutator subgroup, that is ⁅G, G⁆ = G.

Among the basic results, we show that

• a nontrivial perfect group is not solvable (IsPerfect.not_isSolvable);
• an abelian perfect group is trivial (IsPerfect.subsingleton_of_isMulCommutative).

Main Definition

• Group.IsPerfect: a group G is perfect if it equals its own commutator, that is ⁅⊤, ⊤⁆ = ⊤, where ⊤ is the full subgroup G.

Main Theorems

• subsingleton_abelianization_iff_isPerfect: a group is perfect if and only if its abelianization is trivial.
• IsPerfect.map: The image of a perfect group under a monoid homomorphism is perfect.
• IsPerfect.instQuotientSubgroup: The quotient of a perfect group by a normal subgroup is perfect.
• IsPerfect.ofSurjective: The image of a perfect group under a surjective monoid homomorphism is perfect.

class AddGroup.IsPerfect (G : Type u_1) [AddGroup G] : Prop

An additive group G is perfect if G equals its commutator subgroup ⁅G, G⁆.

• addCommutator_eq_top : addCommutator G = ⊤

  The commutator of the group G with itself is the whole group G.

class Group.IsPerfect (G : Type u_1) [Group G] : Prop

A group G is perfect if G equals its commutator subgroup ⁅G, G⁆.

• commutator_eq_top : commutator G = ⊤

  The commutator of the group G with itself is the whole group G.

theorem Group.isPerfect_def {G : Type u_1} [Group G] : IsPerfect G ↔ commutator G = ⊤

theorem AddGroup.isPerfect_def {G : Type u_1} [AddGroup G] : IsPerfect G ↔ addCommutator G = ⊤

theorem Subgroup.isPerfect_iff {G : Type u_1} [Group G] {H : Subgroup G} : Group.IsPerfect ↥H ↔ ⁅H, H⁆ = H

theorem AddSubgroup.isPerfect_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : AddGroup.IsPerfect ↥H ↔ ⁅H, H⁆ = H

theorem Subgroup.commutator_eq_self {G : Type u_1} [Group G] {H : Subgroup G} [hH : Group.IsPerfect ↥H] : ⁅H, H⁆ = H

theorem AddSubgroup.addCommutator_eq_self {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : AddGroup.IsPerfect ↥H] : ⁅H, H⁆ = H

theorem Group.subsingleton_abelianization_iff_isPerfect {G : Type u_1} [Group G] : Subsingleton (Abelianization G) ↔ IsPerfect G

theorem AddGroup.subsingleton_abelianization_iff_isPerfect {G : Type u_1} [AddGroup G] : Subsingleton (Abelianization G) ↔ IsPerfect G

theorem Group.IsPerfect.mem_commutator {G : Type u_1} [Group G] [hP : IsPerfect G] {g : G} : g ∈ commutator G

theorem AddGroup.IsPerfect.mem_addCommutator {G : Type u_1} [AddGroup G] [hP : IsPerfect G] {g : G} : g ∈ addCommutator G

instance Group.IsPerfect.instOfSubsingleton {G : Type u_1} [Group G] [Subsingleton G] : IsPerfect G

The trivial group is perfect.

instance AddGroup.IsPerfect.instOfSubsingleton {G : Type u_1} [AddGroup G] [Subsingleton G] : IsPerfect G

The trivial group is perfect.

theorem Group.IsPerfect.top_iff {G : Type u_1} [Group G] : IsPerfect ↥⊤ ↔ IsPerfect G

theorem AddGroup.IsPerfect.top_iff {G : Type u_1} [AddGroup G] : IsPerfect ↥⊤ ↔ IsPerfect G

instance Group.IsPerfect.instSubtypeMemSubgroupTop {G : Type u_1} [Group G] [IsPerfect G] : IsPerfect ↥⊤

instance AddGroup.IsPerfect.instSubtypeMemAddSubgroupTop {G : Type u_1} [AddGroup G] [IsPerfect G] : IsPerfect ↥⊤

theorem Group.IsPerfect.not_isSolvable (G : Type u_1) [Group G] [Nontrivial G] [IsPerfect G] : ¬IsSolvable G

theorem AddGroup.IsPerfect.not_isSolvable (G : Type u_1) [AddGroup G] [Nontrivial G] [IsPerfect G] : ¬IsSolvable G

theorem Group.IsPerfect.not_isNilpotent (G : Type u_1) [Group G] [Nontrivial G] [IsPerfect G] : ¬IsNilpotent G

theorem AddGroup.IsPerfect.not_isNilpotent (G : Type u_1) [AddGroup G] [Nontrivial G] [IsPerfect G] : ¬IsNilpotent G

theorem Group.IsPerfect.not_isMulCommutative (G : Type u_1) [Group G] [Nontrivial G] [IsPerfect G] : ¬IsMulCommutative G

theorem AddGroup.IsPerfect.not_isAddCommutative (G : Type u_1) [AddGroup G] [Nontrivial G] [IsPerfect G] : ¬IsAddCommutative G

instance Group.IsPerfect.subsingleton_of_isMulCommutative {G : Type u_1} [Group G] [hG : IsPerfect G] [h_comm : IsMulCommutative G] : Subsingleton G

instance AddGroup.IsPerfect.subsingleton_of_isAddCommutative {G : Type u_1} [AddGroup G] [hG : IsPerfect G] [h_comm : IsAddCommutative G] : Subsingleton G

theorem Group.IsPerfect.map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H : Subgroup G} (f : G →* G') [IsPerfect ↥H] : IsPerfect ↥(Subgroup.map f H)

theorem AddGroup.IsPerfect.map {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {H : AddSubgroup G} (f : G →+ G') [IsPerfect ↥H] : IsPerfect ↥(AddSubgroup.map f H)

theorem Group.IsPerfect.range {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') [IsPerfect G] : IsPerfect ↥f.range

theorem AddGroup.IsPerfect.range {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') [IsPerfect G] : IsPerfect ↥f.range

theorem Group.IsPerfect.ofSurjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} [IsPerfect G] (hf : Function.Surjective ⇑f) : IsPerfect G'

theorem AddGroup.IsPerfect.ofSurjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} [IsPerfect G] (hf : Function.Surjective ⇑f) : IsPerfect G'

instance Group.IsPerfect.instQuotientSubgroup {G : Type u_1} [Group G] {H : Subgroup G} [H.Normal] [IsPerfect G] : IsPerfect (G ⧸ H)

instance AddGroup.IsPerfect.instQuotientAddSubgroup {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [H.Normal] [IsPerfect G] : IsPerfect (G ⧸ H)

@[simp]

theorem Group.IsPerfect.derivedSeries_eq_top (G : Type u_1) [Group G] [IsPerfect G] (n : ℕ) : Subgroup.derivedSeries G n = ⊤

@[simp]

theorem AddGroup.IsPerfect.derivedSeries_eq_top (G : Type u_1) [AddGroup G] [IsPerfect G] (n : ℕ) : AddSubgroup.derivedSeries G n = ⊤

@[simp]

theorem Group.IsPerfect.lowerCentralSeries_eq_top {G : Type u_1} [Group G] (H : Subgroup G) [IsPerfect ↥H] (n : ℕ) : H.lowerCentralSeries n = H

@[simp]

theorem AddGroup.IsPerfect.lowerCentralSeries_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsPerfect ↥H] (n : ℕ) : H.lowerCentralSeries n = H

@[simp]

theorem Group.IsPerfect.upperCentralSeries_eq_center (G : Type u_1) [Group G] [IsPerfect G] {n : ℕ} (hn : n ≠ 0) : Subgroup.upperCentralSeries G n = Subgroup.center G

@[simp]

theorem AddGroup.IsPerfect.upperCentralSeries_eq_center (G : Type u_1) [AddGroup G] [IsPerfect G] {n : ℕ} (hn : n ≠ 0) : AddSubgroup.upperCentralSeries G n = AddSubgroup.center G

@[simp]

theorem Group.IsPerfect.center_quotient_center_eq_bot (G : Type u_1) [Group G] [IsPerfect G] : Subgroup.center (G ⧸ Subgroup.center G) = ⊥

Grün's lemma

@[simp]

theorem AddGroup.IsPerfect.center_quotient_center_eq_bot (G : Type u_1) [AddGroup G] [IsPerfect G] : AddSubgroup.center (G ⧸ AddSubgroup.center G) = ⊥