The unit quotient #

The integrality of the Fermat quotient and of the unit quotient, and the congruence between them. For a prime p not dividing x, Fermat's little theorem says that the unit t_x = x ^ (p - 1) is a principal unit at p, so q_p(x) = (t_x - 1) / p is an integer. For an odd prime, lifting the exponent upgrades this to p ^ (k + 1) ∣ t_x ^ (p ^ k) - 1, which makes the unit quotient g_k(x) = (t_x ^ (p ^ k) - 1) / p ^ (k + 1) an integer as well; and a binomial expansion along the tower shows g_k(x) ≡ q_p(x) modulo p for every k.

Main results #

GranvilleMoore.dvd_fermatUnit_sub_one: p ∣ t_x - 1, the unit is principal.
GranvilleMoore.fermatQuotient_eq_intCast: q_p(x) is an integer.
GranvilleMoore.pow_dvd_fermatUnit_pow_sub_one: p ^ (k + 1) ∣ t_x ^ (p ^ k) - 1 for odd p, by lifting the exponent.
GranvilleMoore.unitQuot_eq_intCast: g_k(x) is an integer.
GranvilleMoore.fermatUnit_pow_eq_one_add_pow_mul: the expansion t_x ^ (p ^ k) = 1 + p ^ (k + 1) g_k(x), as an identity in ℤ.
GranvilleMoore.dvd_unitQuot_sub_fermatQuotient: g_k(x) ≡ q_p(x) modulo p.

Implementation notes #

fermatQuotient and unitQuot are ℚ-valued, so "is an integer" is stated as the existence of an integer whose cast is the value. The statements that consume those integers therefore take them as arguments together with the hypothesis identifying them, e.g. fermatUnit_pow_eq_one_add_pow_mul takes hg : unitQuot p x k = (g : ℚ); the integer is unique, so this loses nothing and keeps every downstream statement inside ℤ.

The inductive step of dvd_unitQuot_sub_fermatQuotient is isolated as one_add_pow_eq_of_pow_dvd, a statement about an arbitrary A divisible by p ^ n: the binomial expansion of (1 + A) ^ p is 1 + p A up to p ^ (n + 2). Stating it that way avoids truncated subtraction in the exponents that appear in the paper's proof.

Integrality of the Fermat quotient #

source

theorem GranvilleMoore.dvd_fermatUnit_sub_one {p : ℕ} (hp : Nat.Prime p) {x : ℤ} (hx : ¬↑p ∣ x) :

↑p ∣ fermatUnit p x - 1

The unit is principal: for a prime p with p ∤ x, p divides t_x - 1.

This is Fermat's little theorem in the form the Frobenius tower uses: t_x = x ^ (p - 1) is congruent to 1 modulo p, so it is a principal unit at p.

source

theorem GranvilleMoore.fermatQuotient_eq_intCast {p : ℕ} (hp : Nat.Prime p) {x : ℤ} (hx : ¬↑p ∣ x) :

∃ (q : ℤ), fermatQuotient p x = ↑q

The Fermat quotient is an integer: for a prime p with p ∤ x the rational number q_p(x) is the cast of an integer.

Integrality is phrased as the existence of an integer q with q_p(x) = q, since fermatQuotient is ℚ-valued by definition.

source

theorem GranvilleMoore.not_dvd_fermatUnit {p : ℕ} (hp : Nat.Prime p) {x : ℤ} (hx : ¬↑p ∣ x) :

¬↑p ∣ fermatUnit p x

The unit t_x = x ^ (p - 1) is prime to p whenever x is: a prime dividing a power divides the base.

Divisibility along the Frobenius tower #

source

theorem GranvilleMoore.pow_dvd_fermatUnit_pow_sub_one {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {x : ℤ} (hx : ¬↑p ∣ x) (k : ℕ) :

↑p ^ (k + 1) ∣ fermatUnit p x ^ p ^ k - 1

Divisibility of the Frobenius power of the unit: for an odd prime p with p ∤ x, p ^ (k + 1) divides t_x ^ (p ^ k) - 1.

This is lifting the exponent applied to t_x and 1: the p-adic valuation of t_x ^ (p ^ k) - 1 exceeds that of t_x - 1 by exactly k, and t_x - 1 is already divisible by p by GranvilleMoore.dvd_fermatUnit_sub_one.

source

theorem GranvilleMoore.unitQuot_eq_intCast {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) {x : ℤ} (hx : ¬↑p ∣ x) (k : ℕ) :

∃ (g : ℤ), unitQuot p x k = ↑g

The unit quotient is an integer: for an odd prime p with p ∤ x the rational number g_k(x) is the cast of an integer.

The numerator of GranvilleMoore.unitQuot is divisible by the denominator p ^ (k + 1) by GranvilleMoore.pow_dvd_fermatUnit_pow_sub_one.

source

theorem GranvilleMoore.fermatUnit_pow_eq_one_add_pow_mul {p : ℕ} (hp : p ≠ 0) {x : ℤ} {k : ℕ} {g : ℤ} (hg : unitQuot p x k = ↑g) :

fermatUnit p x ^ p ^ k = 1 + ↑p ^ (k + 1) * g

Expansion of the Frobenius power of the unit, over ℤ: t_x ^ (p ^ k) = 1 + p ^ (k + 1) g_k(x).

GranvilleMoore.pow_eq_one_add_pow_mul_unitQuot is this identity in ℚ; combined with an integer g representing g_k(x) — which exists by GranvilleMoore.unitQuot_eq_intCast — it becomes an identity between integers, which is the form consumers of the tower use. Only p ≠ 0 is needed: the hypotheses making g exist are carried by hg.