Existence, uniqueness and positive integral multiplicity of the filtered Hilbert polynomial of a polynomial quotient, in arbitrary finite dimension. These results construct the polynomial from standard exponents.

def CCDN.standardExponentVectors {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] (I : Ideal (MvPolynomial σ K)) (m : MonomialOrder σ) : Set (σ → ℕ)

The exponent vectors, as functions σ → ℕ, of the standard monomials of I with respect to the monomial order m: those that are not leading monomials of elements of I.

Equations

• CCDN.standardExponentVectors I m = {a : σ → ℕ | Finsupp.equivFunOnFinite.symm a ∈ I.standardExponents m}

theorem CCDN.standardExponentVectors_lower {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] (I : Ideal (MvPolynomial σ K)) (m : MonomialOrder σ) : IsLowerSet (standardExponentVectors I m)

The standard exponent vectors of an ideal form a lower set.

theorem CCDN.standardExponentVectors_nonempty {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) : (standardExponentVectors I MonomialOrder.degLex).Nonempty

A proper ideal has a standard exponent vector for the degree-lexicographic order.

theorem CCDN.filteredCoordinateSpace_finrank_eq_vector_card {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (N : ℕ) : Module.finrank K ↥(filteredCoordinateSpace I N) = Nat.card { a : σ → ℕ // a ∈ standardExponentVectors I MonomialOrder.degLex ∧ ∑ i : σ, a i ≤ N }

The affine Hilbert function of I at N equals the number of standard exponent vectors of I, for the degree-lexicographic order, of total degree at most N.

theorem CCDN.filteredCoordinateSpace_eventually_polynomial {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) : ∃ (P : Polynomial ℚ) (N : ℕ), ∀ n ≥ N, Polynomial.eval (↑n) P = ↑(Module.finrank K ↥(filteredCoordinateSpace I n))

Eventual polynomiality of the filtered coordinate-space dimension.

theorem CCDN.polynomial_eq_of_eventual_nat_eval_eq (P Q : Polynomial ℚ) (h : ∃ (N : ℕ), ∀ n ≥ N, Polynomial.eval (↑n) P = Polynomial.eval (↑n) Q) : P = Q

Two rational polynomials that agree at all sufficiently large natural numbers are equal.

noncomputable def CCDN.filteredHilbertPolynomial {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) : Polynomial ℚ

The uniquely determined filtered Hilbert polynomial.

Equations

• CCDN.filteredHilbertPolynomial I = ⋯.choose

structure CCDN.HasAffineDimensionDegree {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (m d : ℕ) : Prop

The filtered Hilbert polynomial of I has degree m and leading coefficient d / m!: the affine variety cut out by I has dimension m and degree d.

• natDegree_eq : (filteredHilbertPolynomial I).natDegree = m

  The filtered Hilbert polynomial has degree m.

• leadingCoeff_eq : (filteredHilbertPolynomial I).leadingCoeff = ↑d / ↑m.factorial

  The filtered Hilbert polynomial has leading coefficient d / m!.

@[reducible, inline]

abbrev CCDN.HasProjectiveDimensionDegree {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (m d : ℕ) : Prop

The cone over I has filtered Hilbert polynomial of degree m + 1 and leading coefficient d / (m + 1)!. For a homogeneous ideal I this says that the projective variety cut out by I has dimension m and degree d; it is the affine dimension and degree of the cone.

Equations

• CCDN.HasProjectiveDimensionDegree I m d = CCDN.HasAffineDimensionDegree I (m + 1) d

theorem CCDN.HasAffineDimensionDegree.of_filteredHilbertPolynomial_eq {K : Type u_1} {L : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Fintype σ] [LinearOrder σ] [Field L] [Fintype τ] [LinearOrder τ] {I : Ideal (MvPolynomial σ K)} {J : Ideal (MvPolynomial τ L)} {m d : ℕ} (h : HasAffineDimensionDegree I m d) (hJI : filteredHilbertPolynomial J = filteredHilbertPolynomial I) : HasAffineDimensionDegree J m d

Dimension and degree only depend on the filtered Hilbert polynomial.

theorem CCDN.filteredHilbertPolynomial_spec {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) : ∃ (N : ℕ), ∀ n ≥ N, Polynomial.eval (↑n) (filteredHilbertPolynomial I) = ↑(Module.finrank K ↥(filteredCoordinateSpace I n))

The filtered Hilbert polynomial of I agrees at every sufficiently large n with the dimension of the image in K[X] ⧸ I of the polynomials of total degree at most n.

theorem CCDN.filteredHilbertPolynomial_eq_of_eventual {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (P : Polynomial ℚ) (hP : ∃ (N : ℕ), ∀ n ≥ N, Polynomial.eval (↑n) P = ↑(Module.finrank K ↥(filteredCoordinateSpace I n))) : filteredHilbertPolynomial I = P

Any rational polynomial that eventually agrees with the affine Hilbert function of I is the filtered Hilbert polynomial of I.

theorem CCDN.filteredHilbertPolynomial_positive_multiplicity {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) : ∃ (d : ℕ), 0 < d ∧ (filteredHilbertPolynomial I).natDegree ≤ Fintype.card σ ∧ (filteredHilbertPolynomial I).leadingCoeff = ↑d / ↑(filteredHilbertPolynomial I).natDegree.factorial

Proper polynomial quotients have a positive integer factorial-normalized leading coefficient.

theorem CCDN.exists_hasAffineDimensionDegree {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) {m : ℕ} (hdim : (filteredHilbertPolynomial I).natDegree = m) : ∃ (d : ℕ), 0 < d ∧ HasAffineDimensionDegree I m d

A proper ideal whose filtered Hilbert polynomial has degree m has dimension m and some positive degree.