LeanPool.DemazureOperatorsLean.DemazureAux

structure Demazure.PolyFraction' (n : ℕ) : Type

A numerator-denominator representative for a rational expression in the polynomial ring.

• numerator : MvPolynomial (Fin (n + 1)) ℂ

  The numerator polynomial.

• denominator : MvPolynomial (Fin (n + 1)) ℂ

  The denominator polynomial.

• denominator_ne_zero : self.denominator ≠ 0

  The denominator is nonzero.

noncomputable def Demazure.toFrac {n : ℕ} (p : MvPolynomial (Fin (n + 1)) ℂ) : PolyFraction' n

View a polynomial as a fraction with denominator one.

Equations

• Demazure.toFrac p = { numerator := p, denominator := 1, denominator_ne_zero := ⋯ }

def Demazure.r (n : ℕ) : PolyFraction' n → PolyFraction' n → Prop

The proportionality relation on polynomial fractions.

Equations

• Demazure.r n p q = (p.numerator * q.denominator = q.numerator * p.denominator)

theorem Demazure.r_equiv {n : ℕ} : Equivalence (r n)

@[implicit_reducible]

instance Demazure.s (n : ℕ) : Setoid (PolyFraction' n)

Equations

• Demazure.s n = { r := Demazure.r n, iseqv := ⋯ }

@[implicit_reducible]

instance Demazure.hasEquiv {n : ℕ} : HasEquiv (PolyFraction' n)

Equations

• Demazure.hasEquiv = instHasEquivOfSetoid

theorem Demazure.equiv_r {n : ℕ} {a b : PolyFraction' n} : r n a b ↔ a ≈ b

def Demazure.PolyFraction (n : ℕ) : Type

The quotient type of polynomial fractions modulo proportionality.

Equations

• Demazure.PolyFraction n = Quotient (Demazure.s n)

def Demazure.mk {n : ℕ} (p : PolyFraction' n) : PolyFraction n

The quotient map from fraction representatives.

Equations

• Demazure.mk p = ⟦p⟧

noncomputable def Demazure.mk' {n : ℕ} (p : MvPolynomial (Fin (n + 1)) ℂ) : PolyFraction n

The quotient map from polynomials, viewed as fractions with denominator one.

Equations

• Demazure.mk' p = Demazure.mk { numerator := p, denominator := 1, denominator_ne_zero := ⋯ }

theorem Demazure.lift_r {n : ℕ} {a : PolyFraction' n} {f : PolyFraction' n → PolyFraction' n} {c : ∀ (a₁ a₂ : PolyFraction' n), a₁ ≈ a₂ → (mk ∘ f) a₁ = (mk ∘ f) a₂} : Quotient.lift (mk ∘ f) c (mk a) = mk (f a)

@[simp]

theorem Demazure.lift2_r {n : ℕ} {a b : PolyFraction' n} {f : PolyFraction' n → PolyFraction' n → PolyFraction n} {c : ∀ (a₁ b₁ a₂ b₂ : PolyFraction' n), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂} : Quotient.lift₂ f c (mk a) (mk b) = f a b

@[simp]

theorem Demazure.mk_eq {n : ℕ} {a b : PolyFraction' n} : mk a = mk b ↔ a.numerator * b.denominator = a.denominator * b.numerator

theorem Demazure.get_polyfraction_rep {n : ℕ} (p : PolyFraction n) : ∃ (p' : PolyFraction' n), mk p' = p

noncomputable def Demazure.add' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction' n

Addition of polynomial-fraction representatives.

Equations

• Demazure.add' p q = { numerator := p.numerator * q.denominator + q.numerator * p.denominator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

noncomputable def Demazure.addMk {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n

Addition of representatives followed by the quotient map.

Equations

• Demazure.addMk p q = Demazure.mk (Demazure.add' p q)

theorem Demazure.add'_s {n : ℕ} (a₁ b₁ a₂ b₂ : PolyFraction' n) : a₁ ≈ a₂ → b₁ ≈ b₂ → addMk a₁ b₁ = addMk a₂ b₂

noncomputable def Demazure.add {n : ℕ} : PolyFraction n → PolyFraction n → PolyFraction n

Addition on quotient polynomial fractions.

Equations

• Demazure.add p q = Quotient.lift₂ Demazure.addMk ⋯ p q

@[implicit_reducible]

noncomputable instance Demazure.addition {n : ℕ} : Add (PolyFraction n)

Equations

• Demazure.addition = { add := Demazure.add }

@[implicit_reducible]

noncomputable instance Demazure.addition' {n : ℕ} : Add (PolyFraction' n)

Equations

• Demazure.addition' = { add := Demazure.add' }

noncomputable def Demazure.sub' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n

Subtraction of polynomial-fraction representatives, followed by the quotient map.

Equations

• Demazure.sub' p q = Demazure.mk { numerator := p.numerator * q.denominator - q.numerator * p.denominator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

theorem Demazure.sub'_s {n : ℕ} (a₁ b₁ a₂ b₂ : PolyFraction' n) : a₁ ≈ a₂ → b₁ ≈ b₂ → sub' a₁ b₁ = sub' a₂ b₂

noncomputable def Demazure.sub {n : ℕ} : PolyFraction n → PolyFraction n → PolyFraction n

Subtraction on quotient polynomial fractions.

Equations

• Demazure.sub p q = Quotient.lift₂ Demazure.sub' ⋯ p q

noncomputable def Demazure.mul' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction' n

Multiplication of polynomial-fraction representatives.

Equations

• Demazure.mul' p q = { numerator := p.numerator * q.numerator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

noncomputable def Demazure.mulMk {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n

Multiplication of representatives followed by the quotient map.

Equations

• Demazure.mulMk p q = Demazure.mk (Demazure.mul' p q)

theorem Demazure.mul'_s {n : ℕ} (a₁ b₁ a₂ b₂ : PolyFraction' n) : a₁ ≈ a₂ → b₁ ≈ b₂ → mulMk a₁ b₁ = mulMk a₂ b₂

noncomputable def Demazure.mul {n : ℕ} : PolyFraction n → PolyFraction n → PolyFraction n

Multiplication on quotient polynomial fractions.

Equations

• Demazure.mul p q = Quotient.lift₂ Demazure.mulMk ⋯ p q

@[implicit_reducible]

noncomputable instance Demazure.multiplication' {n : ℕ} : Mul (PolyFraction' n)

Equations

• Demazure.multiplication' = { mul := Demazure.mul' }

@[implicit_reducible]

noncomputable instance Demazure.multiplication {n : ℕ} : Mul (PolyFraction n)

Equations

• Demazure.multiplication = { mul := Demazure.mul }

noncomputable def Demazure.one' {n : ℕ} : PolyFraction' n

The multiplicative identity as a fraction representative.

Equations

• Demazure.one' = { numerator := 1, denominator := 1, denominator_ne_zero := ⋯ }

noncomputable def Demazure.one {n : ℕ} : PolyFraction n

The multiplicative identity as a quotient fraction.

Equations

• Demazure.one = Demazure.mk Demazure.one'

noncomputable def Demazure.zero' {n : ℕ} : PolyFraction' n

The additive identity as a fraction representative.

Equations

• Demazure.zero' = { numerator := 0, denominator := 1, denominator_ne_zero := ⋯ }

noncomputable def Demazure.zero {n : ℕ} : PolyFraction n

The additive identity as a quotient fraction.

Equations

• Demazure.zero = Demazure.mk Demazure.zero'

noncomputable def Demazure.neg' {n : ℕ} (p : PolyFraction' n) : PolyFraction' n

Negation of polynomial-fraction representatives.

Equations

• Demazure.neg' p = { numerator := -p.numerator, denominator := p.denominator, denominator_ne_zero := ⋯ }

noncomputable def Demazure.negMk {n : ℕ} (p : PolyFraction' n) : PolyFraction n

Negation of representatives followed by the quotient map.

Equations

• Demazure.negMk p = Demazure.mk (Demazure.neg' p)

theorem Demazure.neg_s (n : ℕ) (a₁ a₂ : PolyFraction' n) : a₁ ≈ a₂ → negMk a₁ = negMk a₂

noncomputable def Demazure.neg {n : ℕ} (p : PolyFraction n) : PolyFraction n

Negation on quotient polynomial fractions.

Equations

• Demazure.neg p = Quotient.lift Demazure.negMk ⋯ p

theorem Demazure.add_comm {n : ℕ} (p q : PolyFraction n) : add p q = add q p

theorem Demazure.add_assoc {n : ℕ} (p q r : PolyFraction n) : add (add p q) r = add p (add q r)

noncomputable def Demazure.DemAux' {n : ℕ} (i : Fin n) : PolyFraction' n → PolyFraction' n

The auxiliary Demazure operator on fraction representatives.

Equations

• One or more equations did not get rendered due to their size.

theorem Demazure.DemAux_well_defined {n : ℕ} (i : Fin n) (p q : PolyFraction' n) : p ≈ q → (mk ∘ DemAux' i) p = (mk ∘ DemAux' i) q

noncomputable def Demazure.DemAux {n : ℕ} (i : Fin n) (p : PolyFraction n) : PolyFraction n

The auxiliary Demazure operator on quotient polynomial fractions.

Equations

• Demazure.DemAux i p = Quotient.lift (Demazure.mk ∘ Demazure.DemAux' i) ⋯ p

theorem Demazure.demazure_definitions_equivalent' {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : mk (DemAux' i (toFrac p)) = mk' (DemazureFun i p)

theorem Demazure.demazure_definitions_equivalent {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : DemAux i (mk' p) = mk' (DemazureFun i p)

theorem Demazure.eq_zero_of_mk'_zero {n : ℕ} {p : MvPolynomial (Fin (n + 1)) ℂ} : mk' p = zero ↔ p = 0

theorem Demazure.eq_of_eq_mk' {n : ℕ} {p q : MvPolynomial (Fin (n + 1)) ℂ} : mk' p = mk' q ↔ p = q

@[simp]

theorem Demazure.simp_add {n : ℕ} {p q : PolyFraction n} : p + q = add p q

theorem Demazure.mk_add {n : ℕ} {p q : PolyFraction' n} : mk p + mk q = mk (p + q)

theorem Demazure.mk'_add {n : ℕ} (p q : MvPolynomial (Fin (n + 1)) ℂ) : mk' (p + q) = mk' p + mk' q

@[simp]

theorem Demazure.simp_mul' {n : ℕ} {p q : PolyFraction' n} : p * q = { numerator := p.numerator * q.numerator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

@[simp]

theorem Demazure.simp_mul {n : ℕ} {p q : PolyFraction n} : p * q = mul p q

theorem Demazure.mk_mul {n : ℕ} {p q : PolyFraction' n} : mk p * mk q = mk (p * q)

theorem Demazure.mk'_mul {n : ℕ} {p q : MvPolynomial (Fin (n + 1)) ℂ} : mk' p * mk' q = mk' (p * q)