Division algorithm with respect to monomial orders

We provide a division algorithm with respect to monomial orders in polynomial rings. Let R be a commutative ring, σ a type of indeterminates and m : MonomialOrder σ a monomial ordering on σ →₀ ℕ.

Consider a family of polynomials b : ι → MvPolynomial σ R with invertible leading coefficients (with respect to m) : we assume hb : ∀ i, IsUnit (m.leadingCoeff (b i))).

• MonomialOrder.div hb f furnishes
  • a finitely supported family g : ι →₀ MvPolynomial σ R
  • and a “remainder” r : MvPolynomial σ R such that the three properties hold: (1) One has f = ∑ (g i) * (b i) + r (2) For every i, m.degree ((g i) * (b i) is less than or equal to that of f (3) For every i, every monomial in the support of r is strictly smaller than the leading term of b i,

The proof is done by induction, using two standard constructions

• MonomialOrder.subLTerm f deletes the leading term of a polynomial f

• MonomialOrder.reduce hb f subtracts from f the appropriate multiple of b : MvPolynomial σ R, provided IsUnit (m.leadingCoeff b).

• MonomialOrder.div_set is the variant of MonomialOrder.div for a set of polynomials.

Reference : [Becker-Weispfenning1993]

TODO

• Prove that under Field F, IsUnit (m.leadingCoeff (b i)) is equivalent to b i ≠ 0.

noncomputable def MonomialOrder.subLTerm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (f : MvPolynomial σ R) : MvPolynomial σ R

Delete the leading term in a multivariate polynomial (for some monomial order)

Equations

• m.subLTerm f = f - (MvPolynomial.monomial (m.degree f)) (m.leadingCoeff f)

theorem MonomialOrder.degree_sub_LTerm_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] (f : MvPolynomial σ R) : m.toSyn (m.degree (m.subLTerm f)) ≤ m.toSyn (m.degree f)

theorem MonomialOrder.degree_sub_LTerm_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} (hf : m.degree f ≠ 0) : m.toSyn (m.degree (m.subLTerm f)) < m.toSyn (m.degree f)

noncomputable def MonomialOrder.reduce {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {b : MvPolynomial σ R} (hb : IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R) : MvPolynomial σ R

Reduce a polynomial modulo a polynomial with unit leading term (for some monomial order)

Equations

• m.reduce hb f = f - (MvPolynomial.monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f) * b

theorem MonomialOrder.degree_reduce_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f b : MvPolynomial σ R} (hb : IsUnit (m.leadingCoeff b)) (hbf : m.degree b ≤ m.degree f) (hf : m.degree f ≠ 0) : m.toSyn (m.degree (m.reduce hb f)) < m.toSyn (m.degree f)

@[irreducible]

theorem MonomialOrder.div {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {ι : Type u_3} {b : ι → MvPolynomial σ R} (hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))) (f : MvPolynomial σ R) : ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧ (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

theorem MonomialOrder.div_set {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} (hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R) : ∃ (g : ↑B →₀ MvPolynomial σ R) (r : MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) g + r ∧ (∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c