Initial Ideals and Dickson's Lemma

This file develops the theory of initial ideals for multivariate polynomials, a cornerstone for the theory of Gröbner bases.

Main Definitions

• MvPolynomial.monomialIdeal: An ideal generated by a set of monomials.
• MonomialOrder.leadingTerm: The leading term of a polynomial f (LT(f)).
• MonomialOrder.initialIdeal: The ideal generated by the leading terms of all polynomials in a given ideal I, ⟨LT(I)⟩.
• MonomialOrder.LM_set: The set of multidegrees of leading terms of polynomials in I.

Main Results

• leadingTermIdeal_is_initialIdeal: Proves that leadingTermIdeal m I is a monomial ideal, specifically monomialIdeal k (LM_set m I).
• Dickson_lemma: The abstract form of Dickson's Lemma, proven by showing that the monomial order on σ →₀ ℕ is a well-quasi-order.
• Dickson_lemma_MV: The concrete form of Dickson's Lemma stating that every monomial ideal is finitely generated.
• initialIdeal_is_FG: The main theorem of this file, which shows that every initial ideal is finitely generated. This is a crucial step in proving Hilbert's Basis Theorem for polynomial rings.

def MvPolynomial.monomialIdeal {σ : Type u_1} (R : Type u_2) [CommSemiring R] (s : Set (σ →₀ ℕ)) : Ideal (MvPolynomial σ R)

Monomial ideal

An ideal I ⊆ R[x_σ] is called a monomial ideal if it is generated by monomials: there exists a (possibly infinite) set A of exponent vectors such that I = ⟨ x^a | a ∈ A ⟩.

Equations

• MvPolynomial.monomialIdeal R s = Ideal.span ((fun (a : σ →₀ ℕ) => (MvPolynomial.monomial a) 1) '' s)

theorem MonomialOrder.degree_le_degree_mul {σ : Type u_1} {k : Type u_3} [Field k] (m : MonomialOrder σ) (p q : MvPolynomial σ k) (hq_ne_zero : q ≠ 0) : m.toSyn (m.degree p) ≤ m.toSyn (m.degree (p * q))

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

the leading coefficient of a multivariate polynomial with respect to a monomial ordering

Equations

• m.leadingTerm f = (MvPolynomial.monomial (m.degree f)) (m.leadingCoeff f)

theorem MonomialOrder.leadingTerm_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} [IsCancelMulZero R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) : m.leadingTerm (f * g) = m.leadingTerm f * m.leadingTerm g

Multiplicativity of leading terms

@[simp]

theorem MonomialOrder.degree_leadingTerm {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (f : MvPolynomial σ R) : m.degree (m.leadingTerm f) = m.degree f

The multidegree of the leading term LT(f) is equal to the degree of f.

theorem MonomialOrder.leadingTerm_eq_zero_imp_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (m : MonomialOrder σ) {f : MvPolynomial σ R} (h_lt_zero : m.leadingTerm f = 0) : f = 0

@[simp]

theorem MonomialOrder.leadingTerm_zero {σ : Type u_1} {k : Type u_3} [Field k] (m : MonomialOrder σ) : m.leadingTerm 0 = 0

@[simp]

theorem MonomialOrder.leadingTerm_ne_zero_iff {σ : Type u_1} {k : Type u_3} [Field k] (m : MonomialOrder σ) {f : MvPolynomial σ k} : m.leadingTerm f ≠ 0 ↔ f ≠ 0

theorem MonomialOrder.eq_leadingTerm_of_degree_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (m : MonomialOrder σ) {f : MvPolynomial σ R} (h_deg : m.degree f = 0) : f = m.leadingTerm f

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

The set of leading terms of nonzero polynomials in an ideal I.

Equations

• m.LT_set I = {f : MvPolynomial σ R | ∃ g ∈ I, g ≠ 0 ∧ m.leadingTerm g = f}

def MonomialOrder.LM_set {σ : Type u_1} {R : Type u_2} [CommSemiring R] (m : MonomialOrder σ) (I : Ideal (MvPolynomial σ R)) : Set (σ →₀ ℕ)

Equations

• m.LM_set I = {f : σ →₀ ℕ | ∃ g ∈ I, g ≠ 0 ∧ m.degree g = f}

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

Equations

• m.leadingTermIdeal I = Ideal.span (m.LT_set I)

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

The ideal generated by the leading monomials of the nonzero elements of I.

Equations

• m.initialIdeal I = MvPolynomial.monomialIdeal R (m.LM_set I)

theorem MonomialOrder.mem_monomialIdeal_iff_divisible {σ : Type u_1} {R : Type u_2} [CommSemiring R] {A : Set (σ →₀ ℕ)} {β : σ →₀ ℕ} [DecidableEq R] [Nontrivial R] : (MvPolynomial.monomial β) 1 ∈ MvPolynomial.monomialIdeal R A ↔ ∃ α ∈ A, α ≤ β

Lemma 2. Let I = ⟨x^α | α ∈ A⟩ be a monomial ideal. Then a monomial x^β lies in I if and only if x^β is divisible by some x^α for α in A, i.e. there exists α ∈ A such that α ≤ β.

theorem MonomialOrder.leading_monomial_set_eq_image_LM_set {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {I : Ideal (MvPolynomial σ R)} : {f : MvPolynomial σ R | ∃ g ∈ I, g ≠ 0 ∧ (MvPolynomial.monomial (m.degree g)) 1 = f} = (fun (s : σ →₀ ℕ) => (MvPolynomial.monomial s) 1) '' m.LM_set I

theorem MonomialOrder.Dickson_lemma {σ : Type u_4} [Fintype σ] : HasDicksonProperty (σ →₀ ℕ)

Theorem (Dickson’s Lemma for exponent vectors).

Assume σ is finite. Then (σ →₀ ℕ) with the componentwise order has the Dickson property: for every subset S ⊆ (σ →₀ ℕ) there exists a finite subset B ⊆ S such that for every a ∈ S there exists b ∈ B with b ≤ a.

theorem MonomialOrder.Dickson_lemma_MV {σ : Type u_1} (R : Type u_2) [CommSemiring R] [Fintype σ] [DecidableEq σ] [DecidableEq R] (S : Set (σ →₀ ℕ)) : (MvPolynomial.monomialIdeal R S).FG

Theorem 5 (Dickson’s Lemma). Let I = ⟨ x^α | α ∈ A ⟩ ⊆ k[x₁, …, xₙ] be a monomial ideal. Then there exists a finite subset s ⊆ A such that I = ⟨ x^α | α ∈ s ⟩. In other words, every monomial ideal has a finite basis.

theorem MonomialOrder.leadingTermIdeal_is_initialIdeal {σ : Type u_1} {k : Type u_3} [Field k] {m : MonomialOrder σ} (I : Ideal (MvPolynomial σ k)) : m.leadingTermIdeal I = m.initialIdeal I

Proposition 3 (i) (Cox, Little, O'Shea, Ch 2, §5, Proposition 3) ⟨LT(I)⟩ is a monomial ideal.

theorem MonomialOrder.initialIdeal_is_FG {σ : Type u_1} {k : Type u_3} [Field k] {m : MonomialOrder σ} [Fintype σ] [DecidableEq σ] [DecidableEq k] (I : Ideal (MvPolynomial σ k)) : (m.initialIdeal I).FG

Proposition 3 (ii) (Cox, Little, O'Shea, Ch 2, §5, Proposition 3). Initial Ideal is finitely generated.