# 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 #

`derivedSeries G n`

: the`n`

th term in the derived series of`G`

, defined by iterating`general_commutator`

starting with the top subgroup`IsSolvable G`

: the group`G`

is 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

- derivedSeries G 0 = ⊤
- derivedSeries G n.succ = ⁅derivedSeries G n, derivedSeries G n⁆

## Instances For

@[simp]

theorem
derivedSeries_succ
(G : Type u_1)
[Group G]
(n : ℕ)
:

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

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

Subgroup.map f (derivedSeries G n) ≤ derivedSeries G' n

theorem
derivedSeries_le_map_derivedSeries
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
{f : G →* G'}
(hf : Function.Surjective ⇑f)
(n : ℕ)
:

derivedSeries G' n ≤ Subgroup.map f (derivedSeries G n)

theorem
map_derivedSeries_eq
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
{f : G →* G'}
(hf : Function.Surjective ⇑f)
(n : ℕ)
:

Subgroup.map f (derivedSeries G n) = derivedSeries 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.

- solvable : ∃ (n : ℕ), derivedSeries G n = ⊥
A group

`G`

is solvable if its derived series is eventually trivial.

## Instances

theorem
IsSolvable.solvable
{G : Type u_1}
:

∀ {inst : Group G} [self : IsSolvable G], ∃ (n : ℕ), derivedSeries G n = ⊥

A group `G`

is solvable if its derived series is eventually trivial.

@[instance 100]

## Equations

- ⋯ = ⋯

@[instance 100]

## Equations

- ⋯ = ⋯

theorem
solvable_of_ker_le_range
{G : Type u_1}
[Group G]
{G' : Type u_3}
{G'' : Type u_4}
[Group G']
[Group G'']
(f : G' →* G)
(g : G →* G'')
(hfg : g.ker ≤ f.range)
[hG' : IsSolvable G']
[hG'' : IsSolvable 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)
[IsSolvable G']
:

instance
subgroup_solvable_of_solvable
{G : Type u_1}
[Group G]
(H : Subgroup G)
[IsSolvable G]
:

IsSolvable ↥H

## Equations

- ⋯ = ⋯

theorem
solvable_of_surjective
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
{f : G →* G'}
(hf : Function.Surjective ⇑f)
[IsSolvable G]
:

IsSolvable G'

instance
solvable_quotient_of_solvable
{G : Type u_1}
[Group G]
(H : Subgroup G)
[H.Normal]
[IsSolvable G]
:

IsSolvable (G ⧸ H)

## Equations

- ⋯ = ⋯

instance
solvable_prod
{G : Type u_1}
[Group G]
{G' : Type u_3}
[Group G']
[IsSolvable G]
[IsSolvable G']
:

IsSolvable (G × G')

## Equations

- ⋯ = ⋯

theorem
IsSimpleGroup.derivedSeries_succ
{G : Type u_1}
[Group G]
[IsSimpleGroup G]
{n : ℕ}
:

derivedSeries G n.succ = commutator G

theorem
IsSimpleGroup.comm_iff_isSolvable
{G : Type u_1}
[Group G]
[IsSimpleGroup G]
:

(∀ (a b : G), a * b = b * a) ↔ IsSolvable G

theorem
not_solvable_of_mem_derivedSeries
{G : Type u_1}
[Group G]
{g : G}
(h1 : g ≠ 1)
(h2 : ∀ (n : ℕ), g ∈ derivedSeries G n)
: