Finite-field characters as linear functionals

Restricting a character to scalar multiples of a vector and using the one-dimensional character equivalence recovers its finite-field linear functional. This gives the exact normalization needed for geometric sums.

noncomputable def EGZ.Expansion.scalarCharacter {p d : ℕ} (χ : AddChar (FpCoord p d) ℂ) (a : FpCoord p d) : AddChar (ZMod p) ℂ

The scalar additive character obtained by restricting a vector-space character to multiples of a.

Equations

• EGZ.Expansion.scalarCharacter χ a = χ.compAddMonoidHom (LinearMap.toSpanSingleton (ZMod p) (EGZ.FpCoord p d) a).toAddMonoidHom

@[simp]

theorem EGZ.Expansion.scalarCharacter_apply {p d : ℕ} (χ : AddChar (FpCoord p d) ℂ) (a : FpCoord p d) (z : ZMod p) : (scalarCharacter χ a) z = χ (z • a)

noncomputable def EGZ.Expansion.characterLog {p d : ℕ} [NeZero p] (χ : AddChar (FpCoord p d) ℂ) : FpCoord p d →+ ZMod p

The additive finite-field logarithm of a complex additive character.

Equations

• EGZ.Expansion.characterLog χ = { toFun := fun (a : EGZ.FpCoord p d) => AddChar.zmodAddEquiv.symm (EGZ.Expansion.scalarCharacter χ a), map_zero' := ⋯, map_add' := ⋯ }

noncomputable def EGZ.Expansion.characterLinear {p d : ℕ} [NeZero p] (χ : AddChar (FpCoord p d) ℂ) : FpCoord p d →ₗ[ZMod p] ZMod p

The finite-field linear functional corresponding to a complex additive character.

Equations

• EGZ.Expansion.characterLinear χ = AddMonoidHom.toZModLinearMap p (EGZ.Expansion.characterLog χ)

theorem EGZ.Expansion.characterLinear_spec {p d : ℕ} [NeZero p] (χ : AddChar (FpCoord p d) ℂ) (a : FpCoord p d) : AddChar.zmodAddEquiv ((characterLinear χ) a) = scalarCharacter χ a

theorem EGZ.Expansion.characterLinear_eval {p d : ℕ} [NeZero p] (χ : AddChar (FpCoord p d) ℂ) (a : FpCoord p d) (n : ℕ) : (AddChar.zmodAddEquiv ((characterLinear χ) a)) ↑n = χ (n • a)

theorem EGZ.Expansion.characterLinear_ne_zero {p d : ℕ} [NeZero p] {χ : AddChar (FpCoord p d) ℂ} (hχ : χ ≠ 0) : characterLinear χ ≠ 0