Diagonalization

TheoremEigenbasis of a semisimple endomorphism with split characteristic polynomial#✓fully proved

Let \(V\) be a finite-dimensional vector space over a field \(K\) and let \(f\) be a semisimple endomorphism of \(V\) (every \(f\)-invariant subspace has an \(f\)-invariant complement) whose characteristic polynomial splits over \(K\). Then for every finite type \(\iota\) with exactly \(\dim_K V\) elements there are a basis \((b_i)_{i \in \iota}\) of \(V\) and scalars \((\mu_i)_{i \in \iota}\) in \(K\) such that each \(b_i\) is an eigenvector of \(f\) with eigenvalue \(\mu_i\).

Proof: The minimal polynomial is squarefree and splits, so it is a product of distinct factors \(X - \mu\). The kernels lemma for these factors, proved by induction from the two-factor case, shows that the eigenspaces span \(V\), and bases of the eigenspaces are collected and reindexed. This is the diagonalizability criterion derived from the kernels lemma in the French Wikipedia article Lemme des noyaux, https://fr.wikipedia.org/wiki/Lemme_des_noyaux.

theorem exists_eigenbasis_of_isSemisimple_of_splits
    {ι : Type*} [Fintype ι]
    (f : Module.End K V) (hs : f.IsSemisimple) (h : f.charpoly.Splits)
    (hdim : Module.finrank K V = Fintype.card ι) :
    ∃ (b : Module.Basis ι K V) (μ : ι → K), ∀ i, f.HasEigenvector (μ i) (b i)

Sources

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Theorem 1.3.12.

TheoremDiagonalizability from a split characteristic polynomial and a squarefree minimal polynomial#✓fully proved

Let \(K\) be a field and let \(A\) be a square matrix over \(K\) with rows and columns indexed by a finite type \(n\). If the characteristic polynomial of \(A\) splits over \(K\) and the minimal polynomial of \(A\) (that is, of the linear map \(x \mapsto Ax\) on \(K^n\)) is squarefree, then there are matrices \(P\) and \(D\) over \(K\) indexed by \(n\), with \(D\) diagonal and \(P\) invertible, such that \(A = P D P^{-1}\).

Proof: A squarefree minimal polynomial makes the linear map \(x \mapsto Ax\) semisimple, so it has a basis of eigenvectors by the eigenbasis theorem for semisimple endomorphisms; conjugating by the change-of-basis matrix from the standard basis gives the diagonal form.

theorem exists_diagonal_similar_of_splits_of_squarefree_minpoly
    {n : Type*} [Fintype n] [DecidableEq n]
    (A : Matrix n n K) (hsplit : A.charpoly.Splits)
    (hsf : Squarefree (minpoly K (Matrix.toLin' A : Module.End K (n → K)))) :
    ∃ P D : Matrix n n K, D.IsDiag ∧ IsUnit P ∧ A = P * D * P⁻¹

Sources

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Theorem 1.3.12.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.