word length in a free group

Stream: Is there code for X?

[Julian Berman]

I see a few discussions which are possibly relevant but no conclusion -- just to be sure I'm not missing it, can I do induction on the length of a word in a free group? Not quite yet right, we don't have word length?

[Floris van Doorn]

It seems like we have docs#free_group.to_word, and you can then do structural induction on the list, or even induction on the length of the list.

[Julian Berman]

I was trying the latter, let me try again maybe I made some simple mistake.

[Reid Barton]

Note that some arguments "by induction on the length of a word" might really just be arguments by induction on the construction of an element

[Reid Barton]

which makes sense even when reduced words do not (if you don't have decidable equality on the generators)

[Julian Berman]

So I'm sure there's some math I don't know as well, I'm not sure I even understand your suggestion sorry :/, but I see things complain at me about decidability already -- I'm here:

import group_theory.is_free_group

variables {G : Type*} [group G] [is_free_group G]

/-- A cyclically reduced word is a word where every cyclic conjugate is reduced. -/
def is_cyclically_red (w : G) := ∀ u v : G, w = u * v * u⁻¹ → w = v

/-- Inverses of cyclically reduced words are cyclically reduced. -/
lemma is_cyclically_red.inv {w : G} (h : is_cyclically_red w) : is_cyclically_red w⁻¹ :=
λ u v huv, inv_eq_iff_inv_eq.mp $ (h u v⁻¹ $ inv_inv w ▸ conj_inv.rec (inv_inj.symm.mp huv)).symm

/-- A word is cyclically reduced iff its inverse is cyclically reduced. -/
@[simp] lemma is_cyclically_red_inv_iff {w : G} : is_cyclically_red w⁻¹ ↔ is_cyclically_red w :=
⟨λ h, inv_inv w ▸ h.inv, is_cyclically_red.inv⟩

/-- The (unique) cyclic reduction of a word. -/
def cyclic_red (w : G) [decidable_eq (is_free_group.generators G)] : ∃ (r : G × G), w = r.1 * r.2 * r.1⁻¹ ∧ is_cyclically_red r.2 := begin
  simp only [prod.exists],
  set n := list.length (free_group.to_word ((is_free_group.to_free_group G) w)),
end

and I wanted to induct on how long w is -- hopefully I'm not already off track. A hint would definitely be appreciated.

[Reid Barton]

I take it cyclic_red is meant to be a lemma?

[Julian Berman]

Er, indeed