Documentation

LeanPool.KasamiCyclicAdditive.Phase.PowerMap

Basic facts: the power map x ↦ x^D and the group μ₃(K) #

The exponent D #

source
theorem KasamiCyclicAdditive.Phase.pow_mul_eq_self {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {m D : ℕ} (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (x : K) :
x ^ (m * D) = x

If m * D ≡ 1 (mod N) with N = #Kˣ, then x ^ (m * D) = x on all of K, so x ↦ x^D and x ↦ x^m are mutually inverse.

source
theorem KasamiCyclicAdditive.Phase.powD_powm {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {m D : ℕ} (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (x : K) :
(x ^ D) ^ m = x

x ↦ x^m undoes x ↦ x^D.

source
theorem KasamiCyclicAdditive.Phase.powm_powD {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {m D : ℕ} (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (x : K) :
(x ^ m) ^ D = x

x ↦ x^D undoes x ↦ x^m.

source
theorem KasamiCyclicAdditive.Phase.powD_bijective {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {m D : ℕ} (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) :
Function.Bijective fun (x : K) => x ^ D

Hence x ↦ x^D is a bijection of K.

source
theorem KasamiCyclicAdditive.Phase.sum_psi_mul_powD {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {m D : ℕ} {ψ : AddChar K ℂ} (hψ : ψ.IsPrimitive) (hm : m ≠ 0) (hD : D ≠ 0) (hmD : m * D ≡ 1 [MOD Fintype.card Kˣ]) (C : K) :
∑ y : K, ψ (C * y ^ D) = if C = 0 then ↑(Fintype.card K) else 0

∑_{y ∈ K} ψ(C y^D) = Q if C = 0 and 0 otherwise.

The group μ₃(K) #

source
@[simp]
theorem KasamiCyclicAdditive.Phase.mem_cubeRootsOne {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {u : K} :
u ∈ cubeRootsOne K ↔ u ^ 3 = 1

Membership in μ₃(K) is the equation u ^ 3 = 1.

source
theorem KasamiCyclicAdditive.Phase.cubeRootsOne_ne_zero {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {u : K} (h : u ∈ cubeRootsOne K) :
u ≠ 0

Cube roots of unity are nonzero.

source
theorem KasamiCyclicAdditive.Phase.mul_mem_cubeRootsOne {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {u v : K} (hu : u ∈ cubeRootsOne K) (hv : v ∈ cubeRootsOne K) :
u * v ∈ cubeRootsOne K

μ₃(K) is closed under multiplication.

source
theorem KasamiCyclicAdditive.Phase.inv_mem_cubeRootsOne {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {u : K} (hu : u ∈ cubeRootsOne K) :
u⁻¹ ∈ cubeRootsOne K

μ₃(K) is closed under inverses.

source
theorem KasamiCyclicAdditive.Phase.mu3Card_ne_zero {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] :
↑(mu3Card K) ≠ 0

Hence mu3Card K is nonzero in ℂ, and may be divided by.