Documentation

Mathlib.RingTheory.MvPolynomial.Ideal

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 xsi, 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 xsi, 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 : σ →₀ ), m MvPolynomial.support xi, 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.