# The trace and norm maps for finite fields #

We state several lemmas about the trace and norm maps for finite fields.

## Main Results #

- `trace_to_zmod_nondegenerate`: the trace map from a finite field of characteristic `p` to `ZMod p` is nondegenerate.
- `algebraMap_trace_eq_sum_pow`: an explicit formula for the trace map: `trace[L/K](x) = ∑ i < [L:K], x ^ ((#K) ^ i)`.
- `algebraMap_norm_eq_prod_pow`: an explicit formula for the norm map: `norm[L/K](x) = ∏ i < [L:K], x ^ ((#K) ^ i)`.

## Tags #

finite field, trace, norm

source
theorem FiniteField.trace_to_zmod_nondegenerate (F : Type u_1) [Field F] [Finite F] [Algebra (ZMod (ringChar F)) F] {a : F} (ha : a ≠ 0) :
∃ (b : F), (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

The trace map from a finite field to its prime field is nongedenerate.

source
theorem FiniteField.algebraMap_trace_eq_sum_pow (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Finite L] [Algebra K L] (x : L) :
(algebraMap K L) ((Algebra.trace K L) x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

An explicit formula for the trace map: `trace[L/K](x) = ∑ i < [L:K], x ^ ((#K) ^ i)`.

source
theorem FiniteField.algebraMap_norm_eq_prod_pow (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Finite L] [Algebra K L] (x : L) :
(algebraMap K L) ((Algebra.norm K) x) = ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

An explicit formula for the norm map: `norm[L/K](x) = ∏ i < [L:K], x ^ ((#K) ^ i)`.

source
theorem FiniteField.algebraMap_norm_eq_pow_sum (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Finite L] [Algebra K L] (x : L) :
(algebraMap K L) ((Algebra.norm K) x) = x ^ ∑ i ∈ Finset.range (Module.finrank K L), Nat.card K ^ i

An explicit formula for the norm map: `norm[L/K](x) = x ^ (∑ i < [L:K], (#K) ^ i)`.