English
In a tower F ⊆ E ⊆ K with algebraic extensions, the normalized trace is transitive: the normalized trace from F to E of the normalized trace from E to K equals the normalized trace from F to K.
Русский
В каскаде F ⊆ E ⊆ K при алгебраических расширениях нормализованный след транзитивен: Tr_F^E(Tr_E^K(a)) = Tr_F^K(a) для всех a ∈ K.
LaTeX
$$$\\forall a \\,\\in\\; K:\\; \\,\\\\operatorname{normalizedTrace}_{F}^{E}(\\\\operatorname{normalizedTrace}_{E}^{K}(a)) = \\\\operatorname{normalizedTrace}_{F}^{K}(a)$$$
Lean4
/-- 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 normalizedTrace_algebraMap_of_lifts [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 :=
by
have ha : IsIntegral F a := IsIntegral.isIntegral a
simp [normalizedTrace_minpoly F a, normalizedTrace_minpoly E a, ← minpoly.map_algebraMap ha h,
(minpoly F a).natDegree_map, (minpoly F a).nextCoeff_map (algebraMap F E).injective, map_mul, map_neg]
/- An auxiliary result to prove `normalizedTrace_trans_apply`. It differs from
`normalizedTrace_trans_apply` only by the extra assumption about finiteness of `E` over `F`. -/
