LeanPool.DemazureOperatorsLean.Demazure

noncomputable def Demazure.SwapVariablesFun {n : ℕ} (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) : MvPolynomial (Fin n) ℂ

The polynomial obtained by swapping the variables indexed by i and j.

Equations

• Demazure.SwapVariablesFun i j p = (MvPolynomial.renameEquiv ℂ (Equiv.swap i j)) p

@[simp]

theorem Demazure.swap_variables_map_zero {n : ℕ} (i j : Fin n) : SwapVariablesFun i j 0 = 0

@[simp]

theorem Demazure.swap_variables_map_one {n : ℕ} {i j : Fin n} : SwapVariablesFun i j 1 = 1

@[simp]

theorem Demazure.swap_variables_add {n : ℕ} {i j : Fin n} (p q : MvPolynomial (Fin n) ℂ) : SwapVariablesFun i j (p + q) = SwapVariablesFun i j p + SwapVariablesFun i j q

@[simp]

theorem Demazure.swap_variables_sub {n : ℕ} {i j : Fin n} (p q : MvPolynomial (Fin n) ℂ) : SwapVariablesFun i j (p - q) = SwapVariablesFun i j p - SwapVariablesFun i j q

@[simp]

theorem Demazure.swap_variables_mul {n : ℕ} {i j : Fin n} (p q : MvPolynomial (Fin n) ℂ) : SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q

theorem Demazure.swap_variables_mul' {n : ℕ} (i j : Fin n) (p q : MvPolynomial (Fin n) ℂ) : SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q

theorem Demazure.swap_variables_mul'' {n : ℕ} {i j : Fin n} {p q : MvPolynomial (Fin n) ℂ} : SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q

theorem Demazure.swap_variables_add'' {n : ℕ} {i j : Fin n} {p q : MvPolynomial (Fin n) ℂ} : SwapVariablesFun i j (p + q) = SwapVariablesFun i j p + SwapVariablesFun i j q

@[simp]

theorem Demazure.swap_variables_commutes {n : ℕ} {i j : Fin n} (r : ℂ) : SwapVariablesFun i j (MvPolynomial.C r) = MvPolynomial.C r

@[simp]

theorem Demazure.swap_variables_order_two {n : ℕ} {i j : Fin n} {p : MvPolynomial (Fin n) ℂ} : SwapVariablesFun i j (SwapVariablesFun i j p) = p

noncomputable def Demazure.SwapVariables {n : ℕ} (i j : Fin n) : MvPolynomial (Fin n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin n) ℂ

The algebra equivalence swapping the variables indexed by i and j.

Equations

• Demazure.SwapVariables i j = MvPolynomial.renameEquiv ℂ (Equiv.swap i j)

@[simp]

theorem Demazure.swap_variables_apply {n : ℕ} (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) : (SwapVariables i j) p = SwapVariablesFun i j p

noncomputable def Demazure.circleEquation : MvPolynomial (Fin 2) ℂ

The polynomial equation of the unit circle in two variables.

Equations

• Demazure.circleEquation = MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 2 - MvPolynomial.C 1

theorem Demazure.swap_variables_ne_zero {n : ℕ} (i j : Fin (n + 1)) (p : MvPolynomial (Fin (n + 1)) ℂ) : p ≠ 0 → (SwapVariables i j) p ≠ 0

@[simp]

theorem Demazure.swap_variables_first {n : ℕ} {i j : Fin (n + 1)} : SwapVariablesFun i j (MvPolynomial.X i) = MvPolynomial.X j

theorem Demazure.swap_variables_symmetrical {n : ℕ} {i j : Fin (n + 1)} {p : MvPolynomial (Fin (n + 1)) ℂ} : SwapVariablesFun i j p = SwapVariablesFun j i p

@[simp]

theorem Demazure.swap_variables_second {n : ℕ} {i j : Fin (n + 1)} : SwapVariablesFun i j (MvPolynomial.X j) = MvPolynomial.X i

@[simp]

theorem Demazure.swap_variables_none {n : ℕ} {i j k : Fin (n + 1)} (h1 : k ≠ i) (h2 : k ≠ j) : SwapVariablesFun i j (MvPolynomial.X k) = MvPolynomial.X k

theorem Demazure.swap_variables_none' {n : ℕ} {i j k : Fin (n + 1)} {h1 : k ≠ i} {h2 : k ≠ j} : SwapVariablesFun i j (MvPolynomial.X k) = MvPolynomial.X k

theorem Demazure.fin_succ_ne_fin_castSucc {n : ℕ} (i : Fin n) : i.succ ≠ i.castSucc

theorem Demazure.wario_number_one {n a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} : ⟨a, h⟩ ≠ ⟨a', h'⟩ ↔ a ≠ a'

theorem Demazure.i_ne_i_plus_1 {n i : ℕ} {h : i < n + 1} {h' : i + 1 < n + 1} : ⟨i, h⟩ ≠ ⟨i + 1, h'⟩

theorem Demazure.demazure_denominator_not_null {n : ℕ} (i : Fin n) : MvPolynomial.X i.castSucc - MvPolynomial.X i.succ ≠ 0

noncomputable def Demazure.DemazureNumerator {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : Polynomial (MvPolynomial (Fin n) ℂ)

The numerator used to define the Demazure operator in one distinguished variable.

Equations

• Demazure.DemazureNumerator i p = (MvPolynomial.finSuccEquiv ℂ n) ((Demazure.SwapVariables i.castSucc 0) (p - (Demazure.SwapVariables i.castSucc i.succ) p))

theorem Demazure.demazure_numerator_add {n : ℕ} (i : Fin n) (p q : MvPolynomial (Fin (n + 1)) ℂ) : DemazureNumerator i (p + q) = DemazureNumerator i p + DemazureNumerator i q

theorem Demazure.demazure_numerator_C_mul {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) (r : ℂ) : DemazureNumerator i (MvPolynomial.C r * p) = Polynomial.C (MvPolynomial.C r) * DemazureNumerator i p

noncomputable def Demazure.DemazureDenominator {n : ℕ} (i : Fin n) : Polynomial (MvPolynomial (Fin n) ℂ)

The monic denominator X - X_i used in the Demazure division step.

Equations

• Demazure.DemazureDenominator i = Polynomial.X - Polynomial.C (MvPolynomial.X i)

theorem Demazure.demazure_denominator_ne_zero {n : ℕ} (i : Fin n) : DemazureDenominator i ≠ 0

theorem Demazure.demazure_denominator_monic {n : ℕ} (i : Fin n) : (DemazureDenominator i).Monic

theorem Demazure.demazure_division_exact {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : DemazureNumerator i p %ₘ DemazureDenominator i = 0

noncomputable def Demazure.DemazureFun {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : MvPolynomial (Fin (n + 1)) ℂ

The Demazure operator as a function on multivariate polynomials.

Equations

• Demazure.DemazureFun i p = (Demazure.SwapVariables i.castSucc 0) ((MvPolynomial.finSuccEquiv ℂ n).symm (Demazure.DemazureNumerator i p /ₘ Demazure.DemazureDenominator i))

theorem Demazure.poly_mul_cancel {n : ℕ} {p q r : Polynomial (MvPolynomial (Fin n) ℂ)} (hr : r ≠ 0) : p = q ↔ r * p = r * q

theorem Demazure.poly_cancel_left {n : ℕ} {p q r : MvPolynomial (Fin n) ℂ} (hr : r ≠ 0) : r * p = r * q → p = q

theorem Demazure.poly_div_cancel {n : ℕ} {p q r : Polynomial (MvPolynomial (Fin n) ℂ)} (hr : r.Monic) (hp : p %ₘ r = 0) (hq : q %ₘ r = 0) : p = q ↔ p /ₘ r = q /ₘ r

theorem Demazure.poly_exact_div_mul_cancel {n : ℕ} {p q : Polynomial (MvPolynomial (Fin n) ℂ)} (_q_monic : q.Monic) (exact_div : p %ₘ q = 0) : q * (p /ₘ q) = p

theorem Demazure.demazure_division_exact' {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : DemazureDenominator i * (DemazureNumerator i p /ₘ DemazureDenominator i) = DemazureNumerator i p

theorem Demazure.demazure_map_add {n : ℕ} (i : Fin n) (p q : MvPolynomial (Fin (n + 1)) ℂ) : DemazureFun i (p + q) = DemazureFun i p + DemazureFun i q

theorem Demazure.demazure_map_smul {n : ℕ} (i : Fin n) (r : ℂ) (p : MvPolynomial (Fin (n + 1)) ℂ) : DemazureFun i (r • p) = r • DemazureFun i p

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

The Demazure operator as a complex-linear map.

Equations

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

theorem Demazure.one_of_div_by_monic_self {n : ℕ} (p : Polynomial (MvPolynomial (Fin n) ℂ)) (_h : p.Monic) : p /ₘ p = 1

theorem Demazure.demazure_not_multiplicative {n : ℕ} (i : Fin n) : ∃ (p : MvPolynomial (Fin (n + 1)) ℂ) (q : MvPolynomial (Fin (n + 1)) ℂ), (DemazureLinear i) (p * q) ≠ (DemazureLinear i) p * (DemazureLinear i) q