Local divisibility for homogeneous evaluation matrices at projective points. Normalize a unit coordinate modulo the required prime power, apply the singular affine estimate to the resulting approximate zeros, then cancel the invertible row factors.

theorem CCDN.dvd_eval_sub_of_dvd_coordinates {σ : Type u_1} (q : ℤ) (x y : σ → ℤ) (hxy : ∀ (j : σ), q ∣ x j - y j) (f : MvPolynomial σ ℤ) : q ∣ (MvPolynomial.eval x) f - (MvPolynomial.eval y) f

If x ≡ y coordinatewise modulo q, then f(x) ≡ f(y) modulo q for every integer polynomial f.

theorem CCDN.exists_integer_inverse_of_isCoprime {q a : ℤ} (h : IsCoprime q a) : ∃ (u : ℤ), q ∣ u * a - 1 ∧ IsCoprime q u

An integer a coprime to q has an inverse u modulo q, itself coprime to q.

theorem CCDN.projective_chart_eval_congr {n M : ℕ} {q u : ℤ} (z : Fin (n + 1) → ℤ) (hu : q ∣ u * z 0 - 1) (F : MvPolynomial (Fin (n + 1)) ℤ) (hF : F.IsHomogeneous M) : q ∣ (MvPolynomial.eval fun (j : Fin n) => u * z j.succ) ((affineChart n) 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_chart_det_divisibility_of_affine {p n s d M e : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hfhom : f.IsHomogeneous d) (F : Fin s → MvPolynomial (Fin (n + 1)) ℤ) (hF : ∀ (j : Fin s), (F j).IsHomogeneous M) (z : Fin s → Fin (n + 1) → ℤ) (a : Fin n → ℤ) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i 0)) (hres : ∀ (i : Fin s) (j : Fin n), ↑p ∣ z i j.succ - a j * z i 0) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) (haffine : ∀ (x : Fin s → Fin n → ℤ), (∀ (i : Fin s) (j : Fin n), ↑p ∣ x i j - a j) → (∀ (i : Fin s), ↑p ^ e ∣ (MvPolynomial.eval (x i)) ((affineChart n) f)) → ∀ (G : Fin s → MvPolynomial (Fin n) ℤ), ↑p ^ e ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (G j)).det) : ↑p ^ e ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (z i)) (F j)).det

An affine determinant bound modulo p ^ e transfers to homogeneous evaluations when the first coordinate is a unit. The exponent is unchanged.

noncomputable def CCDN.projectiveChart {n : ℕ} (k : Fin (n + 1)) (f : MvPolynomial (Fin (n + 1)) ℤ) : MvPolynomial (Fin n) ℤ

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

Equations

• CCDN.projectiveChart k f = (CCDN.affineChart n) ((MvPolynomial.rename ⇑(Equiv.swap 0 k)) f)

theorem CCDN.projective_local_det_divisibility_of_affine {p n s d M e : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hfhom : f.IsHomogeneous d) (F : Fin s → MvPolynomial (Fin (n + 1)) ℤ) (hF : ∀ (j : Fin s), (F j).IsHomogeneous M) (z : Fin s → Fin (n + 1) → ℤ) (k : Fin (n + 1)) (a : Fin n → ℤ) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i k)) (hres : ∀ (i : Fin s) (j : Fin n), ↑p ∣ z i ((Equiv.swap 0 k) j.succ) - a j * z i k) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) (haffine : ∀ (x : Fin s → Fin n → ℤ), (∀ (i : Fin s) (j : Fin n), ↑p ∣ x i j - a j) → (∀ (i : Fin s), ↑p ^ e ∣ (MvPolynomial.eval (x i)) (projectiveChart k f)) → ∀ (G : Fin s → MvPolynomial (Fin n) ℤ), ↑p ^ e ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (G j)).det) : ↑p ^ e ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (z i)) (F j)).det

Transfer an affine determinant bound in any coordinate chart, with its exact exponent.

theorem CCDN.projective_residue_minorGcd_of_affine {p n c s N d M : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hfhom : f.IsHomogeneous d) (F : Fin N → MvPolynomial (Fin (n + 1)) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → Fin (n + 1) → ℤ) (label : Fin s → Fin c) (k : Fin c → Fin (n + 1)) (a : Fin c → Fin n → ℤ) (e : Fin c → ℕ) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i (k (label i)))) (hres : ∀ (i : Fin s) (j : Fin n), ↑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) (haffine : ∀ (i : Fin c) (x : Fin (Fintype.card { j : Fin s // label j = i }) → Fin n → ℤ), (∀ (r : Fin (Fintype.card { j : Fin s // label j = i })) (j : Fin n), ↑p ∣ x r j - a i j) → (∀ (r : Fin (Fintype.card { j : Fin s // label j = i })), ↑p ^ e i ∣ (MvPolynomial.eval (x r)) (projectiveChart (k i) f)) → ∀ (G : Fin (Fintype.card { j : Fin s // label j = i }) → MvPolynomial (Fin n) ℤ), ↑p ^ e i ∣ (Matrix.of fun (r j : Fin (Fintype.card { j : Fin s // label j = i })) => (MvPolynomial.eval (x r)) (G j)).det) : ↑p ^ ∑ i : Fin c, e i ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j))

Assemble affine bounds in separate projective charts into the common minor divisor. Each residue class retains the exponent supplied by its own affine bound.

noncomputable def CCDN.projectivePlaneChart (k : Fin 3) (f : MvPolynomial (Fin 3) ℤ) : MvPolynomial (Fin 2) ℤ

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

Equations

• CCDN.projectivePlaneChart k f = CCDN.projectiveChart k f

theorem CCDN.projective_plane_residue_minorGcd {p c s N d M : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 3) ℤ) (hfhom : f.IsHomogeneous d) (F : Fin N → MvPolynomial (Fin 3) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → Fin 3 → ℤ) (label : Fin s → Fin c) (k : Fin c → Fin 3) (a : Fin c → Fin 2 → ℤ) (μ : Fin c → ℕ) (hf : ∀ (i : Fin c), (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (a i)) (projectivePlaneChart (k i) f)) ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ μ i) (hμ : ∀ (i : Fin c), (MvPolynomial.homogeneousComponent (μ i)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (a i)) (projectivePlaneChart (k i) f))) ≠ 0) (hunit : ∀ (i : Fin s), IsCoprime (↑p) (z i (k (label i)))) (hres : ∀ (i : Fin s) (j : Fin 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, multiplicityExponent (Fintype.card { j : Fin s // label j = i }) (μ 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.