Smooth affine residue classes and their simultaneous cardinality bound. The elementary d*p^(ambient-1) bound suffices when the number of chosen primes is absorbed by a small power of the box size.

def CCDN.SmoothAffineResidue {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (p : ℕ) : Type

The nonsingular 𝔽_p-points of the reduction modulo p of the affine hypersurface f = 0.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance CCDN.instFintypeSmoothAffineResidueOfNeZeroNat {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (p : ℕ) [NeZero p] : Fintype (SmoothAffineResidue f p)

Equations

• CCDN.instFintypeSmoothAffineResidueOfNeZeroNat f p = id inferInstance

def CCDN.SmoothAffineResidueFamily {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (P : Finset ℕ) : Type

A choice, for each prime p in P, of a nonsingular 𝔽_p-point of f mod p.

Equations

• CCDN.SmoothAffineResidueFamily f P = ((p : ↥P) → CCDN.SmoothAffineResidue f ↑p)

theorem CCDN.smoothAffineResidueFamily_card_le {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) : Nat.card (SmoothAffineResidueFamily f P) ≤ f.totalDegree ^ P.card * (∏ p ∈ P, p) ^ n

The number of families of nonsingular residue points of f modulo the primes in P is at most deg(f) ^ #P · (∏_{p ∈ P} p) ^ n.

def CCDN.smoothResidueIntegerLift {n : ℕ} {f : MvPolynomial (Fin n) ℤ} {P : Finset ℕ} (r : SmoothAffineResidueFamily f P) : ℕ → IntPoint n

The integer lift, with coordinates in [0, p), of the residue point modulo p chosen by the family r (and 0 for p ∉ P).

Equations

• CCDN.smoothResidueIntegerLift r p j = if hp : p ∈ P then ↑(↑(r ⟨p, hp⟩) j).val else 0

theorem CCDN.smoothResidueIntegerLift_zero {n : ℕ} {f : MvPolynomial (Fin n) ℤ} {P : Finset ℕ} (r : SmoothAffineResidueFamily f P) (p : ℕ) [NeZero p] (hp : p ∈ P) : MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin n) => ↑(smoothResidueIntegerLift r p j)) f = 0

The reduction of f modulo p ∈ P vanishes at the lift of the residue point chosen by r.

theorem CCDN.smoothResidueIntegerLift_smooth {n : ℕ} {f : MvPolynomial (Fin n) ℤ} {P : Finset ℕ} (r : SmoothAffineResidueFamily f P) (p : ℕ) [NeZero p] (hp : p ∈ P) : ∃ (j : Fin n), (MvPolynomial.eval fun (i : Fin n) => ↑(smoothResidueIntegerLift r p i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0

The lift of the residue point chosen by r modulo p ∈ P is a nonsingular point of f mod p.

def CCDN.smoothResidueFamilyOfPoint {n : ℕ} {f : MvPolynomial (Fin n) ℤ} (x : IntPoint n) (hxf : (MvPolynomial.eval x) f = 0) (P : Finset ℕ) (hs : ∀ p ∈ P, ∃ (j : Fin n), (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0) : SmoothAffineResidueFamily f P

The family of residue points obtained by reducing an integer zero x of f modulo each prime in P at which it is nonsingular.

Equations

• CCDN.smoothResidueFamilyOfPoint x hxf P hs p = ⟨fun (j : Fin n) => ↑(x j), ⋯⟩

theorem CCDN.smoothResidueFamilyOfPoint_congruence {n : ℕ} {f : MvPolynomial (Fin n) ℤ} (x : IntPoint n) (hxf : (MvPolynomial.eval x) f = 0) (P : Finset ℕ) (hs : ∀ p ∈ P, ∃ (j : Fin n), (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0) (p : ℕ) [NeZero p] (hp : p ∈ P) (j : Fin n) : ↑p ∣ x j - smoothResidueIntegerLift (smoothResidueFamilyOfPoint x hxf P hs) p j

An integer zero x of f is congruent modulo each p ∈ P to the integer lift of its own residue family.