CCDN Theorem 1 in the homogeneous-coordinate-ideal formulation: uniform projective dimension growth for every rational prime projective variety of degree at least five. The Hilbert polynomial determines the degree and dimension. Zero-dimensional and empty loci are included.

The bound is assembled once, in projectiveGrowth_of_le, for any degree exponent which dominates the exponents of the zero-dimensional count, the curve bound, the hypersurface bound and the projection bound. The degree exponent 2n² + 5n - 5 follows, and from it the exponent 2n³.

theorem CCDN.ProjectiveGrowth.mono {n E E' : ℕ} (h : ProjectiveGrowth n E) (hE : E ≤ E') : ProjectiveGrowth n E'

Projective dimension growth with degree exponent E implies it with any larger exponent E'.

theorem CCDN.projectiveGrowth_of_le {n E : ℕ} (hpoint : 1 ≤ n → n + 1 ≤ E) (hcurve : 2 ≤ n → 3 * (n + 1) + 4 ≤ E) (hhyper : 3 ≤ n → 18 + 3 * (n - 2) ≤ E) (hproj : ∀ (m k : ℕ), m + k + 1 = n → 1 ≤ m → 2 ≤ k → projectionDegreeExponent m k ≤ E) : ProjectiveGrowth n E

Theorem 1 holds with any degree exponent E which dominates, in ℙⁿ, the exponent n + 1 of the zero-dimensional count, the exponent 3(n+1) + 4 of the curve bound, the exponent 18 + 3(n-2) of the hypersurface bound, and the exponent of the projection bound for every dimension m + 1 ≥ 2 and codimension k ≥ 2.

theorem CCDN.projectiveProjectionDegreeExponent_le {m k n : ℕ} (h : m + k + 1 = n) (hk : 2 ≤ k) : projectionDegreeExponent m k ≤ 2 * n ^ 2 + 2 * n + 6

In ℙⁿ with n = m + k + 1, the projection exponent has the closed form 2mn + 5m + 3n + 21. For codimension k ≥ 2 it is at most its value 2n² + 2n + 6 at k = 2.

def CCDN.projectiveGrowthExponent (n : ℕ) : ℕ

The degree exponent 2n² + 5n - 5 of Theorem 1 in ℙⁿ. Its values 2 and 13 for n = 1, 2 are the exponents of the zero-dimensional count and of the curve bound. For n ≥ 4 it exceeds the projection exponent 2n² + 2n + 6 by 3n - 11.

Equations

• CCDN.projectiveGrowthExponent n = 2 * n ^ 2 + 5 * n - 5

theorem CCDN.projective_dimension_growth (n : ℕ) : ProjectiveGrowth n (projectiveGrowthExponent n)

CCDN Theorem 1 with the degree exponent 2n² + 5n - 5 in every ambient projective dimension n.