The Moore matrix and the reduction ladder

The two matrices whose determinants the main theorems compare: the Moore matrix, whose determinant is the object of study, and the ladder of matrices interpolating between it and a matrix of iterated Fermat quotients.

Main definitions

• GranvilleMoore.mooreMatrix p x: the Moore matrix of x = (x 1, …, x d), whose (i, j) entry is x j ^ p ^ i. Rows are indexed by the Frobenius level i and columns by the point j, so this is the paper's (i, j) entry x_j ^ (p ^ (i - 1)) under the shift from 1-based to 0-based indices.
• GranvilleMoore.ladderMatrix p x i: the i-th matrix L i of the reduction ladder, the matrix over ℚ whose rows are the vectors of iterated Fermat quotients F⁽⁰⁾_0, F⁽¹⁾_0, …, F⁽ⁱ⁾_0, F⁽ⁱ⁾_1, …, F⁽ⁱ⁾_(d - 1 - i) evaluated at x.

Implementation notes

The row of ladderMatrix p x i at index r is F⁽ᵃ⁾_b with (a, b) = (min r i, r - i): the superscript grows along the first i + 1 rows and the subscript grows along the remaining ones, with truncated subtraction on ℕ performing the case split. The two regimes are ladderMatrix_row_of_le and ladderMatrix_row_of_ge, which are the lemmas to use in place of unfolding.

The Moore matrix is defined over any monoid, since its entries are powers and nothing else is needed; the paper's integer matrix is the case R = ℤ, and mooreMatrix_map is the passage to its image over ℚ, where the ladder lives. Neither definition needs p prime, d ≥ 1, or i ≤ d - 1: the standing hypotheses of the paper belong to the results about these matrices, not to the constructions. For d ≤ i + 1 the ladder has stabilised, every row then falling in the first regime.

References

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

The Moore matrix

def GranvilleMoore.mooreMatrix {R : Type u_1} {d : ℕ} [Monoid R] (p : ℕ) (x : Fin d → R) : Matrix (Fin d) (Fin d) R

The Moore matrix of x = (x 1, …, x d) at p: the d × d matrix whose (i, j) entry is x j ^ p ^ i, so that its i-th row is the image of x under the i-th iterate of the p-power map.

Equations

• GranvilleMoore.mooreMatrix p x = Matrix.of fun (i j : Fin d) => x j ^ p ^ ↑i

@[simp]

theorem GranvilleMoore.mooreMatrix_apply {R : Type u_1} {d : ℕ} [Monoid R] (p : ℕ) (x : Fin d → R) (i j : Fin d) : mooreMatrix p x i j = x j ^ p ^ ↑i

The (i, j) entry of the Moore matrix is x j ^ p ^ i.

theorem GranvilleMoore.mooreMatrix_apply_zero {R : Type u_1} {d : ℕ} [Monoid R] (p : ℕ) (x : Fin (d + 1) → R) (j : Fin (d + 1)) : mooreMatrix p x 0 j = x j

The first row of the Moore matrix is x itself.

theorem GranvilleMoore.mooreMatrix_succ_apply {R : Type u_1} {d : ℕ} [Monoid R] (p : ℕ) (x : Fin (d + 1) → R) (i : Fin d) (j : Fin (d + 1)) : mooreMatrix p x i.succ j = mooreMatrix p x i.castSucc j ^ p

Each row of the Moore matrix is the p-th power of the preceding one.

theorem GranvilleMoore.mooreMatrix_map {R : Type u_1} {S : Type u_2} {d : ℕ} [Monoid R] [Monoid S] (p : ℕ) (x : Fin d → R) (f : R →* S) : (mooreMatrix p x).map ⇑f = mooreMatrix p fun (j : Fin d) => f (x j)

Forming the Moore matrix commutes with applying a monoid homomorphism entrywise; this is the passage from the integer Moore matrix to its image over ℚ.

The reduction ladder

def GranvilleMoore.ladderMatrix {d : ℕ} (p : ℕ) (x : Fin d → ℤ) (i : ℕ) : Matrix (Fin d) (Fin d) ℚ

The i-th matrix L i of the reduction ladder of x = (x 1, …, x d) at p: the d × d matrix over ℚ whose rows are, in order, the vectors of iterated Fermat quotients F⁽⁰⁾_0, F⁽¹⁾_0, …, F⁽ⁱ⁾_0, F⁽ⁱ⁾_1, …, F⁽ⁱ⁾_(d - 1 - i) evaluated at x; that is, the row at index r is fun j => iteratedFermatQuot p a b (x j) with (a, b) = (min r i, r - i).

Equations

• GranvilleMoore.ladderMatrix p x i = Matrix.of fun (r j : Fin d) => GranvilleMoore.iteratedFermatQuot p (min (↑r) i) (↑r - i) (x j)

@[simp]

theorem GranvilleMoore.ladderMatrix_apply {d : ℕ} (p : ℕ) (x : Fin d → ℤ) (i : ℕ) (r j : Fin d) : ladderMatrix p x i r j = iteratedFermatQuot p (min (↑r) i) (↑r - i) (x j)

The (r, j) entry of L i is F⁽ᵃ⁾_b (x j) with (a, b) = (min r i, r - i).

theorem GranvilleMoore.ladderMatrix_row {d : ℕ} (p : ℕ) (x : Fin d → ℤ) (i : ℕ) (r : Fin d) : ladderMatrix p x i r = fun (j : Fin d) => iteratedFermatQuot p (min (↑r) i) (↑r - i) (x j)

The row at index r of L i is the vector F⁽ᵃ⁾_b at x with (a, b) = (min r i, r - i).

theorem GranvilleMoore.ladderMatrix_row_of_le {d p : ℕ} {x : Fin d → ℤ} {i : ℕ} {r : Fin d} (h : ↑r ≤ i) : ladderMatrix p x i r = fun (j : Fin d) => iteratedFermatQuot p (↑r) 0 (x j)

The first i + 1 rows of L i carry the growing superscript: the row at index r ≤ i is F⁽ʳ⁾_0.

theorem GranvilleMoore.ladderMatrix_row_of_ge {d p : ℕ} {x : Fin d → ℤ} {i : ℕ} {r : Fin d} (h : i ≤ ↑r) : ladderMatrix p x i r = fun (j : Fin d) => iteratedFermatQuot p i (↑r - i) (x j)

The last d - 1 - i rows of L i carry the growing subscript: the row at index r ≥ i is F⁽ⁱ⁾_(r - i).