Normal form for free group elements

Stream: mathlib4

[Arnav Sabharwal]

Hello!

I'm looking for a theorem of the form:

$$\forall \hspace{1mm} A : \text{Type}, \forall \hspace{1mm} r : \text{FreeGroup } A, \exists \hspace{1mm} a_i \in A, e_i \in \{1, -1\} \text{ such that } r = a_1^{e_1} a_2^{e_2} ... a_n^{e_n}$$

My goal is to be able to rewrite an arbitrary r : FreeGroup A in this form. What is the best way to achieve this? I'm a beginner to group theory, so maybe what I'm asking for isn't even possible as stated. I'd greatly appreciate being corrected and being led in the right direction!

Thank you!

[Filippo A. E. Nuccio]

You can start by doing

import Mathlib.GroupTheory.FreeGroup.Basic

example {α : Type*} {r : FreeGroup α} : ∃ L : List (α × Bool), r = FreeGroup.mk L := by
  rcases r with ⟨L⟩
  use L
  rfl

to produce a list of pairs (a, bool) where a : α and bool : Bool (expressing your $\pm 1$ to write your term r as a product as you wanted. Is it enough for you? It depends now if you want to work with lists and extract elements. The above code can be golfed (=shortened) a lot, but probably if you're starting with these things it is OK to keep as it is. The rcases tactic basically destructures r to its "basic components" and since a term of a free groups is, by definition, an equivalence class of lists in α x Bool, it produces the list.

[Arnav Sabharwal]

Thank you!

[Kevin Buzzard]

Another perhaps weirder answer to your question is to ask another question: why do you want such a theorem? Often mathematicians claim to want this theorem because they like seeing things in some kind of canonical form, but sometimes this is just psychological. If there's an induction principle for FreeGroup of the form "if P is a property of elements, if P(1) is true, if P(a_i) and P(a_i^{-1}) are true for all i, and if P(x) and P(y) implies P(xy), then P(g) is true for all g in the group" then you don't need the theorem which you are asking for.