Local determinant divisibility in arbitrary dimension. The exponent is computed from the cumulative dimensions of the origin-adic layers.

def CCDN.filtrationExponent (r : ℕ → ℕ) (s : ℕ) : ℕ

The sum of the deficits below successive weights. For a graded profile this is a lower bound for the sum of the first s weights, with multiplicity.

Equations

• CCDN.filtrationExponent r s = ∑ k : Fin s, (s - ∑ j : Fin (↑k + 1), r ↑j)

theorem CCDN.sum_weight_tail_counts_le {s : ℕ} (w : Fin s → ℕ) (K : ℕ) : ∑ k : Fin K, {i : Fin s | ↑k < w i}.card ≤ ∑ i : Fin s, w i

Layer-cake inequality with an arbitrary cutoff K: counting, for each k < K, the weights exceeding k never exceeds the total weight.

theorem CCDN.low_weight_card_le {s N : ℕ} (r : ℕ → ℕ) (t : Fin s ↪ (j : Fin N) × Fin (r ↑j)) (k : ℕ) : {i : Fin s | ↑(t i).fst ≤ k}.card ≤ ∑ j : Fin (k + 1), r ↑j

Distinct generators of weight at most k inject into all generators in layers zero through k, independently of the precision used to truncate them.

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

Cauchy--Binet for a finite set of generators indexed in any way.

theorem CCDN.origin_filtration_pow_dvd_det_mod {p n s e : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin (n + 1)) ℤ) (x : Fin s → Fin (n + 1) → ℤ) (hx : ∀ (i : Fin s) (j : Fin (n + 1)), ↑p ∣ x i j) (he : e ≤ filtrationExponent (fun (k : ℕ) => Module.finrank (ZMod p) ↥(originLayer ((MvPolynomial.map (Int.castRingHom (ZMod p))) f) k)) s) (hfx : ∀ (i : Fin s), ↑p ^ e ∣ (MvPolynomial.eval (x i)) f) (F : Fin s → MvPolynomial (Fin (n + 1)) ℤ) : ↑p ^ e ∣ (Matrix.of fun (i j : Fin s) => (MvPolynomial.eval (x i)) (F j)).det

A homogeneous local generating family gives a determinant divisor at any precision and in any dimension.