Zulip Chat Archive

Stream: maths

Topic: solvable groups


Joachim Breitner (Jan 16 2022 at 20:05):

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=G0<G1<<Gk=G1 = G_0 < G_1 < ⋅⋅⋅ < G_k = G, with the right properties, or via the derived series GG(1)G(2)G\triangleright G^{(1)}\triangleright G^{(2)} \triangleright \cdots reaching 11. 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 (Jan 16 2022 at 20:09):

cc @Antoine Chambert-Loir

Eric Rodriguez (Jan 16 2022 at 22:24):

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

Eric Rodriguez (Jan 16 2022 at 22:25):

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

Joachim Breitner (Jan 16 2022 at 22:35):

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

Antoine Chambert-Loir (Jan 16 2022 at 22:36):

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 (Jan 16 2022 at 22:37):

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

Kevin Buzzard (Jan 16 2022 at 22:38):

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 (Jan 17 2022 at 02:29):

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

Joachim Breitner (Jan 17 2022 at 12:52):

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

Kevin Buzzard (Jan 17 2022 at 13:09):

Thanks for removing this rather gaping hole in mathlib!


Last updated: Dec 20 2023 at 11:08 UTC