Determinant divisibility from filtered factorizations

Cauchy–Binet turns a weighted factorization into a determinant valuation bound. The univariate specialization gives the quadratic exponent s*(s-1)/2 for polynomial evaluations in one residue class. The passage from a curve's local ring to such a factorization is proved in FilteredDeterminant in arbitrary ambient dimension. HypersurfaceResidue supplies the sharp singular hypersurface bound.

theorem CCDN.pow_dvd_det_of_weighted_factorization {R : Type u_1} [CommRing R] {s N : ℕ} (U : Matrix (Fin s) (Fin N) R) (V : Matrix (Fin N) (Fin s) R) (p : R) (weight : Fin N → ℕ) (e : ℕ) (hV : ∀ (i : Fin N) (j : Fin s), p ^ weight i ∣ V i j) (he : ∀ (t : Fin s ↪o Fin N), e ≤ ∑ i : Fin s, weight (t i)) : p ^ e ∣ (U * V).det

Cauchy–Binet valuation bound: if p ^ weight i divides the i-th row of V, and every choice of s increasing row indices has total weight at least e, then p ^ e divides det (U * V).

def CCDN.multiplicityExponent (s μ : ℕ) : ℕ

The sum ∑_{i < s} ⌊i / μ⌋ of the first s terms of the weight sequence in which each nonnegative integer occurs μ times.

Equations

• CCDN.multiplicityExponent s μ = ∑ i : Fin s, ↑i / μ

theorem CCDN.multiplicity_pow_dvd_det_of_factorization {R : Type u_1} [CommRing R] {s N : ℕ} (U : Matrix (Fin s) (Fin N) R) (V : Matrix (Fin N) (Fin s) R) (p : R) (μ : ℕ) (hV : ∀ (i : Fin N) (j : Fin s), p ^ (↑i / μ) ∣ V i j) : p ^ multiplicityExponent s μ ∣ (U * V).det

If p ^ ⌊i / μ⌋ divides the i-th row of V, then p ^ multiplicityExponent s μ divides det (U * V).

theorem CCDN.multiplicityExponent_lower_bound (s μ : ℕ) (hμ : 0 < μ) : s ^ 2 ≤ 2 * μ * (multiplicityExponent s μ + s)

An explicit quadratic lower estimate for the repeated-weight exponent.