Proper homogeneous sections of projective curves. The degree is the slope of the graded Hilbert function. Homogeneous interpolation and injective multiplication in the coordinate domain prove the section bound.

instance CCDN.homogeneousCoordinateSpace_finite {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (M : ℕ) : Module.Finite K ↥(homogeneousCoordinateSpace I M)

noncomputable def CCDN.projectiveHilbertFunction {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (M : ℕ) : ℕ

The graded Hilbert function of I: the dimension of the degree-M part of the coordinate ring MvPolynomial (Fin (n + 1)) K ⧸ I, that is, of the image of the homogeneous polynomials of degree M.

Equations

• CCDN.projectiveHilbertFunction I M = Module.finrank K ↥(CCDN.homogeneousCoordinateSpace I M)

def CCDN.HasProjectiveCurveDegree {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) (d : ℕ) : Prop

The ideal I has projective curve degree d: the graded Hilbert function of MvPolynomial (Fin (n + 1)) K ⧸ I eventually equals d * M + c for some constant c. For a homogeneous prime ideal of a projective curve, d is the usual degree.

Equations

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

def CCDN.projectiveIdealZeroLocus {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) K)) : Set (Projectivization K (Fin (n + 1) → K))

A projective point belongs to the zero locus when every representative annihilates the ideal. For homogeneous ideals this is the usual projective zero locus.

Equations

• CCDN.projectiveIdealZeroLocus I = {x : Projectivization K (Fin (n + 1) → K) | ∀ (v : Fin (n + 1) → K) (hv : v ≠ 0), Projectivization.mk K v hv = x → v ∈ CCDN.idealZeroLocus I}

theorem CCDN.projectiveIdealZeroLocus_rep {K : Type u_1} [Field K] {n : ℕ} {I : Ideal (MvPolynomial (Fin (n + 1)) K)} {x : Projectivization K (Fin (n + 1) → K)} (hx : x ∈ projectiveIdealZeroLocus I) : x.rep ∈ idealZeroLocus I

The chosen representative of a point of the projective zero locus of I lies in the affine zero locus of I.

theorem CCDN.projective_section_card_le_degree {K : Type u_1} [Field K] {n d m : ℕ} {ι : Type u_2} [Fintype ι] (I : Ideal (MvPolynomial (Fin (n + 1)) K)) [I.IsPrime] (hdegree : HasProjectiveCurveDegree I d) (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous m) (hfI : f ∉ I) (z : ι → Projectivization K (Fin (n + 1) → K)) (hz : Function.Injective z) (hzI : ∀ (i : ι), z i ∈ projectiveIdealZeroLocus I) (hzf : ∀ (i : ι), (MvPolynomial.eval (z i).rep) f = 0) : Fintype.card ι ≤ d * m

A proper section of degree m meets a degree-d projective prime curve in at most dm distinct points over the base field.

theorem CCDN.homogeneous_ideal_eval_smul {K : Type u_2} {σ : Type u_3} [Field K] (I : Ideal (MvPolynomial σ K)) (hI : IsHomogeneousIdeal I) (v : σ → K) (hv : v ∈ idealZeroLocus I) (a : K) (f : MvPolynomial σ K) (hf : f ∈ I) : (MvPolynomial.eval (a • v)) f = 0

A point of the zero locus of a homogeneous ideal stays in it after scaling.