Lemmas about ideals of MvPolynomial

Notably this contains results about monomial ideals.

Main results

• MvPolynomial.mem_ideal_span_monomial_image
• MvPolynomial.mem_ideal_span_X_image

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 : σ →₀ ℕ) => (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 : σ →₀ ℕ) => (monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, (monomial si) 1 ∣ (monomial xi) (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 (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.