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: thenth term in the derived series ofG, defined by iteratinggeneral_commutatorstarting with the top subgroupis_solvable G: the groupGis solvable
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 = ⊤
@[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⁆
@[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
map_commutator_eq_commutator_map
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
{f : G →* G'}
(H₁ H₂ : subgroup G) :
subgroup.map f ⁅H₁,H₂⁆ = ⁅subgroup.map f H₁,subgroup.map f 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₁ ≤ subgroup.map f H₁)
(h₂ : K₂ ≤ subgroup.map f H₂) :
theorem
map_derived_series_le_derived_series
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(f : G →* G')
(n : ℕ) :
subgroup.map f (derived_series G n) ≤ derived_series 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 : ℕ) :
derived_series G' n ≤ subgroup.map f (derived_series G 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 : ℕ) :
subgroup.map f (derived_series G n) = derived_series G' n
@[class]
- 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.
theorem
is_solvable_def
(G : Type u_1)
[group G] :
is_solvable G ↔ ∃ (n : ℕ), derived_series G n = ⊥
@[instance]
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]
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] :
is_solvable G'
@[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''] :
@[instance]
def
solvable_prod
{G : Type u_1}
[group G]
{G' : Type u_2}
[group G']
[h : is_solvable G]
[h' : is_solvable G'] :
is_solvable (G × G')
theorem
is_simple_group.derived_series_succ
{G : Type u_1}
[group G]
[is_simple_group G]
{n : ℕ} :
derived_series G n.succ = commutator 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) :