Projective hypersurface residue classes give the sharp single-prime determinant bound in every positive dimension. The residue partition, chart units and positive local multiplicities are all constructed from the equation.

Sharp aggregation of local hypersurface exponents. Summing the exact integer cutoff inequalities before optimizing preserves the leading constant and gives a linear error independent of all residue multiplicities.

theorem CCDN.aggregate_hypersurface_exponents_cutoff {ι : Type u_1} [Fintype ι] (m : ℕ) (hm : 0 < m) (s μ : ι → ℕ) (hμ : ∀ (i : ι), 0 < μ i) (K : ℕ) : (∑ i : ι, s i) * K ≤ ∑ i : ι, hypersurfaceMultiplicityExponent m (μ i) (s i) + (∑ i : ι, μ i) * (m + K).choose (m + 1)

A common cutoff aggregates without any loss in the leading coefficient.

theorem CCDN.projectiveHypersurfaceChart_mod_ne_zero {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (k : Fin (n + 3)) : (MvPolynomial.map (Int.castRingHom (ZMod p))) (projectiveHypersurfaceChart k f) ≠ 0

Every affine chart of a homogeneous integer polynomial whose reduction modulo p is nonzero also has nonzero reduction modulo p.

def CCDN.ProjectiveHypersurfaceResidue {n : ℕ} (f : MvPolynomial (Fin (n + 3)) ℤ) (p : ℕ) [Fact (Nat.Prime p)] : Set (ProjectiveResidueSpace (n + 2) p)

The 𝔽_p-points of the reduction modulo p of the projective hypersurface f = 0 in ℙⁿ⁺².

Equations

• CCDN.ProjectiveHypersurfaceResidue f p = {r : CCDN.ProjectiveResidueSpace (n + 2) p | (MvPolynomial.eval (Projectivization.rep r)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) = 0}

@[instance_reducible]

noncomputable instance CCDN.instFintypeElemProjectiveResidueSpaceHAddNatOfNatProjectiveHypersurfaceResidue {n : ℕ} (f : MvPolynomial (Fin (n + 3)) ℤ) (p : ℕ) [Fact (Nat.Prime p)] : Fintype ↑(ProjectiveHypersurfaceResidue f p)

Equations

• CCDN.instFintypeElemProjectiveResidueSpaceHAddNatOfNatProjectiveHypersurfaceResidue f p = Fintype.ofFinite ↑(CCDN.ProjectiveHypersurfaceResidue f p)

noncomputable def CCDN.projectiveHypersurfaceResidueMultiplicity {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (r : ↑(ProjectiveHypersurfaceResidue f p)) : ℕ

The multiplicity of the reduced hypersurface f mod p at the residue point r, computed in the affine chart determined by the pivot of r.

Equations

• CCDN.projectiveHypersurfaceResidueMultiplicity f hf hf0 r = Classical.choose ⋯

theorem CCDN.projectiveHypersurfaceResidueMultiplicity_spec {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (r : ↑(ProjectiveHypersurfaceResidue f p)) : 0 < projectiveHypersurfaceResidueMultiplicity f hf hf0 r ∧ projectiveHypersurfaceResidueMultiplicity f hf hf0 r ≤ d ∧ (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (hypersurfaceResidueChartLift ↑r)) (projectiveHypersurfaceChart (hypersurfaceResiduePivot ↑r) f)) ∈ MvPolynomial.idealOfVars (Fin (n + 2)) (ZMod p) ^ projectiveHypersurfaceResidueMultiplicity f hf hf0 r ∧ (MvPolynomial.homogeneousComponent (projectiveHypersurfaceResidueMultiplicity f hf hf0 r)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (hypersurfaceResidueChartLift ↑r)) (projectiveHypersurfaceChart (hypersurfaceResiduePivot ↑r) f))) ≠ 0

The multiplicity of f mod p at a residue point r is between 1 and the degree d; in the chart of r, translated so that r is the origin, the reduced equation lies in that power of the ideal of the origin and has a nonzero homogeneous component of that degree. This is the local multiplicity used in CCDN Corollary 2.5.

noncomputable def CCDN.projectiveHypersurfaceTotalMultiplicity {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) : ℕ

The total residue multiplicity of the projective hypersurface f = 0 modulo p: the sum of the multiplicities of f mod p at all of its 𝔽_p-points. This is the quantity of CCDN Proposition 2.6.

Equations

• CCDN.projectiveHypersurfaceTotalMultiplicity f hf hf0 = ∑ r : ↑(CCDN.ProjectiveHypersurfaceResidue f p), CCDN.projectiveHypersurfaceResidueMultiplicity f hf hf0 r

theorem CCDN.projectiveHypersurfaceTotalMultiplicity_bounds {n p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) : Fintype.card ↑(ProjectiveHypersurfaceResidue f p) ≤ projectiveHypersurfaceTotalMultiplicity f hf hf0 ∧ projectiveHypersurfaceTotalMultiplicity f hf hf0 ≤ Fintype.card ↑(ProjectiveHypersurfaceResidue f p) * d

The total residue multiplicity of f mod p lies between the number of its 𝔽_p-points and d times that number.

theorem CCDN.projective_hypersurface_reduction_minorGcd {n s N p d M : ℕ} [Fact (Nat.Prime p)] (hs : 0 < s) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (F : Fin N → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → IntPoint (n + 3)) (hprim : ∀ (i : Fin s), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : 0 < projectiveHypersurfaceTotalMultiplicity f hf hf0 ∧ ∃ (e : ℕ), (∀ (K : ℕ), s * K ≤ e + projectiveHypersurfaceTotalMultiplicity f hf hf0 * (n + 1 + K).choose (n + 2)) ∧ (↑(n + 1).factorial / ↑(projectiveHypersurfaceTotalMultiplicity f hf hf0)) ^ (1 / (↑n + 1)) * (↑n + 1) / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1)) - (↑n + 2) * ↑s ≤ ↑e ∧ ↑p ^ e ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j))

Primitive zeros construct all local data. The resulting divisor has the sharp leading constant in terms of the total residue multiplicity.

theorem CCDN.projective_hypersurface_minorGcd_bound {n s N p d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (F : Fin N → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → IntPoint (n + 3)) (hprim : ∀ (i : Fin s), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : ∃ (e : ℕ), (↑(n + 1).factorial / ↑(projectiveHypersurfaceTotalMultiplicity f hf hf0)) ^ (1 / (↑n + 1)) * (↑n + 1) / (↑n + 2) * ↑s ^ (1 + 1 / (↑n + 1)) - (↑n + 2) * ↑s ≤ ↑e ∧ ↑p ^ e ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j))

For primitive integral zeros of a homogeneous hypersurface and homogeneous columns of a common degree, p^e divides the gcd of the maximal minors, where e is bounded below in terms of the total residue multiplicity. The number of rows and of residue points may be zero.