Solvable Groups

In this file we introduce the notion of a solvable group. We define a solvable group as one whose derived series is eventually trivial. This requires defining the commutator of two subgroups and the derived series of a group.

Main definitions

• derivedSeries G n : the nth term in the derived series of G, defined by iterating general_commutator starting with the top subgroup
• IsSolvable G : the group G is solvable

def AddSubgroup.derivedSeries (G : Type u_3) [AddGroup G] : ℕ → AddSubgroup G

The derived series of the additive group G, obtained by starting from the additive subgroup ⊤ and repeatedly taking the commutator of the previous additive subgroup with itself n times.

Equations

• AddSubgroup.derivedSeries G 0 = ⊤
• AddSubgroup.derivedSeries G n.succ = ⁅AddSubgroup.derivedSeries G n, AddSubgroup.derivedSeries G n⁆

def Subgroup.derivedSeries (G : Type u_1) [Group G] : ℕ → Subgroup G

The derived series of the group G, obtained by starting from the subgroup ⊤ and repeatedly taking the commutator of the previous subgroup with itself n times.

Equations

• Subgroup.derivedSeries G 0 = ⊤
• Subgroup.derivedSeries G n.succ = ⁅Subgroup.derivedSeries G n, Subgroup.derivedSeries G n⁆

@[simp]

theorem Subgroup.derivedSeries_zero (G : Type u_1) [Group G] : derivedSeries G 0 = ⊤

@[simp]

theorem AddSubgroup.derivedSeries_zero (G : Type u_1) [AddGroup G] : derivedSeries G 0 = ⊤

@[simp]

theorem Subgroup.derivedSeries_succ (G : Type u_1) [Group G] (n : ℕ) : derivedSeries G (n + 1) = ⁅derivedSeries G n, derivedSeries G n⁆

@[simp]

theorem AddSubgroup.derivedSeries_succ (G : Type u_1) [AddGroup G] (n : ℕ) : derivedSeries G (n + 1) = ⁅derivedSeries G n, derivedSeries G n⁆

theorem Subgroup.derivedSeries_normal (G : Type u_1) [Group G] (n : ℕ) : (derivedSeries G n).Normal

theorem AddSubgroup.derivedSeries_normal (G : Type u_1) [AddGroup G] (n : ℕ) : (derivedSeries G n).Normal

@[simp]

theorem Subgroup.derivedSeries_one (G : Type u_1) [Group G] : derivedSeries G 1 = _root_.commutator G

@[simp]

theorem AddSubgroup.derivedSeries_one (G : Type u_1) [AddGroup G] : derivedSeries G 1 = _root_.addCommutator G

theorem Subgroup.derivedSeries_antitone (G : Type u_1) [Group G] : Antitone (derivedSeries G)

theorem AddSubgroup.derivedSeries_antitone (G : Type u_1) [AddGroup G] : Antitone (derivedSeries G)

instance Subgroup.derivedSeries_characteristic (G : Type u_1) [Group G] (n : ℕ) : (derivedSeries G n).Characteristic

instance AddSubgroup.derivedSeries_characteristic (G : Type u_1) [AddGroup G] (n : ℕ) : (derivedSeries G n).Characteristic

theorem Subgroup.map_derivedSeries_le_derivedSeries {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (n : ℕ) : map f (derivedSeries G n) ≤ derivedSeries G' n

theorem AddSubgroup.map_derivedSeries_le_derivedSeries {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (n : ℕ) : map f (derivedSeries G n) ≤ derivedSeries G' n

theorem Subgroup.derivedSeries_le_map_derivedSeries {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective ⇑f) (n : ℕ) : derivedSeries G' n ≤ map f (derivedSeries G n)

theorem AddSubgroup.derivedSeries_le_map_derivedSeries {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} (hf : Function.Surjective ⇑f) (n : ℕ) : derivedSeries G' n ≤ map f (derivedSeries G n)

theorem Subgroup.map_derivedSeries_eq {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective ⇑f) (n : ℕ) : map f (derivedSeries G n) = derivedSeries G' n

theorem AddSubgroup.map_derivedSeries_eq {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} (hf : Function.Surjective ⇑f) (n : ℕ) : map f (derivedSeries G n) = derivedSeries G' n

@[deprecated Subgroup.derivedSeries (since := "2026-10-17")]

def derivedSeries (G : Type u_1) [Group G] : ℕ → Subgroup G

Alias of Subgroup.derivedSeries.

---

The derived series of the group G, obtained by starting from the subgroup ⊤ and repeatedly taking the commutator of the previous subgroup with itself n times.

Equations

• derivedSeries = Subgroup.derivedSeries

@[deprecated Subgroup.derivedSeries_zero (since := "2026-10-17")]

theorem derivedSeries_zero (G : Type u_1) [Group G] : Subgroup.derivedSeries G 0 = ⊤

Alias of Subgroup.derivedSeries_zero.

@[deprecated Subgroup.derivedSeries_succ (since := "2026-10-17")]

theorem derivedSeries_succ (G : Type u_1) [Group G] (n : ℕ) : Subgroup.derivedSeries G (n + 1) = ⁅Subgroup.derivedSeries G n, Subgroup.derivedSeries G n⁆

Alias of Subgroup.derivedSeries_succ.

@[deprecated Subgroup.derivedSeries_normal (since := "2026-10-17")]

theorem derivedSeries_normal (G : Type u_1) [Group G] (n : ℕ) : (Subgroup.derivedSeries G n).Normal

Alias of Subgroup.derivedSeries_normal.

@[deprecated Subgroup.derivedSeries_one (since := "2026-10-17")]

theorem derivedSeries_one (G : Type u_1) [Group G] : Subgroup.derivedSeries G 1 = commutator G

Alias of Subgroup.derivedSeries_one.

@[deprecated Subgroup.derivedSeries_antitone (since := "2026-10-17")]

theorem derivedSeries_antitone (G : Type u_1) [Group G] : Antitone (Subgroup.derivedSeries G)

Alias of Subgroup.derivedSeries_antitone.

@[deprecated Subgroup.derivedSeries_characteristic (since := "2026-10-17")]

theorem derivedSeries_characteristic (G : Type u_1) [Group G] (n : ℕ) : (Subgroup.derivedSeries G n).Characteristic

Alias of Subgroup.derivedSeries_characteristic.

@[deprecated Subgroup.map_derivedSeries_le_derivedSeries (since := "2026-10-17")]

theorem map_derivedSeries_le_derivedSeries {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (n : ℕ) : Subgroup.map f (Subgroup.derivedSeries G n) ≤ Subgroup.derivedSeries G' n

Alias of Subgroup.map_derivedSeries_le_derivedSeries.

@[deprecated Subgroup.derivedSeries_le_map_derivedSeries (since := "2026-10-17")]

theorem derivedSeries_le_map_derivedSeries {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective ⇑f) (n : ℕ) : Subgroup.derivedSeries G' n ≤ Subgroup.map f (Subgroup.derivedSeries G n)

Alias of Subgroup.derivedSeries_le_map_derivedSeries.

@[deprecated Subgroup.map_derivedSeries_eq (since := "2026-10-17")]

theorem map_derivedSeries_eq {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective ⇑f) (n : ℕ) : Subgroup.map f (Subgroup.derivedSeries G n) = Subgroup.derivedSeries G' n

Alias of Subgroup.map_derivedSeries_eq.

class AddGroup.IsSolvable (G : Type u_3) [AddGroup G] : Prop

An additive group G is solvable if its derived series is eventually trivial.

• solvable : ∃ (n : ℕ), AddSubgroup.derivedSeries G n = ⊥

  An additive group G is solvable if its derived series is eventually trivial.

theorem AddGroup.isSolvable_def (G : Type u_3) [AddGroup G] : IsSolvable G ↔ ∃ (n : ℕ), AddSubgroup.derivedSeries G n = ⊥

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

A group G is solvable if its derived series is eventually trivial.

• solvable : ∃ (n : ℕ), Subgroup.derivedSeries G n = ⊥

  A group G is solvable if its derived series is eventually trivial.

theorem Group.isSolvable_def (G : Type u_1) [Group G] : IsSolvable G ↔ ∃ (n : ℕ), Subgroup.derivedSeries G n = ⊥

@[deprecated Group.IsSolvable (since := "2026-07-16")]

def IsSolvable (G : Type u_1) [Group G] : Prop

Alias of Group.IsSolvable.

---

A group G is solvable if its derived series is eventually trivial.

Equations

• IsSolvable = Group.IsSolvable

@[deprecated Group.isSolvable_def (since := "2026-07-17")]

theorem isSolvable_def (G : Type u_1) [Group G] : Group.IsSolvable G ↔ ∃ (n : ℕ), Subgroup.derivedSeries G n = ⊥

Alias of Group.isSolvable_def.

@[instance 100]

instance Group.instIsSolvableOfIsMulCommutative {G : Type u_3} [Group G] [IsMulCommutative G] : IsSolvable G

@[instance 100]

instance AddGroup.instIsSolvableOfIsAddCommutative {G : Type u_3} [AddGroup G] [IsAddCommutative G] : IsSolvable G

theorem Group.isSolvable_of_comm {G : Type u_3} [hG : Group G] (h : ∀ (a b : G), a * b = b * a) : IsSolvable G

theorem AddGroup.isSolvable_of_comm {G : Type u_3} [hG : AddGroup G] (h : ∀ (a b : G), a + b = b + a) : IsSolvable G

@[deprecated Group.isSolvable_of_comm (since := "2026-07-16")]

theorem isSolvable_of_comm {G : Type u_3} [hG : Group G] (h : ∀ (a b : G), a * b = b * a) : Group.IsSolvable G

Alias of Group.isSolvable_of_comm.

theorem Group.isSolvable_of_top_eq_bot (G : Type u_1) [Group G] (h : ⊤ = ⊥) : IsSolvable G

theorem AddGroup.isSolvable_of_top_eq_bot (G : Type u_1) [AddGroup G] (h : ⊤ = ⊥) : IsSolvable G

@[deprecated Group.isSolvable_of_top_eq_bot (since := "2026-07-16")]

theorem isSolvable_of_top_eq_bot (G : Type u_1) [Group G] (h : ⊤ = ⊥) : Group.IsSolvable G

Alias of Group.isSolvable_of_top_eq_bot.

@[instance 100]

instance Group.instIsSolvableOfSubsingleton (G : Type u_1) [Group G] [Subsingleton G] : IsSolvable G

@[instance 100]

instance AddGroup.instIsSolvableOfSubsingleton (G : Type u_1) [AddGroup G] [Subsingleton G] : IsSolvable G

theorem Group.isSolvable_of_ker_le_range {G : Type u_1} [Group G] {G' : Type u_3} {G'' : Type u_4} [Group G'] [Group G''] (f : G' →* G) (g : G →* G'') (hfg : g.ker ≤ f.range) [hG' : IsSolvable G'] [hG'' : IsSolvable G''] : IsSolvable G

theorem AddGroup.isSolvable_of_ker_le_range {G : Type u_1} [AddGroup G] {G' : Type u_3} {G'' : Type u_4} [AddGroup G'] [AddGroup G''] (f : G' →+ G) (g : G →+ G'') (hfg : g.ker ≤ f.range) [hG' : IsSolvable G'] [hG'' : IsSolvable G''] : IsSolvable G

@[deprecated Group.isSolvable_of_ker_le_range (since := "2026-07-16")]

theorem solvable_of_ker_le_range {G : Type u_1} [Group G] {G' : Type u_3} {G'' : Type u_4} [Group G'] [Group G''] (f : G' →* G) (g : G →* G'') (hfg : g.ker ≤ f.range) [hG' : Group.IsSolvable G'] [hG'' : Group.IsSolvable G''] : Group.IsSolvable G

Alias of Group.isSolvable_of_ker_le_range.

theorem Group.isSolvable_of_isSolvable_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Injective ⇑f) [IsSolvable G'] : IsSolvable G

theorem AddGroup.isSolvable_of_isSolvable_injective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} (hf : Function.Injective ⇑f) [IsSolvable G'] : IsSolvable G

@[deprecated Group.isSolvable_of_isSolvable_injective (since := "2026-07-16")]

theorem solvable_of_solvable_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Injective ⇑f) [Group.IsSolvable G'] : Group.IsSolvable G

Alias of Group.isSolvable_of_isSolvable_injective.

instance Group.instIsSolvableSubtypeMemSubgroup {G : Type u_1} [Group G] (H : Subgroup G) [IsSolvable G] : IsSolvable ↥H

instance AddGroup.instIsSolvableSubtypeMemAddSubgroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [IsSolvable G] : IsSolvable ↥H

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

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

@[deprecated Group.isSolvable_of_surjective (since := "2026-07-16")]

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

Alias of Group.isSolvable_of_surjective.

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

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

theorem Group.isSolvable_iff_subgroup_quotient {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : IsSolvable G ↔ IsSolvable ↥H ∧ IsSolvable (G ⧸ H)

theorem AddGroup.isSolvable_iff_addSubgroup_quotient {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] : IsSolvable G ↔ IsSolvable ↥H ∧ IsSolvable (G ⧸ H)

theorem Group.isSolvable_of_subgroup_quotient {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [IsSolvable ↥H] [IsSolvable (G ⧸ H)] : IsSolvable G

theorem AddGroup.isSolvable_of_addSubgroup_quotient {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Normal] [IsSolvable ↥H] [IsSolvable (G ⧸ H)] : IsSolvable G

instance Group.instIsSolvableProd {G : Type u_1} [Group G] {G' : Type u_3} [Group G'] [IsSolvable G] [IsSolvable G'] : IsSolvable (G × G')

instance AddGroup.instIsSolvableSum {G : Type u_1} [AddGroup G] {G' : Type u_3} [AddGroup G'] [IsSolvable G] [IsSolvable G'] : IsSolvable (G × G')

theorem Group.IsSolvable.commutator_lt_top_of_nontrivial (G : Type u_1) [Group G] [hG : IsSolvable G] [Nontrivial G] : commutator G < ⊤

theorem AddGroup.IsSolvable.addCommutator_lt_top_of_nontrivial (G : Type u_1) [AddGroup G] [hG : IsSolvable G] [Nontrivial G] : addCommutator G < ⊤

@[deprecated Group.IsSolvable.commutator_lt_top_of_nontrivial (since := "2026-07-16")]

theorem IsSolvable.commutator_lt_top_of_nontrivial (G : Type u_1) [Group G] [hG : Group.IsSolvable G] [Nontrivial G] : commutator G < ⊤

Alias of Group.IsSolvable.commutator_lt_top_of_nontrivial.

theorem Group.IsSolvable.commutator_lt_of_ne_bot {G : Type u_1} [Group G] [IsSolvable G] {H : Subgroup G} (hH : H ≠ ⊥) : ⁅H, H⁆ < H

theorem AddGroup.IsSolvable.addCommutator_lt_of_ne_bot {G : Type u_1} [AddGroup G] [IsSolvable G] {H : AddSubgroup G} (hH : H ≠ ⊥) : ⁅H, H⁆ < H

@[deprecated Group.IsSolvable.commutator_lt_of_ne_bot (since := "2026-07-16")]

theorem IsSolvable.commutator_lt_of_ne_bot {G : Type u_1} [Group G] [Group.IsSolvable G] {H : Subgroup G} (hH : H ≠ ⊥) : ⁅H, H⁆ < H

Alias of Group.IsSolvable.commutator_lt_of_ne_bot.

theorem Group.isSolvable_iff_commutator_lt {G : Type u_1} [Group G] [WellFoundedLT (Subgroup G)] : IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H

theorem AddGroup.isSolvable_iff_addCommutator_lt {G : Type u_1} [AddGroup G] [WellFoundedLT (AddSubgroup G)] : IsSolvable G ↔ ∀ (H : AddSubgroup G), H ≠ ⊥ → ⁅H, H⁆ < H

@[deprecated Group.isSolvable_iff_commutator_lt (since := "2026-07-16")]

theorem isSolvable_iff_commutator_lt {G : Type u_1} [Group G] [WellFoundedLT (Subgroup G)] : Group.IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H

Alias of Group.isSolvable_iff_commutator_lt.

theorem Group.isSolvable_commutator_iff {G : Type u_1} [Group G] : IsSolvable ↥(commutator G) ↔ IsSolvable G

theorem AddGroup.isSolvable_addCommutator_iff {G : Type u_1} [AddGroup G] : IsSolvable ↥(addCommutator G) ↔ IsSolvable G

theorem IsSimpleGroup.derivedSeries_succ {G : Type u_1} [Group G] [IsSimpleGroup G] {n : ℕ} : Subgroup.derivedSeries G n.succ = commutator G

theorem IsSimpleAddGroup.derivedSeries_succ {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] {n : ℕ} : AddSubgroup.derivedSeries G n.succ = addCommutator G

theorem IsSimpleGroup.comm_iff_isSolvable {G : Type u_1} [Group G] [IsSimpleGroup G] : (∀ (a b : G), a * b = b * a) ↔ Group.IsSolvable G

theorem IsSimpleAddGroup.comm_iff_isSolvable {G : Type u_1} [AddGroup G] [IsSimpleAddGroup G] : (∀ (a b : G), a + b = b + a) ↔ AddGroup.IsSolvable G

theorem Group.not_isSolvable_of_mem_derivedSeries {G : Type u_1} [Group G] {g : G} (h1 : g ≠ 1) (h2 : ∀ (n : ℕ), g ∈ Subgroup.derivedSeries G n) : ¬IsSolvable G

theorem AddGroup.not_isSolvable_of_mem_derivedSeries {G : Type u_1} [AddGroup G] {g : G} (h1 : g ≠ 0) (h2 : ∀ (n : ℕ), g ∈ AddSubgroup.derivedSeries G n) : ¬IsSolvable G

@[deprecated Group.not_isSolvable_of_mem_derivedSeries (since := "2026-10-17")]

theorem not_isSolvable_of_mem_derivedSeries {G : Type u_1} [Group G] {g : G} (h1 : g ≠ 1) (h2 : ∀ (n : ℕ), g ∈ Subgroup.derivedSeries G n) : ¬Group.IsSolvable G

Alias of Group.not_isSolvable_of_mem_derivedSeries.

@[deprecated Group.not_isSolvable_of_mem_derivedSeries (since := "2026-07-16")]

theorem not_solvable_of_mem_derivedSeries {G : Type u_1} [Group G] {g : G} (h1 : g ≠ 1) (h2 : ∀ (n : ℕ), g ∈ Subgroup.derivedSeries G n) : ¬Group.IsSolvable G

Alias of Group.not_isSolvable_of_mem_derivedSeries.

theorem Equiv.Perm.not_isSolvable_fin_5 : ¬Group.IsSolvable (Perm (Fin 5))

@[deprecated Equiv.Perm.not_isSolvable_fin_5 (since := "2026-07-16")]

theorem Equiv.Perm.fin_5_not_solvable : ¬Group.IsSolvable (Perm (Fin 5))

Alias of Equiv.Perm.not_isSolvable_fin_5.

theorem Equiv.Perm.not_isSolvable (X : Type u_3) (hX : 5 ≤ Cardinal.mk X) : ¬Group.IsSolvable (Perm X)

@[deprecated Equiv.Perm.not_isSolvable (since := "2026-07-16")]

theorem Equiv.Perm.not_solvable (X : Type u_3) (hX : 5 ≤ Cardinal.mk X) : ¬Group.IsSolvable (Perm X)

Alias of Equiv.Perm.not_isSolvable.