Frobenius transport between complementary parameters

Since the Kasami parameters k and n - k are related by a Frobenius twist, the two derivative images Δ_k and Δ_(n-k) have the same cardinality. This is what lets the half-size fact be proved for odd k only and then transported to the even case, where coprimality forces n - k to be odd.

Also recorded here is the elementary fact that 0 ∈ Δ_k for every k (take the derivative parameter b = 0), and the packaging of the half-size fact into the derivative-image half-size equation at both k and the complementary parameter n - k.

The complementary Frobenius equivalence

noncomputable def KasamiCyclicAdditive.complementFrobeniusEquiv {K : Type u_1} [Field K] [Fintype K] [CharP K 2] (k : ℕ) : K ≃+* K

The Frobenius map used to transport data from parameter n - k to k.

The parameter n is not needed to define the equivalence; it enters only in the identity below relating the Kasami exponents at k and n - k.

Equations

• KasamiCyclicAdditive.complementFrobeniusEquiv k = RingEquiv.ofBijective (iterateFrobenius K 2 (2 * k)) ⋯

@[simp]

theorem KasamiCyclicAdditive.complementFrobeniusEquiv_apply {K : Type u_1} [Field K] [Fintype K] [CharP K 2] (k : ℕ) (x : K) : (complementFrobeniusEquiv k) x = (iterateFrobenius K 2 (2 * k)) x

complementFrobeniusEquiv k acts as the 2 ^ (2k)-power Frobenius.

Frobenius transport of the derivative image

theorem KasamiCyclicAdditive.kasamiExponent_cast (k : ℕ) : ↑(kasamiExponent k) = 4 ^ k - 2 ^ k + 1

The Kasami exponent over ℤ, free of truncated subtraction.

theorem KasamiCyclicAdditive.kasamiExponent_complement {n k : ℕ} (hk : k ≤ n) : 2 ^ (2 * k) * kasamiExponent (n - k) = kasamiExponent k + (2 ^ n - 1) * (2 ^ n - 2 ^ k + 1)

2 ^ (2k) times the complementary Kasami exponent differs from the Kasami exponent at k by a multiple of 2 ^ n - 1.

theorem KasamiCyclicAdditive.pow_add_card_sub_one_mul {K : Type u_1} [Field K] [Fintype K] (x : K) (e c : ℕ) (he : e ≠ 0) : x ^ (e + (Fintype.card K - 1) * c) = x ^ e

Exponents may be shifted by multiples of #K - 1 on all of K.

theorem KasamiCyclicAdditive.pow_kasamiExponent_complement {K : Type u_1} [Field K] [Fintype K] {n k : ℕ} (hk : k ≤ n) (hcard : Fintype.card K = 2 ^ n) (x : K) : x ^ (kasamiExponent (n - k) * 2 ^ (2 * k)) = x ^ kasamiExponent k

On a field of order 2 ^ n the two exponents therefore act alike: x ^ (d_(n-k) * 2 ^ (2k)) = x ^ d_k.

theorem KasamiCyclicAdditive.kasamiDerivative_complement {K : Type u_1} [Field K] [Fintype K] [CharP K 2] {n k : ℕ} (hk : k ≤ n) (hcard : Fintype.card K = 2 ^ n) (b : K) : kasamiDerivative k b = (iterateFrobenius K 2 (2 * k)) (kasamiDerivative (n - k) b)

The derivative at k is the 2 ^ (2k)-power Frobenius image of the derivative at n - k.

theorem KasamiCyclicAdditive.derivativeImage_complement_eq_image {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k : ℕ} (hk : k ≤ n) (hcard : Fintype.card K = 2 ^ n) : derivativeImage k K = Finset.image (⇑(complementFrobeniusEquiv k)) (derivativeImage (n - k) K)

The complementary derivative image is the Frobenius image of the original derivative image.

theorem KasamiCyclicAdditive.card_derivativeImage_complement {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] {n k : ℕ} (hk : k ≤ n) (hcard : Fintype.card K = 2 ^ n) : (derivativeImage k K).card = (derivativeImage (n - k) K).card

Frobenius transport preserves the size of the Kasami derivative image: |Δ_k| = |Δ_(n-k)|.

Zero always lies in the derivative image

theorem KasamiCyclicAdditive.zero_mem_derivativeImage {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [CharP K 2] (k : ℕ) : 0 ∈ derivativeImage k K

Zero belongs to every Kasami derivative image.