The Frobenius annihilator on E(K)

For a finite field K with |K| = 2^n, the n-th power of the Frobenius endomorphism is the identity on E(K), simply because every coordinate satisfies x^(2^n) = x. In even dimension n = 2j the CM relation π² = [-2] additionally gives π^n = [(-2)^j], so comparing the two descriptions shows that

nn n = (-2)^j - 1

annihilates E(K). That is the hypothesis hann of Isogeny.gMap_bijective, and together with Descent.isCoprime_nn it makes G bijective on E(K) — no algebraic closure and no kernel decomposition.

theorem KasamiCyclicAdditive.PointFrobenius.frobEnd_pow_card_eq {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n : ℕ} (hcard : Fintype.card K = 2 ^ n) (P : (FermatCubic.fer K).toAffine.Point) : (frobEnd K ^ n) P = P

The n-th Frobenius power is the identity on K-rational points.

theorem KasamiCyclicAdditive.PointFrobenius.piIter_frobPt {K : Type u_1} [Field K] [DecidableEq K] [CharP K 2] (k : ℕ) (P : (FermatCubic.fer K).toAffine.Point) : Isogeny.piIter (frobPt K) k P = (frobEnd K ^ k) P

The abstract iterate Isogeny.piIter agrees with the Frobenius endomorphism power.

theorem KasamiCyclicAdditive.PointFrobenius.nn_smul_eq_zero {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n : ℕ} (hn : Even n) (hcard : Fintype.card K = 2 ^ n) (P : (FermatCubic.fer K).toAffine.Point) : Descent.nn n • P = 0

nn n annihilates E(K) in even dimension.

Inverting G on E(K)

theorem KasamiCyclicAdditive.PointFrobenius.exists_gMap_preimage {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k m : ℕ} (hn : Even n) (hk : Odd k) (hcard : Fintype.card K = 2 ^ n) (he : 2 ^ k + 1 = 3 * m) (hm : m.Coprime (2 ^ n - 1)) (R : (FermatCubic.fer K).toAffine.Point) : ∃ (a : ℤ) (b : ℤ) (r : ℕ) (Y : (FermatCubic.fer K).toAffine.Point), k = 2 * r + 1 ∧ a + 2 * b = 1 ∧ a - b = (-2) ^ r ∧ Isogeny.gMap (frobPt K) a b Y = R

For odd k = 2r+1 in even dimension, the prime-to-3 factor G is a bijection of E(K), so every point has a G-preimage.

The 3-primary obstruction is the separate factor 1 + π, and G is inverted by Bézout against the annihilator nn n, over K itself. The factorization (1 + π) ∘ G = 1 + π^k is Isogeny.gMap_factor, applied by the caller where it is needed.