Standard monomials of an ideal

For an ideal I of MvPolynomial σ K and a monomial order m, the standard exponents are those not divisible by the leading exponent of any nonzero element of I. A nonzero polynomial supported on standard exponents never lies in I, and division by all nonzero elements of I produces such a representative. For the degree lexicographic order the representative has total degree at most that of the original polynomial.

Main definitions

• Ideal.standardExponents I m: the exponents not divisible by m.degree f for any nonzero f ∈ I.
• Ideal.boundedStandardExponents I m N: the standard exponents of total degree at most N.

Main results

• Ideal.eq_zero_of_mem_restrictSupport_standardExponents: a polynomial in I supported on standard exponents is zero.
• Ideal.exists_standard_representative_degLex: every polynomial is congruent modulo I to a polynomial supported on standard exponents for degLex, of no larger total degree.

def Ideal.standardExponents {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (m : MonomialOrder σ) : Set (σ →₀ ℕ)

Exponents not divisible by any leading exponent of a nonzero ideal element.

Equations

• I.standardExponents m = {a : σ →₀ ℕ | ∀ f ∈ I, f ≠ 0 → ¬m.degree f ≤ a}

theorem Ideal.isLowerSet_standardExponents {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (m : MonomialOrder σ) : IsLowerSet (I.standardExponents m)

Standard exponents form a lower set.

theorem Ideal.eq_zero_of_mem_restrictSupport_standardExponents {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (m : MonomialOrder σ) {f : MvPolynomial σ K} (hf : f ∈ MvPolynomial.restrictSupport K (I.standardExponents m)) (hI : f ∈ I) : f = 0

A standard polynomial belonging to the ideal is zero.

theorem Ideal.exists_standard_representative_degLex {K : Type u_1} {σ : Type u_2} [Field K] [LinearOrder σ] [WellFoundedGT σ] (I : Ideal (MvPolynomial σ K)) (f : MvPolynomial σ K) : ∃ r ∈ MvPolynomial.restrictSupport K (I.standardExponents MonomialOrder.degLex), r.totalDegree ≤ f.totalDegree ∧ f - r ∈ I

Division with respect to degLex gives a standard representative modulo I of no larger total degree.

def Ideal.boundedStandardExponents {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (m : MonomialOrder σ) (N : ℕ) : Set (σ →₀ ℕ)

Standard exponents of total degree at most N.

Equations

• I.boundedStandardExponents m N = {a : σ →₀ ℕ | a ∈ I.standardExponents m ∧ Finsupp.degree a ≤ N}