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 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 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 isSolvable_def (G : Type u_1) [Group G] : IsSolvable G ↔ ∃ (n : ℕ), derivedSeries G n = ⊥

@[instance 100]

instance CommGroup.isSolvable {G : Type u_3} [CommGroup G] : IsSolvable G

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

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

@[instance 100]

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

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' : IsSolvable G'] [hG'' : IsSolvable G''] : IsSolvable G

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

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

theorem solvable_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'

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

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

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

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

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

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) ↔ IsSolvable G

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

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

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