Diagonalizable endomorphisms are semisimple

Mathlib records that a semisimple endomorphism of a finite-dimensional vector space over an algebraically closed field is diagonalizable (Module.End.IsSemisimple.iSup_eigenspace_eq_top). This file proves the converse, which needs no hypothesis on the field and no finiteness hypothesis on the space: an endomorphism whose eigenspaces span is, as a K[X]-module, the sum of those eigenspaces, and on each of them X acts by a scalar, so each is annihilated by the squarefree polynomial X - C μ and is semisimple.

Main results

• Ado.isSemisimple_of_iSup_eigenspace_eq_top: an endomorphism whose eigenspaces span the space is semisimple.

theorem Ado.isSemisimple_of_iSup_eigenspace_eq_top {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} (hf : ⨆ (μ : K), f.eigenspace μ = ⊤) : f.IsSemisimple

A diagonalizable endomorphism is semisimple. If the eigenspaces of f span the space then f is semisimple.

Semisimplicity of f is semisimplicity of V as a K[X]-module, and the eigenspaces are K[X]-submodules spanning it, so it is enough that each is semisimple. On the μ-eigenspace X acts by the scalar μ, so the restriction of f is annihilated by the squarefree polynomial X - C μ and Module.End.isSemisimple_of_squarefree_aeval_eq_zero applies. Neither algebraic closure nor finite dimension is needed; the converse Module.End.IsSemisimple.iSup_eigenspace_eq_top is where both enter.