Normalized trace

This file defines the normalized trace map; that is, an F-linear map from the algebraic closure of F to F defined as the trace of an element from its adjoin extension divided by its degree.

To avoid heavy imports, we define it here as a map from an arbitrary algebraic (equivalently integral) extension of F.

Main definitions

• normalizedTrace: the trace of an element from the simple adjoin divided by the degree; it is a non-trivial F-linear map from an arbitrary algebraic extension K to F.

Main results

• normalizedTrace_intermediateField: for a tower K / E / F of algebraic extensions, normalizedTrace F E agrees with normalizedTrace F K on E.
• normalizedTrace_trans: for a tower K / E / F of algebraic extensions, the normalized trace from K to E composed with the normalized trace from E to F equals the normalized trace from K to F.
• normalizedTrace_self: normalizedTrace F F is the identity map.

noncomputable def Algebra.normalizedTrace (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] : K →ₗ[F] F

The normalized trace map from an algebraic extension K to the base field F.

theorem Algebra.normalizedTrace_def (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] (a : K) : (normalizedTrace F K) a = (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮a⟯) (IntermediateField.AdjoinSimple.gen F a)

theorem Algebra.normalizedTrace_minpoly (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] (a : K) : (normalizedTrace F K) a = (↑(minpoly F a).natDegree)⁻¹ • -(minpoly F a).nextCoeff

Normalized trace defined purely in terms of the degree and the next coefficient of the minimal polynomial. Could be an alternative definition but it is harder to work with linearity.

theorem Algebra.normalizedTrace_self_apply {F : Type u_1} [Field F] [CharZero F] (a : F) : (normalizedTrace F F) a = a

@[simp]

theorem Algebra.normalizedTrace_self (F : Type u_1) [Field F] [CharZero F] : normalizedTrace F F = LinearMap.id

theorem Algebra.normalizedTrace_eq_of_finiteDimensional_apply (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] [FiniteDimensional F K] (a : K) : (normalizedTrace F K) a = (↑(Module.finrank F K))⁻¹ • (trace F K) a

@[deprecated Algebra.normalizedTrace_eq_of_finiteDimensional_apply (since := "2025-10-22")]

theorem Algebra.normalizedTrace_eq_of_fininteDimensional_apply (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] [FiniteDimensional F K] (a : K) : (normalizedTrace F K) a = (↑(Module.finrank F K))⁻¹ • (trace F K) a

Alias of Algebra.normalizedTrace_eq_of_finiteDimensional_apply.

theorem Algebra.normalizedTrace_eq_of_finiteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] [FiniteDimensional F K] : normalizedTrace F K = (↑(Module.finrank F K))⁻¹ • trace F K

@[deprecated Algebra.normalizedTrace_eq_of_finiteDimensional (since := "2025-10-22")]

theorem Algebra.normalizedTrace_eq_of_fininteDimensional (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] [FiniteDimensional F K] : normalizedTrace F K = (↑(Module.finrank F K))⁻¹ • trace F K

Alias of Algebra.normalizedTrace_eq_of_finiteDimensional.

@[simp]

theorem Algebra.normalizedTrace_map (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] {E : Type u_3} [Field E] [Algebra F E] [Algebra.IsIntegral F E] (f : E →ₐ[F] K) (a : E) : (normalizedTrace F K) (f a) = (normalizedTrace F E) a

The normalized trace transfers via (injective) maps.

theorem Algebra.normalizedTrace_intermediateField (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] {E : IntermediateField F K} (a : ↥E) : (normalizedTrace F K) ↑a = (normalizedTrace F ↥E) a

The normalized trace transfers via restriction to a subextension.

@[simp]

theorem Algebra.normalizedTrace_algebraMap_apply (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Field E] [Field K] [Algebra F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K] [Algebra.IsIntegral F E] [Algebra.IsIntegral F K] [CharZero F] (a : E) : (normalizedTrace F K) ((algebraMap E K) a) = (normalizedTrace F E) a

@[simp]

theorem Algebra.normalizedTrace_algebraMap (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Field E] [Field K] [Algebra F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K] [Algebra.IsIntegral F E] [Algebra.IsIntegral F K] [CharZero F] : normalizedTrace F K ∘ₗ ↑F (Algebra.linearMap E K) = normalizedTrace F E

theorem Algebra.normalizedTrace_algebraMap_of_lifts (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Field E] [Field K] [Algebra F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K] [Algebra.IsIntegral F K] [CharZero F] [CharZero E] [Algebra.IsIntegral E K] (a : K) (h : minpoly E a ∈ Polynomial.lifts (algebraMap F E)) : (algebraMap F E) ((normalizedTrace F K) a) = (normalizedTrace E K) a

If all the coefficients of minpoly E a are in F, then the normalized trace of a from K to E equals the normalized trace of a from K to F.

theorem Algebra.normalizedTrace_trans_apply (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Field E] [Field K] [Algebra F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K] [Algebra.IsIntegral F E] [Algebra.IsIntegral F K] [CharZero F] [Algebra.IsIntegral E K] [CharZero E] (a : K) : (normalizedTrace F E) ((normalizedTrace E K) a) = (normalizedTrace F K) a

For a tower K / E / F of algebraic extensions, the normalized trace from K to E composed with the normalized trace from E to F equals the normalized trace from K to F.

@[simp]

theorem Algebra.normalizedTrace_trans (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Field E] [Field K] [Algebra F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K] [Algebra.IsIntegral F E] [Algebra.IsIntegral F K] [CharZero F] [Algebra.IsIntegral E K] [CharZero E] : normalizedTrace F E ∘ₗ ↑F (normalizedTrace E K) = normalizedTrace F K

theorem Algebra.normalizedTrace_algebraMap_apply_eq_self (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] (a : F) : (normalizedTrace F K) ((algebraMap F K) a) = a

theorem Algebra.normalizedTrace_algebraMap_eq_id (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] : normalizedTrace F K ∘ₗ Algebra.linearMap F K = LinearMap.id

The normalized trace map is a left inverse of the algebra map.

@[simp]

theorem Algebra.normalizedTrace_comp_algHom (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] {E : Type u_3} [Field E] [Algebra F E] [Algebra.IsIntegral F E] (f : E →ₐ[F] K) : normalizedTrace F K ∘ₗ ↑f = normalizedTrace F E

The normalized trace commutes with (injective) maps.

theorem Algebra.normalizedTrace_surjective (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] : Function.Surjective ⇑(normalizedTrace F K)

theorem Algebra.normalizedTrace_ne_zero (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [CharZero F] [Algebra.IsIntegral F K] : normalizedTrace F K ≠ 0

The normalized trace map is non-trivial.