Homogeneous zero loci on rational projective space and their integer representatives. Membership is independent of the representative.

theorem CCDN.homogeneous_eval_smul {K : Type u_1} {σ : Type u_2} [CommSemiring K] {f : MvPolynomial σ K} {d : ℕ} (hf : f.IsHomogeneous d) (a : K) (v : σ → K) : (MvPolynomial.eval (a • v)) f = a ^ d * (MvPolynomial.eval v) f

Evaluating a homogeneous polynomial of degree d at a • v multiplies its value at v by a ^ d.

theorem CCDN.homogeneous_eval_zero_iff_smul {K : Type u_1} {σ : Type u_2} [Field K] {f : MvPolynomial σ K} {d : ℕ} (hf : f.IsHomogeneous d) {a : K} (ha : a ≠ 0) (v : σ → K) : (MvPolynomial.eval (a • v)) f = 0 ↔ (MvPolynomial.eval v) f = 0

Over a field, a homogeneous polynomial vanishes at a • v, for a ≠ 0, exactly when it vanishes at v.

theorem CCDN.homogeneous_eval_zero_iff_projective_eq {K : Type u_1} [Field K] {n d : ℕ} {f : MvPolynomial (Fin (n + 1)) K} (hf : f.IsHomogeneous d) {v w : Fin (n + 1) → K} (hv : v ≠ 0) (hw : w ≠ 0) (he : Projectivization.mk K v hv = Projectivization.mk K w hw) : (MvPolynomial.eval v) f = 0 ↔ (MvPolynomial.eval w) f = 0

A homogeneous polynomial vanishes at one nonzero vector exactly when it vanishes at any other nonzero vector spanning the same projective point.

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

The projective points whose chosen representative is a zero of f; for homogeneous f this is the projective zero locus of f, independent of the representative.

Equations

• CCDN.projectiveZeroLocus f = {x : Projectivization K (Fin (n + 1) → K) | (MvPolynomial.eval x.rep) f = 0}

theorem CCDN.mem_projectiveZeroLocus_mk {K : Type u_1} [Field K] {n d : ℕ} {f : MvPolynomial (Fin (n + 1)) K} (hf : f.IsHomogeneous d) (v : Fin (n + 1) → K) (hv : v ≠ 0) : Projectivization.mk K v hv ∈ projectiveZeroLocus f ↔ (MvPolynomial.eval v) f = 0

For homogeneous f, the projective point spanned by a nonzero vector v lies in the projective zero locus of f exactly when f vanishes at v.

theorem CCDN.mem_projectiveZeroLocus_primitive {n d : ℕ} {f : MvPolynomial (Fin (n + 1)) ℚ} (hf : f.IsHomogeneous d) (x : ProjectivePoint n) : x ∈ projectiveZeroLocus f ↔ (MvPolynomial.eval (rationalPoint (primitiveProjectiveRep x))) f = 0

For homogeneous rational f, a rational projective point lies in the zero locus of f exactly when f vanishes at its primitive integer representative.

theorem CCDN.mem_integer_projectiveZeroLocus {n d : ℕ} {f : MvPolynomial (Fin (n + 1)) ℤ} (hf : f.IsHomogeneous d) (x : ProjectivePoint n) : x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) ↔ (MvPolynomial.eval (primitiveProjectiveRep x)) f = 0

For a homogeneous integer polynomial f, a rational projective point lies in the projective zero locus of f (viewed over ℚ) exactly when f vanishes at the point's primitive integer representative.

theorem CCDN.projective_zero_count_le_of_family_bound {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (B R : ℝ) (hbound : ∀ (t : ℕ) (z : Fin t → IntPoint (n + 1)) (hz : ∀ (i : Fin t), z i ≠ 0), (Function.Injective fun (i : Fin t) => Projectivization.mk ℚ (rationalPoint (z i)) ⋯) → (∀ (i : Fin t), Finset.univ.gcd (z i) = 1) → (∀ (i : Fin t), (MvPolynomial.eval (z i)) f = 0) → (∀ (i : Fin t), InBox (z i) B) → ↑t ≤ R) : ↑(projectiveCount (projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B) ≤ R

Reduce a projective count to a finite family of bounded primitive integer vectors representing distinct projective points.