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.

• MonomialOrder.div_single is the variant of MonomialOrder.div for a single polynomial.

Reference : [Becker-Weispfenning1993]

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

Division by a family of multivariate polynomials whose leading coefficients are invertible with respect to a monomial order

Module doc as workaround for a parser error that prevents using set_option after a decreasing_by block with focus dots.

See https://github.com/leanprover/lean4/issues/12573

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

Division by a set of multivariate polynomials whose leading coefficients are invertible with respect to a monomial order

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

Division by a multivariate polynomial whose leading coefficient is invertible with respect to a monomial order