# mathlibdocumentation

group_theory.solvable

# 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 #

• derived_series G n : the nth term in the derived series of G, defined by iterating general_commutator starting with the top subgroup
• is_solvable G : the group G is solvable
def derived_series (G : Type u_1) [group 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
@[simp]
theorem derived_series_zero (G : Type u_1) [group G] :
@[simp]
theorem derived_series_succ (G : Type u_1) [group G] (n : ) :
(n + 1) = ,
theorem derived_series_normal (G : Type u_1) [group G] (n : ) :
n).normal
@[simp]
theorem general_commutator_eq_commutator (G : Type u_1) [group G] :
theorem commutator_def' (G : Type u_1) [group G] :
= subgroup.closure {x : G | ∃ (p q : G), ((p * q) * p⁻¹) * q⁻¹ = x}
@[simp]
theorem derived_series_one (G : Type u_1) [group G] :
theorem map_commutator_eq_commutator_map {G : Type u_1} {G' : Type u_2} [group G] [group G'] {f : G →* G'} (H₁ H₂ : subgroup G) :
H₁,H₂ = H₁, H₂
theorem commutator_le_map_commutator {G : Type u_1} {G' : Type u_2} [group G] [group G'] {f : G →* G'} {H₁ H₂ : subgroup G} {K₁ K₂ : subgroup G'} (h₁ : K₁ H₁) (h₂ : K₂ H₂) :
K₁,K₂ H₁,H₂
theorem map_derived_series_le_derived_series {G : Type u_1} {G' : Type u_2} [group G] [group G'] (f : G →* G') (n : ) :
n) n
theorem derived_series_le_map_derived_series {G : Type u_1} {G' : Type u_2} [group G] [group G'] {f : G →* G'} (hf : function.surjective f) (n : ) :
n n)
theorem map_derived_series_eq {G : Type u_1} {G' : Type u_2} [group G] [group G'] {f : G →* G'} (hf : function.surjective f) (n : ) :
n) = n
@[class]
structure is_solvable (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.

Instances
theorem is_solvable_def (G : Type u_1) [group G] :
∃ (n : ), =
@[protected, instance]
def comm_group.is_solvable {G : Type u_1} [comm_group G] :
theorem is_solvable_of_comm {G : Type u_1} [hG : group G] (h : ∀ (a b : G), a * b = b * a) :
theorem is_solvable_of_top_eq_bot (G : Type u_1) [group G] (h : = ) :
@[protected, instance]
def is_solvable_of_subsingleton (G : Type u_1) [group G] [subsingleton 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) [h : is_solvable G'] :
@[protected, instance]
def subgroup_solvable_of_solvable {G : Type u_1} [group G] (H : subgroup G) [h : is_solvable G] :
theorem solvable_of_surjective {G : Type u_1} {G' : Type u_2} [group G] [group G'] {f : G →* G'} (hf : function.surjective f) [h : is_solvable G] :
@[protected, instance]
def solvable_quotient_of_solvable {G : Type u_1} [group G] (H : subgroup G) [H.normal] [h : is_solvable G] :
theorem solvable_of_ker_le_range {G : Type u_1} [group G] {G' : Type u_2} {G'' : Type u_3} [group G'] [group G''] (f : G' →* G) (g : G →* G'') (hfg : g.ker f.range) [hG' : is_solvable G'] [hG'' : is_solvable G''] :
@[protected, instance]
def solvable_prod {G : Type u_1} [group G] {G' : Type u_2} [group G'] [h : is_solvable G] [h' : is_solvable G'] :
theorem is_simple_group.derived_series_succ {G : Type u_1} [group G] {n : } :
theorem is_simple_group.comm_iff_is_solvable {G : Type u_1} [group G]  :
(∀ (a b : G), a * b = b * a)
theorem not_solvable_of_mem_derived_series {G : Type u_1} [group G] {g : G} (h1 : g 1) (h2 : ∀ (n : ), g ) :
theorem equiv.perm.not_solvable (X : Type u_1) (hX : 5 # X) :