Jordan normal form

7 fully proved

Jordan blocks

DefinitionJordan block#✓fully proved

For a natural number \(s\) and a scalar \(\mu\) in a field \(K\), the Jordan block of size \(s\) with eigenvalue \(\mu\) is the \(s \times s\) matrix over \(K\), with rows and columns indexed by \(\{0, \dots, s-1\}\), whose \((i, j)\) entry is \(1\) if \(j = i + 1\), \(\mu\) if \(i = j\), and \(0\) otherwise: it has \(\mu\) on the diagonal, \(1\) on the first superdiagonal and \(0\) elsewhere.

def jordanBlock (s : ℕ) (μ : K) : Matrix (Fin s) (Fin s) K :=
  fun i j => if i.val + 1 = j.val then 1 else if i = j then μ else 0

Sources

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

Used by 6

Used byJordan chain basis for an endomorphism with split characteristic polynomial · Jordan chain basis for a nilpotent endomorphism · Jordan normal form · Entries of a Jordan block · Matrix of an endomorphism on a basis of Jordan chains · Matrix of an endomorphism on a Jordan chain

TheoremEntries of a Jordan block#✓fully proved

For a natural number \(s\), a scalar \(\mu\) in a field \(K\) and indices \(i, j \in \{0, \dots, s-1\}\), the \((i, j)\) entry of the Jordan block of size \(s\) with eigenvalue \(\mu\) is \(1\) if \(j = i + 1\), is \(\mu\) if \(i = j\), and is \(0\) otherwise.

theorem jordanBlock_apply (s : ℕ) (μ : K) (i j : Fin s) :
    jordanBlock s μ i j = (if i.val + 1 = j.val then 1 else if i = j then μ else 0)

Sources

• https://en.wikipedia.org/wiki/Jordan_normal_form.

Uses 1

Statement usesJordan block

Linear Map

TheoremMatrix of an endomorphism on a Jordan chain#✓fully proved

Let \(V\) be a vector space over a field \(K\), let \(f\) be a linear endomorphism of \(V\), let \(\mu \in K\), and let \(b_0, \dots, b_d\) be a basis of \(V\) such that \(f(b_0) = \mu b_0\) and \(f(b_{j+1}) = \mu b_{j+1} + b_j\) for every \(j < d\). Then the matrix of \(f\) with respect to the basis \((b_0, \dots, b_d)\) is the Jordan block of size \(d + 1\) with eigenvalue \(\mu\).

theorem toMatrix_eq_jordanBlock
    {V : Type*} [AddCommGroup V] [Module K V]
    (d : ℕ) (b : Basis (Fin (d + 1)) K V) (f : Module.End K V) (μ : K)
    (hzero : f (b 0) = μ • b 0)
    (hsucc : ∀ j : Fin d, f (b j.succ) = μ • b j.succ + b j.castSucc) :
    LinearMap.toMatrix b b f = jordanBlock (d + 1) μ

Uses 1

Statement usesJordan block

TheoremMatrix of an endomorphism on a basis of Jordan chains#✓fully proved

Let \(V\) be a vector space over a field \(K\), let \(f\) be a linear endomorphism of \(V\), and let \(\iota\) be a finite set. For each \(i \in \iota\) let \(d_i \in \mathbb{N}\) and \(\mu_i \in K\), and let \((b_{i,r})\), indexed by \(i \in \iota\) and \(0 \le r \le d_i\), be a basis of \(V\) such that \(f(b_{i,0}) = \mu_i b_{i,0}\) and \(f(b_{i,j+1}) = \mu_i b_{i,j+1} + b_{i,j}\) for every \(i \in \iota\) and every \(j < d_i\). Then the matrix of \(f\) with respect to \(b\) is the block-diagonal matrix whose \(i\)-th diagonal block is the Jordan block of size \(d_i + 1\) with eigenvalue \(\mu_i\).

theorem toMatrix_eq_blockDiagonal_jordanBlock
    {V ι : Type*} [AddCommGroup V] [Module K V] [Fintype ι] [DecidableEq ι]
    (d : ι → ℕ) (b : Basis (Σ i, Fin (d i + 1)) K V) (f : Module.End K V) (μ : ι → K)
    (hzero : ∀ i, f (b ⟨i, 0⟩) = μ i • b ⟨i, 0⟩)
    (hsucc : ∀ i (j : Fin (d i)),
      f (b ⟨i, j.succ⟩) = μ i • b ⟨i, j.succ⟩ + b ⟨i, j.castSucc⟩) :
    LinearMap.toMatrix b b f =
      Matrix.blockDiagonal' (fun i ↦ jordanBlock (d i + 1) (μ i))

Uses 1 · Used by 2

Statement usesJordan block

Used byJordan chain basis for an endomorphism with split characteristic polynomial · Jordan chain basis for a nilpotent endomorphism

Endomorphisms

TheoremJordan chain basis for a nilpotent endomorphism#✓fully proved

Let \(V\) be a finite-dimensional vector space over a field \(K\) and let \(f\) be a nilpotent linear endomorphism of \(V\). Then there are \(k \in \mathbb{N}\), natural numbers \(d_0, \dots, d_{k-1}\) and a basis \((b_{i,r})\) of \(V\), indexed by \(i < k\) and \(0 \le r \le d_i\), such that \(f(b_{i,0}) = 0\) and \(f(b_{i,j+1}) = b_{i,j}\) for every \(i < k\) and every \(j < d_i\), and such that the matrix of \(f\) with respect to \(b\) is the block-diagonal matrix whose \(i\)-th diagonal block is the Jordan block of size \(d_i + 1\) with eigenvalue \(0\).

theorem exists_jordanBasis_of_isNilpotent
    {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    (f : Module.End K V) (hf : IsNilpotent f) :
    ∃ (k : ℕ) (d : Fin k → ℕ) (b : Basis (Σ i, Fin (d i + 1)) K V),
      (∀ i, f (b ⟨i, 0⟩) = 0) ∧
      (∀ i (j : Fin (d i)), f (b ⟨i, j.succ⟩) = b ⟨i, j.castSucc⟩) ∧
      LinearMap.toMatrix b b f =
        Matrix.blockDiagonal' (fun i ↦ jordanBlock (d i + 1) 0)

Uses 2 · Used by 1

Statement usesJordan block

Proof usesMatrix of an endomorphism on a basis of Jordan chains

Used byJordan chain basis for an endomorphism with split characteristic polynomial

TheoremJordan chain basis for an endomorphism with split characteristic polynomial#✓fully proved

Let \(V\) be a finite-dimensional vector space over a field \(K\) and let \(f\) be a linear endomorphism of \(V\) whose characteristic polynomial splits into linear factors over \(K\). Then there are \(k \in \mathbb{N}\), natural numbers \(d_0, \dots, d_{k-1}\), scalars \(\mu_0, \dots, \mu_{k-1} \in K\) and a basis \((b_{i,r})\) of \(V\), indexed by \(i < k\) and \(0 \le r \le d_i\), such that \(f(b_{i,0}) = \mu_i b_{i,0}\) and \(f(b_{i,j+1}) = \mu_i b_{i,j+1} + b_{i,j}\) for every \(i < k\) and every \(j < d_i\), and such that the matrix of \(f\) with respect to \(b\) is the block-diagonal matrix whose \(i\)-th diagonal block is the Jordan block of size \(d_i + 1\) with eigenvalue \(\mu_i\).

theorem exists_jordanBasis_of_charpoly_splits
    {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    (f : Module.End K V) (hf : f.charpoly.Splits) :
    ∃ (k : ℕ) (d : Fin k → ℕ) (μ : Fin k → K)
      (b : Basis (Σ i, Fin (d i + 1)) K V),
      (∀ i, f (b ⟨i, 0⟩) = μ i • b ⟨i, 0⟩) ∧
      (∀ i (j : Fin (d i)),
        f (b ⟨i, j.succ⟩) = μ i • b ⟨i, j.succ⟩ + b ⟨i, j.castSucc⟩) ∧
      LinearMap.toMatrix b b f =
        Matrix.blockDiagonal' (fun i ↦ jordanBlock (d i + 1) (μ i))

Uses 3 · Used by 1

Statement usesJordan block

Proof usesMatrix of an endomorphism on a basis of Jordan chains · Jordan chain basis for a nilpotent endomorphism

Used byJordan normal form

Jordan normal form

TheoremJordan normal form#✓fully proved

Let \(A\) be a square matrix over a field \(K\), with rows and columns indexed by a finite set \(N\), whose characteristic polynomial splits into linear factors over \(K\). Then \(A\) is similar to a block-diagonal matrix of Jordan blocks: there are \(k \in \mathbb{N}\), positive integers \(s_0, \dots, s_{k-1}\), scalars \(\mu_0, \dots, \mu_{k-1} \in K\), an invertible matrix \(P\) with rows and columns indexed by \(N\), and a bijection \(e\) from the set of pairs \((i, r)\) with \(i < k\) and \(r < s_i\) onto \(N\), such that \(A = P J P^{-1}\), where \(J\) is the block-diagonal matrix whose \(i\)-th diagonal block is the Jordan block of size \(s_i\) with eigenvalue \(\mu_i\), with its rows and columns relabelled by \(e\).

Proof: Decompose into the maximal generalized eigenspaces (Axler, Linear Algebra Done Right, 4th ed., 8.22), take a Jordan-chain basis of each nilpotent restriction, and collect them as in the proof of Axler 8.46. The nilpotent case is proved by induction on the range, extending chains by preimages and adding kernel vectors, as in Wikipedia, "Jordan normal form", section "A proof".

theorem exists_jordan_normal_form_of_splits
    {n : Type*} [Fintype n] [DecidableEq n]
    (A : Matrix n n K) (h : A.charpoly.Splits) :
    ∃ (k : ℕ) (s : Fin k → ℕ) (μ : Fin k → K) (P : Matrix n n K)
      (e : (Σ i, Fin (s i)) ≃ n),
      (∀ i, 0 < s i) ∧ IsUnit P ∧
        A = P * Matrix.reindex e e
          (Matrix.blockDiagonal' (fun i => jordanBlock (s i) (μ i))) * P⁻¹

Sources

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

Uses 2

Statement usesJordan block

Proof usesJordan chain basis for an endomorphism with split characteristic polynomial

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.