The Division Algorithm and Buchberger's Criterion

This file defines the multivariate division algorithm (normalForm) and proves the main theorem of Gröbner basis theory: Buchberger's Criterion.

Main Definitions

• MvPolynomial.normalForm: Computes the remainder of a polynomial f upon division by a set of polynomials B. This is often called the "normal form" of f.
• MvPolynomial.IsGroebnerBasis: Defines a Gröbner basis G for an ideal I as a basis whose leading terms generate the initial ideal of I.
• MonomialOrder.S_polynomial: The S-polynomial of two polynomials f and g.

Main Results

• MvPolynomial.normalForm_spec: Guarantees that the normalForm function satisfies the properties of the division algorithm (the division equation, the degree condition, and the remainder condition).
• MvPolynomial.normalForm_exists_unique: Shows that for a Gröbner basis, the remainder is unique.
• MvPolynomial.mem_Ideal_iff_GB_normalForm_eq_zero: A polynomial f is in an ideal I if and only if its normal form with respect to a Gröbner basis of I is zero.
• MonomialOrder.Spolynomial_syzygy_of_degree_cancellation: The crucial "Cancellation Lemma" used in the proof of Buchberger's Criterion.
• MvPolynomial.Buchberger_criterion: The main theorem. A basis G of an ideal I is a Gröbner basis if and only if the S-polynomial of every pair of elements in G reduces to zero.

theorem MonomialOrder.toSyn_degree_eq_sup_support {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : m.toSyn (m.degree f) = f.support.sup ⇑m.toSyn

theorem MonomialOrder.degree_add_lt_of_le_lt {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} {δ : m.syn} (hf : m.toSyn (m.degree f) < δ) (hg : m.toSyn (m.degree g) < δ) : m.toSyn (m.degree (f + g)) < δ

theorem MonomialOrder.degree_sum_le_syn {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (h : ι → MvPolynomial σ R) : m.toSyn (m.degree (∑ i ∈ s, h i)) ≤ s.sup fun (i : ι) => m.toSyn (m.degree (h i))

noncomputable def MvPolynomial.quotients {σ : Type u_1} {k : Type u_2} [Field k] (m : MonomialOrder σ) {B : Set (MvPolynomial σ k)} (hB : ∀ b ∈ B, b ≠ 0) (f : MvPolynomial σ k) : ↑B →₀ MvPolynomial σ k

Equations

• MvPolynomial.quotients m hB f = ⋯.choose

noncomputable def MvPolynomial.normalForm {σ : Type u_1} {k : Type u_2} [Field k] (m : MonomialOrder σ) {B : Set (MvPolynomial σ k)} (hB : ∀ b ∈ B, b ≠ 0) (f : MvPolynomial σ k) : MvPolynomial σ k

Equations

• MvPolynomial.normalForm m hB f = ⋯.choose

theorem MvPolynomial.normalForm_spec {σ : Type u_1} {k : Type u_2} [Field k] (m : MonomialOrder σ) {B : Set (MvPolynomial σ k)} (hB : ∀ b ∈ B, b ≠ 0) (f : MvPolynomial σ k) : have q := quotients m hB f; have r := normalForm m hB f; f = (Finsupp.linearCombination (MvPolynomial σ k) fun (b : ↑B) => ↑b) q + r ∧ (∀ (p : ↑B), m.toSyn (m.degree (↑p * q p)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c

This lemma states that the quotients and normalForm functions satisfy the properties guaranteed by the division algorithm.

theorem MvPolynomial.representation_of_f_of_normalForm_zero {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] {B : Set (MvPolynomial σ k)} (hB : ∀ b ∈ B, b ≠ 0) (f : MvPolynomial σ k) (h0 : normalForm m hB f = 0) : f = (Finsupp.linearCombination (MvPolynomial σ k) fun (b : ↑B) => ↑b) (quotients m hB f)

If normalForm m B hB f = 0, then in fact f = ∑ (quotients m B hB f) • b.

def MvPolynomial.GroebnerBasis_prop {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] (I : Ideal (MvPolynomial σ k)) (G : Finset (MvPolynomial σ k)) : Prop

Gröbner basis property. For an ideal I and a finite set G, this means:

• G ⊆ I, and
• ⟨ LT(G) ⟩ = ⟨ LT(I) ⟩,

where LT(G) = { LT(g) | g ∈ G } and LT(I) = { LT(f) | f ∈ I \ {0} }.

Equations

• MvPolynomial.GroebnerBasis_prop m I G = (↑G ⊆ ↑I ∧ Ideal.span ((fun (g : MvPolynomial σ k) => m.leadingTerm g) '' ↑G) = m.leadingTermIdeal I)

theorem MvPolynomial.GroebnerBasis_prop_remove_zero {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] (I : Ideal (MvPolynomial σ k)) (G : Finset (MvPolynomial σ k)) : GroebnerBasis_prop m I G ↔ GroebnerBasis_prop m I (G \ {0})

Removing 0 from G does not change the Gröbner basis property:

G satisfies G ⊆ I and ⟨ LT(G) ⟩ = ⟨ LT(I) ⟩ if and only if G \ {0} satisfies the same conditions.

def MvPolynomial.IsGroebnerBasis {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] (I : Ideal (MvPolynomial σ k)) (G : Finset (MvPolynomial σ k)) : Prop

Cox, Little, O'Shea, Ch 2, §5 Definition 5. Groebner_basis A finite subset G of an ideal I is called a Gröbner basis (or standard basis) if

1. 0 ∉ G, and
2. G ⊆ I, and
3. ⟨ LT(G) ⟩ = ⟨ LT(I) ⟩ (the ideal generated by the leading terms of the elements of G equals the leading term ideal of I).

We adopt the convention ⟨∅⟩ = {0}, so ∅ is a Gröbner basis of the zero ideal.

Equations

• MvPolynomial.IsGroebnerBasis m I G = ((∀ g ∈ G, g ≠ 0) ∧ MvPolynomial.GroebnerBasis_prop m I G)

theorem MvPolynomial.IsGroebnerBasis.initialIdeal_eq_monomialIdeal {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] {I : Ideal (MvPolynomial σ k)} {G : Finset (MvPolynomial σ k)} (hGB : IsGroebnerBasis m I G) : m.leadingTermIdeal I = monomialIdeal k ↑(Finset.image (fun (g : MvPolynomial σ k) => m.degree g) G)

theorem MvPolynomial.normalForm_exists_unique {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] {I : Ideal (MvPolynomial σ k)} {G : Finset (MvPolynomial σ k)} (hGB : IsGroebnerBasis m I G) (f : MvPolynomial σ k) : ∃! r : MvPolynomial σ k, (∃ g ∈ I, f = g + r) ∧ ∀ c ∈ r.support, ∀ gi ∈ G, ¬m.degree gi ≤ c

Proposition. If G is a Gröbner basis for I, then every f admits a unique decomposition f = g + r with

1. g ∈ I, and
2. no term of r is divisible by any LT gᵢ.

theorem MvPolynomial.mem_Ideal_iff_GB_normalForm_eq_zero {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] {I : Ideal (MvPolynomial σ k)} {G : Finset (MvPolynomial σ k)} (hGB : IsGroebnerBasis m I G) (f : MvPolynomial σ k) : f ∈ I ↔ normalForm m ⋯ f = 0

§6 Corollary 2 Let $G = \{g_1,\dots,g_t\}$ be a Gröbner basis for an ideal $I \subseteq k[x_1,\dots,x_n]$ and let $f \in k[x_1,\dots,x_n]$. Then $f \in I$ if and only if the remainder on division of $f$ by $G$ is zero.

noncomputable def MvPolynomial.S_polynomial {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] (f g : MvPolynomial σ k) : MvPolynomial σ k

The S-polynomial.

Equations

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

theorem MvPolynomial.Spolynomial_syzygy_of_degree_cancellation {σ : Type u_1} {k : Type u_2} [Field k] {ι : Type u_3} [DecidableEq ι] (m : MonomialOrder σ) (δ : σ →₀ ℕ) (p : ι →₀ MvPolynomial σ k) (hp_ne_zero : ∀ i ∈ p.support, p i ≠ 0) (hp_deg : ∀ i ∈ p.support, m.degree (p i) = δ) (hsum : m.toSyn (m.degree (∑ i ∈ p.support, p i)) < m.toSyn δ) : (∃ (c : ι × ι → k), ∑ i ∈ p.support, p i = ∑ ij ∈ p.support.offDiag, c ij • S_polynomial m (p ij.1) (p ij.2)) ∧ ∀ i ∈ p.support, ∀ j ∈ p.support, m.toSyn (m.degree (S_polynomial m (p i) (p j))) < m.toSyn δ

Lemma 5 (Cox, Little, O'Shea, Ch 2, §6, Lemma 5): Cancellation Lemma Suppose we have a sum P = ∑ pᵢ where all pᵢ have the same multidegree δ. If m.degree P < δ, then P is a linear combination of the S-polynomials S(pⱼ, pₗ), and each S(pⱼ, pₗ) has multidegree less than δ.

theorem MvPolynomial.degree_S_polynomial_lt_lcm {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] (f g : MvPolynomial σ k) (hf : f ≠ 0) (hg : g ≠ 0) (hγ : m.degree f ⊔ m.degree g > 0) : have γ := m.degree f ⊔ m.degree g; m.toSyn (m.degree (S_polynomial m f g)) < m.toSyn γ

**(Cox, Little, O'Shea, Ch 2, §6, Exercise 7)

theorem MvPolynomial.Spolynomial_of_monomial_mul_eq_monomial_mul_Spolynomial {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] (gᵢ gⱼ : MvPolynomial σ k) (hgᵢ_ne_zero : gᵢ ≠ 0) (hgⱼ_ne_zero : gⱼ ≠ 0) (aᵢ aⱼ : σ →₀ ℕ) (cᵢ cⱼ : k) (hcᵢ_ne_zero : cᵢ ≠ 0) (hcⱼ_ne_zero : cⱼ ≠ 0) (h_deg_eq : aᵢ + m.degree gᵢ = aⱼ + m.degree gⱼ) : have pᵢ := (monomial aᵢ) cᵢ * gᵢ; have pⱼ := (monomial aⱼ) cⱼ * gⱼ; S_polynomial m pᵢ pⱼ = (monomial (aᵢ + m.degree gᵢ - m.degree gᵢ ⊔ m.degree gⱼ)) 1 * S_polynomial m gᵢ gⱼ

**(Cox, Little, O'Shea, Ch 2, §6, Exercise 8)

theorem MvPolynomial.Buchberger_criterion {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] {I : Ideal (MvPolynomial σ k)} {G : Finset (MvPolynomial σ k)} (hG : ∀ g ∈ G, g ≠ 0) (hGI : I = Ideal.span ↑G) : IsGroebnerBasis m I G ↔ ∀ (g₁ g₂ : MvPolynomial σ k), g₁ ∈ G → g₂ ∈ G → g₁ ≠ g₂ → normalForm m hG (S_polynomial m g₁ g₂) = 0

(Cox, Little, O'Shea, Ch 2, §6, Theorem 6): Buchberger’s Criterion : Let I be a polynomial ideal and let G be a basis of I (i.e. I = ideal.span G). Then G is a Gröbner basis if and only if for all pairs of distinct polynomials g₁, g₂ ∈ G, the remainder on division of S_polynomial g₁ g₂ by G is zero.

theorem MvPolynomial.grobner_basis_remove_redundant {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_2} [Field k] [DecidableEq k] [DecidableEq σ] {I : Ideal (MvPolynomial σ k)} {G : Finset (MvPolynomial σ k)} {p : MvPolynomial σ k} (hG : IsGroebnerBasis m I G) (hpG : p ∈ G) (hLT : m.leadingTerm p ∈ Ideal.span ↑(Finset.image (fun (g : MvPolynomial σ k) => m.leadingTerm g) (G.erase p))) : IsGroebnerBasis m I (G.erase p)