instance CoxeterSystem.instDecidableEq_demazureOperators_1 {W : Type} : DecidableEq W

Equations

• CoxeterSystem.instDecidableEq_demazureOperators_1 = Classical.typeDecidableEq W

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

• 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

theorem CoxeterSystem.MatsumotoCondition.one_le_M {B : Type} {W : Type} : ∀ {inst : Group W} {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [self : cs.MatsumotoCondition] (i j : B), 1 ≤ M.M i j

theorem CoxeterSystem.MatsumotoCondition.alternatingWords_ne_one {B : Type} {W : Type} : ∀ {inst : Group W} {M : CoxeterMatrix B} {cs : CoxeterSystem M W} [self : cs.MatsumotoCondition] (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 : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Type

• i : B
• p : ℕ

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

• i : B
• j : B
• p : ℕ

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

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

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

Equations

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

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

Equations

• cs.apply_braidMove { 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.apply_braidMove { i := i, j := j, p := p_2.succ } [] = []
• cs.apply_braidMove { i := i, j := j, p := p_2.succ } (h :: t) = h :: cs.apply_braidMove { i := i, j := j, p := p_2 } t

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

Equations

• cs.apply_coxeterMove (CoxeterSystem.CoxeterMove.nil nm) l = cs.apply_nilMove nm l
• cs.apply_coxeterMove (CoxeterSystem.CoxeterMove.braid bm) l = cs.apply_braidMove bm l

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

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

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

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

Equations

• cs.apply_coxeterMove_sequence cms l = List.foldr cs.apply_coxeterMove l cms

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

Equations

• cs.apply_braidMoveSequence [] l = l
• cs.apply_braidMoveSequence (bm :: bms') l = cs.apply_braidMove bm (cs.apply_braidMoveSequence bms' l)

theorem CoxeterSystem.apply_braidMoveSequence_cons {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bm : cs.BraidMove) (bms : List cs.BraidMove) (l : List B) : cs.apply_braidMoveSequence (bm :: bms) l = cs.apply_braidMove bm (cs.apply_braidMoveSequence 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.shift_braidMove {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bm : cs.BraidMove) : cs.BraidMove

Equations

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

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

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

theorem CoxeterSystem.isReduced_cons {B : Type} {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 : Type} {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 : Type} {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 : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (i : B) (j : B) (p : ℕ) (hp : p < M.M i j) (hij : i ≠ j) (k : ℕ) (hk : k < p) : cs.wordProd (CoxeterSystem.alternatingWord i j (p + 1)) ≠ cs.wordProd ((CoxeterSystem.alternatingWord i j p).eraseIdx k)

theorem CoxeterSystem.prefix_braidWord_aux {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (w : W) (l : List B) (l' : List B) (i : B) (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 (CoxeterSystem.alternatingWord i j p ++ t) = w ∧ cs.IsReduced (CoxeterSystem.alternatingWord i j p ++ t)

theorem CoxeterSystem.prefix_braidWord {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (l : List B) (l' : List B) (i : B) (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 (CoxeterSystem.braidWord M i j ++ t) ∧ cs.IsReduced (CoxeterSystem.braidWord M i j ++ t)

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

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

theorem CoxeterSystem.isReduced_of_eq_length {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (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 : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (l : List B) (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 : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (p : ℕ) (l_t : List B) (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.apply_braidMoveSequence bms l = l') : ∃ (bms : List cs.BraidMove), cs.apply_braidMoveSequence bms (i :: l_t) = i :: l'_t

theorem CoxeterSystem.matsumoto_reduced_aux {B : Type} {W : Type} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [cs.MatsumotoCondition] (p : ℕ) (l : List B) (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.apply_braidMoveSequence bms l = l'

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