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
• MvPolynomial.mem_pow_idealOfVars_iff
• MvPolynomial.span_X_image_isPrime: The ideal generated by a set of indeterminates of a polynomial ring is prime over a nontrivial semiring with no zero divisors.

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) (x.coeff xi)

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 MvPolynomial.span_X_image_eq_ker_aeval_ite_mem {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : Set σ) [DecidablePred fun (x : σ) => x ∈ s] : Ideal.span (X '' s) = RingHom.ker (aeval fun (x : σ) => if x ∈ sᶜ then X x else 0)

theorem MvPolynomial.span_X_image_isPrime {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] (s : Set σ) : (Ideal.span (X '' s)).IsPrime

@[reducible, inline]

noncomputable abbrev MvPolynomial.idealOfVars (σ : Type u_1) (R : Type u_2) [CommSemiring R] : Ideal (MvPolynomial σ R)

The ideal spanned by all variables.

Equations

• MvPolynomial.idealOfVars σ R = Ideal.span (Set.range MvPolynomial.X)

theorem MvPolynomial.isPrime_idealOfVars (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] : (idealOfVars σ R).IsPrime

theorem MvPolynomial.fg_idealOfVars (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Finite σ] : (idealOfVars σ R).FG

@[deprecated MvPolynomial.fg_idealOfVars (since := "2026-10-18")]

theorem MvPolynomial.idealOfVars_fg (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Finite σ] : (idealOfVars σ R).FG

Alias of MvPolynomial.fg_idealOfVars.

theorem MvPolynomial.idealOfVars_eq_restrictSupportIdeal {σ : Type u_1} {R : Type u_2} [CommSemiring R] : idealOfVars σ R = restrictSupportIdeal R (⇑Finsupp.degree ⁻¹' Set.Ici 1) ⋯

theorem MvPolynomial.pow_idealOfVars {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) : idealOfVars σ R ^ n = restrictSupportIdeal R (⇑Finsupp.degree ⁻¹' Set.Ici n) ⋯

theorem MvPolynomial.pow_idealOfVars_eq_span {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) : idealOfVars σ R ^ n = Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' ⇑Finsupp.degree ⁻¹' {n})

The nth power of idealOfVars is spanned by all monic monomials of total degree n.

theorem MvPolynomial.mem_pow_idealOfVars_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) (p : MvPolynomial σ R) : p ∈ idealOfVars σ R ^ n ↔ ∀ x ∈ p.support, n ≤ Finsupp.degree x

theorem MvPolynomial.mem_pow_idealOfVars_iff' {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) (p : MvPolynomial σ R) : p ∈ idealOfVars σ R ^ n ↔ ∀ (x : σ →₀ ℕ), Finsupp.degree x < n → p.coeff x = 0

theorem MvPolynomial.monomial_mem_pow_idealOfVars_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) (x : σ →₀ ℕ) {r : R} (h : r ≠ 0) : (monomial x) r ∈ idealOfVars σ R ^ n ↔ n ≤ Finsupp.degree x

theorem MvPolynomial.C_mem_pow_idealOfVars_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) (r : R) : C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

theorem MvPolynomial.mkₐ_eq_aeval {A : Type u_3} {σ : Type u_4} [CommRing A] (I : Ideal (MvPolynomial σ A)) : Ideal.Quotient.mkₐ A I = aeval fun (d : σ) => (Ideal.Quotient.mk I) (X d)

theorem MvPolynomial.mk_eq_eval₂ {A : Type u_3} {σ : Type u_4} [CommRing A] (I : Ideal (MvPolynomial σ A)) : (↑↑(Ideal.Quotient.mk I)).toFun = eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) fun (d : σ) => (Ideal.Quotient.mk I) (X d)

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}))

theorem MonomialOrder.sPolynomial_mem_sup_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {I J : Ideal (MvPolynomial σ R)} {p q : MvPolynomial σ R} (hp : p ∈ I) (hq : q ∈ J) : m.sPolynomial p q ∈ I ⊔ J

theorem MonomialOrder.sPolynomial_mem_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] {I : Ideal (MvPolynomial σ R)} {p q : MvPolynomial σ R} (hp : p ∈ I) (hq : q ∈ I) : m.sPolynomial p q ∈ I