Dihedral Groups

Stream: new members

[Alex Griffin]

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]

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

[Alex Griffin]

Thank you for the lead.

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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]

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]

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