Semisimplicity from a trace form #
A finite-dimensional complex algebra carrying a linear functional
that vanishes on nilpotents and is nondegenerate in the form
(∀ b, τ (b * a) = 0) → a = 0 is semisimple: every element of the
Jacobson radical is nilpotent (the radical of an Artinian ring is a
nilpotent ideal), so the functional kills b * j for every b,
forcing j = 0.
theorem
RS.isSemisimpleRing_of_trace
{A : Type u}
[Ring A]
[Algebra ℂ A]
[FiniteDimensional ℂ A]
(τ : A →ₗ[ℂ] ℂ)
(hnil : ∀ (x : A), IsNilpotent x → τ x = 0)
(hnondeg : ∀ (a : A), (∀ (b : A), τ (b * a) = 0) → a = 0)
:
A finite-dimensional complex algebra with a linear functional
vanishing on nilpotents and nondegenerate in the form
(∀ b, τ (b * a) = 0) → a = 0 is semisimple.