Arithmetic facts for the descent

This file formalises the arithmetic behind the even-dimensional descent step. For even n, c_n = (-2)^(n/2) is the integer with π^n = [c_n], and N = c_n - 1:

• cN_sq : c_n^2 = Q = 2^n;
• nn_dvd : N ∣ Q - 1, since Q - 1 = (c_n - 1)(c_n + 1);
• isCoprime_nn : gcd(N, m) = 1 whenever gcd(m, Q - 1) = 1.

N is the annihilator of E(K) used by Isogeny.gMap_bijective; see Geometry/FrobeniusAnnihilator.lean.

def KasamiCyclicAdditive.Descent.cN (n : ℕ) : ℤ

c_n = (-2)^(n/2), the integer with π^n = [c_n] for even n.

Equations

• KasamiCyclicAdditive.Descent.cN n = (-2) ^ (n / 2)

def KasamiCyclicAdditive.Descent.nn (n : ℕ) : ℤ

N = c_n - 1.

Equations

• KasamiCyclicAdditive.Descent.nn n = KasamiCyclicAdditive.Descent.cN n - 1

theorem KasamiCyclicAdditive.Descent.cN_sq {n : ℕ} (hn : Even n) : cN n ^ 2 = 2 ^ n

c_n^2 = Q = 2^n for even n.

theorem KasamiCyclicAdditive.Descent.nn_dvd {n : ℕ} (hn : Even n) : nn n ∣ 2 ^ n - 1

N ∣ Q - 1, since Q - 1 = (c_n-1)(c_n+1).

theorem KasamiCyclicAdditive.Descent.isCoprime_nn {n m : ℕ} (hn : Even n) (hm : m.Coprime (2 ^ n - 1)) : IsCoprime (nn n) ↑m

gcd(N,m) = 1 follows from gcd(m,Q-1)=1 and N ∣ Q-1.