A sharp affine curve intersection bound from the Hilbert function. Bounds intersections with arbitrary section polynomials. No projective intersection theorem or point-counting axiom is used.
theorem
CCDN.polynomial_section_card_le_degree
{K : Type u_1}
{σ : Type u_2}
{ι : Type u_3}
[Field K]
[Finite σ]
[Fintype ι]
(p : Ideal (MvPolynomial σ K))
[p.IsPrime]
(d : ℕ)
(hdegree : HasFilteredCurveDegree p d)
(l : MvPolynomial σ K)
(hl : l ∉ p)
(m : ℕ)
(hld : l.totalDegree ≤ m)
(z : ι → σ → K)
(hz : Function.Injective z)
(hzp : ∀ (i : ι), z i ∈ idealZeroLocus p)
(hzl : ∀ (i : ι), (MvPolynomial.eval (z i)) l = 0)
:
A proper polynomial section of a prime curve contains at most the product of the curve's affine Hilbert degree and the section degree many distinct points.