mathlib3 documentation

ring_theory.mv_polynomial.ideal

Lemmas about ideals of mv_polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Notably this contains results about monomial ideals.

Main results #

theorem mv_polynomial.mem_ideal_span_monomial_image {σ : Type u_1} {R : Type u_2} [comm_semiring R] {x : mv_polynomial σ R} {s : set →₀ )} :
x ideal.span ((λ (s : σ →₀ ), (mv_polynomial.monomial s) 1) '' s) (xi : σ →₀ ), xi x.support ( (si : σ →₀ ) (H : si s), si xi)

x is in a monomial ideal generated by s iff every element of 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 mv_polynomial.mem_ideal_span_X_image {σ : Type u_1} {R : Type u_2} [comm_semiring R] {x : mv_polynomial σ R} {s : set σ} :
x ideal.span (mv_polynomial.X '' s) (m : σ →₀ ), m x.support ( (i : σ) (H : i s), m i 0)

x is in a monomial ideal generated by variables X iff every element of of its support has a component in s.