English
The trace of a nilpotent element in an algebra is nilpotent.
Русский
След элемента, являющегося нильпотентом, в алгебре также нильпотентен.
LaTeX
$$$\\operatorname{trace}(R,S)(x) \\text{ is nilpotent if } x \\text{ is nilpotent}$$$
Lean4
/-- The dual basis of a power basis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`,
with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.
-/
theorem traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [Algebra.IsSeparable K L] (pb : PowerBasis K L) (i) :
(Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) pb.basis i =
(minpolyDiv K pb.gen).coeff i / aeval pb.gen (derivative <| minpoly K pb.gen) :=
by
classical
apply ((Algebra.traceForm K L).toDual (traceForm_nondegenerate K L)).injective
apply pb.basis.ext
intro j
simp only [BilinForm.toDual_def, BilinForm.apply_dualBasis_left]
apply (algebraMap K (AlgebraicClosure K)).injective
have :=
congr_arg (coeff · i)
(sum_smul_minpolyDiv_eq_X_pow (AlgebraicClosure K) pb.adjoin_gen_eq_top (r := j) (pb.finrank.symm ▸ j.prop))
simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, finset_sum_coeff, coeff_smul, coeff_map,
smul_eq_mul, coeff_X_pow, ← Fin.ext_iff, @eq_comm _ i] at this
rw [PowerBasis.coe_basis]
simp only [MonoidWithZeroHom.map_ite_one_zero, traceForm_apply]
rw [← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)]
apply Finset.sum_congr rfl
intro σ _
simp only [map_mul, map_div₀, map_pow]
ring
