theorem Demazure.demaux_order_two {n : ℕ} (i : Fin n) (p : Demazure.PolyFraction n) : (Demazure.DemAux i ∘ Demazure.DemAux i) p = Demazure.zero

def Demazure.NonAdjacent {n : ℕ} (i : Fin n) (j : Fin n) : Prop

Equations

• Demazure.NonAdjacent i j = (i.castSucc ≠ j.castSucc ∧ i.castSucc ≠ j.succ ∧ i.succ ≠ j.castSucc ∧ i.succ ≠ j.succ)

theorem Demazure.Equiv.swap_mul_eq_comp {n : ℕ} {a : Fin n} {b : Fin n} {c : Fin n} {d : Fin n} {k : Fin n} : (Equiv.swap a b * Equiv.swap c d) k = (⇑(Equiv.swap a b) ∘ ⇑(Equiv.swap c d)) k

theorem Demazure.renameEquiv_swap_ext {n : ℕ} {a : Fin n} {b : Fin n} {c : Fin n} {d : Fin n} {R : Type} [CommSemiring R] : MvPolynomial.rename ⇑(Equiv.swap a b * Equiv.swap c d) = MvPolynomial.rename (⇑(Equiv.swap a b) ∘ ⇑(Equiv.swap c d))

theorem Demazure.transposition_commutes_non_adjacent {n : ℕ} (i : Fin n) (j : Fin n) (h : Demazure.NonAdjacent i j) : Equiv.swap i.castSucc i.succ * Equiv.swap j.castSucc j.succ = Equiv.swap j.castSucc j.succ * Equiv.swap i.castSucc i.succ

theorem Demazure.transposition_commutes_non_adjacent' {n : ℕ} (i : Fin n) (j : Fin n) (h : Demazure.NonAdjacent i j) : ⇑(Equiv.swap i.castSucc i.succ) ∘ ⇑(Equiv.swap j.castSucc j.succ) = ⇑(Equiv.swap j.castSucc j.succ) ∘ ⇑(Equiv.swap i.castSucc i.succ)

theorem Demazure.swap_variables_commutes_non_adjacent {n : ℕ} (i : Fin n) (j : Fin n) (h : Demazure.NonAdjacent i j) {p : MvPolynomial (Fin (n + 1)) ℂ} : Demazure.SwapVariablesFun i.castSucc i.succ (Demazure.SwapVariablesFun j.castSucc j.succ p) = Demazure.SwapVariablesFun j.castSucc j.succ (Demazure.SwapVariablesFun i.castSucc i.succ p)

theorem Demazure.demaux_commutes_non_adjacent {n : ℕ} (i : Fin n) (j : Fin n) (h : Demazure.NonAdjacent i j) (p : MvPolynomial (Fin (n + 1)) ℂ) : (Demazure.DemAux i ∘ Demazure.DemAux j) (Demazure.mk' p) = (Demazure.DemAux j ∘ Demazure.DemAux i) (Demazure.mk' p)

theorem Demazure.demaux_mul_monomial_non_adjacent {n : ℕ} (i : Fin n) (j : Fin n) (h : Demazure.NonAdjacent i j) (p : MvPolynomial (Fin (n + 1)) ℂ) : Demazure.DemAux i (Demazure.mk' (p * MvPolynomial.X j.castSucc)) = Demazure.DemAux i (Demazure.mk' p) * Demazure.mk' (MvPolynomial.X j.castSucc)

Prove some relations between Demazure operators and multiplication by monomials, in the adjacent and non-adjacent cases

theorem Demazure.demaux_mul_monomial_adjacent {n : ℕ} (i : Fin n) (h : ↑i + 1 < n) (p : MvPolynomial (Fin (n + 1)) ℂ) : Demazure.DemAux i (Demazure.mk' (p * MvPolynomial.X i.castSucc)) = Demazure.DemAux i (Demazure.mk' p) * Demazure.mk' (MvPolynomial.X i.succ) + Demazure.mk' p

theorem Demazure.symm_invariant_swap_variables {n : ℕ} {i : Fin n} {j : Fin n} {g : MvPolynomial (Fin n) ℂ} (h : g.IsSymmetric) : Demazure.SwapVariablesFun i j g = g

def Demazure.IsSymmetric {n : ℕ} (p : Demazure.PolyFraction n) : Prop

Equations

• Demazure.IsSymmetric p = ∃ (p' : Demazure.PolyFraction' n), Demazure.mk p' = p ∧ p'.numerator.IsSymmetric ∧ p'.denominator.IsSymmetric

theorem Demazure.demaux_mul_symm {n : ℕ} (i : Fin n) (g : Demazure.PolyFraction n) (f : Demazure.PolyFraction n) (h : Demazure.IsSymmetric g) : Demazure.DemAux i (g * f) = g * Demazure.DemAux i f

theorem Demazure.transposition_commutes_adjacent {n : ℕ} {i : Fin n} {j : Fin (n + 1)} (h0 : ↑i < n + 1) (h1 : ↑i + 1 < n + 1) (h2 : ↑i + 2 < n + 1) : (Equiv.swap ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩) ((Equiv.swap ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩) ((Equiv.swap ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩) j)) = (Equiv.swap ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩) ((Equiv.swap ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩) ((Equiv.swap ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩) j))

theorem Demazure.transposition_commutes_adjacent' {n : ℕ} {i : Fin n} (h0 : ↑i < n + 1) (h1 : ↑i + 1 < n + 1) (h2 : ↑i + 2 < n + 1) : ⇑(Equiv.swap ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩) ∘ ⇑(Equiv.swap ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩) ∘ ⇑(Equiv.swap ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩) = ⇑(Equiv.swap ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩) ∘ ⇑(Equiv.swap ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩) ∘ ⇑(Equiv.swap ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩)

theorem Demazure.swap_variables_commutes_adjacent {n : ℕ} {i : Fin n} {p : MvPolynomial (Fin (n + 1)) ℂ} (h0 : ↑i < n + 1) (h1 : ↑i + 1 < n + 1) (h2 : ↑i + 2 < n + 1) : Demazure.SwapVariablesFun ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩ (Demazure.SwapVariablesFun ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩ (Demazure.SwapVariablesFun ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩ p)) = Demazure.SwapVariablesFun ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩ (Demazure.SwapVariablesFun ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩ (Demazure.SwapVariablesFun ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩ p))

@[simp]

theorem Demazure.omg {i : ℕ} : i + 1 + 1 = i + 2

theorem Demazure.demaux_commutes_adjacent {n : ℕ} (i : Fin n) (h : ↑i + 1 < n) (p : MvPolynomial (Fin (n + 1)) ℂ) : (Demazure.DemAux i ∘ Demazure.DemAux ⟨↑i + 1, h⟩ ∘ Demazure.DemAux i) (Demazure.mk' p) = (Demazure.DemAux ⟨↑i + 1, h⟩ ∘ Demazure.DemAux i ∘ Demazure.DemAux ⟨↑i + 1, h⟩) (Demazure.mk' p)