Solvable Group

Statement

The derived series of a group $G$ is defined by $G^{(0)} = G$ and $G^{(k+1)} = [G^{(k)}, G^{(k)}]$, the subgroup generated by all commutators $[a,b] = aba^{-1}b^{-1}$ in $G^{(k)}$.

$G$ is solvable if $G^{(n)} = \{e\}$ for some $n \geq 0$.

Equivalently, $G$ has a subnormal series $G = G_0 \supset G_1 \supset \cdots \supset G_n = \{e\}$ where each quotient $G_i/G_{i+1}$ is abelian.

Visualization

Derived series of $S_3$:

S_3  (order 6)
 |   [S_3, S_3] = A_3 = {e, (123), (132)}
A_3  (order 3, cyclic, hence abelian)
 |   [A_3, A_3] = {e}
{e}

Step-by-step:

• $S_3^{(0)} = S_3$ has 6 elements: $e, (12), (13), (23), (123), (132)$.
• $S_3^{(1)} = [S_3, S_3] = A_3 = \{e,(123),(132)\}$. Check: $(12)(13)(12)^{-1}(13)^{-1} = (123)$.
• $S_3^{(2)} = [A_3, A_3]$. Since $A_3 \cong \mathbb{Z}/3$ is abelian, all commutators are trivial.

So $S_3^{(2)} = \{e\}$ and $S_3$ is solvable with derived length 2.

Why $S_5$ is not solvable:

$[S_5, S_5] = A_5$ and $[A_5, A_5] = A_5$ (since $A_5$ is simple and nonabelian). The derived series stabilizes at $A_5 \neq \{e\}$, so $S_5$ is not solvable. This is the group-theoretic core of the Impossibility of the Quintic FormulaImpossibility of the Quintic Formula$$S_5 \text{ is not solvable} \implies \text{no radical formula for degree } \geq 5$$No general algebraic formula exists for polynomials of degree 5 or higherRead more →.

Proof Sketch

1. Every abelian group is solvable (derived series hits $\{e\}$ in one step).
2. Subgroups and quotients of solvable groups are solvable (the derived series restricts / projects).
3. Extensions of solvable groups are solvable: if $N \trianglelefteq G$ and both $N$ and $G/N$ are solvable, then so is $G$.
4. $S_n$ is solvable for $n \leq 4$: the chain $S_n \supset A_n \supset V_4 \supset \mathbb{Z}/2 \supset \{e\}$ (for $n = 4$) has abelian quotients. For $n \geq 5$, $A_n$ is simple and nonabelian, blocking the process.

Connections

Solvability of a Galois group precisely characterizes polynomial equations solvable by radicals — the content of the Fundamental Theorem of Galois TheoryFundamental Theorem of Galois Theory$$\{\text{intermediate fields}\} \longleftrightarrow \{\text{subgroups of } \text{Gal}(K/F)\}$$Bijection between intermediate fields and subgroups of the Galois groupRead more →. The structure of solvable groups is coarser than nilpotent ones: every nilpotent group is solvable, but $S_3$ is solvable yet not nilpotent (see Nilpotent GroupNilpotent Group$$G = \gamma_0 \supset \gamma_1 \supset \cdots \supset \gamma_n = \{e\}$$A group is nilpotent if its lower central series reaches the trivial subgroup in finitely many steps.Read more →).

/-- Every abelian group is solvable: its derived series reaches {e} in one step
    because [G,G] = {e} when G is abelian. Mathlib provides this as an instance. -/
theorem abelian_is_solvable (G : Type*) [CommGroup G] : IsSolvable G :=
  CommGroup.isSolvable

/-- Solvability is preserved by surjective homomorphisms: if G is solvable and
    f : G → H is surjective, then H is solvable (the derived series of G maps onto
    the derived series of H). -/
theorem solvable_image {G H : Type*} [Group G] [Group H] (f : G →* H)
    (hf : Function.Surjective f) [IsSolvable G] : IsSolvable H :=
  solvable_of_surjective hf

/-- Abelian groups form a solvable class: both ℤ/2 and ℤ/3 are solvable.
    This captures the two layers of S_3's derived series. -/
example : IsSolvable (Multiplicative (ZMod 2)) := CommGroup.isSolvable
example : IsSolvable (Multiplicative (ZMod 3)) := CommGroup.isSolvable