A proper positive-codimension prime ideal of positive Hilbert dimension contains a nonzero equation of degree at most its Hilbert multiplicity. The independent coordinate subtuple and the equation are both constructed.
theorem
CCDN.exists_mem_ideal_degree_le_multiplicity
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
{n : ℕ}
(I : Ideal (MvPolynomial σ K))
[I.IsPrime]
(d : ℕ)
(hdimdeg : HasProjectiveDimensionDegree I n d)
(hcodim : n + 1 < Fintype.card σ)
:
∃ (f : MvPolynomial σ K), f ≠ 0 ∧ f ∈ I ∧ f.totalDegree ≤ d
A prime ideal of projective dimension n and degree d in more than n + 1 variables contains
a nonzero polynomial of total degree at most d.