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 #

@[instance]
def general_commutator {G : Type u_1} [group G] :

The commutator of two subgroups H₁ and H₂.

Equations
theorem general_commutator_def {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
H₁,H₂ = subgroup.closure {x : G | ∃ (p : G) (H : p H₁) (q : G) (H : q H₂), ((p * q) * p⁻¹) * q⁻¹ = x}
@[instance]
def general_commutator_normal {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h₁ : H₁.normal] [h₂ : H₂.normal] :
H₁,H₂.normal
theorem general_commutator_mono {G : Type u_1} [group G] {H₁ H₂ K₁ K₂ : subgroup G} (h₁ : H₁ K₁) (h₂ : H₂ K₂) :
H₁,H₂ K₁,K₂
theorem general_commutator_def' {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
H₁,H₂ = subgroup.normal_closure {x : G | ∃ (p : G) (H : p H₁) (q : G) (H : q H₂), ((p * q) * p⁻¹) * q⁻¹ = x}
theorem general_commutator_le {G : Type u_1} [group G] (H₁ H₂ K : subgroup G) :
H₁,H₂ K ∀ (p : G), p H₁∀ (q : G), q H₂((p * q) * p⁻¹) * q⁻¹ K
theorem general_commutator_containment {G : Type u_1} [group G] (H₁ H₂ : subgroup G) {p q : G} (hp : p H₁) (hq : q H₂) :
((p * q) * p⁻¹) * q⁻¹ H₁,H₂
theorem general_commutator_comm {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
H₁,H₂ = H₂,H₁
theorem general_commutator_le_right {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₂.normal] :
H₁,H₂ H₂
theorem general_commutator_le_left {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₁.normal] :
H₁,H₂ H₁
@[simp]
theorem general_commutator_bot {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem bot_general_commutator {G : Type u_1} [group G] (H : subgroup G) :
theorem general_commutator_le_inf {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
H₁,H₂ H₁ H₂
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 commutator_def' (G : Type u_1) [group G] :
commutator 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) :
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₁ subgroup.map f H₁) (h₂ : K₂ subgroup.map f H₂) :
K₁,K₂ subgroup.map f 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 : ) :
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
theorem is_solvable_def (G : Type u_1) [group G] :
@[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 : = ) :
@[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'] :
@[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] :
@[instance]
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''] :
@[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 # X) :