Zulip Chat Archive

Stream: maths

Topic: database of groups


view this post on Zulip Kevin Buzzard (Nov 23 2018 at 09:47):

Looking at the second year group theory problem sheets, there seem to be just as many "prove this is false" questions as "prove this is true" ones. I want to deduce from this that mathematicians are interested in not only theorems about groups, but examples of groups (e.g. as a source of counterexamples). @Amelia Livingston would in particular be interested in these, and we've tentatively begun discussions on what should go in there -- cyclic groups, dihedral groups, C_2 x C_2, symmetric and alternating groups.

Got to go and give a lecture, but briefly: (1) does it matter what the underlying type is for these groups (2) does anyone know about whether the standard databases I've used in the past in GAP and magma have been formally verified?

view this post on Zulip Reid Barton (Nov 23 2018 at 14:21):

Semidirect products would let you construct a bunch of small groups and many other things of interest.

view this post on Zulip Reid Barton (Nov 23 2018 at 14:22):

Do we not already have some of these things in some form?
I guess mathematicians are in the habit of giving different names to the same thing in different settings (CnC_n, Z/nZ\mathbb{Z}/n\mathbb{Z}, Fp\mathbb{F}_p when n=pn = p is prime) but I don't know whether that is a good idea in Lean

view this post on Zulip Johan Commelin (Nov 23 2018 at 14:57):

Well, we will want Fq\mathbb{F}_q at some point... so then we will also get a Fp\mathbb{F}_p...

view this post on Zulip Reid Barton (Nov 23 2018 at 15:35):

I guess I'm not sure exactly what a "database of groups" would look like in Lean... maybe that's part of the question

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 16:28):

What I need them for is to be able to answer questions such as "true or false: if G is abelian then G is cyclic".

view this post on Zulip Scott Morrison (Nov 23 2018 at 23:07):

@Kevin Buzzard, you might look at the abortive start I made on the (statement of the) classification of finite simple groups.

view this post on Zulip Scott Morrison (Nov 23 2018 at 23:07):

Unfortunately, even constructing the sporadics is a big project.

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 07:51):

I think our questions are much more mundane. For example how should one define the dihedral groups? As a presentation? A subgroup of a permutation group? An explicit list of elements with a given multiplication? etc

view this post on Zulip Scott Morrison (Nov 24 2018 at 08:09):

Oh, I forgot to put a link, sorry. https://github.com/leanprover/mathlib/compare/master...leanprover-community:cfsg

view this post on Zulip Scott Morrison (Nov 24 2018 at 08:11):

I was defining things as terms of Grp, a bundled group. This gives you some freedom to chose different ways to define different groups. You can see some examples in that diff. For example, I did the Mathieu 12 and 24 via generators in a permutation group, M23 and M22 as stabilisers, but the alternating group as a subtype of perm (fin n).

view this post on Zulip Johan Commelin (Nov 24 2018 at 08:13):

It would be nice to have gap_db(n,m) constructor that would give you a representative of the group with n elements that is listed as mth iso-class in the GAP database.

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 08:14):

ha ha, you could write an interface to gap which pulls off the group from the GAP database, lists all the elements, makes a new inductive type with a constructor for each object, and then just puts together the multiplication table manually and proves it's a group with dec_trivial :-)

view this post on Zulip Johan Commelin (Nov 24 2018 at 08:32):

@Kevin Buzzard I think there might be quite some potential in such an interface...

view this post on Zulip Johan Commelin (Nov 24 2018 at 08:33):

I don't know if it should be an inductive type or whatever, I guess GAP can also give you generators and relations etc... Anyway, this is just wishful thinking from my side atm.

view this post on Zulip Mario Carneiro (Nov 24 2018 at 08:39):

we could certainly have a way to define groups by their generators and relations

view this post on Zulip Mario Carneiro (Nov 24 2018 at 08:39):

of course lots of questions about finitely presented groups are very hard to solve

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 08:51):

and some are impossible to solve!


Last updated: May 11 2021 at 16:22 UTC