solvable groups

Stream: maths

[Joachim Breitner]

Following a suggestion from Kevin Buzzard, I might take a stab at defining solvable groups, with the goal to prove that nilpotent groups are solvable. My motivation is that proving things is fun, and that this is maybe a nice task to get to learn more about lean and mathlib, especially if I may bugger you with questions here :-)

Before I set out tomorrow: There are two definitions for solvable group (based on freshing up my memory on Wikipedia): The existence of subgroups $1 = G_0 < G_1 < ⋅⋅⋅ < G_k = G$, with the right properties, or via the derived series $G\triangleright G^{(1)}\triangleright G^{(2)} \triangleright \cdots$ reaching $1$. Which one would make the better definition?

Intuitively I’d say the second one, as then there are much less existentially bound objects to juggle around? Does that make sense?

[Yaël Dillies]

cc @Antoine Chambert-Loir

[Eric Rodriguez]

We have abel ruffini, so we definitely have some form of solvable groups

[Eric Rodriguez]

docs#is_solvable; it seems to use the derived series.

[Joachim Breitner]

Oh, so it is formalized already. Guess then my task is “just” the proof. Nevermind, should have searched myself

[Antoine Chambert-Loir]

I would have said the same. And then proving the theorems that it is stable under subgroup, quotient and extension. All of them seem to exist. Nilpotent groups exist as well, see docs#group.is_nilpotent but it remains to prove that nilpotent groups are solvable. In the context of finite groups, prove that $p$-groups are nilpotent, more generally, that a group is nilpotent iff all of its sylow subgroups are normal. Why not nilpotent/solvable subgroups of GL(n,C).

[Kevin Buzzard]

Sorry Joachim, seems we're further ahead than I realised. But still plenty to do!

[Kevin Buzzard]

I guess the 5 equivalent statements here for finite nilpotent groups https://en.wikipedia.org/wiki/Nilpotent_group#Properties would be an interesting challenge and might reveal holes in our API.

[Thomas Browning]

Frattini's argument is in mathlib, which makes some of the implications easier, iirc.

[Joachim Breitner]

nilpotent → solvable was indeed nicely low-hanging: https://github.com/leanprover-community/mathlib/pull/11512

[Kevin Buzzard]

Thanks for removing this rather gaping hole in mathlib!