Buchberger's criterion

Let m be a monomial order on σ →₀ ℕ and let G be a set of multivariate polynomials whose nonzero members have unit leading coefficients, for instance any set of polynomials over a field. Buchberger's criterion says that G is a Gröbner basis of the ideal it generates if and only if 0 is a remainder of every S-polynomial m.sPolynomial g₁ g₂ with g₁, g₂ ∈ G on division by G. This turns the infinitely many conditions in the definition of a Gröbner basis into finitely many checks when G is finite, and is the key step in the correctness of Buchberger's algorithm.

Main results

• MonomialOrder.IsGroebnerBasis.isRemainder_sPolynomial_zero: the S-polynomials of a Gröbner basis have remainder 0.
• MonomialOrder.isGroebnerBasis_span_of_isRemainder_sPolynomial_zero: Buchberger's criterion, if every S-polynomial of G has remainder 0 on division by G, then G is a Gröbner basis of Ideal.span G.
• MonomialOrder.isGroebnerBasis_span_iff_isRemainder_sPolynomial_zero and MonomialOrder.isGroebnerBasis_iff_span_eq_and_isRemainder_sPolynomial_zero: the resulting characterizations of Gröbner bases.

Implementation notes

A remainder 0 of f on division by G is a standard representation f = ∑ q_b * b with every q_b * b of degree at most that of f. The proof works with the R-span of the products X^a * b, b ∈ G, whose degree a + deg b lies below a bound d. Products of degree exactly d with b ≠ 0 differ, after normalizing their leading coefficients, by monomial multiples of S-polynomials, and these have representations of degree < d by hypothesis. So a representation of degree at most d of a polynomial whose coefficient at d vanishes can be replaced by one of degree < d, and well-founded induction on d shows that every element of Ideal.span G has a standard representation. Its leading monomial is then divisible by the leading monomial of an element of G.

The theorems hold over any commutative ring, assuming only that the nonzero members of G have unit leading coefficients; over a field this is MonomialOrder.isUnit_leadingCoeff.

References

• D. Cox, J. Little, D. O'Shea, Ideals, Varieties, and Algorithms, Chapter 2, §6, Theorem 6 (Buchberger's criterion) and Lemma 5 (cancellation of leading terms by S-polynomials).

theorem MonomialOrder.IsGroebnerBasis.isRemainder_sPolynomial_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) {g₁ g₂ : MvPolynomial σ R} (hg₁ : g₁ ∈ G) (hg₂ : g₂ ∈ G) : m.IsRemainder (m.sPolynomial g₁ g₂) G 0

The S-polynomials of two members of a Gröbner basis have remainder 0 on division by that basis.

theorem MonomialOrder.isGroebnerBasis_span_of_isRemainder_sPolynomial_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) (hS : ∀ g₁ ∈ G, ∀ g₂ ∈ G, m.IsRemainder (m.sPolynomial g₁ g₂) G 0) : m.IsGroebnerBasis G (Ideal.span G)

Buchberger's criterion. If the nonzero members of G have unit leading coefficients and the S-polynomial of any two members of G has remainder 0 on division by G, then G is a Gröbner basis of the ideal it generates.

theorem MonomialOrder.isGroebnerBasis_iff_span_eq_and_isRemainder_sPolynomial_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) : m.IsGroebnerBasis G I ↔ Ideal.span G = I ∧ ∀ g₁ ∈ G, ∀ g₂ ∈ G, m.IsRemainder (m.sPolynomial g₁ g₂) G 0

Buchberger's criterion. A set G whose nonzero members have unit leading coefficients is a Gröbner basis of I if and only if it generates I and the S-polynomial of any two members of G has remainder 0 on division by G.

theorem MonomialOrder.isGroebnerBasis_span_iff_isRemainder_sPolynomial_zero {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} [CommRing R] {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, g ≠ 0 → IsUnit (m.leadingCoeff g)) : m.IsGroebnerBasis G (Ideal.span G) ↔ ∀ g₁ ∈ G, ∀ g₂ ∈ G, m.IsRemainder (m.sPolynomial g₁ g₂) G 0

Buchberger's criterion. A set G whose nonzero members have unit leading coefficients is a Gröbner basis of the ideal it generates if and only if the S-polynomial of any two members of G has remainder 0 on division by G.