The Moore determinant

The two main theorems. GranvilleMoore.Ladder factors the Moore determinant as p^C(d+1,3) times the determinant of the last rung L_{d-1} of the reduction ladder; GranvilleMoore.MasterExpansion makes every entry of that rung an integer and pins it down modulo p; and GranvilleMoore.VandermondeReduction evaluates the resulting determinant. Putting the three together gives the exact power of p dividing the Moore determinant.

Main results

• GranvilleMoore.exists_intCast_det_ladderMatrix_last: det L_{d-1} ∈ ℤ for d ≤ p.
• GranvilleMoore.prod_factorial_mul_intCast_det_ladderMatrix_last: for d ≤ p - 1, (∏_i i!) det L_{d-1} ≡ (∏_j x_j) ∏_{i<j} (q_p(x_j) - q_p(x_i)) modulo p.
• GranvilleMoore.prod_factorial_mul_intCast_det_ladderMatrix_last_of_eq: the same identity at the boundary d = p, where the exceptional Fermat congruence is consumed.
• GranvilleMoore.not_dvd_det_ladderMatrix_last_iff: for d ≤ p, p ∤ det L_{d-1} exactly when the residues q_p(x_j) are pairwise distinct modulo p.
• GranvilleMoore.det_mooreMatrix_eq_pow_mul: the factorisation GranvilleMoore.det_mooreMatrix_eq_pow_mul_det_ladderMatrix as an identity in ℤ, det M = p^C(d+1,3) * det L_{d-1}.
• GranvilleMoore.pow_dvd_det_mooreMatrix (thm_lower_bound) and GranvilleMoore.not_pow_succ_dvd_det_mooreMatrix_iff (thm_main): the lower bound and the equality criterion.

Implementation notes

Both main theorems are usually phrased as statements about v_p(det M). They are stated here as divisibilities in ℤ instead: p^C(d+1,3) ∣ det M for the bound, and ¬ p^{C(d+1,3)+1} ∣ det M for equality. The reason is the one recorded in the implementation notes of GranvilleMoore.CollapsedCoeff and GranvilleMoore.MasterExpansion: padicValRat p 0 = 0, so a valuation inequality says nothing at a vanishing argument and would silently hold for the wrong reason. The divisibility form is unconditional, says exactly what v_p ≥ C(d+1,3) and v_p = C(d+1,3) mean for a nonzero determinant, and is what the equality theorem needs anyway.

The standing hypotheses d ≥ 1 and det M ≠ 0 of the paper are kept, so that the two main theorems read exactly as it states them, but in the divisibility form neither is needed; they are named with a leading underscore to record that. Nothing is lost at det M = 0: there det L_{d-1} = 0, so p ∣ det L_{d-1} and the equivalence of GranvilleMoore.not_pow_succ_dvd_det_mooreMatrix_iff holds with both of its sides false.

The objects that are ℚ-valued by definition — det L_{d-1} and the Fermat quotients q_p(x_j) — are handled by the house convention of GranvilleMoore.UnitQuotient: the representing integers D and q j are taken as arguments together with the hypotheses identifying them, so that no cast appears inside a proof. The congruences are stated as equalities in ZMod p rather than as divisibilities in ℤ, because GranvilleMoore.det_of_eq_mul_pow and GranvilleMoore.det_of_eq_mul_pow_ne_zero_iff are about a matrix over a commutative ring and ZMod p is the ring in question; over an integral domain the vanishing criterion is then immediate.

Rescaling row r of the reduced rung by r! is done in one stroke with Matrix.det_mul_column, which — despite its name — scales rows; see the implementation notes of GranvilleMoore.VandermondeReduction.

References

• A. Granville, The p-divisibility of the integer Moore determinant and iterated Fermat quotients.

Integrality of the last ladder determinant

theorem GranvilleMoore.exists_intCast_det_ladderMatrix_last {p d : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (hdp : d ≤ p) {x : Fin d → ℤ} (hx : ∀ (j : Fin d), ¬↑p ∣ x j) : ∃ (D : ℤ), (ladderMatrix p x (d - 1)).det = ↑D

Integrality of the last ladder determinant (lem_ladder_last_integral): for an odd prime p, d ≤ p and integers x_j prime to p, the determinant of the last rung of the ladder is an integer.

Integrality is phrased as the existence of an integer whose cast is the value, matching GranvilleMoore.exists_intCast_iteratedFermatQuot. Every entry of L (d-1) is an iterated Fermat quotient of superscript at most p - 1, hence an integer, and a determinant is a polynomial with integer coefficients in its entries.

The entries of the last rung modulo p

The last rung is Vandermonde modulo p

theorem GranvilleMoore.prod_factorial_mul_intCast_det_ladderMatrix_last {p d : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (_hd : 1 ≤ d) (hdp : d ≤ p - 1) {x : Fin d → ℤ} (hx : ∀ (j : Fin d), ¬↑p ∣ x j) {D : ℤ} (hD : (ladderMatrix p x (d - 1)).det = ↑D) {q : Fin d → ℤ} (hq : ∀ (j : Fin d), fermatQuotient p (x j) = ↑(q j)) : (∏ i : Fin d, ↑(↑i).factorial) * ↑D = (∏ j : Fin d, ↑(x j)) * ∏ i : Fin d, ∏ j > i, (↑(q j) - ↑(q i))

The last ladder matrix is Vandermonde modulo p (lem_ladder_last_vandermonde): for an odd prime p, 1 ≤ d ≤ p - 1 and integers x_j prime to p,

(∏_i i!) det L_{d-1} ≡ (∏_j x_j) ∏_{i<j} (q_p(x_j) - q_p(x_i))  (mod p) .

The congruence is stated as an equality in ZMod p between the images of the integer D representing det L_{d-1} and of the integers q j representing q_p(x_j).

Since every row index r satisfies r ≤ d - 1 ≤ p - 2, GranvilleMoore.dvd_factorial_mul_sub_mul_pow applies to every entry; scaling row r by r! therefore turns the reduction of L (d-1) into the matrix with entries x_j q_p(x_j)^r, which is the shape GranvilleMoore.det_of_eq_mul_pow evaluates.

theorem GranvilleMoore.prod_factorial_mul_intCast_det_ladderMatrix_last_of_eq {p d : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (hdp : d = p) {x : Fin d → ℤ} (hx : ∀ (j : Fin d), ¬↑p ∣ x j) {D : ℤ} (hD : (ladderMatrix p x (d - 1)).det = ↑D) {q : Fin d → ℤ} (hq : ∀ (j : Fin d), fermatQuotient p (x j) = ↑(q j)) : (∏ i : Fin d, ↑(↑i).factorial) * ↑D = (∏ j : Fin d, ↑(x j)) * ∏ i : Fin d, ∏ j > i, (↑(q j) - ↑(q i))

The last ladder determinant at d = p (lem_ladder_last_vandermonde_eq_p): the conclusion of GranvilleMoore.prod_factorial_mul_intCast_det_ladderMatrix_last continues to hold at the boundary d = p, with the same scaling factor ∏_i i!.

This is where GranvilleMoore.dvd_factorial_mul_sub_exceptional is consumed. The rows r ≤ p - 2 behave as before, but the bottom row has r = p - 1 and k = 0, the one pair at which the master expansion has a second surviving term: there (p-1)! F⁽ᵖ⁻¹⁾_0(x_j) ≡ x_j q_p(x_j)^{p-1} - x_j q_p(x_j). So the rescaled matrix is the Vandermonde shape with its bottom row replaced by the bottom row minus the row of index 1, and GranvilleMoore.det_of_eq_mul_pow_updateRow_sub says that this row operation changes nothing. A weaker form allows an unspecified unit ε in place of ∏_i i!; the sharp form of the exceptional congruence makes ε = ∏_i i! exactly.

The last ladder determinant is a unit exactly when the quotients are distinct

theorem GranvilleMoore.not_dvd_det_ladderMatrix_last_iff {p d : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (hd : 1 ≤ d) (hdp : d ≤ p) {x : Fin d → ℤ} (hx : ∀ (j : Fin d), ¬↑p ∣ x j) {D : ℤ} (hD : (ladderMatrix p x (d - 1)).det = ↑D) {q : Fin d → ℤ} (hq : ∀ (j : Fin d), fermatQuotient p (x j) = ↑(q j)) : ¬↑p ∣ D ↔ Function.Injective fun (j : Fin d) => ↑(q j)

The last ladder determinant is a unit exactly when the quotients are distinct (lem_ladder_last_nonzero): for an odd prime p, 1 ≤ d ≤ p and integers x_j prime to p, p ∤ det L_{d-1} if and only if the residues q_p(x_1), …, q_p(x_d) are pairwise distinct modulo p.

Pairwise distinctness is phrased as injectivity of j ↦ q_p(x_j) in ZMod p.

Both scaling factors of the two preceding lemmas are units modulo p: each i! with i ≤ d - 1 ≤ p - 1 is prime to p by Nat.Prime.dvd_factorial, and each x_j is prime to p by hypothesis. So the residue of det L_{d-1} is nonzero exactly when the Vandermonde product is, and GranvilleMoore.det_of_eq_mul_pow_ne_zero_iff — over the field ZMod p, which is a domain — turns that into injectivity.

The exact power of p in the Moore determinant

theorem GranvilleMoore.det_mooreMatrix_eq_pow_mul {p d : ℕ} (hp : Nat.Prime p) {x : Fin d → ℤ} {D : ℤ} (hD : (ladderMatrix p x (d - 1)).det = ↑D) : (mooreMatrix p x).det = ↑p ^ (d + 1).choose 3 * D

Factoring the Moore determinant, in ℤ: det M = p^C(d+1,3) det L_{d-1}, with det L_{d-1} the integer D of GranvilleMoore.exists_intCast_det_ladderMatrix_last.

This is GranvilleMoore.det_mooreMatrix_eq_pow_mul_det_ladderMatrix, which lives in ℚ because the ladder does, pushed back down to ℤ by injectivity of the cast. Both main theorems read off this identity.

theorem GranvilleMoore.pow_dvd_det_mooreMatrix {p d : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (_hd : 1 ≤ d) (hdp : d ≤ p) {x : Fin d → ℤ} (hx : ∀ (j : Fin d), ¬↑p ∣ x j) (_hdet : (mooreMatrix p x).det ≠ 0) : ↑p ^ (d + 1).choose 3 ∣ (mooreMatrix p x).det

The lower bound (thm_lower_bound): for an odd prime p, 1 ≤ d ≤ p and integers x_j prime to p with det M_p(x) ≠ 0, the power p^C(d+1,3) divides det M_p(x).

This is usually stated as v_p(det M) ≥ C(d+1,3); the divisibility is the same assertion for a nonzero determinant and does not degenerate at 0, see the implementation notes, which also explain why 1 ≤ d and det M ≠ 0 are carried but unused.

GranvilleMoore.det_mooreMatrix_eq_pow_mul exhibits det M as p^C(d+1,3) times the integer D of GranvilleMoore.exists_intCast_det_ladderMatrix_last, which is the divisibility.

theorem GranvilleMoore.not_pow_succ_dvd_det_mooreMatrix_iff {p d : ℕ} (hp : Nat.Prime p) (hodd : Odd p) (hd : 1 ≤ d) (hdp : d ≤ p) {x : Fin d → ℤ} (hx : ∀ (j : Fin d), ¬↑p ∣ x j) {q : Fin d → ℤ} (hq : ∀ (j : Fin d), fermatQuotient p (x j) = ↑(q j)) (_hdet : (mooreMatrix p x).det ≠ 0) : ¬↑p ^ ((d + 1).choose 3 + 1) ∣ (mooreMatrix p x).det ↔ Function.Injective fun (j : Fin d) => ↑(q j)

Equality in the Moore determinant bound (thm_main): for an odd prime p, 1 ≤ d ≤ p and integers x_j prime to p with det M_p(x) ≠ 0, the exact power of p dividing det M_p(x) is C(d+1,3) — that is, p^{C(d+1,3)+1} does not divide it — if and only if the residues q_p(x_1), …, q_p(x_d) are pairwise distinct modulo p.

This is usually stated as v_p(det M) = C(d+1,3); together with GranvilleMoore.pow_dvd_det_mooreMatrix the failure of the next divisibility is the same assertion, and it does not degenerate at 0, see the implementation notes, which also explain why det M ≠ 0 is carried but unused. Pairwise distinctness of the residues is phrased as injectivity of j ↦ q_p(x_j) in ZMod p, as in GranvilleMoore.not_dvd_det_ladderMatrix_last_iff.

By GranvilleMoore.det_mooreMatrix_eq_pow_mul, det M = p^C(d+1,3) D, so one further power of p divides det M exactly when p ∣ D; the claim is therefore GranvilleMoore.not_dvd_det_ladderMatrix_last_iff. The range is the paper's d ≤ p, the boundary case d = p being covered by GranvilleMoore.prod_factorial_mul_intCast_det_ladderMatrix_last_of_eq.