Zulip Chat Archive

Stream: new members

Topic: Dihedral Groups


Alex Griffin (Oct 04 2020 at 19:00):

I am trying to make a definition of a dihedral group as a simple example of a definition of a mathematical object in Lean. However, as there are multiple ways of defining a dihedral groups in everyday usage (i.e. as a presented group, as a semidirect product of a cyclic group with the group of order 2, etc.) I am wondering if there is some sort of preferred way of defining such an object in Lean. Also, while by this point I am somewhat familiar with how one goes about proving statements in Lean (I have gone through the Natural Number Game) I am still somewhat new to defining new classes in Lean, so after I figure out what direction to go in for how they should be defined, I might need some help with putting it together.

Patrick Massot (Oct 04 2020 at 19:02):

There is an abandoned PR that tried to do that, see #1076

Alex Griffin (Oct 04 2020 at 19:03):

Thank you for the lead.

Patrick Massot (Oct 04 2020 at 19:03):

If you are interested in this topic it would be great to try to rescue this PR.

Patrick Massot (Oct 04 2020 at 19:04):

It seems there was no real obstacle, the author simply got bored and left.

Kevin Buzzard (Oct 04 2020 at 22:15):

The question about which definition to use is really a question about which definition is the easiest to make the API for, and also what you want the scope of the definition to cover. Do you want to allow the infinite dihedral group, for example?

Kevin Buzzard (Oct 04 2020 at 22:15):

If you are just interested in trying this as a one off project then I would just choose any definition which you can formalise, and then play with that.

Kevin Buzzard (Oct 04 2020 at 22:16):

As an example challenge you could figure out the centres of these groups

Johan Commelin (Oct 05 2020 at 05:35):

I imagine that we'll need characteristic properties again. (Will the Galois group of some degree 10 extension be an actual dihedral group? Probably not...)

Kevin Buzzard (Oct 05 2020 at 06:23):

Yes there's this perennial problem with examples because mathematicians often say "...hence G is dihedral" but what they don't mean by this is that G is literally equal to the definition of a dihedral group"

Kevin Buzzard (Oct 05 2020 at 06:24):

So as long as the API is there it doesn't really matter what the definition is.


Last updated: Dec 20 2023 at 11:08 UTC