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 subgroupsH₁
andH₂
derived_series G n
: then
th term in the derived series ofG
, defined by iteratinggeneral_commutator
starting with the top subgroupis_solvable G
: the groupG
is solvable
@[instance]
The commutator of two subgroups H₁
and H₂
.
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}
[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₂⁆
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₂) :
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
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)
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
@[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}
[group G]
{G' : Type u_2}
[group G']
{f : G →* G'}
(hf : function.injective ⇑f)
[h : is_solvable G'] :
@[instance]
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'
@[instance]
def
solvable_quotient_of_solvable
{G : Type u_1}
[group G]
(H : subgroup G)
[H.normal]
[h : is_solvable G] :