Standard monomials in a filtered coordinate ring #
Degree lexicographic standard representatives (Ideal.exists_standard_representative_degLex)
preserve the total-degree filtration, giving an exact combinatorial model for the dimensions
of the filtered coordinate spaces.
theorem
CCDN.filteredCoordinateSpace_finrank_eq_standard_card
{K : Type u_1}
{σ : Type u_2}
[Field K]
[LinearOrder σ]
[WellFoundedGT σ]
(I : Ideal (MvPolynomial σ K))
(N : ℕ)
:
The filtered Hilbert function counts the standard monomials of bounded degree.