Documentation

LeanPool.CCDN.Hypersurface.ProjectiveHypersurfaceDimensionGrowth

Projective hypersurface dimension growth in every degree at least five, from the affine bound on the cone. The equation need only be irreducible over ℚ: an equation which splits over the algebraic closure of ℚ has few points by the nonabsolute count.

A projective point count is bounded by the integer count on its affine cone at the same height. Chosen primitive representatives give a height-preserving injection.

CCDN Theorem 1 for rationally irreducible projective hypersurfaces of degree at least five in ℙ^(n+2), with degree exponent 18 + 3n. As in the paper (Corollary 4.1.4 and Remark 4.1.5), the equation may split over the algebraic closure of ℚ.

theorem CCDN.ProjectiveHypersurfaceGrowth.ideal {n e : ℕ} (h : ProjectiveHypersurfaceGrowth n e) :
∃ (C : ℝ), 0 < C ∧ ∀ (I : Ideal (MvPolynomial (Fin (n + 3)) ℚ)), I.IsPrime → IsHomogeneousIdeal I → ∀ (d : ℕ), 5 ≤ d → HasProjectiveDimensionDegree I (n + 1) d → ∀ (B : ℝ), 1 ≤ B → ↑(projectiveCount (projectiveIdealZeroLocus I) B) ≤ C * ↑d ^ e * B ^ (n + 1)

The hypersurface bound in the Hilbert-polynomial formulation: a homogeneous prime ideal of codimension one is generated by an irreducible homogeneous equation of degree d.