Four finite-field facts: Fermat series, residue classes, monomial isolation, odd powers

Auxiliary facts over ZMod p, p prime.

Main results

• ConjeturaC.fermat_series: (k : ZMod p)^(p−1) = if p ∣ k then 0 else 1.
• ConjeturaC.crt_Xc: for 2m + 1 = p n with gcd(p, n) = 1 and n ∤ c, the set X_c = {x ∈ [−m, m] | x ≡ c (mod n)} has p elements, does not contain 0, and reduction modulo p is a bijection from X_c onto ZMod p.
• ConjeturaC.isolate_monomial_fin, ConjeturaC.isolate_monomial: p distinct points of ZMod p carry weights λ with ∑_x λ x · x^i = δ_ij for all i < p (Vandermonde).
• ConjeturaC.det_oddChar_ne_zero: det [l^e]_{l = 1..(p−1)/2, e = 1, 3, …, p−2} ≠ 0 in ZMod p (a diagonal times a Vandermonde matrix in l²).

The Fermat series

theorem ConjeturaC.fermat_series {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) : ↑k ^ (p - 1) = if ↑p ∣ k then 0 else 1

Residue classes in [−m, m]

def ConjeturaC.Xc (m n : ℕ) (c : ℤ) : Finset ℤ

X_c = {x ∈ [-m, m] : x ≡ c [ZMOD n]}.

Equations

• ConjeturaC.Xc m n c = {x ∈ Finset.Icc (-↑m) ↑m | x ≡ c [ZMOD ↑n]}

theorem ConjeturaC.crt_Xc {p : ℕ} [hp : Fact (Nat.Prime p)] (n m : ℕ) (hn : 1 ≤ n) (hcop : p.Coprime n) (hm : 2 * m + 1 = p * n) (c : ℤ) (hc : ¬↑n ∣ c) : (Xc m n c).card = p ∧ 0 ∉ Xc m n c ∧ Set.InjOn (fun (x : ℤ) => ↑x) ↑(Xc m n c) ∧ ∀ (r : ZMod p), ∃ x ∈ Xc m n c, ↑x = r

Isolating a monomial

theorem ConjeturaC.isolate_monomial_fin {K : Type u_1} [Field K] {n : ℕ} (v : Fin n → K) (hv : Function.Injective v) (j : Fin n) : ∃ (μ : Fin n → K), ∀ (i : Fin n), ∑ k : Fin n, μ k * v k ^ ↑i = if i = j then 1 else 0

Vandermonde core: n distinct points of a field, weights isolating the monomial X^j.

theorem ConjeturaC.isolate_monomial {p : ℕ} [hp : Fact (Nat.Prime p)] (S : Finset (ZMod p)) (hS : S.card = p) (j : ℕ) (hj : j < p) : ∃ (lam : ZMod p → ZMod p), ∀ i < p, ∑ x ∈ S, lam x * x ^ i = if i = j then 1 else 0

Isolating a monomial, as used: S ⊆ ZMod p with p points (i.e. the reductions of X_c).

Odd powers

def ConjeturaC.oddCharMat (p : ℕ) : Matrix (Fin ((p - 1) / 2)) (Fin ((p - 1) / 2)) (ZMod p)

Rows l = a+1 ∈ {1..(p-1)/2}, columns e = 2b+1 ∈ {1,3,..,p-2}, entry l^e.

Equations

• ConjeturaC.oddCharMat p = Matrix.of fun (a b : Fin ((p - 1) / 2)) => ↑(↑a + 1) ^ (2 * ↑b + 1)

theorem ConjeturaC.det_oddChar_ne_zero {p : ℕ} [hp : Fact (Nat.Prime p)] : (oddCharMat p).det ≠ 0