English
If the base extension is not separable, then the trace is identically zero.
Русский
Если разложение базового поля неразделимо, след равен нулю.
LaTeX
$$$\\text{If } \\neg \\mathrm{IsSeparable}(K,L)\\text{ then } \\operatorname{trace}_{K L} = 0$$$
Lean4
theorem trace_eq_sum_embeddings [FiniteDimensional K L] [Algebra.IsSeparable K L] {x : L} :
algebraMap K E (Algebra.trace K L x) = ∑ σ : L →ₐ[K] E, σ x :=
by
have hx := Algebra.IsSeparable.isIntegral K x
let pb := adjoin.powerBasis hx
rw [trace_eq_trace_adjoin K x, Algebra.smul_def, RingHom.map_mul, ← adjoin.powerBasis_gen hx,
trace_eq_sum_embeddings_gen E pb (IsAlgClosed.splits_codomain _), ← Algebra.smul_def, algebraMap_smul]
· exact (sum_embeddings_eq_finrank_mul L E pb).symm
· haveI := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
exact Algebra.IsSeparable.isSeparable K _
