mathlib documentation

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 #

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 : ) :
theorem derived_series_normal (G : Type u_1) [group G] (n : ) :
@[simp]
theorem derived_series_one (G : Type u_1) [group G] :
theorem map_derived_series_le_derived_series {G : Type u_1} {G' : Type u_2} [group G] [group G'] (f : G →* G') (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 : ) :
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 : ) :
@[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 of this typeclass
theorem is_solvable_def (G : Type u_1) [group G] :
@[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_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''] :
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] :
@[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.comm_iff_is_solvable {G : Type u_1} [group G] [is_simple_group G] :
(∀ (a b : G), a * b = b * a) is_solvable G
theorem not_solvable_of_mem_derived_series {G : Type u_1} [group G] {g : G} (h1 : g 1) (h2 : ∀ (n : ), g derived_series G n) :
theorem equiv.perm.not_solvable (X : Type u_1) (hX : 5 cardinal.mk X) :