def Symm (n : ℕ) : CoxeterSystem (CoxeterSystem.M n) (CoxeterSystem.S (n + 1))

Equations

• Symm n = CoxeterSystem.S_cox n

instance instMatsumotoConditionFinSHAddNatOfNatSymm {n : ℕ} : (Symm n).MatsumotoCondition

Equations

• instMatsumotoConditionFinSHAddNatOfNatSymm = CoxeterSystem.instOfMatsumotoReady n

theorem one_le_M {n : ℕ} (i : Fin n) (j : Fin n) : 1 ≤ (CoxeterSystem.M n).M i j

theorem braidWord_ne_nil {n : ℕ} (i : Fin n) (j : Fin n) : CoxeterSystem.braidWord (CoxeterSystem.M n) i j ≠ []

def DemazureOfWord {n : ℕ} (l : List (Fin n)) : MvPolynomial (Fin (n + 1)) ℂ →ₗ[ℂ] MvPolynomial (Fin (n + 1)) ℂ

Equations

• DemazureOfWord [] = LinearMap.id
• DemazureOfWord (i :: l_2) = Demazure.Demazure i ∘ₗ DemazureOfWord l_2

theorem demazureOfWord_append {n : ℕ} (l : List (Fin n)) (l' : List (Fin n)) : DemazureOfWord (l ++ l') = DemazureOfWord l ∘ₗ DemazureOfWord l'

theorem demazure_of_braidMove {n : ℕ} (l : List (Fin n)) (bm : (Symm n).BraidMove) : DemazureOfWord l = DemazureOfWord ((Symm n).apply_braidMove bm l)

theorem demazure_of_braidMoveSequence {n : ℕ} (l : List (Fin n)) (bms : List (Symm n).BraidMove) : DemazureOfWord l = DemazureOfWord ((Symm n).apply_braidMoveSequence bms l)

theorem DemazureOfWord_eq_equivalentWord {n : ℕ} (l : List (Fin n)) (l' : List (Fin n)) (h_eq : (Symm n).wordProd l = (Symm n).wordProd l') (hr : (Symm n).IsReduced l) (hr' : (Symm n).IsReduced l') : DemazureOfWord l = DemazureOfWord l'

def DemazureOfProd {n : ℕ} (w : CoxeterSystem.S (n + 1)) : MvPolynomial (Fin (n + 1)) ℂ →ₗ[ℂ] MvPolynomial (Fin (n + 1)) ℂ

Equations

• DemazureOfProd w = DemazureOfWord (Classical.choose ⋯)