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

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.

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).

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).

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).