Remainders and Gröbner bases

Let m be a monomial order on σ →₀ ℕ. This file defines remainders on division by a set of multivariate polynomials, and Gröbner bases of an ideal, and proves that remainders on division by a Gröbner basis decide ideal membership.

• MonomialOrder.IsRemainder m f B r: r is a remainder of f on division by B, i.e. f = ∑ g_b * b + r where each product g_b * b has degree at most that of f, and no monomial of r is divisible by the leading monomial of a nonzero b ∈ B. The degree condition is stated with MonomialOrder.withBotDegree, so that the zero polynomial has degree ⊥, and as the inequality deg b + deg g_b ≤ deg f; the remainder condition only concerns divisibility, not a comparison of degrees.
• MonomialOrder.IsGroebnerBasis m G I: G is a subset of the ideal I whose leading terms span the same ideal as the leading terms of all elements of I.

Main results

• MonomialOrder.exists_isRemainder: remainders exist when every nonzero divisor has a unit leading coefficient; this is MonomialOrder.div_set.
• MonomialOrder.IsGroebnerBasis.exists_degree_le_degree: the leading monomial of every nonzero element of I is divisible by the leading monomial of a nonzero element of a Gröbner basis.
• MonomialOrder.isGroebnerBasis_iff_forall_exists_degree_le_degree: the converse, for a family whose nonzero members have unit leading coefficients.
• MonomialOrder.IsGroebnerBasis.image_leadingTerm: the leading terms of such a Gröbner basis of I form a Gröbner basis of the ideal of leading terms of I.
• MonomialOrder.IsGroebnerBasis.sub_mem_iff: for remainders r₁, r₂ of f₁, f₂ on division by a Gröbner basis of I, f₁ - f₂ ∈ I if and only if r₁ = r₂. In particular remainders on division by a Gröbner basis are unique (MonomialOrder.IsGroebnerBasis.eq_of_isRemainder) and a remainder vanishes exactly on I (MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem).
• MonomialOrder.IsGroebnerBasis.isRemainder_zero_iff_mem: 0 is a remainder of f on division by a Gröbner basis of I if and only if f ∈ I, whatever the leading coefficients of the basis: every element of I has a standard representation (Adams–Loustaunau, Theorem 4.1.12).
• MonomialOrder.IsGroebnerBasis.ideal_eq_span: a Gröbner basis generates its ideal.
• MonomialOrder.isGroebnerBasis_iff_isRemainder_zero: G ⊆ I is a Gröbner basis of I if and only if every element of I has remainder 0 on division by G.

None of these results assume that the coefficients form a field: the statements needing division assume that the nonzero members of the divisor set have unit leading coefficients, which over a field is discharged by MonomialOrder.isUnit_leadingCoeff.

References

The definitions IsRemainder and IsGroebnerBasis are those of Junyu Guo and Hao Shen in Mathlib pull request 29203, upstreamed from the WuProver Gröbner basis project.

• D. Cox, J. Little, D. O'Shea, Ideals, Varieties, and Algorithms, Chapter 2, §§5–6.
• W. W. Adams, P. Loustaunau, An Introduction to Gröbner Bases, Graduate Studies in Mathematics 3, American Mathematical Society, 1994, §4.1: Gröbner bases over rings and standard representations.

def MonomialOrder.IsRemainder {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (f : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : Prop

r is a remainder of f on division by the set B for the monomial order m: there is a finitely supported family g : B →₀ MvPolynomial σ R such that

1. f = ∑ g_b * b + r;
2. for each b ∈ B, deg b + deg g_b ≤ deg f, degrees being taken in WithBot so that the zero polynomial has degree ⊥;
3. no monomial of r is divisible by the leading monomial of a nonzero b ∈ B.

def MonomialOrder.IsGroebnerBasis {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) : Prop

A subset G of an ideal I is a Gröbner basis of I for the monomial order m if the leading terms of the elements of G span the same ideal as the leading terms of all elements of I.

theorem MonomialOrder.isRemainder_iff {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {f r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} : m.IsRemainder f B r ↔ (∃ (g : ↑B →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) g + r ∧ ∀ (b : ↑B), m.toWithBotSyn (m.withBotDegree ↑b) + m.toWithBotSyn (m.withBotDegree (g b)) ≤ m.toWithBotSyn (m.withBotDegree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, b ≠ 0 → ¬m.degree b ≤ c

Unfolding lemma for MonomialOrder.IsRemainder.

theorem MonomialOrder.IsRemainder.exists_linearCombination {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {f r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : m.IsRemainder f B r) : ∃ (g : ↑B →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) g + r ∧ ∀ (b : ↑B), m.toWithBotSyn (m.withBotDegree ↑b) + m.toWithBotSyn (m.withBotDegree (g b)) ≤ m.toWithBotSyn (m.withBotDegree f)

The division representation of a remainder: f = ∑ g_b * b + r with deg b + deg g_b ≤ deg f for each b ∈ B.

theorem MonomialOrder.IsRemainder.not_degree_le {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {f r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : m.IsRemainder f B r) {c : σ →₀ ℕ} (hc : c ∈ r.support) {b : MvPolynomial σ R} (hb : b ∈ B) (hb0 : b ≠ 0) : ¬m.degree b ≤ c

No monomial of a remainder is divisible by the leading monomial of a nonzero divisor.

theorem MonomialOrder.isGroebnerBasis_iff {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} : m.IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ Ideal.span (m.leadingTerm '' ↑I) = Ideal.span (m.leadingTerm '' G)

Unfolding lemma for MonomialOrder.IsGroebnerBasis.

theorem MonomialOrder.IsGroebnerBasis.mk {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hGI : G ⊆ ↑I) (hspan : Ideal.span (m.leadingTerm '' ↑I) = Ideal.span (m.leadingTerm '' G)) : m.IsGroebnerBasis G I

A subset of I whose leading terms span the ideal of leading terms of I is a Gröbner basis of I.

theorem MonomialOrder.toWithBotSyn_withBotDegree_add_le_iff {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {f p q : MvPolynomial σ R} (hp : p ≠ 0) (hq : q ≠ 0) (hf : f ≠ 0) : m.toWithBotSyn (m.withBotDegree p) + m.toWithBotSyn (m.withBotDegree q) ≤ m.toWithBotSyn (m.withBotDegree f) ↔ m.toSyn (m.degree p) + m.toSyn (m.degree q) ≤ m.toSyn (m.degree f)

For nonzero p, q and f, the WithBot degree bound deg p + deg q ≤ deg f used in MonomialOrder.IsRemainder is the corresponding bound on MonomialOrder.degree.

@[simp]

theorem MonomialOrder.isRemainder_zero_left_iff {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} : m.IsRemainder 0 B r ↔ r = 0

The remainders of 0 are exactly 0.

theorem MonomialOrder.isRemainder_self_iff {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} : m.IsRemainder r B r ↔ ∀ c ∈ r.support, ∀ b ∈ B, b ≠ 0 → ¬m.degree b ≤ c

A polynomial is a remainder of itself on division by B exactly when none of its monomials is divisible by the leading monomial of a nonzero element of B.

theorem MonomialOrder.leadingTerm_mem_span_leadingTerm_of_isRemainder_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {f : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : m.IsRemainder f B 0) : m.leadingTerm f ∈ Ideal.span (m.leadingTerm '' B)

If 0 is a remainder of f on division by B, then the leading term of f lies in the ideal spanned by the leading terms of B.

theorem MonomialOrder.exists_degree_le_of_mem_span_leadingTerm {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {p : MvPolynomial σ R} (hp : p ∈ Ideal.span (m.leadingTerm '' G)) {c : σ →₀ ℕ} (hc : c ∈ p.support) : ∃ g ∈ G, g ≠ 0 ∧ m.degree g ≤ c

Every monomial of an element of the ideal spanned by the leading terms of G is divisible by the leading monomial of a nonzero element of G.

theorem MonomialOrder.exists_degree_le_degree_of_isRemainder_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {f : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : m.IsRemainder f B 0) (hf : f ≠ 0) : ∃ b ∈ B, b ≠ 0 ∧ m.degree b ≤ m.degree f

If 0 is a remainder of a nonzero f on division by B, then the leading monomial of f is divisible by the leading monomial of a nonzero element of B.

theorem MonomialOrder.coeff_mem_span_leadingCoeff {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {p : MvPolynomial σ R} (hp : p ∈ Ideal.span (m.leadingTerm '' G)) (D : σ →₀ ℕ) : p.coeff D ∈ Ideal.span (m.leadingCoeff '' {g : MvPolynomial σ R | g ∈ G ∧ m.degree g ≤ D})

The coefficient of X^D in an element of the ideal spanned by the leading terms of G lies in the ideal of R spanned by the leading coefficients of those g ∈ G with deg g ≤ D.

theorem MonomialOrder.IsGroebnerBasis.subset {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) : G ⊆ ↑I

A Gröbner basis of I is contained in I.

theorem MonomialOrder.IsGroebnerBasis.span_leadingTerm_image {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) : Ideal.span (m.leadingTerm '' ↑I) = Ideal.span (m.leadingTerm '' G)

The leading terms of a Gröbner basis of I span the ideal of leading terms of I.

theorem MonomialOrder.isGroebnerBasis_self {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] (I : Ideal (MvPolynomial σ R)) : m.IsGroebnerBasis (↑I) I

An ideal is a Gröbner basis of itself.

theorem MonomialOrder.IsGroebnerBasis.mono {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G G' : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (hGG' : G ⊆ G') (hG'I : G' ⊆ ↑I) : m.IsGroebnerBasis G' I

Adjoining further elements of I to a Gröbner basis of I gives a Gröbner basis of I.

@[simp]

theorem MonomialOrder.isGroebnerBasis_sdiff_singleton_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} : m.IsGroebnerBasis (G \ {0}) I ↔ m.IsGroebnerBasis G I

Removing 0 does not change whether a set is a Gröbner basis.

theorem MonomialOrder.IsGroebnerBasis.exists_degree_le_degree {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) {p : MvPolynomial σ R} (hp : p ∈ I) (hp0 : p ≠ 0) : ∃ g ∈ G, g ≠ 0 ∧ m.degree g ≤ m.degree p

The leading monomial of every nonzero element of I is divisible by the leading monomial of a nonzero element of a Gröbner basis of I.

theorem MonomialOrder.IsGroebnerBasis.not_degree_le_of_isRemainder {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {f r : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (hr : m.IsRemainder f G r) {c : σ →₀ ℕ} (hc : c ∈ r.support) {p : MvPolynomial σ R} (hp : p ∈ I) (hp0 : p ≠ 0) : ¬m.degree p ≤ c

No monomial of a remainder on division by a Gröbner basis of I is divisible by the leading monomial of a nonzero element of I.

theorem MonomialOrder.isGroebnerBasis_iff_forall_exists_degree_le_degree {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) : m.IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ ∀ p ∈ I, p ≠ 0 → ∃ g ∈ G, g ≠ 0 ∧ m.degree g ≤ m.degree p

A subset G of I whose nonzero members have unit leading coefficients is a Gröbner basis of I if and only if the leading monomial of every nonzero element of I is divisible by the leading monomial of a nonzero element of G.

theorem MonomialOrder.isUnit_leadingCoeff_of_mem_image_leadingTerm {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) (p : MvPolynomial σ R) : p ∈ m.leadingTerm '' G → p ≠ 0 → IsUnit (m.leadingCoeff p)

If the nonzero members of G have unit leading coefficients, then so do the nonzero leading terms of members of G.

theorem MonomialOrder.IsGroebnerBasis.image_leadingTerm {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommSemiring R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) : m.IsGroebnerBasis (m.leadingTerm '' G) (Ideal.span (m.leadingTerm '' ↑I))

The leading terms of a Gröbner basis G of I whose nonzero members have unit leading coefficients form a Gröbner basis of the ideal of leading terms of I.

theorem MonomialOrder.IsRemainder.sub_mem_span {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {f r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : m.IsRemainder f B r) : f - r ∈ Ideal.span B

A polynomial differs from its remainders by an element of the ideal spanned by the divisors.

theorem MonomialOrder.exists_isRemainder {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {B : Set (MvPolynomial σ R)} (hB : ∀ b ∈ B, b ≠ 0 → IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R) : ∃ (r : MvPolynomial σ R), m.IsRemainder f B r

Existence of remainders. If every nonzero element of B has a unit leading coefficient, then every polynomial has a remainder on division by B.

theorem MonomialOrder.IsGroebnerBasis.sub_mem_iff {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {f₁ f₂ r₁ r₂ : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (h₁ : m.IsRemainder f₁ G r₁) (h₂ : m.IsRemainder f₂ G r₂) : f₁ - f₂ ∈ I ↔ r₁ = r₂

Remainders modulo a Gröbner basis. If r₁ and r₂ are remainders of f₁ and f₂ on division by a Gröbner basis of I, then f₁ - f₂ ∈ I if and only if r₁ = r₂.

theorem MonomialOrder.IsGroebnerBasis.eq_of_isRemainder {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {f r₁ r₂ : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (h₁ : m.IsRemainder f G r₁) (h₂ : m.IsRemainder f G r₂) : r₁ = r₂

Uniqueness of remainders. Remainders on division by a Gröbner basis are unique.

theorem MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {f r : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (hr : m.IsRemainder f G r) : r = 0 ↔ f ∈ I

Ideal membership. A remainder on division by a Gröbner basis of I vanishes if and only if the divided polynomial lies in I.

theorem MonomialOrder.IsGroebnerBasis.monic_monomial_sub_of_isRemainder {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {r : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) {a : σ →₀ ℕ} (hr : m.IsRemainder ((MvPolynomial.monomial a) 1) G r) {p : MvPolynomial σ R} (hp : p ∈ I) (hp0 : p ≠ 0) (hpa : m.degree p = a) : (MvPolynomial.monomial a) 1 - r ∈ I ∧ (MvPolynomial.monomial a) 1 - r ≠ 0 ∧ m.degree ((MvPolynomial.monomial a) 1 - r) = a ∧ m.Monic ((MvPolynomial.monomial a) 1 - r)

If r is a remainder of X^a on division by a Gröbner basis of I, and a is the leading exponent of a nonzero element of I, then X^a - r is a nonzero monic element of I with leading exponent a.

theorem MonomialOrder.IsGroebnerBasis.isRemainder_zero_iff_mem {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {f : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) : m.IsRemainder f G 0 ↔ f ∈ I

For a Gröbner basis G of I, 0 is a remainder of f on division by G exactly when f ∈ I. No condition on the leading coefficients of G is needed.

theorem MonomialOrder.IsGroebnerBasis.ideal_eq_span {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) : I = Ideal.span G

A Gröbner basis of I generates I.

theorem MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) (f : MvPolynomial σ R) : ∃! r : MvPolynomial σ R, m.IsRemainder f G r

Remainders on division by a Gröbner basis whose nonzero members have unit leading coefficients exist and are unique.

theorem MonomialOrder.isGroebnerBasis_iff_isRemainder_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} : m.IsGroebnerBasis G I ↔ G ⊆ ↑I ∧ ∀ f ∈ I, m.IsRemainder f G 0

A subset G of I is a Gröbner basis of I if and only if every element of I has remainder 0 on division by G.