## Stream: new members

### Topic: Word metric on group

#### Rémi Bottinelli (Feb 09 2022 at 07:30):

Hey!
In the code below, I'm trying to figure out how to define the word metric on a group given an indexed set of generators.
I'm stuck at showing that the word metric is always realized by a geodesic.
My problem is that the way I define the length of a group element is as a shortest word: geod_for in the code, and I can't see how to "inspect" the function's body to be able to say that "if there is some word representing this group element, then there is a geodesic one, and the length is realized" (that's the length_realized function).
I have two versions of geod_for, one of which is a composite of "first deciding emptiness of the set of words", and "then finding a geod in case it is non-empty". I thought this would help, but it doesn't seem to.
What am I doing wrong? Thanks!

import group_theory.free_group
import group_theory.quotient_group
import data.real.ennreal
import data.nat.enat

open option
open set function list
open well_founded
open classical
open_locale classical

noncomputable theory

namespace word_metric

variables {G : Type*} [group G] {ι : Type*} (letters : ι → G)

def val : (free_group ι) → G := λ w, free_group.lift letters w
def len : (free_group ι) → ℕ := λ w, (free_group.to_word w).length

def words_for (g : G) : set (free_group ι) :=
{ w : free_group ι | val letters w = g }
def geods_for  (g : G) : set (free_group ι) :=
{ w ∈  words_for letters g | ∀ u ∈ words_for letters g, (len u) ≥ (len w) }

lemma geods_have_same_length
(g : G) (w₁ w₂ : geods_for letters g) : len (w₁ : free_group ι) = len (w₂ : free_group ι) :=
let
⟨f₁,word₁,geod₁⟩ := w₁
, ⟨f₂,word₂,geod₂⟩ := w₂
in
ge_antisymm (geod₂ f₁ word₁) (geod₁ f₂ word₂)

def geod_for (g : G)  : option (geods_for letters g) :=
let
wg := words_for letters g
in
if h : wg.nonempty then
let
w := argmin_on len nat.lt_wf wg h
, w_word_for_g := argmin_on_mem len nat.lt_wf wg h
, w_shortest   := λ (w' : free_group ι) (w'_in : w' ∈ wg), argmin_on_le len nat.lt_wf wg w'_in h
in
option.some ( ⟨w,w_word_for_g,w_shortest⟩ )
else
none

def geod_for_helper (g : G)
(emp : psum (words_for letters g).nonempty ¬(words_for letters g).nonempty ) :
option (geods_for letters g) :=
let
wg := words_for letters g
in
psum.rec
( λ h,  let
w := argmin_on len nat.lt_wf wg h
, w_word_for_g := argmin_on_mem len nat.lt_wf wg h
, w_shortest   := λ (w' : free_group ι) (w'_in : w' ∈ wg), argmin_on_le len nat.lt_wf wg w'_in h
in
option.some ( ⟨w,w_word_for_g,w_shortest⟩ : geods_for letters g ))
( λ h, none)
emp

def get_emp (g : G) :
psum (words_for letters g).nonempty ¬(words_for letters g).nonempty :=
dite (words_for letters g).nonempty (λ h, psum.inl h) (λ h, psum.inr h)

def geod_for' (g : G) := geod_for_helper letters g (get_emp letters g)

def word_length  (g : G) : enat :=
option.elim (geod_for' letters g) ⊤ (λ w, len (w : free_group ι))

lemma word_length_realized (g : G) (w : free_group ι) (win : w ∈ words_for letters g):
∃ u ∈ geods_for letters g, word_length letters g = len u :=
begin
rcases get_emp letters g with (nonempty|empty),
{-- Confusion here
sorry},
{ exfalso,
-- seems overly convoluted
exact (eq_empty_iff_forall_not_mem.mp $not_nonempty_iff_eq_empty.mp empty) w win,} end lemma word_length_le_word (g : G) (w : free_group ι) (win : w ∈ words_for letters g) : word_length letters g ≤ len (w : free_group ι) := begin rcases word_length_realized letters g w win with ⟨f,⟨word,geod⟩,exact⟩, calc word_length letters g = len f : exact ... ≤ len (w : free_group ι) : enat.coe_le_coe.mpr$ ge.le \$ geod w win,
end

lemma word_length_top_iff_no_words (g : G) :
word_length letters g = ⊤ ↔ words_for letters g = ∅ :=
sorry
lemma word_length_fin_iff_words (g : G) :
word_length letters g < ⊤ ↔ words_for letters g ≠ ∅ :=
sorry

end word_metric


Last updated: Dec 20 2023 at 11:08 UTC