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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

Equations

• Demazure.SwapVariables i j = { toFun := Demazure.SwapVariablesFun i j, invFun := Demazure.SwapVariablesFun i j, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def Demazure.circleEquation : MvPolynomial (Fin 2) ℂ

Equations

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Equations

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

theorem Demazure.unfold_demazure_numerator {n : ℕ} {i : Fin n} {p : MvPolynomial (Fin (n + 1)) ℂ} : Demazure.DemazureNumerator i p = MvPolynomial.eval₂ (Polynomial.C.comp MvPolynomial.C) (fun (i : Fin (n + 1)) => Fin.cases Polynomial.X (fun (k : Fin n) => Polynomial.C (MvPolynomial.X k)) i) (Demazure.SwapVariablesFun i.castSucc 0 (p - Demazure.SwapVariablesFun i.castSucc i.succ p))

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

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

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

Equations

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

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

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

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

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

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 : Polynomial (MvPolynomial (Fin n) ℂ)} {q : Polynomial (MvPolynomial (Fin n) ℂ)} {r : Polynomial (MvPolynomial (Fin n) ℂ)} (hr : r ≠ 0) : p = q ↔ r * p = r * q

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

theorem Demazure.poly_div_cancel {n : ℕ} {p : Polynomial (MvPolynomial (Fin n) ℂ)} {q : Polynomial (MvPolynomial (Fin n) ℂ)} {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 : Polynomial (MvPolynomial (Fin n) ℂ)} {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)) ℂ) : Demazure.DemazureDenominator i * (Demazure.DemazureNumerator i p /ₘ Demazure.DemazureDenominator i) = Demazure.DemazureNumerator i p

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

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

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

Equations

• Demazure.Demazure 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)) ℂ), (Demazure.Demazure i) (p * q) ≠ (Demazure.Demazure i) p * (Demazure.Demazure i) q