# 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`

.