Stating that a group has a specific presentation

Stream: Is there code for X?

[Stepan Nesterov]

I am trying to state a theorem that the dihedral group has the presentation <r,s | r^n=s^2=1, rsr^(-1)=s^(-1)>. One way this could be done is that I can construct a particular isomorphism, and then state a theorem that the particular elements map to the generators. This is what I have so far, but it is a bit unwieldy:

import Mathlib.GroupTheory.SpecificGroups.Dihedral
import Mathlib.GroupTheory.PresentedGroup

inductive DGen : Type
| r | s
deriving DecidableEq, Repr

open DGen

namespace DPres

/-- In the free group, the formal generators `r` and `s`. -/
def rF : FreeGroup DGen := FreeGroup.of r
def sF : FreeGroup DGen := FreeGroup.of s

/-- The relators for the dihedral presentation:
    `r^n = 1`, `s^2 = 1`, and `s r s r = 1` (equivalent to `s r s = r⁻¹`). -/
def rels (n : ℕ) : Set (FreeGroup DGen) :=
  { rF ^ n, sF ^ 2, sF * rF * sF * rF }

/-- The group presented by `⟨ r, s | r^n = 1, s^2 = 1, s r s = r⁻¹ ⟩`. -/
abbrev PresentedDihedralGroup (n : ℕ) : Type := PresentedGroup (rels n)

def DihedralPresentation (n : ℕ) : DihedralGroup n ≃* PresentedDihedralGroup n  where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry
  map_mul' := sorry

/-- Stating that the isomorphism maps r and sr to the generators--/
theorem DihedralPresentation_r_to_rF (n : ℕ) : DihedralPresentation n (DihedralGroup.r 1) = PresentedGroup.mk (rels n) rF := by
  sorry

theorem DihedralPresentation_sr_to_sF (n : ℕ) : DihedralPresentation n (DihedralGroup.sr 1) = PresentedGroup.mk (rels n) sF := by
  sorry

Is there a good way to package this information in one statement?

[Kenny Lau]

you can define the type Presentation in general (to be a (maybe ordered) subset of a free group, for example)

[Vlad Tsyrklevich]

I have a proof of this specific statement here, no promises it's the best way to write it though

[Vlad Tsyrklevich]

I think using .of r is easy enough that it makes the rF/sF vars unnecessary. Otherwise basically the same as what you have written.

[Vlad Tsyrklevich]

Regarding the original question, there is not currently a way to package it into one statement.

[Kevin Buzzard]

Isn't "the dihedral group has the presentation <r,s | r^n=s^2=1, rsr^(-1)=s^(-1)>." just this theorem

example (n : ℕ) : Nonempty (DihedralGroup n ≃* PresentedDihedralGroup n)

?

[Vlad Tsyrklevich]

I think the "packaging" is of the isomorphism as well the facts that the individual generators map onto specific elements in the target group.

[Thomas Browning]

You could state it as the kernel of the map from the free group being the closure of a specific finite set.

[Stepan Nesterov]

Kevin Buzzard said:

Isn't "the dihedral group has the presentation <r,s | r^n=s^2=1, rsr^(-1)=s^(-1)>." just this theorem

example (n : ℕ) : Nonempty (DihedralGroup n ≃* PresentedDihedralGroup n)

?

Not quite, because I would like the statement to include the fact that these r and s are specific elements of the dihedral group, not just that there exist elements which generate the group and have these relations

[Kevin Buzzard]

Then how about

example (n : ℕ) : ∃ e : DihedralGroup n ≃* PresentedDihedralGroup n,
    e (DihedralGroup.r 1) = PresentedGroup.mk (rels n) rF ∧
    e (DihedralGroup.sr 1) = PresentedGroup.mk (rels n) sF :=
  sorry

[Aaron Liu]

at this point why not just make it a definition

[Aaron Liu]

since it's uniquely determined by its action on r and sr

[Kevin Buzzard]

right -- this not particularly idiomatic, but I'm just trying to answer the question.

By the way, my mental model of what sr i means is $sr^i$ so I would have chosen DihedralGroup.sr 0

[Aaron Liu]

they're all equivalent

[Kevin Buzzard]

I guess so, but I'm talking about semantics. The stuff like r_mul_sr : r i * sr j = sr (j - i) is supposed to be interpreted as $r^isr^j=sr^{j-i}$.

[Aaron Liu]

(I would've chosen sr 0 too)