LeanPool.DemazureOperatorsLean.DemazureRelations

theorem Demazure.demazure_order_two {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : (DemazureLinear i) ((DemazureLinear i) p) = 0

theorem Demazure.demazure_commutes_adjacent {n : ℕ} (i : Fin n) (h : ↑i + 1 < n) (p : MvPolynomial (Fin (n + 1)) ℂ) : (⇑(DemazureLinear i) ∘ ⇑(DemazureLinear ⟨↑i + 1, h⟩) ∘ ⇑(DemazureLinear i)) p = (⇑(DemazureLinear ⟨↑i + 1, h⟩) ∘ ⇑(DemazureLinear i) ∘ ⇑(DemazureLinear ⟨↑i + 1, h⟩)) p

theorem Demazure.demazure_commutes_non_adjacent {n : ℕ} (i j : Fin n) (h : NonAdjacent i j) (p : MvPolynomial (Fin (n + 1)) ℂ) : (⇑(DemazureLinear i) ∘ ⇑(DemazureLinear j)) p = (⇑(DemazureLinear j) ∘ ⇑(DemazureLinear i)) p

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

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

theorem Demazure.demazure_mul_symm {n : ℕ} (i : Fin n) (g f : MvPolynomial (Fin (n + 1)) ℂ) (h : g.IsSymmetric) : (DemazureLinear i) (g * f) = g * (DemazureLinear i) f

noncomputable def Demazure.Dem {n : ℕ} (i : Fin n) : MvPolynomial (Fin (n + 1)) ℂ →ₗ[↥(MvPolynomial.symmetricSubalgebra (Fin (n + 1)) ℂ)] MvPolynomial (Fin (n + 1)) ℂ

The Demazure operator as a linear map over the symmetric-polynomial subalgebra.

Equations

• Demazure.Dem i = { toFun := Demazure.DemazureFun i, map_add' := ⋯, map_smul' := ⋯ }