Working with group presentations

Stream: mathlib4

[Vlad Tsyrklevich]

As an exercise to get familiar with working with presented groups/free groups in Lean I defined the isomorphism between the dihedral group(s) and their group presentation. PresentedGroups are defined using two quotients (one in the definition of PresentedGroup, and one inherited from FreeGroup), and this can lead to some senseless duplication, for example in my definition I mostly use a/b to reference the two generators in the presented group, fa/fb for the free group representation, and in myOp I need to define a function on the letters of the FreeGroup. Example snippets pulled from the code:

import Mathlib
open DihedralGroup

abbrev freeGroup := FreeGroup (Unit ⊕ Unit)
abbrev fa : freeGroup := .of (.inl ())
abbrev fb : freeGroup := .of (.inr ())

abbrev rels (n : ℕ) : Set freeGroup := { fa^2, fb^2, (fa * fb)^n }
abbrev dihedralPresentation (n : ℕ) := PresentedGroup (rels n)

abbrev a {n : ℕ} : dihedralPresentation n := .of (.inl ())
abbrev b {n : ℕ} : dihedralPresentation n := .of (.inr ())

abbrev myOp {n : ℕ} : Unit ⊕ Unit → DihedralGroup n
  | .inl () => sr 1
  | .inr () => sr 1 * r 1

This seems pretty unnecessary since in all 3 cases I am referring to the same generator. Is there an obvious pattern that I'm missing, or should there perhaps be coercions here? Going from α → (FreeGroup α) and α → (@PresentedGroup α β) is easy to implement but I could see it being error prone if you're working with multiple presentations with the same number/types of generators.

[Patrick Massot]

I think your choice of Unit ⊕ Unit is making it a lot worse than it could be. Why not

inductive gens
| A | B

open gens

and then use A instead of .inl ()?

[Patrick Massot]

Then you can’t really avoid the fact there are three types here, the generating type, the free group and your group. Note there is also docs#PresentedGroup.mk which is a group morphism from the free group to the presented group. So you could have abbrev a {n : ℕ} : dihedralPresentation n := .mk (rels n) fa (and rels n can probably be implicit here since the expected type is known).

[Vlad Tsyrklevich]

Thanks Patrick, the use of the inductive is definitely better than the Sum. It also makes the rest of the conversions less painful to use since sprinkling .of a is also not as ugly as what I had before.