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 #

general_commutator H₁ H₂ : the commutator of the subgroups H₁ and H₂
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

source

@[instance]

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

has_bracket (subgroup G) (subgroup G)

The commutator of two subgroups H₁ and H₂.

Equations

general_commutator = {bracket := λ (H₁ H₂ : subgroup G), subgroup.closure {x : G | ∃ (p : G) (H : p ∈ H₁) (q : G) (H : q ∈ H₂), ((p * q) * p⁻¹) * q⁻¹ = x}}

source

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}

source

@[instance]

def general_commutator_normal {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h₁ : H₁.normal] [h₂ : H₂.normal] :

⁅H₁,H₂⁆.normal

source

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₂⁆

source

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}

source

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

source

theorem general_commutator_comm {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :

⁅H₁,H₂⁆ = ⁅H₂,H₁⁆

source

theorem general_commutator_le_right {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₂.normal] :

⁅H₁,H₂⁆ ≤ H₂

source

theorem general_commutator_le_left {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₁.normal] :

⁅H₁,H₂⁆ ≤ H₁

source

@[simp]

theorem general_commutator_bot {G : Type u_1} [group G] (H : subgroup G) :

⁅H,⊥⁆ = ⊥

source

@[simp]

theorem bot_general_commutator {G : Type u_1} [group G] (H : subgroup G) :

⁅⊥,H⁆ = ⊥

source

theorem general_commutator_le_inf {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :

⁅H₁,H₂⁆ ≤ H₁ ⊓ H₂

source

def derived_series (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

derived_series G (n + 1) = ⁅derived_series G n,derived_series G n⁆
derived_series G 0 = ⊤

source

@[simp]

theorem derived_series_zero (G : Type u_1) [group G] :

derived_series G 0 = ⊤

source

@[simp]

theorem derived_series_succ (G : Type u_1) [group G] (n : ℕ) :

derived_series G (n + 1) = ⁅derived_series G n,derived_series G n⁆

source

theorem derived_series_normal (G : Type u_1) [group G] (n : ℕ) :

(derived_series G n).normal

source

@[simp]

theorem general_commutator_eq_commutator (G : Type u_1) [group G] :

⁅⊤,⊤⁆ = commutator G

source

theorem commutator_def' (G : Type u_1) [group G] :

commutator G = subgroup.closure {x : G | ∃ (p q : G), ((p * q) * p⁻¹) * q⁻¹ = x}

source

@[simp]

theorem derived_series_one (G : Type u_1) [group G] :

derived_series G 1 = commutator G

source

theorem map_commutator_eq_commutator_map {G : Type u_1} [group G] {G' : Type u_2} [group G'] {f : G →* G'} (H₁ H₂ : subgroup G) :

subgroup.map f ⁅H₁,H₂⁆ = ⁅subgroup.map f H₁,subgroup.map f H₂⁆

source

theorem commutator_le_map_commutator {G : Type u_1} [group G] {G' : Type u_2} [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₂⁆

source

theorem map_derived_series_le_derived_series {G : Type u_1} [group G] {G' : Type u_2} [group G'] (f : G →* G') (n : ℕ) :

subgroup.map f (derived_series G n) ≤ derived_series G' n

source

theorem derived_series_le_map_derived_series {G : Type u_1} [group G] {G' : Type u_2} [group G'] {f : G →* G'} (hf : function.surjective ⇑f) (n : ℕ) :

derived_series G' n ≤ subgroup.map f (derived_series G n)

source

theorem map_derived_series_eq {G : Type u_1} [group G] {G' : Type u_2} [group G'] {f : G →* G'} (hf : function.surjective ⇑f) (n : ℕ) :

subgroup.map f (derived_series G n) = derived_series G' n

source

@[class]

structure is_solvable (G : Type u_1) [group G] :

Prop

solvable : ∃ (n : ℕ), derived_series G n = ⊥

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

source

theorem is_solvable_def (G : Type u_1) [group G] :

is_solvable G ↔ ∃ (n : ℕ), derived_series G n = ⊥

source

@[instance]

def is_solvable_of_comm {G : Type u_1} [comm_group G] :

is_solvable G

source

theorem is_solvable_of_top_eq_bot (G : Type u_1) [group G] (h : ⊤ = ⊥) :

is_solvable G

source

@[instance]

def is_solvable_of_subsingleton (G : Type u_1) [group G] [subsingleton G] :

is_solvable G

source

theorem solvable_of_solvable_injective {G : Type u_1} [group G] {G' : Type u_2} [group G'] {f : G →* G'} (hf : function.injective ⇑f) [h : is_solvable G'] :

is_solvable G

source

@[instance]

def subgroup_solvable_of_solvable {G : Type u_1} [group G] (H : subgroup G) [h : is_solvable G] :

is_solvable ↥H

source

theorem solvable_of_surjective {G : Type u_1} [group G] {G' : Type u_2} [group G'] {f : G →* G'} (hf : function.surjective ⇑f) [h : is_solvable G] :

is_solvable G'

source

@[instance]

def solvable_quotient_of_solvable {G : Type u_1} [group G] (H : subgroup G) [H.normal] [h : is_solvable G] :

is_solvable (quotient_group.quotient H)