Auxiliary nonmultiples

The determinant method produces an auxiliary polynomial g for an equation f: a nonzero polynomial that is not a multiple of f but vanishes on the points to be counted, so that these points lie on the intersection of f = 0 and g = 0. Three forms occur, according to how the points are given.

• CCDN.IsBoxAuxiliary f g B: g vanishes at every integral zero of f in the box of radius B.
• CCDN.IsPointAuxiliary f g M z: g is a form of degree M vanishing at the finitely many points z i.
• CCDN.IsProjectiveAuxiliary f g M B: g is a form of degree M vanishing at every rational projective zero of f of multiplicative height at most B.

The degree bound on g, which differs from statement to statement, is kept separate.

structure CCDN.IsBoxAuxiliary {n : ℕ} (f g : MvPolynomial (Fin n) ℤ) (B : ℝ) : Prop

g is an auxiliary polynomial for the integral affine equation f on the box of radius B: it is nonzero, it is not a multiple of f, and it vanishes at every integral zero of f all of whose coordinates are at most B in absolute value.

• ne_zero : g ≠ 0

  The auxiliary polynomial is nonzero.

• not_dvd : ¬f ∣ g

  The auxiliary polynomial is not a multiple of f.

• vanishes (x : IntPoint n) : InBox x B → (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval x) g = 0

  The auxiliary polynomial vanishes at every integral zero of f in the box of radius B.

theorem CCDN.exists_isBoxAuxiliary_and_iff {n : ℕ} {f : MvPolynomial (Fin n) ℤ} {B : ℝ} {P : MvPolynomial (Fin n) ℤ → Prop} : (∃ (g : MvPolynomial (Fin n) ℤ), IsBoxAuxiliary f g B ∧ P g) ↔ ∃ (g : MvPolynomial (Fin n) ℤ), g ≠ 0 ∧ ¬f ∣ g ∧ P g ∧ ∀ (x : IntPoint n), InBox x B → (MvPolynomial.eval x) f = 0 → (MvPolynomial.eval x) g = 0

Unbundled form of an auxiliary polynomial on a box satisfying a further condition P, typically a degree bound, in the order in which the auxiliary theorems are stated.

structure CCDN.IsPointAuxiliary {σ : Type u_1} {R : Type u_2} {ι : Type u_3} [CommRing R] (f g : MvPolynomial σ R) (M : ℕ) (z : ι → σ → R) : Prop

g is a homogeneous auxiliary polynomial of degree M for f through the points z: a nonzero form of degree M that vanishes at every point z i but is not a multiple of f.

• ne_zero : g ≠ 0

  The auxiliary form is nonzero.

• isHomogeneous : g.IsHomogeneous M

  The auxiliary form is homogeneous of degree M.

• eval_eq_zero (i : ι) : (MvPolynomial.eval (z i)) g = 0

  The auxiliary form vanishes at every point z i.

• not_dvd : ¬f ∣ g

  The auxiliary form is not a multiple of f.

theorem CCDN.isPointAuxiliary_iff {σ : Type u_1} {R : Type u_2} {ι : Type u_3} [CommRing R] {f g : MvPolynomial σ R} {M : ℕ} {z : ι → σ → R} : IsPointAuxiliary f g M z ↔ g ≠ 0 ∧ g.IsHomogeneous M ∧ (∀ (i : ι), (MvPolynomial.eval (z i)) g = 0) ∧ ¬f ∣ g

Unbundled form of CCDN.IsPointAuxiliary.

theorem CCDN.dvd_of_not_exists_isPointAuxiliary {σ : Type u_1} {R : Type u_2} {ι : Type u_3} [CommRing R] {f : MvPolynomial σ R} {M : ℕ} {z : ι → σ → R} (h : ¬∃ (g : MvPolynomial σ R), IsPointAuxiliary f g M z) (g : MvPolynomial σ R) (hg : g.IsHomogeneous M) (hz : ∀ (i : ι), (MvPolynomial.eval (z i)) g = 0) : f ∣ g

If there is no auxiliary form of degree M through the points z, then every form of degree M vanishing at all of them is a multiple of f. This is the hypothesis under which the determinant method bounds the number of points.

structure CCDN.IsProjectiveAuxiliary {n : ℕ} (f g : MvPolynomial (Fin (n + 1)) ℤ) (M : ℕ) (B : ℝ) : Prop

g is a projective auxiliary form of degree M for the integral form f at height B: a nonzero form of degree M, not a multiple of f, whose rational projective zero locus contains every rational projective zero of f of multiplicative height at most B.

• ne_zero : g ≠ 0

  The auxiliary form is nonzero.

• isHomogeneous : g.IsHomogeneous M

  The auxiliary form is homogeneous of degree M.

• vanishes (x : ProjectivePoint n) : Projectivization.mulHeight x ≤ B → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) → x ∈ projectiveZeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) g)

  The auxiliary form vanishes at every rational projective zero of f of multiplicative height at most B.

• not_dvd : ¬f ∣ g

  The auxiliary form is not a multiple of f.