Finite standard-monomial prefixes for a principal equation, their exact Hilbert ranks, and the sum of their total degrees.
noncomputable def
CCDN.standardMonomialPrefix
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
(I : Ideal (MvPolynomial σ K))
(m : MonomialOrder σ)
(N : ℕ)
:
The finite set of standard exponents of I, for the monomial order m, of total degree at most
N.
Equations
- CCDN.standardMonomialPrefix I m N = ⋯.toFinset
Instances For
@[simp]
theorem
CCDN.mem_standardMonomialPrefix
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
(I : Ideal (MvPolynomial σ K))
(m : MonomialOrder σ)
(N : ℕ)
(a : σ →₀ ℕ)
:
An exponent lies in standardMonomialPrefix I m N exactly when it is a standard exponent of I
of degree at most N.
theorem
CCDN.standardMonomialPrefix_card
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
(N : ℕ)
:
The number of degree-lexicographic standard exponents of I of degree at most N equals the
affine Hilbert function of I at N.
theorem
CCDN.standardMonomialPrefix_weight_identity
{K : Type u_1}
{σ : Type u_2}
[Field K]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
(N : ℕ)
:
∑ a ∈ standardMonomialPrefix I MonomialOrder.degLex N, Finsupp.degree a + ∑ k ∈ Finset.range N, Module.finrank K ↥(filteredCoordinateSpace I k) = N * Module.finrank K ↥(filteredCoordinateSpace I N)
The total degree of a standard prefix is exactly the rank-weighted cutoff minus the preceding filtered Hilbert ranks.
theorem
CCDN.principal_standard_prefix_rank
{K : Type u_1}
[Field K]
{n : ℕ}
(f : MvPolynomial (Fin (n + 1)) K)
(hf : f ≠ 0)
{N : ℕ}
(hN : f.totalDegree ≤ N)
:
(standardMonomialPrefix (Ideal.span {f}) MonomialOrder.degLex N).card + (n + 1 + (N - f.totalDegree)).choose (N - f.totalDegree) = (n + 1 + N).choose N
The exact principal Hilbert rank is the same binomial difference used for homogeneous hypersurfaces with one extra variable.