A prime projective variety of degree greater than one cannot have full ambient Hilbert dimension. This uses the Hilbert polynomial of the polynomial ring, rather than an additional geometric hypothesis.
theorem
CCDN.filteredHilbertPolynomial_bot
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
:
The filtered Hilbert polynomial of the zero ideal in |σ| variables is the binomial polynomial
preHilbertPoly ℚ |σ| 0.
theorem
CCDN.hilbert_dimension_lt_ambient_of_degree_gt_one
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
(hI : I ≠ ⊤)
(d : ℕ)
(hd : 1 < d)
(hdegree : (filteredHilbertPolynomial I).leadingCoeff = ↑d / ↑(filteredHilbertPolynomial I).natDegree.factorial)
:
A proper ideal of Hilbert degree d > 1 has Hilbert dimension smaller than the number of
variables.