Factoring 1 + π^k through a prime-to-3 automorphism

For odd k = 2r+1, the isogeny 1 + π^k factors as (1 + π) ∘ G with G = a - bπ, where a + 2b = 1, a - b = (-2)^r and a² + 2b² = m, and H = a + bπ satisfies H ∘ G = G ∘ H = [m]. Whenever [m] is invertible on the group — which on E(K) follows from an annihilator N coprime to m via Bézout — G is bijective.

That isolates the entire 3-primary obstruction into the single factor 1 + π, and it is all abstract: this file is a calculation in a ℤ-module equipped with an endomorphism π satisfying π² = [-2]. No field, curve, Frobenius map or algebraic closure appears.

def KasamiCyclicAdditive.Isogeny.piIter {G : Type u_1} [AddCommGroup G] (pi : G →+ G) : ℕ → G → G

The n-fold iterate of pi.

Equations

• KasamiCyclicAdditive.Isogeny.piIter pi 0 x✝ = x✝
• KasamiCyclicAdditive.Isogeny.piIter pi n.succ x✝ = pi (KasamiCyclicAdditive.Isogeny.piIter pi n x✝)

def KasamiCyclicAdditive.Isogeny.gMap {G : Type u_1} [AddCommGroup G] (pi : G →+ G) (a b : ℤ) (x : G) : G

a - b*pi.

Equations

• KasamiCyclicAdditive.Isogeny.gMap pi a b x = a • x - b • pi x

def KasamiCyclicAdditive.Isogeny.hMap {G : Type u_1} [AddCommGroup G] (pi : G →+ G) (a b : ℤ) (x : G) : G

a + b*pi.

Equations

• KasamiCyclicAdditive.Isogeny.hMap pi a b x = a • x + b • pi x

theorem KasamiCyclicAdditive.Isogeny.gMap_zsmul {G : Type u_1} [AddCommGroup G] (pi : G →+ G) (a b c : ℤ) (x : G) : gMap pi a b (c • x) = c • gMap pi a b x

gMap commutes with multiplication by an integer.

theorem KasamiCyclicAdditive.Isogeny.gMap_add_map {G : Type u_1} [AddCommGroup G] (pi : G →+ G) (a b : ℤ) (x : G) : gMap pi a b x + pi (gMap pi a b x) = gMap pi a b (x + pi x)

gMap commutes with 1 + pi.

theorem KasamiCyclicAdditive.Isogeny.neg_two_pow_eq_one_add_three_mul (r : ℕ) : ∃ (c : ℤ), (-2) ^ r = 1 + 3 * c

(-2)^r is congruent to 1 modulo 3.

theorem KasamiCyclicAdditive.Isogeny.exists_factor_coefficients {r m : ℕ} (he : 2 ^ (2 * r + 1) + 1 = 3 * m) : ∃ (a : ℤ) (b : ℤ), a + 2 * b = 1 ∧ a - b = (-2) ^ r ∧ a ^ 2 + 2 * b ^ 2 = ↑m

Arithmetic coefficients for the factorisation.

For k = 2*r+1 and 2^k+1 = 3*m, there are integers a,b such that

a + 2b = 1,
a - b = (-2)^r,
a^2 + 2b^2 = m.

Explicitly one may take

b = (1 - (-2)^r)/3,
a = (1 + 2*(-2)^r)/3.

theorem KasamiCyclicAdditive.Isogeny.piIter_even {G : Type u_1} [AddCommGroup G] (pi : G →+ G) (hpi2 : ∀ (x : G), pi (pi x) = -2 • x) (n : ℕ) (x : G) : piIter pi (2 * n) x = (-2) ^ n • x

Iterating π² = [-2]: the even powers of π are integer multiplications.

theorem KasamiCyclicAdditive.Isogeny.gMap_factor {G : Type u_1} [AddCommGroup G] (pi : G →+ G) {r : ℕ} {a b : ℤ} (hpi2 : ∀ (x : G), pi (pi x) = -2 • x) (hab1 : a + 2 * b = 1) (hab2 : a - b = (-2) ^ r) (x : G) : x + piIter pi (2 * r + 1) x = gMap pi a b x + pi (gMap pi a b x)

The factorization (1 + π) ∘ G = 1 + π^(2r+1), with no invertibility hypothesis. Stated separately because it is needed over the algebraic closure, where the group has no finite annihilator and G need not be bijective.

theorem KasamiCyclicAdditive.Isogeny.gMap_bijective {G : Type u_1} [AddCommGroup G] (pi : G →+ G) {m : ℕ} {N a b : ℤ} (hpi2 : ∀ (x : G), pi (pi x) = -2 • x) (hnorm : a ^ 2 + 2 * b ^ 2 = ↑m) (hann : ∀ (x : G), N • x = 0) (hcop : IsCoprime (↑m) N) : Function.Bijective (gMap pi a b)

Invertibility of G = a - b*pi.

Assume pi² = [-2] on an abelian group, and put H = a + b*pi. The norm identity a² + 2b² = m gives HG = GH = [m], so if every element of the group is killed by an integer N coprime to m, multiplication by m is invertible by Bezout and hence G is bijective.

This needs neither r nor the coefficient identities: the factorization (1 + pi) G = 1 + pi^(2r+1) is the separate statement gMap_factor.