A distinguished variable in a homogeneous prime relation #
If a homogeneous polynomial uses one distinguished variable together with a set of auxiliary variables, then subtracting its pure distinguished monomial puts it in the ideal generated by the auxiliary variables. Consequently, a prime containing the polynomial and every auxiliary variable also contains the distinguished variable, provided the pure coefficient is a unit.
theorem
AlgebraicAnalysis.MvPolynomial.sub_pureMonomial_mem_span_X
{R : Type u_1}
{σ : Type u_2}
[CommRing R]
{P : MvPolynomial σ R}
{N : ℕ}
{t : σ}
{s : Set σ}
{c : R}
(hP : P.IsHomogeneous N)
(hvars : ↑P.vars ⊆ insert t s)
(hcoeff : P.coeff (Finsupp.single t N) = c)
:
Removing the pure distinguished monomial from a homogeneous polynomial leaves an element of the ideal generated by its other allowed variables.
theorem
AlgebraicAnalysis.MvPolynomial.X_mem_of_homogeneous_mem_prime
{R : Type u_1}
{σ : Type u_2}
[CommRing R]
{P : MvPolynomial σ R}
{N : ℕ}
{t : σ}
{s : Set σ}
{c : R}
(hP : P.IsHomogeneous N)
(hvars : ↑P.vars ⊆ insert t s)
(hcoeff : P.coeff (Finsupp.single t N) = c)
(hc : IsUnit c)
{p : Ideal (MvPolynomial σ R)}
(hp : p.IsPrime)
(hPmem : P ∈ p)
(hsmem : ∀ i ∈ s, MvPolynomial.X i ∈ p)
:
A prime containing a homogeneous relation, all auxiliary variables, and a unit pure coefficient must contain the distinguished variable.