Zulip Chat Archive

Stream: maths

Topic: classification of finite simple groups


view this post on Zulip Scott Morrison (Sep 22 2018 at 06:13):

I made a very preliminary start on the statement of the classification of finite simple groups.

view this post on Zulip Scott Morrison (Sep 22 2018 at 06:13):

https://github.com/leanprover-community/mathlib/blob/cfsg/group_theory/classification_of_finite_simple_groups.lean

view this post on Zulip Scott Morrison (Sep 22 2018 at 06:13):

It contains a statement, but most of the branches quickly devolve in sorry.

view this post on Zulip Scott Morrison (Sep 22 2018 at 06:14):

So far it just has the cyclic, alternating, and Mathieu groups.

view this post on Zulip Scott Morrison (Sep 22 2018 at 06:14):

Please feel very free, anyone, to push directly to the cfsg branch on lean-prover community if you feel like adding some groups. :-)

view this post on Zulip Mario Carneiro (Sep 22 2018 at 06:15):

by the way, you can use pprod in place of psigma in the place you asked about earlier

view this post on Zulip Mario Carneiro (Sep 22 2018 at 06:15):

or better yet, just use a structure :)

view this post on Zulip Mario Carneiro (Sep 22 2018 at 06:20):

I think this would make a nice target for fabstracts

view this post on Zulip Mario Carneiro (Sep 22 2018 at 06:35):

Actually, you don't even need to know nodup for your perm.of_cycles definition. Just take the product of a bunch of swaps. You only need nodup to ensure that the cycles of the result are indeed what you claimed.

view this post on Zulip Mario Carneiro (Sep 22 2018 at 06:37):

Do you (or anyone else) have any insight in the infinite families part? "Classical Lie groups" is surprisingly hard to define precisely

view this post on Zulip Scott Morrison (Sep 22 2018 at 06:46):

Yeah, there's a reason I started on the sporadics. :-)

view this post on Zulip Scott Morrison (Sep 22 2018 at 06:48):

I'm worried that there's nothing much better than defining the 4 two parameter familes of classical groups, and the 10 one parameter families of exceptional/twisted groups...

view this post on Zulip Mario Carneiro (Sep 22 2018 at 07:52):

The main theorem in Robert Wilson "The Finite Simple Groups" is proving that all these groups are in fact simple. How do you rate that for hardness? :)

view this post on Zulip Scott Morrison (Sep 22 2018 at 10:05):

I was definitely considering that far out of scope. :-)

view this post on Zulip Chris Hughes (Sep 22 2018 at 10:33):

I while ago I did start writing a list_to_cycle definition, but it was much harder than expected. Now that I've proved some other stuff about cyclic permutations it will probably be much easier. Is this something people care about?

view this post on Zulip Thales (Jan 14 2019 at 21:47):

Thanks to everyone at Lean Together, who helped me get back on track with Formal Abstracts.

This post is to get the statement of the classification of finite simple groups started in a big way. Here is a blog post of my non-expert understanding of the classification as it relates to Lean: https://formalabstracts.wordpress.com/2019/01/14/the-journey-begins/

My suggestion is to do the classification statement as a formal abstract. What that means concretely is that it should be entirely compatible with Lean3 and mathlib, but with the "cheat" of axiom proof_omitted {A : Prop} : A wherever needed, and where people stake reputation points on the correctness of props asserted by proof_omitted.

Some questions that would be helped by discussion before getting too far into it.
- Is the best path to affine varieties (over an algebraically closed field) through Kevin's general construction of schemes? It is overkill, but perhaps the simplest way forward.
- Is there agreement about the approach sketched for the groups of Lie type? In particular, about the choice of using Lie structure theory rather than concrete implementations of the groups through their faithful representations as matrix groups. My preference is for a Lie structural approach.
- What counts as an acceptable specification of a finite simple group. For instance, for the pariahs, can we say that they are specified by their order?
- What sanity checks can we produce that the definitions are correct?

view this post on Zulip Patrick Massot (Jan 15 2019 at 08:10):

@Assia Mahboubi

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 08:11):

@Scott Morrison

view this post on Zulip Patrick Massot (Jan 15 2019 at 08:17):

In my daily arXiv email this morning: https://arxiv.org/abs/1901.04223:

The proof of Theorem 1.6 is based on Theorem 1.4 (whose proof on its turn is based on [34], which uses the CFSG), and hence is very different from that in [39], which is based on the classification of compact complex surfaces.

I think CFSG stands for the title of this thread

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 08:40):

I didn't even define k-points of a scheme, for k a field (or a ring), but this will not be hard once we've refactored schemes and done them "properly" via locally ringed spaces etc (I took shortcuts in my formalisation -- what I have is provably equivalent to a scheme, but I used that Spec(A) was a locally ringed space without proving it). I'm meeting Ramon today and we will be working on this project seriously this term (both of us were busy with other things last term). The scheme route would lead to schemes called things like SLnSL_n whose kk-points for kk a finite field would be the familiar SLn(k)SL_n(k); I think you then have to leave the world of schemes and take the quotient group to make PSLn(k)PSL_n(k). I think that I had better read the statement of the classification myself actually!

view this post on Zulip Thales (Jan 16 2019 at 01:53):

We will definitely need products and morphisms to define affine algebraic groups. Have products and morphisms of schemes been defined? Or is that something we need to do?

I think it is best to define the quotient PSL(n,k) of SL(n,k) as a quotient of k-points rather than as the k-points of a quotient of varieties.

Today, I have been adding more details to the sporadic group constructions at the url posted yesterday.

view this post on Zulip Johan Commelin (Jan 16 2019 at 06:52):

As far as I know, neither morphisms nor products are defined.

view this post on Zulip Kevin Buzzard (Jan 16 2019 at 08:58):

To define these things we need to take a more mature approach to schemes, which I did not do initially (it was just a race to the definition because I was having fun and learning). I did not even define locally ringed spaces, I cheated. My student Ramon Fernandez Mir has now defined locally ringed spaces in a private repo, and things are slowly but surely proceeding. When we met yesterday I urged him to make his work public. I think that the definition of binary products of schemes would be very interesting to do in Lean, not least because I remember well skipping over the details of the 7 point process in Hartshorne as a graduate student!

As for PSL(n,k), yes, I think you have to define it as a quotient of points, the quotient scheme PSL equals PGL and PGL(n,k) is not in general simple, indeed it usually contains PSL(n,k) as an index 2 subgroup. The map from SL_n to PGL_n is surjective as fppf sheaves but not on k-points.

view this post on Zulip Thales (Jan 17 2019 at 23:03):

It makes me wonder if the algebraic geometry will become the largest part of this project.

The url above now has informal description of all sporadic groups that I think should be sufficient for this project, except that a few conjugacy classes in the monster should be better specified. (It states a few claims that are not completely backed by sources yet.)

In describing the sporadic groups, it became apparent that there are numerous constructions from the Feit-Thompson theorem that should be useful. That project presumably has libraries with topics such as semidirect products, covers, central extensions, extraspecial p-groups, quadratic forms, basic facts about orbits and stabilizers that would be useful here.


Last updated: May 14 2021 at 20:13 UTC