LeanPool.DemazureOperatorsLean.Matsumoto

@[implicit_reducible]

noncomputable instance CoxeterSystem.instDecidableEqMatsumotoLeanPool {W : Type} : DecidableEq W

Equations

• CoxeterSystem.instDecidableEqMatsumotoLeanPool = Classical.typeDecidableEq W

class CoxeterSystem.MatsumotoCondition {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Prop

Extra nondegeneracy assumptions used in the Matsumoto theorem development.

• one_le_M (i j : B) : 1 ≤ M.M i j
• alternatingWords_ne_one (i j : B) : i ≠ j → ∀ (p : ℕ), 0 < p → p < M.M i j → (cs.simple i * cs.simple j) ^ p ≠ 1

structure CoxeterSystem.NilMove {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Type

A nil move removes two adjacent equal simple reflections at a given offset.

• i : B

  The simple reflection index used by the nil move.

• p : ℕ

  The offset where the nil move is applied.

structure CoxeterSystem.BraidMove {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Type

A braid move replaces a braid word by the opposite braid word at a given offset.

• i : B

  The first simple reflection index in the braid word.

• j : B

  The second simple reflection index in the braid word.

• p : ℕ

  The offset where the braid move is applied.

inductive CoxeterSystem.CoxeterMove {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Type

A Coxeter move is either a nil move or a braid move.

• nil {B W : Type} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} : cs.NilMove → cs.CoxeterMove
• braid {B W : Type} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} : cs.BraidMove → cs.CoxeterMove

def CoxeterSystem.applyNilMove {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (nm : cs.NilMove) (l : List B) : List B

Apply a nil move to a word.

Equations

• cs.applyNilMove { i := i, p := 0 } l = if List.take 2 l = [i, i] then List.drop 2 l else l
• cs.applyNilMove { i := i, p := p_2.succ } [] = []
• cs.applyNilMove { i := i, p := p_2.succ } (h :: t) = h :: cs.applyNilMove { i := i, p := p_2 } t

def CoxeterSystem.applyBraidMove {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bm : cs.BraidMove) (l : List B) : List B

Apply a braid move to a word.

Equations

• cs.applyBraidMove { i := i, j := j, p := 0 } l = if List.take (M.M i j) l = CoxeterSystem.braidWord M i j then CoxeterSystem.braidWord M j i ++ List.drop (M.M i j) l else l
• cs.applyBraidMove { i := i, j := j, p := p_2.succ } [] = []
• cs.applyBraidMove { i := i, j := j, p := p_2.succ } (h :: t) = h :: cs.applyBraidMove { i := i, j := j, p := p_2 } t

noncomputable def CoxeterSystem.applyCoxeterMove {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (cm : cs.CoxeterMove) (l : List B) : List B

Apply either kind of Coxeter move to a word.

Equations

• cs.applyCoxeterMove (CoxeterSystem.CoxeterMove.nil nm) l = cs.applyNilMove nm l
• cs.applyCoxeterMove (CoxeterSystem.CoxeterMove.braid bm) l = cs.applyBraidMove bm l

theorem CoxeterSystem.nilMove_wordProd {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (nm : cs.NilMove) (l : List B) : cs.wordProd (cs.applyNilMove nm l) = cs.wordProd l

theorem CoxeterSystem.braidMove_wordProd {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bm : cs.BraidMove) (l : List B) : cs.wordProd (cs.applyBraidMove bm l) = cs.wordProd l

theorem CoxeterSystem.coxeterMove_wordProd {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (cm : cs.CoxeterMove) (l : List B) : cs.wordProd (cs.applyCoxeterMove cm l) = cs.wordProd l

noncomputable def CoxeterSystem.applyCoxeterMoveSequence {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (cms : List cs.CoxeterMove) (l : List B) : List B

Apply a list of Coxeter moves to a word from right to left.

Equations

• cs.applyCoxeterMoveSequence cms l = List.foldr cs.applyCoxeterMove l cms

def CoxeterSystem.applyBraidMoveSequence {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bms : List cs.BraidMove) (l : List B) : List B

Apply a sequence of braid moves to a word.

Equations

• cs.applyBraidMoveSequence [] l = l
• cs.applyBraidMoveSequence (bm :: bms') l = cs.applyBraidMove bm (cs.applyBraidMoveSequence bms' l)

theorem CoxeterSystem.apply_braidMoveSequence_cons {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bm : cs.BraidMove) (bms : List cs.BraidMove) (l : List B) : cs.applyBraidMoveSequence (bm :: bms) l = cs.applyBraidMove bm (cs.applyBraidMoveSequence bms l)

theorem CoxeterSystem.cons_of_length_succ {α : Type} (l : List α) {p : ℕ} (h : l.length = p + 1) : ∃ (a : α) (t : List α), l = a :: t ∧ t.length = p

def CoxeterSystem.shiftBraidMove {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bm : cs.BraidMove) : cs.BraidMove

Shift a braid move one position to the right.

Equations

• cs.shiftBraidMove { i := i, j := j, p := p } = { i := i, j := j, p := p + 1 }

theorem CoxeterSystem.braidMove_cons {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bm : cs.BraidMove) (l : List B) (a : B) : a :: cs.applyBraidMove bm l = cs.applyBraidMove (cs.shiftBraidMove bm) (a :: l)

theorem CoxeterSystem.braidMoveSequence_cons {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bms : List cs.BraidMove) (l : List B) (a : B) : a :: cs.applyBraidMoveSequence bms l = cs.applyBraidMoveSequence (List.map cs.shiftBraidMove bms) (a :: l)

theorem CoxeterSystem.isReduced_cons {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (a : B) (l : List B) : cs.IsReduced (a :: l) → cs.IsReduced l

theorem CoxeterSystem.leftDescent_of_cons {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : cs.IsLeftDescent (cs.wordProd (i :: l)) i

theorem CoxeterSystem.leftInversion_of_cons {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : cs.IsLeftInversion (cs.wordProd (i :: l)) (cs.simple i)

theorem CoxeterSystem.alternatingWord_succ_ne_alternatingWord_eraseIdx {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (i j : B) (p : ℕ) (hp : p < M.M i j) (hij : i ≠ j) (k : ℕ) : k < p → cs.wordProd (alternatingWord i j (p + 1)) ≠ cs.wordProd ((alternatingWord i j p).eraseIdx k)

theorem CoxeterSystem.prefix_braidWord_aux {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (w : W) (l l' : List B) (i j : B) (i_ne_j : i ≠ j) (hil : cs.wordProd (i :: l) = w) (hjl' : cs.wordProd (j :: l') = w) (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) (p : ℕ) : p ≤ M.M i j → ∃ (t : List B), cs.wordProd (alternatingWord i j p ++ t) = w ∧ cs.IsReduced (alternatingWord i j p ++ t)

theorem CoxeterSystem.prefix_braidWord {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (l l' : List B) (i j : B) (i_ne_j : i ≠ j) (pi_eq : cs.wordProd (i :: l) = cs.wordProd (j :: l')) (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) : ∃ (t : List B), cs.wordProd (i :: l) = cs.wordProd (braidWord M i j ++ t) ∧ cs.IsReduced (braidWord M i j ++ t)

theorem CoxeterSystem.apply_braidMove_sequence_append {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bms bms' : List cs.BraidMove) (l : List B) : cs.applyBraidMoveSequence (bms ++ bms') l = cs.applyBraidMoveSequence bms (cs.applyBraidMoveSequence bms' l)

theorem CoxeterSystem.concatenate_braidMove_sequences {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l l' l'' : List B) (h : ∃ (bms : List cs.BraidMove), cs.applyBraidMoveSequence bms l = l') (h' : ∃ (bms' : List cs.BraidMove), cs.applyBraidMoveSequence bms' l' = l'') : ∃ (bms'' : List cs.BraidMove), cs.applyBraidMoveSequence bms'' l = l''

theorem CoxeterSystem.isReduced_of_eq_length {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l l' : List B) (h_len : l.length = l'.length) (h_eq : cs.wordProd l = cs.wordProd l') (hr : cs.IsReduced l) : cs.IsReduced l'

theorem CoxeterSystem.eq_length_of_isReduced {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l l' : List B) (h_eq : cs.wordProd l = cs.wordProd l') (hr : cs.IsReduced l) (hr' : cs.IsReduced l') : l.length = l'.length

theorem CoxeterSystem.matsumoto_reduced_inductionStep_of_firstLetterEq {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (p : ℕ) (l_t l'_t : List B) (i : B) (len_l_t_eq_p : l_t.length = p) (len_l'_t_eq_p : l'_t.length = p) (h_eq : cs.wordProd (i :: l_t) = cs.wordProd (i :: l'_t)) (l_reduced : cs.IsReduced (i :: l_t)) (l'_reduced : cs.IsReduced (i :: l'_t)) (ih : ∀ (l l' : List B), l.length = p → l'.length = p → cs.IsReduced l → cs.IsReduced l' → cs.wordProd l = cs.wordProd l' → ∃ (bms : List cs.BraidMove), cs.applyBraidMoveSequence bms l = l') : ∃ (bms : List cs.BraidMove), cs.applyBraidMoveSequence bms (i :: l_t) = i :: l'_t

theorem CoxeterSystem.matsumoto_reduced_aux {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (p : ℕ) (l l' : List B) (len_l_eq_p : l.length = p) (len_l'_eq_p : l'.length = p) (l_reduced : cs.IsReduced l) (l'_reduced : cs.IsReduced l') (h_eq : cs.wordProd l = cs.wordProd l') : ∃ (bms : List cs.BraidMove), cs.applyBraidMoveSequence bms l = l'

theorem CoxeterSystem.matsumoto_reduced {B W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (l l' : List B) (hr : cs.IsReduced l) (hr' : cs.IsReduced l') (h : cs.wordProd l = cs.wordProd l') : ∃ (bms : List cs.BraidMove), cs.applyBraidMoveSequence bms l = l'