## Stream: maths

### Topic: database of groups

#### 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?

#### 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.

#### 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 ($C_n$, $\mathbb{Z}/n\mathbb{Z}$, $\mathbb{F}_p$ when $n = p$ is prime) but I don't know whether that is a good idea in Lean

#### Johan Commelin (Nov 23 2018 at 14:57):

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

#### 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

#### 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".

#### 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.

#### Scott Morrison (Nov 23 2018 at 23:07):

Unfortunately, even constructing the sporadics is a big project.

#### 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

#### 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

#### 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).

#### 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.

#### 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 :-)

#### Johan Commelin (Nov 24 2018 at 08:32):

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

#### 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.

#### Mario Carneiro (Nov 24 2018 at 08:39):

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

#### Mario Carneiro (Nov 24 2018 at 08:39):

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

#### Kevin Buzzard (Nov 24 2018 at 08:51):

and some are impossible to solve!

Last updated: May 11 2021 at 16:22 UTC