A strict containment of affine prime ideals strictly lowers the Hilbert dimension. The proof uses a polynomial in their difference.
theorem
CCDN.prime_ideal_not_le_of_same_positive_dimension
{K : Type u_1}
[Field K]
{n m : ℕ}
(I J : Ideal (MvPolynomial (Fin n) K))
[I.IsPrime]
[J.IsPrime]
(hI : (filteredHilbertPolynomial I).natDegree = m + 1)
(hJ : (filteredHilbertPolynomial J).natDegree = m + 1)
(hne : I ≠ J)
:
Distinct prime ideals of the same positive Hilbert dimension are not contained in one another.
theorem
CCDN.exists_prime_generator_of_hilbert_dimension
{n : ℕ}
(I : Ideal (MvPolynomial (Fin (n + 2)) ℚ))
[hI : I.IsPrime]
(hdim : (filteredHilbertPolynomial I).natDegree = n + 1)
:
∃ (p : MvPolynomial (Fin (n + 2)) ℚ), Prime p ∧ 0 < p.totalDegree ∧ I = Ideal.span {p}
A prime ideal in n + 2 variables whose Hilbert polynomial has degree n + 1, that is a
projective hypersurface, is generated by one nonconstant prime element.