The rational kernel of 1 + π^k on the Fermat cubic over 𝔽₂

Let E : X³ + Y³ = Z³ be the Fermat cubic over 𝔽₂, with origin O = [1 : 1 : 0], and let π be the 2-power Frobenius endomorphism.

Everything in this file is phrased directly in terms of homogeneous coordinates. This is possible because both maps involved admit a purely coordinatewise description:

• Frobenius is π [X : Y : Z] = [X² : Y² : Z²], hence π^k [X : Y : Z] = [X^(2^k) : ⋯];
• negation on the Fermat cubic with origin [1 : 1 : 0] swaps the first two coordinates, -[X : Y : Z] = [Y : X : Z].

Consequently (1 + π^k) R = O if and only if π^k R = -R, which is the coordinate condition IsKernelPoint below: the two triples (X^(2^k), Y^(2^k), Z^(2^k)) and (Y, X, Z) are proportional. No use of the group law itself is needed.

Main results

Let K be a field with 2^n elements and gcd (k, n) = 1.

• rational_kernel_odd: if n is odd, the K-rational points of ker (1 + π^k) reduce to the origin O = [1 : 1 : 0].
• rational_kernel_even: if n is even, they are exactly the points at infinity Z = 0.
• geometric_kernel_one_add_frobenius: over any field of characteristic 2, ker (1 + π) consists exactly of the points at infinity [1 : ω : 0] with ω³ = 1.

Notes on the key steps

1. The fixed-field/Bézout step π^(2k) R = R, π^n R = R ⟹ π^(gcd (2k, n)) R = R is pow_two_pow_gcd, applied coordinatewise to the affine coordinate X / Z in Z_eq_zero_of_isKernelPoint. Here gcd (2k, n) = gcd (2, n) ∈ {1, 2}, and in both cases the affine coordinate satisfies x⁴ = x; the two cases of the informal proof are thereby merged into one.
2. π^k = π on cube roots of unity for odd k is pow_two_pow_of_cube_root.
3. That the points at infinity are precisely ker (1 + π) is geometric_kernel_one_add_frobenius.
4. Instead of deducing #ker (1 + π) = 3 from deg (1 + π) = 3 and separability, step 3 proves directly, over an arbitrary field of characteristic 2, that there are no further kernel points; this is a self-contained substitute for the degree/separability argument.

The corollary of the informal text — for odd n the endomorphism 1 + π^k is injective, hence bijective, on the finite group E(K) — is exactly the triviality of the rational kernel proved in rational_kernel_odd, combined with the standard fact that a group homomorphism with trivial kernel is injective; the group law on E itself is not developed here.

def KasamiCyclicAdditive.FermatCubicFrobenius.IsPoint {K : Type u_1} [Field K] (X Y Z : K) : Prop

IsPoint X Y Z says that [X : Y : Z] is a point of the projective Fermat cubic X³ + Y³ = Z³: the coordinates are not all zero and they satisfy the equation.

Equations

• KasamiCyclicAdditive.FermatCubicFrobenius.IsPoint X Y Z = (¬(X = 0 ∧ Y = 0 ∧ Z = 0) ∧ X ^ 3 + Y ^ 3 = Z ^ 3)

def KasamiCyclicAdditive.FermatCubicFrobenius.IsKernelPoint {K : Type u_1} [Field K] (k : ℕ) (X Y Z : K) : Prop

IsKernelPoint k X Y Z says that (1 + π^k) [X : Y : Z] = O, equivalently π^k [X : Y : Z] = -[X : Y : Z], i.e. that the triples (X^(2^k), Y^(2^k), Z^(2^k)) and (Y, X, Z) define the same projective point.

Equations

• KasamiCyclicAdditive.FermatCubicFrobenius.IsKernelPoint k X Y Z = ∃ (c : K), c ≠ 0 ∧ X ^ 2 ^ k = c * Y ∧ Y ^ 2 ^ k = c * X ∧ Z ^ 2 ^ k = c * Z

Basic facts about the origin and the points at infinity

theorem KasamiCyclicAdditive.FermatCubicFrobenius.ne_zero_of_isPoint_infinity {K : Type u_1} [Field K] {X Y : K} (hP : IsPoint X Y 0) : X ≠ 0 ∧ Y ≠ 0

On a point at infinity (Z = 0) both remaining coordinates are nonzero.

theorem KasamiCyclicAdditive.FermatCubicFrobenius.cube_eq_of_isPoint_infinity {K : Type u_1} [Field K] (h2 : 2 = 0) {X Y : K} (hP : IsPoint X Y 0) : Y ^ 3 = X ^ 3

On a point at infinity in characteristic 2 we have Y³ = X³.

theorem KasamiCyclicAdditive.FermatCubicFrobenius.cube_ratio_of_isPoint_infinity {K : Type u_1} [Field K] (h2 : 2 = 0) {X Y : K} (hP : IsPoint X Y 0) : (Y / X) ^ 3 = 1

In characteristic 2, the ratio ω = Y / X of a point at infinity [X : Y : 0] is a cube root of unity, so the point is [1 : ω : 0].

Characteristic and Frobenius facts for a field with 2^n elements

theorem KasamiCyclicAdditive.FermatCubicFrobenius.two_eq_zero_of_card {K : Type u_1} [Field K] [Fintype K] {n : ℕ} (hcard : Fintype.card K = 2 ^ n) : 2 = 0

A field with 2^n elements has characteristic 2.

theorem KasamiCyclicAdditive.FermatCubicFrobenius.pow_two_pow_card {K : Type u_1} [Field K] [Fintype K] {n : ℕ} (hcard : Fintype.card K = 2 ^ n) (x : K) : x ^ 2 ^ n = x

Every element of a field with 2^n elements is fixed by the n-th power of Frobenius.

theorem KasamiCyclicAdditive.FermatCubicFrobenius.cube_root_eq_one_of_odd {K : Type u_1} [Field K] [Fintype K] {n : ℕ} (hn : Odd n) (hcard : Fintype.card K = 2 ^ n) {a : K} (ha : a ^ 3 = 1) : a = 1

For odd n the only cube root of unity in a field with 2^n elements is 1.

There is no affine kernel point

theorem KasamiCyclicAdditive.FermatCubicFrobenius.not_kernel_of_Z_ne_zero {K : Type u_1} [Field K] (h2 : 2 = 0) {k : ℕ} {X Y Z : K} (hP : IsPoint X Y Z) (hK : IsKernelPoint k X Y Z) (hZ : Z ≠ 0) (h4 : (X / Z) ^ 4 = X / Z) : False

The core computation: an affine (Z ≠ 0) kernel point whose affine x-coordinate lies in 𝔽₄ cannot exist.

theorem KasamiCyclicAdditive.FermatCubicFrobenius.Z_eq_zero_of_isKernelPoint {K : Type u_1} [Field K] [Fintype K] {n k : ℕ} (hcard : Fintype.card K = 2 ^ n) (hkn : k.Coprime n) {X Y Z : K} (hP : IsPoint X Y Z) (hK : IsKernelPoint k X Y Z) : Z = 0

No affine kernel points. If gcd (k, n) = 1 then every K-rational point of ker (1 + π^k) is a point at infinity.

The points at infinity and the kernel condition

theorem KasamiCyclicAdditive.FermatCubicFrobenius.isKernelPoint_infinity_iff {K : Type u_1} [Field K] (h2 : 2 = 0) {k : ℕ} {X Y : K} (hP : IsPoint X Y 0) : IsKernelPoint k X Y 0 ↔ (Y / X) ^ 2 ^ k = (Y / X) ^ 2

For a point at infinity [X : Y : 0] with ω = Y / X, the kernel condition π^k R = -R is equivalent to ω^(2^k) = ω².

theorem KasamiCyclicAdditive.FermatCubicFrobenius.pow_two_pow_of_cube_root {K : Type u_1} [Field K] {k : ℕ} (hk : Odd k) {w : K} (hw : w ^ 3 = 1) : w ^ 2 ^ k = w ^ 2

For odd k we have 2^k ≡ 2 [MOD 3], hence ω^(2^k) = ω² for every cube root of unity. (π^k = π on E(𝔽₄).)

The main theorems

theorem KasamiCyclicAdditive.FermatCubicFrobenius.rational_kernel_odd {K : Type u_1} [Field K] [Fintype K] {n k : ℕ} (hn : Odd n) (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) {X Y Z : K} (hP : IsPoint X Y Z) : IsKernelPoint k X Y Z ↔ Z = 0 ∧ X = Y

Odd n: the rational kernel is trivial.

For K a field with 2^n elements, n odd and gcd (k, n) = 1, a point of E(K) lies in ker (1 + π^k) if and only if it is the origin O = [1 : 1 : 0] (i.e. Z = 0 and X = Y).

The hypothesis "k is odd" of the informal statement is not needed here.

theorem KasamiCyclicAdditive.FermatCubicFrobenius.rational_kernel_even {K : Type u_1} [Field K] [Fintype K] {n k : ℕ} (hn : Even n) (hkn : k.Coprime n) (hcard : Fintype.card K = 2 ^ n) {X Y Z : K} (hP : IsPoint X Y Z) : IsKernelPoint k X Y Z ↔ Z = 0

Even n: the rational kernel is the set of points at infinity.

For K a field with 2^n elements, n even and gcd (k, n) = 1, a point of E(K) lies in ker (1 + π^k) if and only if it is a point at infinity, Z = 0.

Note that k is automatically odd here, since gcd (k, n) = 1 and n is even.

theorem KasamiCyclicAdditive.FermatCubicFrobenius.geometric_kernel_one_add_frobenius {K : Type u_1} [Field K] (h2 : 2 = 0) {X Y Z : K} (hP : IsPoint X Y Z) : IsKernelPoint 1 X Y Z ↔ Z = 0

The geometric kernel of 1 + π.

Over any field of characteristic 2 (in particular over an algebraic closure of 𝔽₂), the kernel of 1 + π consists exactly of the points at infinity [1 : ω : 0], ω³ = 1, so it has exactly three points, without appealing to the degree of the isogeny or to separability.

Non-vacuity checks

The hypotheses of the two main theorems are satisfiable: they apply to 𝔽₂ (n = 1) and to 𝔽₄ (n = 2).