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 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 for n times.

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

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 : ℕ) : derivedSeries G' n ≤ Subgroup.map f (derivedSeries G n)

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 (derivedSeries G n) = 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. We use this definition because it's the most convenient one to work with.

• solvable : ∃ (n : ℕ), 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 : ℕ), 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. We use this definition because it's the most convenient one to work with.

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 : ℕ), derivedSeries G n = ⊥

Alias of Group.isSolvable_def.

@[instance 100]

instance Group.instIsSolvable {G : Type u_3} [CommGroup 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

@[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

@[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

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

@[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

@[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

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'

@[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)

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

instance Group.instIsSolvableProd {G : Type u_1} [Group G] {G' : Type u_3} [Group 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 < ⊤

@[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

@[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

@[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 IsSimpleGroup.derivedSeries_succ {G : Type u_1} [Group G] [IsSimpleGroup G] {n : ℕ} : derivedSeries G n.succ = commutator 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 not_isSolvable_of_mem_derivedSeries {G : Type u_1} [Group G] {g : G} (h1 : g ≠ 1) (h2 : ∀ (n : ℕ), g ∈ derivedSeries G n) : ¬Group.IsSolvable G

@[deprecated 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 ∈ derivedSeries G n) : ¬Group.IsSolvable G

Alias of 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.