Frobenius auxiliary polynomials: noncancellation, tangent-derivative constraints, and their resulting count of smooth rational points.
A polynomial criterion for the multiplicity form of plane Bézout. All formal branches are constructed from the nonsingularity assumptions.
theorem
CCDN.planeFrobeniusAuxiliary_point_bound
{ι : Type u_1}
{κ : Type u_2}
[Fintype ι]
[Fintype κ]
(p : ℕ)
[Fact (Nat.Prime p)]
(f : MvPolynomial (Fin 2) (ZMod p))
(hf : Irreducible f)
(z : ι → Fin 2 → ZMod p)
(hz : Function.Injective z)
(hzero : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0)
(j : Fin 2)
(hsmooth : ∀ (i : ι), (MvPolynomial.eval (z i)) ((MvPolynomial.pderiv j.rev) f) ≠ 0)
(h a : κ → MvPolynomial (Fin 2) (ZMod p))
{D A N : ℕ}
(hD : f.totalDegree * D < p)
(hN : N ≤ p)
(hd : ∀ (k : κ), (h k).totalDegree ≤ D)
(ha : ∀ (k : κ), (a k).totalDegree ≤ A)
(hi : LinearIndependent (ZMod p) fun (k : κ) => (Ideal.Quotient.mkₐ (ZMod p) (Ideal.span {f})) (h k))
(hne : ∃ (k : κ), ¬f ∣ a k)
(hdiv : ∀ r < N, f ∣ ∑ k : κ, (⇑(planeTangent f j))^[r] (h k) * a k)
:
The smooth rational-point bound supplied by any nontrivial solution of the finite linear system defining a Frobenius auxiliary polynomial.