Documentation

Mathlib.RingTheory.MvPolynomial.Ideal

Lemmas about ideals of MvPolynomial #

Notably this contains results about monomial ideals.

Main results #

source
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.

source
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)
source
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.

source
def MvPolynomial.idealOfVars (σ : Type u_1) (R : Type u_2) [CommSemiring R] :
Ideal (MvPolynomial σ R)

The ideal spanned by all variables.

Equations
Instances For
    source
    theorem MvPolynomial.idealOfVars_eq_restrictSupportIdeal {σ : Type u_1} {R : Type u_2} [CommSemiring R] :
    idealOfVars σ R = restrictSupportIdeal R (⇑Finsupp.degree ⁻¹' Set.Ici 1) ⋯
    source
    theorem MvPolynomial.pow_idealOfVars {σ : Type u_1} {R : Type u_2} [CommSemiring R] (n : ℕ) :
    idealOfVars σ R ^ n = restrictSupportIdeal R (⇑Finsupp.degree ⁻¹' Set.Ici n) ⋯
    source
    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.

    source
    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
    source
    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 → coeff x p = 0
    source
    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
    source
    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
    source
    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)
    source
    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)
    source
    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)
    source
    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}))
    source
    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}))
    source
    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
    source
    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