The additive character attached to the trace

Let A be a commutative algebra over ZMod n and let ζ be a primitive n-th root of unity in a ring R. Composing the trace of A over ZMod n with the character of ZMod n attached to ζ gives an additive character of A with values in R.

This file defines that character and establishes its basic properties.

The construction of FiniteField.primitiveChar is the same over a finite field, but there the root of unity is chosen in a cyclotomic extension of the target field. Here it is any given primitive root of unity, in any commutative ring, which gives more flexibility.

Main definitions

• AddChar.traceChar: the additive character of A sending x to ζ ^ Algebra.trace (ZMod n) A x.

Main results

• AddChar.mk_traceChar_apply_eq_one_add_smul: first-order expansion of traceChar modulo the square of an ideal containing ζ - 1.
• AddChar.map_traceChar_apply_eq_mulShift: applying a homomorphism of R that sends ζ to ζ ^ m to a value of traceChar gives the corresponding value of the shift of traceChar by m.
• AddChar.isPrimitive_traceChar: over a finite field, the character traceChar is primitive.

Tags

additive character, trace

TODO

• Define FiniteField.primitiveChar using AddChar.traceChar.

noncomputable def AddChar.traceChar {n : ℕ} [NeZero n] (A : Type u_1) [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) : AddChar A R

The additive character of A sending x to ζ ^ Algebra.trace (ZMod n) A x, where ζ is a primitive n-th root of unity.

Equations

• AddChar.traceChar A hζ = (AddChar.zmodChar n ⋯).compAddMonoidHom (Algebra.trace (ZMod n) A).toAddMonoidHom

theorem AddChar.traceChar_apply {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) (x : A) : (traceChar A hζ) x = ζ ^ ((Algebra.trace (ZMod n) A) x).val

The value of traceChar at x, as a power of ζ with exponent the canonical natural number representing the trace of x.

@[simp]

theorem AddChar.traceChar_apply_eq_one_iff {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) {x : A} : (traceChar A hζ) x = 1 ↔ (Algebra.trace (ZMod n) A) x = 0

The character traceChar is trivial at x if and only if the trace of x vanishes.

theorem AddChar.traceChar_eq_one_iff {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) : traceChar A hζ = 1 ↔ Algebra.trace (ZMod n) A = 0

The character traceChar is trivial if and only if the trace vanishes.

theorem AddChar.mk_traceChar_apply_eq_one {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) {𝓟 : Ideal R} (h : ζ - 1 ∈ 𝓟) (x : A) : (Ideal.Quotient.mk 𝓟) ((traceChar A hζ) x) = 1

The values of traceChar are congruent to 1 modulo any ideal containing ζ - 1.

theorem AddChar.mk_traceChar_apply_eq_one_add_smul {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) {𝓟 : Ideal R} (h : ζ - 1 ∈ 𝓟) (x : A) : (Ideal.Quotient.mk (𝓟 ^ 2)) ((traceChar A hζ) x) = 1 + ((Algebra.trace (ZMod n) A) x).val • (Ideal.Quotient.mk (𝓟 ^ 2)) (ζ - 1)

First-order expansion of traceChar modulo the square of an ideal containing ζ - 1.

theorem AddChar.compAddChar_traceChar {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) {S : Type u_3} [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) : (↑f).compAddChar (traceChar A hζ) = traceChar A ⋯

Pushing traceChar along an injective ring homomorphism f : R → S gives the character attached to f ζ.

theorem AddChar.compAddChar_traceChar_algebraMap {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) {S : Type u_3} [CommRing S] [Algebra R S] [FaithfulSMul R S] : (↑(algebraMap R S)).compAddChar (traceChar A hζ) = traceChar A ⋯

Pushing traceChar along an algebra homomorphism R → S gives the character attached to the image of ζ.

theorem AddChar.map_traceChar_apply_eq_mulShift {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) {G : Type u_3} [FunLike G R R] [MonoidHomClass G R R] {f : G} {m : ℕ} (h : f ζ = ζ ^ m) (x : A) : f ((traceChar A hζ) x) = ((traceChar A hζ).mulShift ↑m) x

If a homomorphism of R sends ζ to ζ ^ m, then it sends the value of traceChar at x to the value at x of the shift of traceChar by m.

theorem AddChar.traceChar_apply_algEquiv {n : ℕ} [NeZero n] {A : Type u_1} [CommRing A] [Algebra (ZMod n) A] {R : Type u_2} [CommRing R] {ζ : R} (hζ : IsPrimitiveRoot ζ n) {B : Type u_3} [CommRing B] [Algebra (ZMod n) B] (e : A ≃ₐ[ZMod n] B) (x : A) : (traceChar B hζ) (e x) = (traceChar A hζ) x

The character traceChar is invariant under isomorphisms of ZMod n-algebras.

theorem AddChar.traceChar_ne_one {R : Type u_2} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_3} [Field F] [Finite F] [Algebra (ZMod p) F] {ζ : R} (hζ : IsPrimitiveRoot ζ p) : traceChar F hζ ≠ 1

Over a finite field, the character traceChar is nontrivial.

theorem AddChar.isPrimitive_traceChar {R : Type u_2} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_3} [Field F] [Finite F] [Algebra (ZMod p) F] {ζ : R} (hζ : IsPrimitiveRoot ζ p) : (traceChar F hζ).IsPrimitive

Over a finite field, the character traceChar is primitive.

theorem AddChar.traceChar_apply_pow {R : Type u_2} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_3} [Field F] [Finite F] [Algebra (ZMod p) F] {ζ : R} (hζ : IsPrimitiveRoot ζ p) (x : F) : (traceChar F hζ) (x ^ p) = (traceChar F hζ) x

Over a finite field, the character traceChar is invariant under the Frobenius x ↦ x ^ p.