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 ∈ x.support, ∃ 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 ∈ x.support, ∃ 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 ∈ Ideal.span (MvPolynomial.X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
x is in a monomial ideal generated by variables X iff every element of its support
has a component in s.