Projective hypersurface determinants in all positive dimensions. Unit normalization modulo prime powers transfers the local affine bound to homogeneous evaluation matrices of a common degree.

Singular local determinant bounds at a residue point in arbitrary dimension. Multiplicity is obtained from the first nonzero translated homogeneous component.

theorem CCDN.hypersurface_residue_pow_dvd_det_mod {p n μ s : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 2)) ℤ) (a : Fin (n + 2) → ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) f) ∈ MvPolynomial.idealOfVars (Fin (n + 2)) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) f)) ≠ 0) (x : Fin s → Fin (n + 2) → ℤ) (hx : ∀ (i : Fin s) (j : Fin (n + 2)), ↑p ∣ x i j - a j) (hfx : ∀ (i : Fin s), ↑p ^ hypersurfaceMultiplicityExponent (n + 1) μ s ∣ (MvPolynomial.eval (x i)) f) (F : Fin s → MvPolynomial (Fin (n + 2)) ℤ) : ↑p ^ hypersurfaceMultiplicityExponent (n + 1) μ s ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (F j)).det

Translation carries the finite-precision determinant theorem to any residue class. Its divisor and its precision use the same explicit exponent.

theorem CCDN.projective_hypersurface_chart_eval_congr {n M : ℕ} {q u : ℤ} (z : Fin (n + 3) → ℤ) (hu : q ∣ u * z 0 - 1) (F : MvPolynomial (Fin (n + 3)) ℤ) (hF : F.IsHomogeneous M) : q ∣ (MvPolynomial.eval fun (j : Fin (n + 2)) => u * z j.succ) ((affineChart (n + 2)) F) - u ^ M * (MvPolynomial.eval z) F

Unit normalization in the first homogeneous coordinate preserves the evaluation of a degree-M form, up to the corresponding unit row factor.

theorem CCDN.projective_hypersurface_chart_det_divisibility {p n μ s d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hfhom : f.IsHomogeneous d) (F : Fin s → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin s), (F j).IsHomogeneous M) (z : Fin s → Fin (n + 3) → ℤ) (a : Fin (n + 2) → ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) ((affineChart (n + 2)) f)) ∈ MvPolynomial.idealOfVars (Fin (n + 2)) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) ((affineChart (n + 2)) f))) ≠ 0) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i 0)) (hres : ∀ (i : Fin s) (j : Fin (n + 2)), ↑p ∣ z i j.succ - a j * z i 0) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : ↑p ^ hypersurfaceMultiplicityExponent (n + 1) μ s ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (z i)) (F j)).det

Projective local determinant estimate in a chart whose first coordinate is a p-adic unit. The affine multiplicity belongs to the chart equation.

noncomputable def CCDN.projectiveHypersurfaceChart {n : ℕ} (k : Fin (n + 3)) (f : MvPolynomial (Fin (n + 3)) ℤ) : MvPolynomial (Fin (n + 2)) ℤ

Move coordinate k to the first position before taking the affine chart.

Equations

• CCDN.projectiveHypersurfaceChart k f = CCDN.projectiveChart k f

theorem CCDN.projective_hypersurface_local_det_divisibility {p n μ s d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hfhom : f.IsHomogeneous d) (F : Fin s → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin s), (F j).IsHomogeneous M) (z : Fin s → Fin (n + 3) → ℤ) (k : Fin (n + 3)) (a : Fin (n + 2) → ℤ) (hf : (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) (projectiveHypersurfaceChart k f)) ∈ MvPolynomial.idealOfVars (Fin (n + 2)) (ZMod p) ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift a) (projectiveHypersurfaceChart k f))) ≠ 0) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i k)) (hres : ∀ (i : Fin s) (j : Fin (n + 2)), ↑p ∣ z i ((Equiv.swap 0 k) j.succ) - a j * z i k) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : ↑p ^ hypersurfaceMultiplicityExponent (n + 1) μ s ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (z i)) (F j)).det

The local projective divisor is available in every coordinate chart.

theorem CCDN.projective_hypersurface_residue_minorGcd {p n c s N d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 3)) ℤ) (hfhom : f.IsHomogeneous d) (F : Fin N → MvPolynomial (Fin (n + 3)) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → Fin (n + 3) → ℤ) (label : Fin s → Fin c) (k : Fin c → Fin (n + 3)) (a : Fin c → Fin (n + 2) → ℤ) (μ : Fin c → ℕ) (hf : ∀ (i : Fin c), (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (a i)) (projectiveHypersurfaceChart (k i) f)) ∈ MvPolynomial.idealOfVars (Fin (n + 2)) (ZMod p) ^ μ i) (hμ : ∀ (i : Fin c), (MvPolynomial.homogeneousComponent (μ i)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (a i)) (projectiveHypersurfaceChart (k i) f))) ≠ 0) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i (k (label i)))) (hres : ∀ (i : Fin s) (j : Fin (n + 2)), ↑p ∣ z i ((Equiv.swap 0 (k (label i))) j.succ) - a (label i) j * z i (k (label i))) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : ↑p ^ ∑ i : Fin c, hypersurfaceMultiplicityExponent (n + 1) (μ i) (Fintype.card { j : Fin s // label j = i }) ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j))

Assemble local projective residue classes in their own coordinate charts. Every maximal minor acquires the sum of their local multiplicity exponents.