The affine Hilbert degree of a curve

An affine algebraic set is represented by an ideal in ℚ[x₁,…,xₙ]. For an integral curve, its degree is the slope of the eventually linear affine Hilbert function: the dimension of polynomials of total degree at most M in its coordinate ring is d*M + c for large M. The slope of an eventually linear function is unique, and a pointwise inequality between two eventually linear functions compares their slopes (eventual_linear_slope_le).

@[reducible, inline]

abbrev CCDN.CoordinatePolynomial (n : ℕ) : Type

The polynomial ring ℚ[x₁, …, xₙ] in which affine algebraic sets are cut out.

Equations

• CCDN.CoordinatePolynomial n = MvPolynomial (Fin n) ℚ

noncomputable def CCDN.affineHilbertFunction {n : ℕ} (I : Ideal (CoordinatePolynomial n)) (M : ℕ) : ℕ

The affine Hilbert function: the dimension of the polynomials of total degree at most M in the coordinate ring.

Equations

• CCDN.affineHilbertFunction I M = Module.finrank ℚ ↥(CCDN.filteredCoordinateSpace I M)

def CCDN.HasAffineCurveDegree {n : ℕ} (I : Ideal (CoordinatePolynomial n)) (d : ℕ) : Prop

Degree via the eventual affine Hilbert polynomial. This condition is mathematical data about the coordinate ring, and contains no point-counting estimate.

Equations

• CCDN.HasAffineCurveDegree I d = ∃ (N : ℕ) (c : ℤ), ∀ (M : ℕ), N ≤ M → ↑(CCDN.affineHilbertFunction I M) = ↑d * ↑M + c

theorem CCDN.affineCurveDegree_unique {n : ℕ} {I : Ideal (CoordinatePolynomial n)} {d e : ℕ} (hd : HasAffineCurveDegree I d) (he : HasAffineCurveDegree I e) : d = e

The affine Hilbert degree of a curve is unique: if I has affine curve degree d and e, then d = e.

theorem CCDN.eventual_linear_slope_le (f g : ℕ → ℕ) (a b : ℕ) (hf : ∃ (N : ℕ) (c : ℤ), ∀ n ≥ N, ↑(f n) = ↑a * ↑n + c) (hg : ∃ (N : ℕ) (c : ℤ), ∀ n ≥ N, ↑(g n) = ↑b * ↑n + c) (hle : ∀ (n : ℕ), f n ≤ g n) : a ≤ b

Pointwise domination of eventually linear functions compares their slopes.