LeanPool.DemazureOperatorsLean.DemazureAuxRelations

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

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

Two indices are non-adjacent when the adjacent transpositions they determine are disjoint.

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 b c d 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 b c 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 j : Fin n) (h : 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 j : Fin n) (h : 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 j : Fin n) (h : NonAdjacent i j) {p : MvPolynomial (Fin (n + 1)) ℂ} : SwapVariablesFun i.castSucc i.succ (SwapVariablesFun j.castSucc j.succ p) = SwapVariablesFun j.castSucc j.succ (SwapVariablesFun i.castSucc i.succ p)

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

theorem Demazure.demaux_mul_monomial_non_adjacent {n : ℕ} (i j : Fin n) (h : NonAdjacent i j) (p : MvPolynomial (Fin (n + 1)) ℂ) : DemAux i (mk' (p * MvPolynomial.X j.castSucc)) = DemAux i (mk' p) * 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)) ℂ) : DemAux i (mk' (p * MvPolynomial.X i.castSucc)) = DemAux i (mk' p) * mk' (MvPolynomial.X i.succ) + mk' p

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

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

A quotient fraction represented by symmetric numerator and denominator polynomials.

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 f : PolyFraction n) (h : IsSymmetric g) : DemAux i (g * f) = g * 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) : SwapVariablesFun ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩ (SwapVariablesFun ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩ (SwapVariablesFun ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩ p)) = SwapVariablesFun ⟨↑i + 1, h1⟩ ⟨↑i + 2, h2⟩ (SwapVariablesFun ⟨↑i, h0⟩ ⟨↑i + 1, h1⟩ (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)) ℂ) : (DemAux i ∘ DemAux ⟨↑i + 1, h⟩ ∘ DemAux i) (mk' p) = (DemAux ⟨↑i + 1, h⟩ ∘ DemAux i ∘ DemAux ⟨↑i + 1, h⟩) (mk' p)