Eventual linearity from a linear Hilbert bound #
The standard monomial set eventually consists of finitely many disjoint rays. Its sufficiently high degree shells therefore have constant cardinality.
theorem
CCDN.filteredCoordinateSpace_eventually_linear
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Finite σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
(C : ℕ)
(hbound : ∀ N ≥ 14, Module.finrank K ↥(filteredCoordinateSpace I N) ≤ C * (N + 2))
:
∃ d ≤ C, HasFilteredCurveDegree I d
Any linear upper bound on a filtered coordinate ring implies an eventually affine Hilbert function, with natural slope at most that upper-bound slope.
theorem
CCDN.transcendental_coordinate_filtered_lower
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Finite σ]
(I : Ideal (MvPolynomial σ K))
{j : σ}
(hj : Transcendental K ((Ideal.Quotient.mk I) (MvPolynomial.X j)))
(N : ℕ)
:
A transcendental coordinate contributes all of its powers to the filtration.