The defining identity of the Fermat quotient and the Frobenius exponent

This file proves the three basic identities that make the definitions of GranvilleMoore.Defs.TheFermatQuotient usable without unfolding them.

Main results

• GranvilleMoore.fermatUnit_eq_one_add_natCast_mul_fermatQuotient: the defining identity t_x = 1 + p * q_p(x), an equation in ℚ.
• GranvilleMoore.sub_one_mul_frobeniusExponent: the closed form (p - 1) * e_k = p ^ k - 1 of the Frobenius exponent, together with the subtraction-free GranvilleMoore.sub_one_mul_frobeniusExponent_add_one.
• GranvilleMoore.pow_pow_eq_mul_pow_frobeniusExponent: the reason e_k is the exponent it is, namely x ^ p ^ k = x * (x ^ (p - 1)) ^ e_k.

Implementation notes

The defining identity is stated in ℚ, where fermatQuotient lives, and so needs only p ≠ 0: the hypothesis p ∤ x is what makes q_p(x) an integer, which is a separate statement about the same rational number and not part of this identity.

The closed form (p - 1) * e_k = p ^ k - 1 is stated in ℕ with truncated subtraction and needs no hypothesis at all — at p = 0 both sides vanish. Consumers who want to move the - 1 across should use sub_one_mul_frobeniusExponent_add_one, which is where the hypothesis p ≠ 0 is genuinely needed.

pow_pow_eq_mul_pow_frobeniusExponent is stated for an arbitrary monoid, since nothing in it is about ℤ. For x : ℤ its right-hand side is x * fermatUnit p x ^ frobeniusExponent p k, fermatUnit being reducible.

The defining identity

theorem GranvilleMoore.fermatUnit_eq_one_add_natCast_mul_fermatQuotient {p : ℕ} (hp : p ≠ 0) (x : ℤ) : ↑(fermatUnit p x) = 1 + ↑p * fermatQuotient p x

The defining identity of the Fermat quotient: t_x = 1 + p * q_p(x).

This is the equation of GranvilleMoore.fermatQuotient multiplied by p with 1 added to both sides, and it is the form in which consumers use the Fermat quotient. It is an identity in ℚ; that both sides are integers when p ∤ x is the separate integrality statement.

The closed form of the Frobenius exponent

theorem GranvilleMoore.sub_one_mul_frobeniusExponent_add_one {p : ℕ} (hp : p ≠ 0) (k : ℕ) : (p - 1) * frobeniusExponent p k + 1 = p ^ k

The Frobenius exponent in subtraction-free form: (p - 1) * e_k + 1 = p ^ k.

This is the shape in which the closed form is used as an exponent identity, see GranvilleMoore.pow_pow_eq_mul_pow_frobeniusExponent.

theorem GranvilleMoore.sub_one_mul_frobeniusExponent (p k : ℕ) : (p - 1) * frobeniusExponent p k = p ^ k - 1

The Frobenius exponent, closed form: (p - 1) * e_k = p ^ k - 1.

The subtraction is truncated, which is why no hypothesis on p is needed; for the version that moves the - 1 to the other side see GranvilleMoore.sub_one_mul_frobeniusExponent_add_one.

Frobenius powers in terms of the unit

theorem GranvilleMoore.pow_pow_eq_mul_pow_frobeniusExponent {M : Type u_1} [Monoid M] {p : ℕ} (hp : p ≠ 0) (x : M) (k : ℕ) : x ^ p ^ k = x * (x ^ (p - 1)) ^ frobeniusExponent p k

Frobenius powers in terms of the unit: x ^ p ^ k = x * (x ^ (p - 1)) ^ e_k.

For x : ℤ the right-hand factor is GranvilleMoore.fermatUnit p x ^ frobeniusExponent p k; this is the identity that makes the Frobenius exponent the exponent of the unit t_x contributed by the p ^ k-th power map.