English
For a tower F ⊆ E ⊆ K with E and K integral over F, and a ∈ K, the transitivity holds: Tr_{F}^{E}(Tr_{E}^{K}(a)) = Tr_{F}^{K}(a).
Русский
Для каскада F ⊆ E ⊆ K с условиями интегральности и элемента a ∈ K выполняется Tr_{F}^{E}(Tr_{E}^{K}(a)) = Tr_{F}^{K}(a).
LaTeX
$$$\\forall a \\in K:\\; \\operatorname{normalizedTrace}_{F}^{E}(\\\\operatorname{normalizedTrace}_{E}^{K}(a)) = \\\\operatorname{normalizedTrace}_{F}^{K}(a)$$$
Lean4
/-- 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`. -/
theorem normalizedTrace_trans_apply [Algebra.IsIntegral E K] [CharZero E] (a : K) :
normalizedTrace F E (normalizedTrace E K a) = normalizedTrace F K a :=
let S : Set E := (minpoly E a).coeffs
let E₀ := IntermediateField.adjoin F S
have : FiniteDimensional F E₀ := IntermediateField.finiteDimensional_adjoin fun x _ ↦ Algebra.IsIntegral.isIntegral x
have : Algebra.IsIntegral E₀ E := IsIntegral.tower_top F
have : Algebra.IsIntegral E₀ K := IsIntegral.trans E
have hsub : S ⊆ (algebraMap E₀ E).range :=
Subalgebra.range_algebraMap E₀.toSubalgebra ▸ IntermediateField.subset_adjoin F S
have hlifts := (Polynomial.lifts_iff_coeffs_subset_range _).mpr hsub
(normalizedTrace_trans_apply_aux F E₀ K _ ▸
normalizedTrace_algebraMap_apply F E₀ E _ ▸
congrArg (normalizedTrace F E) (normalizedTrace_algebraMap_of_lifts E₀ E K a hlifts)).symm
