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.

theorem MonomialOrder.span_leadingTerm_sdiff_singleton_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (B : Set (MvPolynomial σ R)) : Ideal.span (m.leadingTerm '' (B \ {0})) = Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.span_leadingTerm_insert_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} (B : Set (MvPolynomial σ R)) : Ideal.span (m.leadingTerm '' insert 0 B) = Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.span_leadingTerm_eq_span_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {B : Set (MvPolynomial σ R)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)) : Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' B)

theorem MonomialOrder.span_leadingTerm_eq_span_monomial₀ {σ : Type u_1} {R : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {B : Set (MvPolynomial σ R)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0) : Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))

theorem MonomialOrder.span_leadingTerm_eq_span_monomial' {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {B : Set (MvPolynomial σ k)} : Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun (p : MvPolynomial σ k) => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))