Lemmas about ideals of MvPolynomial #
Notably this contains results about monomial ideals.
Main results #
theorem
MvPolynomial.mem_ideal_span_monomial_image
{σ : Type u_1}
{R : Type u_2}
[CommSemiring R]
{x : MvPolynomial σ R}
{s : Set (σ →₀ ℕ)}
:
x ∈ Ideal.span ((fun s => ↑(MvPolynomial.monomial s) 1) '' s) ↔ ∀ (xi : σ →₀ ℕ), xi ∈ MvPolynomial.support x → ∃ si, si ∈ s ∧ si ≤ xi
x is in a monomial ideal generated by s iff every element of its support dominates one of
the generators. Note that si ≤ xi is analogous to saying that the monomial corresponding to si
divides the monomial corresponding to xi.
theorem
MvPolynomial.mem_ideal_span_monomial_image_iff_dvd
{σ : Type u_1}
{R : Type u_2}
[CommSemiring R]
{x : MvPolynomial σ R}
{s : Set (σ →₀ ℕ)}
:
x ∈ Ideal.span ((fun s => ↑(MvPolynomial.monomial s) 1) '' s) ↔ ∀ (xi : σ →₀ ℕ),
xi ∈ MvPolynomial.support x →
∃ si, si ∈ s ∧ ↑(MvPolynomial.monomial si) 1 ∣ ↑(MvPolynomial.monomial xi) (MvPolynomial.coeff xi x)
theorem
MvPolynomial.mem_ideal_span_X_image
{σ : Type u_1}
{R : Type u_2}
[CommSemiring R]
{x : MvPolynomial σ R}
{s : Set σ}
:
x is in a monomial ideal generated by variables X iff every element of its support
has a component in s.