Advanced linear algebra · The Lumenary

Lens

MotivationH

Three questions a first course leaves open

A structural engineer in Nairobi models the stress at a point of a concrete beam by a symmetric $3 \times 3$ matrix. She needs the principal stresses — directions in which the material is pulled or pushed straight, with no shear — and she is confident that there are exactly three of them, at right angles to each other. Why should a symmetric matrix always have three mutually perpendicular eigenvector directions, when a general matrix need not have any real eigenvectors at all? The same question, asked by a statistician in São Paulo about a covariance matrix, is the foundation of principal component analysis.

A student in Hanoi solves the differential equation $x'' - 2x' + x = 0$ and finds the solutions $e^t$ and $t\,e^t$ . Where does the factor $t$ come from? Writing the equation as a system $\mathbf x' = A\mathbf x$ with $A = \begin{pmatrix} 0 & 1 \\ -1 & 2 \end{pmatrix}$ , the answer is that $A$ cannot be diagonalised. Something replaces diagonalisation for such matrices, and it is just as computable.

Finally, a physicist writes the state of two entangled photons as $\tfrac{1}{\sqrt2}(\lvert 0 \rangle \otimes \lvert 0 \rangle + \lvert 1 \rangle \otimes \lvert 1 \rangle)$ , and insists that it cannot be written as (state of photon 1) $\otimes$ (state of photon 2). What kind of object is $\otimes$ , and why is that impossible?

The first course in linear algebra stated the spectral theorem and mentioned the Jordan form. This lesson proves them, and builds the coordinate-free tools — dual spaces and tensor products — that answer the third question and underlie most of higher mathematics.

IntuitionH

Choosing coordinates well

A linear operator $T : V \to V$ has a different matrix in every basis; changing basis replaces $A$ by $P^{-1}AP$ . So the real question about $T$ is: in which basis does its matrix look simplest? Two answers organise the lesson.

If $V$ has an inner product and $T$ is self-adjoint (symmetric, in an orthonormal basis), we may insist on an orthonormal basis and still make the matrix diagonal, with real entries. Geometrically: $T$ maps the unit sphere to an ellipsoid, and the axes of the ellipsoid are perpendicular eigenvector directions. That is the spectral theorem.
For an arbitrary operator on a complex vector space we cannot always diagonalise, but we can always reach the Jordan normal form: block diagonal, each block having one eigenvalue on its diagonal and $1$ s just above it. The $1$ s record exactly how far $T$ is from being diagonalisable, and they are what produce the $t\,e^t$ .

The second half of the lesson goes the other way and removes coordinates altogether. A linear functional — a linear map $V \to k$ — is the coordinate-free version of a row vector; they form the dual space $V^*$ . A tensor product $V \otimes W$ is the space in which bilinear expressions in $v$ and $w$ become linear. Both are defined by what they do, not by a choice of basis, and the difference between "natural" and "chosen" identifications turns out to be mathematics in its own right.

DefinitionsH

Definitions

Throughout, $k$ is a field and vector spaces are finite-dimensional unless said otherwise.

Definition— inner product space

A real inner product space is a real vector space $V$ with a map $\langle \cdot, \cdot \rangle : V \times V \to \R$ that is bilinear, symmetric ( $\langle v, w \rangle = \langle w, v \rangle$ ) and positive definite ( $\langle v, v \rangle > 0$ for $v \neq 0$ ). A complex inner product is instead sesquilinear: conjugate-linear in the first slot and linear in the second, with $\langle w, v \rangle = \overline{\langle v, w \rangle}$ and $\langle v, v \rangle > 0$ for $v \ne 0$ . (Physicists and Mathlib use this convention; many algebra texts put the conjugate in the second slot. Nothing below depends on the choice.) We write $\|v\| = \sqrt{\langle v, v \rangle}$ . Vectors are orthogonal if $\langle v, w \rangle = 0$ , and $U^\perp = \{ v : \langle u, v \rangle = 0 \text{ for all } u \in U \}$ .

Definition— adjoint, self-adjoint, normal, unitary

The adjoint of $T : V \to V$ is the unique operator $T^*$ with $\langle Tv, w \rangle = \langle v, T^* w \rangle$ for all $v, w$ . (It exists: for fixed $w$ , the map $v \mapsto \langle w, Tv \rangle$ is a linear functional, so by the Riesz representation of Theorem 13 it equals $\langle u, \cdot \rangle$ for a unique $u$ ; conjugating, $\langle Tv, w \rangle = \langle v, u \rangle$ , and we set $T^* w = u$ .) In an orthonormal basis, the matrix of $T^*$ is the conjugate transpose $\overline{A}^{\mathsf T}$ of the matrix $A$ of $T$ . The operator $T$ is self-adjoint if $T^* = T$ (a symmetric matrix $A^{\mathsf T} = A$ over $\R$ , a Hermitian matrix $\overline{A}^{\mathsf T} = A$ over $\C$ ), normal if $TT^* = T^*T$ , and unitary (orthogonal over $\R$ ) if $T^*T = I$ .

Definition— minimal polynomial

The minimal polynomial $m_T$ of $T$ is the monic polynomial of least degree with $m_T(T) = 0$ . (It exists because $I, T, T^2, \dots, T^{n^2}$ are $n^2 + 1$ vectors in the $n^2$ -dimensional space of operators, hence dependent.) The characteristic polynomial is $\chi_T(x) = \det(xI - T)$ .

Definition— generalised eigenspace, Jordan block

For an eigenvalue $\lambda$ of $T$ on an $n$ -dimensional space, the generalised eigenspace is $G_\lambda = \ker (T - \lambda I)^n$ . The Jordan block $J_m(\lambda)$ is the $m \times m$ matrix with $\lambda$ on the diagonal, $1$ directly above the diagonal and $0$ elsewhere:

J_3(\lambda) = \begin{pmatrix} \lambda & 1 & 0 \\ 0 & \lambda & 1 \\ 0 & 0 & \lambda \end{pmatrix}.

A matrix is in Jordan normal form if it is block diagonal with Jordan blocks on the diagonal. An operator $N$ is nilpotent if $N^r = 0$ for some $r$ .

Definition— dual space, dual basis, dual map

The dual space of $V$ is $V^* = \Hom(V, k)$ , the space of linear functionals. If $e_1, \dots, e_n$ is a basis of $V$ , the dual basis $e_1^*, \dots, e_n^*$ of $V^*$ is defined by $e_i^*(e_j) = 1$ if $i = j$ and $0$ otherwise. A linear map $f : V \to W$ has a dual map (transpose) $f^* : W^* \to V^*$ , $f^*(\varphi) = \varphi \circ f$ ; note that it goes backwards. The evaluation map $\mathrm{ev}_V : V \to V^{**}$ sends $v$ to the functional "evaluate at $v$ ": $\mathrm{ev}_V(v)(\varphi) = \varphi(v)$ .

Definition— tensor product

A map $B : V \times W \to U$ is bilinear if it is linear in each variable when the other is fixed. A tensor product of $V$ and $W$ is a vector space $V \otimes W$ with a bilinear map $\otimes : V \times W \to V \otimes W$ , $(v, w) \mapsto v \otimes w$ , such that every bilinear map $B : V \times W \to U$ factors uniquely as $B(v, w) = \varphi(v \otimes w)$ for a linear map $\varphi : V \otimes W \to U$ . Elements of the form $v \otimes w$ are called pure (or simple, or rank-one) tensors.

Worked examplesH

Examples and non-examples

Example— Principal axes of a quadratic form

The quadratic form $q(x, y) = 5x^2 + 4xy + 2y^2$ is $q(\mathbf x) = \mathbf x^{\mathsf T} A \mathbf x$ with the symmetric matrix $A = \begin{pmatrix} 5 & 2 \\ 2 & 2 \end{pmatrix}$ . Its characteristic polynomial is $\lambda^2 - 7\lambda + 6 = (\lambda - 6)(\lambda - 1)$ , with eigenvectors $(2, 1)$ for $6$ and $(1, -2)$ for $1$ — orthogonal, as the spectral theorem promises. With the orthonormal coordinates $u = (2x + y)/\sqrt5$ and $v = (x - 2y)/\sqrt5$ ,

5x^2 + 4xy + 2y^2 = 6u^2 + v^2,

as one checks by expanding: $6(2x + y)^2 + (x - 2y)^2 = 25x^2 + 20xy + 10y^2$ . So the curve $q = 6$ is an ellipse with semi-axis $1$ along $(2, 1)$ and semi-axis $\sqrt6$ along $(1, -2)$ . The cross term $4xy$ only says that we were using the wrong axes.

The ellipse and its principal axes

A point moves along the curve as t changes: x and y are both functions of t.

5x² + 4xy + 2y² = 6
semi-axis 1 along (2, 1)
semi-axis √6 along (1, −2)

Move along tt = 0.79

(1.407, −1.233)
(−0.671, −0.335)
(−0.822, 1.643)

Example— Normal but not symmetric; neither normal nor diagonalisable

The rotation $R = \begin{pmatrix} 0 & -1 \\ 1 & 0 \end{pmatrix}$ is orthogonal, hence normal ( $RR^{\mathsf T} = I = R^{\mathsf T}R$ ), but not symmetric. It has no real eigenvalues, so it is not diagonalisable over $\R$ ; over $\C$ it has eigenvalues $\pm i$ with orthogonal eigenvectors $(1, \mp i)$ and is unitarily diagonalisable, as Theorem 6 predicts. The shear $S = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}$ is not normal ( $SS^{\mathsf T} \ne S^{\mathsf T}S$ ) and not diagonalisable over any field: it is the Jordan block $J_2(1)$ . And beware: the complex matrix $\begin{pmatrix} 1 & i \\ i & -1 \end{pmatrix}$ is symmetric but squares to $0$ , so it is nilpotent and not diagonalisable. Over $\C$ the right condition is Hermitian, not symmetric.

Example— A Jordan form, worked

Let $A = \begin{pmatrix} 1 & 1 & 0 \\ -1 & 3 & 0 \\ 0 & 0 & 2 \end{pmatrix}$ . Then $\chi_A(x) = \big((x - 1)(x - 3) + 1\big)(x - 2) = (x - 2)^3$ , so $2$ is the only eigenvalue. Put $N = A - 2I = \begin{pmatrix} -1 & 1 & 0 \\ -1 & 1 & 0 \\ 0 & 0 & 0 \end{pmatrix}$ : it has rank $1$ , and $N^2 = 0$ . By the rank formula of Theorem 12, the number of Jordan blocks of size at least $1$ is $3 - 1 = 2$ , and of size at least $2$ is $1 - 0 = 1$ . So the blocks have sizes $2$ and $1$ :

A \sim J_2(2) \oplus J_1(2) = \begin{pmatrix} 2 & 1 & 0 \\ 0 & 2 & 0 \\ 0 & 0 & 2 \end{pmatrix}, \qquad m_A(x) = (x - 2)^2 \ne \chi_A(x).

To find the basis: pick $v = e_1$ with $Nv = (-1, -1, 0) \ne 0$ ; then $N(Nv) = 0$ . In the basis $(Nv, v, e_3)$ we have $A(Nv) = 2\,Nv$ , $Av = 2v + Nv$ and $Ae_3 = 2e_3$ , which is the matrix above.

Example— The ODE with a repeated root

The companion matrix $A = \begin{pmatrix} 0 & 1 \\ -1 & 2 \end{pmatrix}$ of $x'' - 2x' + x = 0$ has $\chi_A(x) = (x - 1)^2$ and $A - I \neq 0$ , so $A \sim J_2(1) = I + N$ with $N^2 = 0$ . Since $I$ and $N$ commute, $e^{tJ_2(1)} = e^t e^{tN} = e^t (I + tN) = \begin{pmatrix} e^t & t e^t \\ 0 & e^t \end{pmatrix}$ . The $1$ above the diagonal is the $t\,e^t$ .

Example— A dual basis depends on the whole basis

In $V = \R^2$ take the basis $b_1 = (1, 0)$ , $b_2 = (1, 1)$ . Its dual basis is $b_1^*(x, y) = x - y$ and $b_2^*(x, y) = y$ : check that $b_1^*(b_1) = 1$ , $b_1^*(b_2) = 0$ , $b_2^*(b_1) = 0$ , $b_2^*(b_2) = 1$ . Although $b_1$ is the standard vector $e_1$ , its dual $b_1^*$ is not the standard functional $e_1^*(x, y) = x$ . There is no such thing as "the dual of a vector" — only the dual of a basis.

Example— Tensors as matrices; a tensor that is not pure

$\R^2 \otimes \R^3$ has basis $e_i \otimes f_j$ , so it is $6$ -dimensional, and sending $e_i \otimes f_j$ to the matrix unit $E_{ij}$ identifies it with the $2 \times 3$ matrices. Under this identification $v \otimes w \mapsto v\,w^{\mathsf T}$ ; for example $(1, 2) \otimes (1, 0, 1) \mapsto \begin{pmatrix} 1 & 0 & 1 \\ 2 & 0 & 2 \end{pmatrix}$ , a matrix of rank $1$ . Pure tensors are exactly the matrices of rank at most $1$ . Hence $e_1 \otimes e_1 + e_2 \otimes e_2 \in \R^2 \otimes \R^2$ , which corresponds to the identity matrix of rank $2$ , is not a pure tensor. In the same way $k[x] \otimes k[y] \cong k[x, y]$ via $x^i \otimes y^j \mapsto x^i y^j$ , pure tensors are products $f(x) g(y)$ , and $x + y$ is not one: if $f(x)g(y) = x + y$ , setting $y = 0$ gives $g(0) \neq 0$ and $f(0) = 0$ , while setting $x = 0$ gives $f(0) \neq 0$ .

ProofH

The spectral theorem

Let $V$ be a finite-dimensional real or complex inner product space and $T$ a self-adjoint operator on it.

Theorem— Lemma 1 (eigenvalues are real)

Every eigenvalue of a self-adjoint operator is real.

Proof

If $Tv = \mu v$ with $v \neq 0$ , then $\overline{\mu}\langle v, v \rangle = \langle Tv, v \rangle = \langle v, Tv \rangle = \mu \langle v, v \rangle$ , and $\langle v, v \rangle \neq 0$ , so $\overline\mu = \mu$ .

∎

Theorem— Lemma 2 (orthogonality of eigenvectors)

Eigenvectors of a self-adjoint operator for distinct eigenvalues are orthogonal.

Proof

If $Tv = av$ and $Tw = bw$ with $a \neq b$ (both real by Lemma 1), then $a\langle v, w \rangle = \langle Tv, w \rangle = \langle v, Tw \rangle = b\langle v, w \rangle$ , so $(a - b)\langle v, w \rangle = 0$ and $\langle v, w \rangle = 0$ .

∎

Theorem— Lemma 3 (invariant complements)

If $T$ is self-adjoint and $T(U) \subseteq U$ for a subspace $U$ , then $T(U^\perp) \subseteq U^\perp$ .

Proof

Let $w \in U^\perp$ and $u \in U$ . Then $\langle u, Tw \rangle = \langle Tu, w \rangle = 0$ because $Tu \in U$ . So $Tw \in U^\perp$ .

∎

Theorem— Lemma 4 (an eigenvector exists)

A self-adjoint operator on a non-zero space has an eigenvector.

Proof

Over $\C$ this is the fundamental theorem of algebra applied to $\chi_T$ . Over $\R$ we give a proof that uses no complex numbers. The Rayleigh quotient $q(v) = \langle Tv, v \rangle$ is continuous on the unit sphere $S = \{ \|v\| = 1 \}$ , which is compact, so $q$ attains a maximum at some $v_0 \in S$ . Let $w \perp v_0$ and put $f(t) = q\big((v_0 + tw)/\|v_0 + tw\|\big)$ , which has a maximum at $t = 0$ . Using $\langle Tw, v_0 \rangle = \langle w, Tv_0 \rangle$ ,

f(t) = \frac{\langle Tv_0, v_0 \rangle + 2t\langle Tv_0, w \rangle + t^2 \langle Tw, w \rangle}{1 + t^2\|w\|^2},

so $0 = f'(0) = 2\langle Tv_0, w \rangle$ . Thus $Tv_0$ is orthogonal to every $w \perp v_0$ , which means $Tv_0 \in (v_0^\perp)^\perp = \R v_0$ : $v_0$ is an eigenvector, with eigenvalue $\lambda_{\max} = \max_S q$ .

∎

Theorem— Theorem 5 (spectral theorem)

If $T$ is a self-adjoint operator on a finite-dimensional real or complex inner product space $V$ , then $V$ has an orthonormal basis of eigenvectors of $T$ , and all eigenvalues are real. Equivalently: every real symmetric matrix is $A = Q\Lambda Q^{\mathsf T}$ with $Q$ orthogonal and $\Lambda$ real diagonal, and every Hermitian matrix is $A = U \Lambda U^*$ with $U$ unitary and $\Lambda$ real diagonal. Conversely, a real operator with an orthonormal eigenbasis is symmetric.

Proof

Induction on $n = \dim V$ ; the case $n = 0$ is empty. For $n \geq 1$ , Lemma 4 gives a unit eigenvector $v_1$ , with real eigenvalue by Lemma 1. The line $U = k v_1$ is $T$ -invariant, so by Lemma 3 so is $W = U^\perp$ , which has dimension $n - 1$ . The restriction $T|_W$ is still self-adjoint (the defining identity holds for vectors of $W$ ), so by induction $W$ has an orthonormal basis $v_2, \dots, v_n$ of eigenvectors. Then $v_1, \dots, v_n$ is an orthonormal eigenbasis of $V$ . In matrix terms, the columns of $Q$ are the $v_i$ : $Q$ is orthogonal (or unitary) and $Q^{-1}AQ = \Lambda$ . Conversely, if $A = Q\Lambda Q^{\mathsf T}$ with $\Lambda$ real diagonal, then $A^{\mathsf T} = Q\Lambda^{\mathsf T}Q^{\mathsf T} = A$ .

∎

The proof of Lemma 4 gives more: $\lambda_{\max} = \max_{\|v\| = 1} \langle Tv, v \rangle$ , and repeating it on $v_1^\perp$ yields every eigenvalue as a constrained maximum (the Courant–Fischer minimax principle). For complex operators that are not self-adjoint the best possible statement is this.

Theorem— Theorem 6 (complex spectral theorem)

An operator $T$ on a finite-dimensional complex inner product space has an orthonormal basis of eigenvectors if and only if $T$ is normal.

Proof

If $T$ is diagonal in an orthonormal basis, so is $T^*$ (with conjugated entries), and diagonal matrices commute: $T$ is normal. Conversely, over $\C$ every operator has an upper triangular matrix in some basis $u_1, \dots, u_n$ (induct, using an eigenvector and the quotient space), which says the subspaces $\operatorname{span}(u_1, \dots, u_j)$ are $T$ -invariant. Gram–Schmidt produces an orthonormal basis with the same spans, so $T$ is upper triangular in an orthonormal basis — this is Schur's theorem. Now suppose $T$ is normal with upper triangular matrix $(a_{ij})$ in the orthonormal basis $e_1, \dots, e_n$ . For every $v$ , $\|Tv\|^2 = \langle v, T^*Tv \rangle = \langle v, TT^*v \rangle = \|T^*v\|^2$ . With $v = e_1$ : $\|Te_1\|^2 = |a_{11}|^2$ , while $\|T^* e_1\|^2 = \sum_j |a_{1j}|^2$ , since the first row of $A$ is the conjugated first column of $A^*$ . Hence $a_{12} = \dots = a_{1n} = 0$ . Repeating with $e_2, e_3, \dots$ shows that every off-diagonal entry vanishes.

∎

ProofH

Cayley–Hamilton, minimal polynomials and the Jordan form

Theorem— Theorem 7 (Cayley–Hamilton)

For every $n \times n$ matrix $A$ over a commutative ring, $\chi_A(A) = 0$ .

Proof

The tempting argument " $\chi_A(A) = \det(AI - A) = \det 0 = 0$ " is not valid: inside the determinant, $x$ multiplies the entries of $I$ , so substituting a matrix for $x$ is meaningless. Instead, let $B(x) = \operatorname{adj}(xI - A)$ . Its entries are polynomials of degree at most $n - 1$ , so $B(x) = \sum_{k=0}^{n-1} B_k x^k$ with matrices $B_k$ . The adjugate identity gives $(xI - A)B(x) = \chi_A(x) I$ . Write $\chi_A(x) = \sum_{k=0}^n c_k x^k$ and compare coefficients of $x^k$ , with $B_{-1} = B_n = 0$ :

B_{k-1} - AB_k = c_k I \qquad (0 \le k \le n).

Multiply the $k$ -th equation on the left by $A^k$ and add them up. The right-hand side is $\sum_k c_k A^k = \chi_A(A)$ ; the left-hand side $\sum_k (A^k B_{k-1} - A^{k+1}B_k)$ telescopes to $A^0B_{-1} - A^{n+1}B_n = 0$ .

∎

Theorem— Proposition 8 (minimal polynomial)

If $p(T) = 0$ then $m_T$ divides $p$ ; in particular $m_T \mid \chi_T$ . The roots of $m_T$ are exactly the eigenvalues of $T$ .

Proof

Divide: $p = q\,m_T + r$ with $\deg r < \deg m_T$ . Then $r(T) = p(T) - q(T)m_T(T) = 0$ , so $r = 0$ by minimality. If $Tv = \lambda v$ with $v \ne 0$ then $0 = m_T(T)v = m_T(\lambda)v$ , so $m_T(\lambda) = 0$ . Conversely, if $m_T(\lambda) = 0$ write $m_T = (x - \lambda)q$ ; since $\deg q < \deg m_T$ there is $w$ with $v = q(T)w \ne 0$ , and $(T - \lambda)v = m_T(T)w = 0$ .

∎

Theorem— Lemma 9 (kernel lemma)

If $p = p_1 p_2$ with $\gcd(p_1, p_2) = 1$ and $p(T) = 0$ , then $V = \ker p_1(T) \oplus \ker p_2(T)$ , and both summands are $T$ -invariant.

Proof

By Bézout there are polynomials $a, b$ with $a p_1 + b p_2 = 1$ , so $v = a(T)p_1(T)v + b(T)p_2(T)v$ for every $v$ . The first term lies in $\ker p_2(T)$ because $p_2(T)a(T)p_1(T)v = a(T)p(T)v = 0$ , and likewise the second lies in $\ker p_1(T)$ . If $v$ is in both kernels, the same identity gives $v = 0$ . Invariance holds because $T$ commutes with $p_i(T)$ .

∎

Theorem— Theorem 10 (diagonalisability)

$T$ is diagonalisable if and only if $m_T$ is a product of distinct linear factors.

Proof

If $T$ is diagonal with distinct eigenvalues $\lambda_1, \dots, \lambda_r$ , then $\prod (T - \lambda_i)$ kills every basis vector, so $m_T$ divides $\prod(x - \lambda_i)$ . Conversely, if $m_T = \prod_{i=1}^r (x - \lambda_i)$ with distinct $\lambda_i$ , repeated use of Lemma 9 gives $V = \bigoplus_i \ker(T - \lambda_i)$ , a direct sum of eigenspaces.

∎

Applied to $\chi_T = \prod_\lambda (x - \lambda)^{a_\lambda}$ over an algebraically closed field, Lemma 9 and Cayley–Hamilton split $V$ into the generalised eigenspaces, $V = \bigoplus_\lambda \ker(T - \lambda)^{a_\lambda} = \bigoplus_\lambda G_\lambda$ , and on $G_\lambda$ the operator $T - \lambda$ is nilpotent. So everything reduces to nilpotent operators.

Theorem— Theorem 11 (structure of nilpotent operators)

If $N$ is nilpotent on $V$ , there are vectors $v_1, \dots, v_m$ and integers $k_1, \dots, k_m \geq 1$ such that the vectors $N^j v_i$ ( $1 \le i \le m$ , $0 \le j < k_i$ ) form a basis of $V$ and $N^{k_i} v_i = 0$ . In this basis (each chain listed as $N^{k_i - 1}v_i, \dots, Nv_i, v_i$ ) the matrix of $N$ is $J_{k_1}(0) \oplus \dots \oplus J_{k_m}(0)$ .

Proof

Induction on $\dim V$ . If $N = 0$ , any basis works with all $k_i = 1$ . Otherwise $U = N(V)$ is a proper subspace (a nilpotent operator is not surjective) that $N$ maps into itself, so by induction $U$ has a basis $N^j u_i$ ( $0 \le j < k_i$ ) with $N^{k_i} u_i = 0$ . Choose $v_i$ with $Nv_i = u_i$ , and let $S$ be the list of vectors $N^j v_i$ for $0 \le j \le k_i$ (one longer chain each).

$S$ is independent. Suppose $\sum_{i,j} a_{ij} N^j v_i = 0$ . Applying $N$ gives $\sum_{i, j < k_i} a_{ij} N^j u_i = 0$ (the terms with $j = k_i$ die), so $a_{ij} = 0$ for $j < k_i$ . What is left is $\sum_i a_{ik_i} N^{k_i - 1} u_i = 0$ , again a sub-list of a basis, so all $a_{ik_i} = 0$ .

Extending. Extend $S$ to a basis of $V$ by vectors $w_1, \dots, w_p$ . Each $Nw_l$ lies in $U$ , which is spanned by $N$ applied to vectors of $S$ , so $Nw_l = Nx_l$ with $x_l \in \operatorname{span} S$ . Replace $w_l$ by $w_l - x_l$ : we still have a basis, and now $N(w_l - x_l) = 0$ , so each $w_l - x_l$ is a chain of length $1$ .

∎

Theorem— Theorem 12 (Jordan normal form)

Let $T$ be an operator on a finite-dimensional vector space over an algebraically closed field (such as $\C$ ). Then $T$ has a matrix in Jordan normal form, and this form is unique up to the order of the blocks. Precisely, for each eigenvalue $\lambda$ and $k \geq 1$ ,

\#\{\text{blocks } J_m(\lambda) \text{ with } m \ge k\} = \operatorname{rank}(T - \lambda)^{k-1} - \operatorname{rank}(T - \lambda)^k.

Proof

Existence. Decompose $V = \bigoplus_\lambda G_\lambda$ as above, apply Theorem 11 to the nilpotent operator $T - \lambda$ on each $G_\lambda$ , and add $\lambda I$ : a nilpotent Jordan block becomes $J_m(\lambda)$ .

Uniqueness. For a single block, $\operatorname{rank} J_m(0)^j = \max(m - j, 0)$ : each power shifts the chain by one more step. For $\mu \ne \lambda$ the block $J_m(\mu) - \lambda I$ is invertible, so its powers keep full rank $m$ . Adding over blocks, $\operatorname{rank}(T - \lambda)^{k-1} - \operatorname{rank}(T - \lambda)^k$ counts the blocks for $\lambda$ whose rank still drops at step $k$ , that is, those of size at least $k$ . These numbers depend only on $T$ , not on the basis, so they determine the multiset of blocks.

∎

So the minimal polynomial is $\prod_\lambda (x - \lambda)^{s_\lambda}$ with $s_\lambda$ the size of the largest block for $\lambda$ , while the characteristic polynomial records the total size $a_\lambda$ , and the number of blocks for $\lambda$ is $\dim \ker(T - \lambda)$ , the geometric multiplicity. Over a field that is not algebraically closed (such as $\Q$ or $\R$ ) the same theory, phrased with irreducible polynomials, gives the rational canonical form: every operator is similar to a block diagonal matrix of companion matrices of polynomials $d_1 \mid d_2 \mid \dots \mid d_r$ (the invariant factors, with $d_r = m_T$ and $d_1 \cdots d_r = \chi_T$ ), uniquely. We state it without proof: it is the structure theorem for finitely generated modules over the principal ideal domain $k[x]$ (see the algebra viewpoint below).

ProofH

Dual spaces: natural and unnatural isomorphisms

Theorem— Theorem 13 (dual basis)

If $e_1, \dots, e_n$ is a basis of $V$ , then $e_1^*, \dots, e_n^*$ is a basis of $V^*$ ; so $\dim V^* = \dim V$ . Every $\varphi \in V^*$ is $\varphi = \sum_i \varphi(e_i)\,e_i^*$ . If $V$ has an inner product, every $\varphi \in V^*$ is $\varphi = \langle u, \cdot \rangle$ for a unique $u \in V$ (the Riesz representation).

Proof

Both sides of $\varphi = \sum_i \varphi(e_i) e_i^*$ are linear and agree on each $e_j$ , so they are equal; this shows the $e_i^*$ span. If $\sum_i c_i e_i^* = 0$ , evaluating at $e_j$ gives $c_j = 0$ . For the Riesz statement, take an orthonormal basis and $u = \sum_i \overline{\varphi(e_i)}\,e_i$ ; then $\langle u, e_j \rangle = \varphi(e_j)$ for all $j$ . Uniqueness: if $\langle u - u', \cdot \rangle = 0$ , take the argument to be $u - u'$ .

∎

So $V \cong V^*$ for finite-dimensional $V$ — but every isomorphism we can write down uses a basis or an inner product. The double dual is different.

Theorem— Theorem 14 (the double dual)

The evaluation map $\mathrm{ev}_V : V \to V^{**}$ is linear and injective, hence an isomorphism when $V$ is finite-dimensional. It is natural: for every linear map $f : V \to W$ , $f^{**} \circ \mathrm{ev}_V = \mathrm{ev}_W \circ f$ .

Proof

Linearity is clear. If $v \neq 0$ , extend $v$ to a basis $v = e_1, e_2, \dots$ ; then $e_1^*(v) = 1$ , so $\mathrm{ev}_V(v) \neq 0$ . Since $\dim V^{**} = \dim V^* = \dim V$ , an injective linear map $V \to V^{**}$ is bijective. Naturality: for $\varphi \in W^*$ , $\big(f^{**}(\mathrm{ev}_V v)\big)(\varphi) = \mathrm{ev}_V(v)(f^* \varphi) = (\varphi \circ f)(v) = \mathrm{ev}_W(f v)(\varphi)$ .

∎

Naturality of the double dual: the square commutes for every linear map

f

, and no basis was chosen.

Theorem— Proposition 15 (no natural isomorphism with the dual)

Let $k$ be a field with more than three elements. There is no family of isomorphisms $\eta_V : V \to V^*$ , one for each finite-dimensional $V$ , such that $\eta_V = f^* \circ \eta_W \circ f$ for every isomorphism $f : V \to W$ .

Proof

The condition is the only sensible notion of naturality here: $V^*$ depends contravariantly on $V$ , so $f$ must be used on both sides. Take $V = W = k$ and $f = c \cdot \mathrm{id}$ with $c^2 \neq 1$ , which exists since $x^2 = 1$ has at most two roots and $k$ has more than three elements. Then $f^* = c \cdot \mathrm{id}$ as well, so the condition reads $\eta_k = c^2 \eta_k$ , forcing $\eta_k = 0$ , which is not an isomorphism.

∎

The same conclusion holds over every field, using $V = k^3$ instead of $k$ : the condition says that the bilinear form $b(v, w) = \eta(v)(w)$ satisfies $b(Av, Aw) = b(v, w)$ for all $A \in GL_3(k)$ . Since $GL_3(k)$ moves any pair of independent vectors to any other, $b(u, v) = c$ for all independent $u, v$ and $b(v, v) = d$ for all $v \ne 0$ ; then $c = b(u, v + w) = 2c$ and $c = b(v, v + w) = d + c$ (for independent $u, v, w$ ) force $c = d = 0$ , so $b = 0$ . An inner product does give an isomorphism $V \to V^*$ , $u \mapsto \langle u, \cdot \rangle$ (Theorem 13), natural with respect to the maps that preserve the inner product — this is the physicists' "raising and lowering of indices". In infinite dimensions $V \not\cong V^*$ in general: $V = k[x]$ has countable dimension, $V^*$ can be identified with the power series $k[[x]]$ , and when $k$ is countable $V^*$ has uncountable dimension (a theorem of Erdős and Kaplansky), so $\mathrm{ev}_V$ is injective but not surjective.

ProofH

Tensor products and multilinear algebra

Theorem— Theorem 16 (existence, uniqueness and dimension)

The tensor product $V \otimes W$ exists and is unique up to a unique isomorphism compatible with $\otimes$ . If $(e_i)$ is a basis of $V$ and $(f_j)$ a basis of $W$ , then $(e_i \otimes f_j)$ is a basis of $V \otimes W$ ; in particular $\dim(V \otimes W) = \dim V \cdot \dim W$ .

Proof

Existence. Let $T$ be the vector space with basis symbols $t_{ij}$ and define $v \otimes w = \sum_{i,j} a_i b_j t_{ij}$ for $v = \sum a_i e_i$ , $w = \sum b_j f_j$ ; this is bilinear. Given a bilinear $B$ , a linear $\varphi$ with $\varphi(v \otimes w) = B(v, w)$ must satisfy $\varphi(t_{ij}) = \varphi(e_i \otimes f_j) = B(e_i, f_j)$ , which determines $\varphi$ on a basis; conversely this $\varphi$ works, by bilinearity of $B$ . So $T$ is a tensor product and $e_i \otimes f_j = t_{ij}$ is a basis.

Uniqueness. If $(P, \otimes)$ and $(P', \otimes')$ both have the universal property, the bilinear map $\otimes'$ factors as $\alpha \circ \otimes$ and $\otimes$ as $\beta \circ \otimes'$ . Then $\beta\alpha \circ \otimes = \otimes = \mathrm{id} \circ \otimes$ , and uniqueness in the universal property gives $\beta \alpha = \mathrm{id}$ ; likewise $\alpha \beta = \mathrm{id}$ .

∎

Theorem— Proposition 17 (tensors as linear maps)

For finite-dimensional $V, W$ the linear map $V^* \otimes W \to \Hom(V, W)$ induced by $(\varphi, w) \mapsto (v \mapsto \varphi(v)\,w)$ is an isomorphism. A tensor is pure exactly when the corresponding map has rank at most $1$ , and every tensor $t$ is a sum of $r$ pure tensors, where $r = \operatorname{rank}$ of the corresponding map, and no fewer.

Proof

The map sends the basis $e_i^* \otimes f_j$ to the map $e_i \mapsto f_j$ , other basis vectors $\mapsto 0$ — the matrix unit $E_{ji}$ — so it sends a basis to a basis. A pure tensor $\varphi \otimes w$ goes to $v \mapsto \varphi(v)w$ , whose image lies in the line through $w$ . A map of rank $r$ is a sum of $r$ maps of rank $1$ (choose a basis $w_1, \dots, w_r$ of its image and write it as $v \mapsto \sum_l \varphi_l(v)w_l$ ), and a sum of fewer than $r$ rank-one maps has rank less than $r$ .

∎

Multilinear algebra and the determinant. Tensor powers $V^{\otimes p} \otimes (V^*)^{\otimes q}$ hold the objects of physics and geometry (vectors, covectors, bilinear forms, stress and curvature tensors), and dividing out by symmetries gives the symmetric powers $S^pV$ (polynomials) and the exterior powers $\Lambda^p V$ . Their most famous use is a coordinate-free determinant: if $\dim V = n$ , the alternating $n$ -linear forms on $V$ form a one-dimensional space (such a form is fixed by its value on a basis, since expanding $\omega(\sum a_{i1}e_i, \dots)$ by multilinearity kills repeated vectors and turns permutations into signs, and the Leibniz formula gives a non-zero one). So for any non-zero alternating form $\omega$ there is a unique scalar $\det T$ with $\omega(Tv_1, \dots, Tv_n) = \det T \cdot \omega(v_1, \dots, v_n)$ , independent of $\omega$ . Then $\det(ST) = \det S \det T$ is immediate: apply the definition twice.

Formal mathematicsF

The theorems in Lean and Mathlib

Mathlib's InnerProductSpace 𝕜 E works over 𝕜 = ℝ or ℂ at once (the class RCLike), and T.IsSymmetric means $\langle Tx, y \rangle = \langle x, Ty \rangle$ . As in the lesson, the inner product is conjugate-linear in the first slot. Lemmas 1 and 2, proved here exactly as above:

eigenvalue_realLean 4Proved here from basic factsFormally verified

/-- **Eigenvalues of a self-adjoint operator are real.** If `T v = μ v` with `v ≠ 0`, then
`conj μ ⟪v, v⟫ = ⟪T v, v⟫ = ⟪v, T v⟫ = μ ⟪v, v⟫`, and `⟪v, v⟫ ≠ 0` can be cancelled. (Mathlib's
inner product is conjugate-linear in the *first* slot, hence the `conj` on the left.) This is
Lemma 1 of the lesson; Mathlib's version is `LinearMap.IsSymmetric.conj_eigenvalue_eq_self`. -/
theorem eigenvalue_real {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
    {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {μ : 𝕜} {v : E} (hv0 : v ≠ 0) (hv : T v = μ • v) :
    starRingEnd 𝕜 μ = μ := by
  have h : starRingEnd 𝕜 μ * inner 𝕜 v v = μ * inner 𝕜 v v :=
    calc starRingEnd 𝕜 μ * inner 𝕜 v v = inner 𝕜 (T v) v := by rw [hv, inner_smul_left]
      _ = inner 𝕜 v (T v) := hT v v
      _ = μ * inner 𝕜 v v := by rw [hv, inner_smul_right]
  exact mul_right_cancel₀ (inner_self_ne_zero.mpr hv0) h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

eigenvectors_orthogonalLean 4Proved here from basic factsFormally verified

/-- **Eigenvectors of a symmetric operator for distinct eigenvalues are orthogonal.** The proof
is Lemma 2 of the lesson: `a ⟪v, w⟫ = ⟪T v, w⟫ = ⟪v, T w⟫ = b ⟪v, w⟫`, so `(a - b) ⟪v, w⟫ = 0`
and `a ≠ b` forces `⟪v, w⟫ = 0`. -/
theorem eigenvectors_orthogonal {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) {a b : ℝ} {v w : E}
    (hv : T v = a • v) (hw : T w = b • w) (hab : a ≠ b) : inner ℝ v w = 0 := by
  have h : a * inner ℝ v w = b * inner ℝ v w :=
    calc a * inner ℝ v w = inner ℝ (T v) w := by rw [hv, real_inner_smul_left]
      _ = inner ℝ v (T w) := hT v w
      _ = b * inner ℝ v w := by rw [hw, real_inner_smul_right]
  have h2 : (a - b) * inner ℝ v w = 0 := by rw [sub_mul, h, sub_self]
  exact (mul_eq_zero.mp h2).resolve_left (sub_ne_zero.mpr hab)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

The spectral theorem (Theorem 5) and its matrix form are in Mathlib. Its proof shows that the eigenspaces are orthogonal and together span $E$ — a variant of the induction above:

spectral_theoremLean 4Applies a library theoremFormally verified

/-- **The spectral theorem.** A self-adjoint operator `T` on a finite-dimensional real or complex
inner product space of dimension `n` has an orthonormal basis `b` of eigenvectors, with *real*
eigenvalues `μ i`. This packages Mathlib's `LinearMap.IsSymmetric.eigenvectorBasis`,
`eigenvalues` and `apply_eigenvectorBasis`; Mathlib's proof is the lesson's (eigenspaces are
orthogonal and together span `E`). -/
theorem spectral_theorem {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
    [FiniteDimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) {T : E →ₗ[𝕜] E}
    (hT : T.IsSymmetric) :
    ∃ (b : OrthonormalBasis (Fin n) 𝕜 E) (μ : Fin n → ℝ), ∀ i, T (b i) = (μ i : 𝕜) • b i :=
  ⟨hT.eigenvectorBasis hn, hT.eigenvalues hn, hT.apply_eigenvectorBasis hn⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

symmetric_matrix_eigenbasisLean 4Applies a library theoremFormally verified

/-- **Real symmetric matrices are orthogonally diagonalisable.** For a real matrix with `Aᵀ = A`
there is an orthonormal basis of `ℝⁿ` (the columns of an orthogonal matrix `Q`) consisting of
eigenvectors of `A`; equivalently `A = Q Λ Qᵀ`. Over `ℝ` the conjugate transpose is the
transpose, so `A` is Hermitian, and Mathlib's `Matrix.IsHermitian.mulVec_eigenvectorBasis`
applies. -/
theorem symmetric_matrix_eigenbasis {n : Type*} [Fintype n] [DecidableEq n]
    (A : Matrix n n ℝ) (hA : Aᵀ = A) :
    ∃ (b : OrthonormalBasis n ℝ (EuclideanSpace ℝ n)) (μ : n → ℝ),
      ∀ j, A.mulVec (b j) = μ j • (b j : n → ℝ) := by
  have hH : A.IsHermitian := by
    rw [Matrix.IsHermitian, Matrix.conjTranspose_eq_transpose_of_trivial]
    exact hA
  exact ⟨hH.eigenvectorBasis, hH.eigenvalues, hH.mulVec_eigenvectorBasis⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

Why the hypothesis over $\C$ must be Hermitian, not merely symmetric:

complex_symmetric_nilpotentLean 4Proved here from basic factsFormally verified

/-- **"Symmetric" is not enough over `ℂ`.** The complex symmetric matrix with rows `(1, i)` and
`(i, -1)` is non-zero but squares to zero, so it is nilpotent and not diagonalisable. Over `ℂ` the
spectral theorem needs *Hermitian* (`A* = A`), not symmetric (`Aᵀ = A`). -/
theorem complex_symmetric_nilpotent :
    let A : Matrix (Fin 2) (Fin 2) ℂ := !![1, Complex.I; Complex.I, -1]
    Aᵀ = A ∧ A ≠ 0 ∧ A * A = 0 := by
  intro A
  refine ⟨?_, ?_, ?_⟩
  · ext i j
    fin_cases i <;> fin_cases j <;> simp [A]
  · intro h
    have := congrFun (congrFun h 0) 0
    simp [A] at this
  · ext i j
    fin_cases i <;> fin_cases j <;> simp [A, Matrix.mul_apply, Fin.sum_univ_two]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

Cayley–Hamilton: a direct computation for $2 \times 2$ matrices, and the general theorem from Mathlib, proved there with the adjugate as in Theorem 7.

cayley_hamilton_twoLean 4Proved here from basic factsFormally verified

/-- **Cayley–Hamilton for 2 × 2 matrices**, by direct computation over any commutative ring:
`A² − (tr A) A + (det A) I = 0`. The characteristic polynomial of `A` is
`x² − (tr A) x + det A`, so this says `χ_A(A) = 0`. -/
theorem cayley_hamilton_two {R : Type*} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) :
    A * A - A.trace • A + A.det • (1 : Matrix (Fin 2) (Fin 2) R) = 0 := by
  ext i j
  fin_cases i <;> fin_cases j <;>
    simp [Matrix.mul_apply, Fin.sum_univ_two, Matrix.trace_fin_two, Matrix.det_fin_two] <;> ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

cayley_hamiltonLean 4Applies a library theoremFormally verified

/-- **The Cayley–Hamilton theorem**: every square matrix over a commutative ring is a root of its
characteristic polynomial, `χ_A(A) = 0`. This is Mathlib's `Matrix.aeval_self_charpoly`, proved
(like the lesson) with the adjugate identity `(x I − A) · adj(x I − A) = χ_A(x) I`. -/
theorem cayley_hamilton {R : Type*} [CommRing R] {n : Type*} [Fintype n] [DecidableEq n]
    (A : Matrix n n R) : Polynomial.aeval A A.charpoly = 0 :=
  Matrix.aeval_self_charpoly A

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

A Jordan block and its minimal polynomial: $N = J_3(\mu) - \mu I$ satisfies $N^3 = 0$ but $N^2 \ne 0$ , so $m = (x - \mu)^3$ .

jordanBlock3Lean 4Formally verified

/-- The 3 × 3 **Jordan block** `J₃(μ)`: `μ` on the diagonal, `1` just above it. -/
def jordanBlock3 {K : Type*} [Field K] (μ : K) : Matrix (Fin 3) (Fin 3) K :=
  !![μ, 1, 0; 0, μ, 1; 0, 0, μ]

Axioms used: propext, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

jordan_block3_nilpotentLean 4Proved here from basic factsFormally verified

/-- `N = J₃(μ) − μ I` is nilpotent: `N³ = 0`. So `(x − μ)³` annihilates `J₃(μ)`. -/
theorem jordan_block3_nilpotent {K : Type*} [Field K] (μ : K) :
    (jordanBlock3 μ - μ • (1 : Matrix (Fin 3) (Fin 3) K)) ^ 3 = 0 := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [jordanBlock3, pow_succ, Matrix.mul_apply, Fin.sum_univ_three]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

jordan_block3_sq_ne_zeroLean 4Proved here from basic factsFormally verified

/-- …but `N² ≠ 0` (its top-right entry is `1`). Together with `N³ = 0` this shows that the
minimal polynomial of `J₃(μ)` is `(x − μ)³`, equal to the characteristic polynomial: no
polynomial of smaller degree kills it, so it is not diagonalisable. -/
theorem jordan_block3_sq_ne_zero {K : Type*} [Field K] (μ : K) :
    (jordanBlock3 μ - μ • (1 : Matrix (Fin 3) (Fin 3) K)) ^ 2 ≠ 0 := by
  intro h
  have h02 := congrFun (congrFun h 0) 2
  simp [jordanBlock3, pow_succ, Matrix.mul_apply, Fin.sum_univ_three] at h02

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

The first half of the Jordan normal form theorem, the decomposition into generalised eigenspaces:

generalized_eigenspace_decompositionLean 4Applies a library theoremFormally verified

/-- **The generalised eigenspace (primary) decomposition**, the first half of the Jordan normal
form theorem: over an algebraically closed field, the generalised eigenspaces
`ker (f − μ)^∞` of an operator on a finite-dimensional space are independent and together span
the space, so `V` is their direct sum. Mathlib: `Module.End.independent_maxGenEigenspace` and
`Module.End.iSup_maxGenEigenspace_eq_top` (the latter following Axler's proof). -/
theorem generalized_eigenspace_decomposition {K V : Type*} [Field K] [IsAlgClosed K]
    [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) :
    iSupIndep f.maxGenEigenspace ∧ ⨆ μ : K, f.maxGenEigenspace μ = ⊤ :=
  ⟨f.independent_maxGenEigenspace, f.iSup_maxGenEigenspace_eq_top⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

Duality. Naturality of $V \to V^{**}$ is true by definition — Lean accepts rfl — which is a precise sense in which no choice was made. The isomorphism itself, and $\dim V^* = \dim V$ , come from Mathlib:

eval_naturalLean 4Proved here from basic factsFormally verified

/-- **`V → V**` is natural.** For every linear map `f : V → W`, the square
`V → V** → W**` equals `V → W → W**`: evaluating at `v` and then transporting along `f**` is the
same as evaluating at `f v`. No basis appears anywhere — the proof is a definitional unfolding
(`rfl`), which is exactly what "natural" means in practice. -/
theorem eval_natural {K V W : Type*} [Field K] [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W] (f : V →ₗ[K] W) :
    f.dualMap.dualMap ∘ₗ Dual.eval K V = Dual.eval K W ∘ₗ f := by
  ext v φ
  rfl

Axioms used: propext, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

eval_bijectiveLean 4Applies a library theoremFormally verified

/-- **`V ≅ V**` in finite dimensions**: the evaluation map is bijective (Mathlib's
`Module.bijective_dual_eval`, using that finite-dimensional spaces are reflexive). -/
theorem eval_bijective {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] : Function.Bijective (Dual.eval K V) :=
  bijective_dual_eval K V

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

dual_finrankLean 4Applies a library theoremFormally verified

/-- `dim V* = dim V` for finite-dimensional `V` (Mathlib's `Subspace.dual_finrank_eq`, proved
with the dual basis). So `V ≅ V*` — but only through a choice, as the lesson explains. -/
theorem dual_finrank {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] : finrank K (Dual K V) = finrank K V :=
  Subspace.dual_finrank_eq

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

Tensor products. Mathlib defines $V \otimes W$ by a quotient construction and proves its universal property; existence and uniqueness of the factorisation are TensorProduct.lift and TensorProduct.ext':

tensor_universalLean 4Applies a library theoremFormally verified

/-- **The universal property of `V ⊗ W`.** Every bilinear map `B : V × W → U` factors through
`(v, w) ↦ v ⊗ w` by exactly one linear map `φ : V ⊗ W → U`. Existence is
`TensorProduct.lift`; uniqueness is `TensorProduct.ext'` (linear maps that agree on pure tensors
agree everywhere, because pure tensors span). -/
theorem tensor_universal {K V W U : Type*} [Field K] [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W] [AddCommGroup U] [Module K U] (B : V →ₗ[K] W →ₗ[K] U) :
    ∃! φ : TensorProduct K V W →ₗ[K] U, ∀ v w, φ (v ⊗ₜ w) = B v w := by
  refine ⟨TensorProduct.lift B, fun v w => TensorProduct.lift.tmul v w, ?_⟩
  intro ψ hψ
  exact TensorProduct.ext' fun v w => by rw [hψ, TensorProduct.lift.tmul]

Axioms used: propext, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

finrank_tensorLean 4Applies a library theoremFormally verified

/-- `dim (V ⊗ W) = dim V · dim W` (Mathlib's `Module.finrank_tensorProduct`, from the basis
`eᵢ ⊗ fⱼ`). Compare `dim (V × W) = dim V + dim W`. -/
theorem finrank_tensor {K V W : Type*} [Field K] [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W] [FiniteDimensional K V] [FiniteDimensional K W] :
    finrank K (TensorProduct K V W) = finrank K V * finrank K W :=
  Module.finrank_tensorProduct

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

Finally, the misconception "every tensor is pure", refuted with coordinate functionals built from the universal property:

coordLean 4Formally verified

/-- The `(i, j)` **coordinate** of a tensor in `K² ⊗ K²`: the linear map induced, through the
universal property, by the bilinear map `(v, w) ↦ vᵢ wⱼ`. On a pure tensor it gives the entries
of the "outer product" matrix `v wᵀ`. -/
noncomputable def coord {K : Type*} [Field K] (i j : Fin 2) :
    TensorProduct K (Fin 2 → K) (Fin 2 → K) →ₗ[K] K :=
  TensorProduct.lift (LinearMap.mk₂ K (fun v w => v i * w j)
    (fun _ _ _ => by simp [add_mul]) (fun _ _ _ => by simp [mul_assoc])
    (fun _ _ _ => by simp [mul_add]) (fun _ _ _ => by simp [mul_left_comm]))

Axioms used: propext, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

not_pure_tensorLean 4Proved here from basic factsFormally verified

/-- **Not every tensor is pure.** `e₁ ⊗ e₁ + e₂ ⊗ e₂` is not of the form `v ⊗ w`. Taking
coordinates: a pure tensor has coordinates `vᵢ wⱼ`, so we would need `v₁ w₁ = 1`, `v₂ w₂ = 1`
and `v₁ w₂ = 0` — impossible, since the last forces `v₁ = 0` or `w₂ = 0`. In matrix language:
the identity matrix has rank 2, while `v wᵀ` has rank at most 1. -/
theorem not_pure_tensor {K : Type*} [Field K] :
    ¬ ∃ v w : Fin 2 → K, v ⊗ₜ[K] w =
      (Pi.single 0 1 : Fin 2 → K) ⊗ₜ Pi.single 0 1 + Pi.single 1 1 ⊗ₜ Pi.single 1 1 := by
  rintro ⟨v, w, h⟩
  have c00 := congrArg (coord (K := K) 0 0) h
  have c11 := congrArg (coord (K := K) 1 1) h
  have c01 := congrArg (coord (K := K) 0 1) h
  simp [coord] at c00 c11 c01
  rcases c01 with h0 | h1
  · simp [h0] at c00
  · simp [h1] at c11

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdvancedLinearAlgebra.leanTry it in the Lean web editor

What is and is not formalised. Independent: Lemmas 1 and 2, the complex symmetric counterexample, Cayley–Hamilton for $2 \times 2$ matrices, the minimal polynomial of $J_3(\mu)$ , naturality of $\mathrm{ev}$ , and the non-pure tensor. From Mathlib: Theorem 5, Theorem 7, the generalised eigenspace decomposition, Theorem 14's isomorphism, $\dim V^* = \dim V$ and Theorem 16. Not formalised: the Jordan normal form as a statement about block matrices (Mathlib has the generalised eigenspace decomposition and the Jordan–Chevalley decomposition $T = S + N$ , not yet the block form or Theorem 11), the rational canonical form, Theorem 6 and Proposition 15. The Lean exercises ask you to reprove Lemma 2 and the $2 \times 2$ Cayley–Hamilton identity.

ComputationC

Jordan forms exactly, spectra numerically

The rank formula of Theorem 12 is an algorithm. The first program builds an integer $5 \times 5$ matrix, computes the ranks of $(A - \lambda I)^k$ in exact rational arithmetic, reads off the Jordan blocks, checks them against SymPy's jordan_form, verifies $\chi_A(A) = 0$ and the minimal polynomial, and finally shows two $4 \times 4$ matrices with the same characteristic and minimal polynomials that are nevertheless not similar.

Jordan forms from ranks, and Cayley-Hamilton, exactlyPythonExact computationSymbolic computationComputationally tested

"""Reading off a Jordan normal form from ranks, in exact arithmetic.

The lesson proves that the Jordan form of A is determined by the numbers
rank (A - lambda I)^k: the number of Jordan blocks for lambda of size at least
k is rank (A - lambda I)^(k-1) - rank (A - lambda I)^k. Here a 5 x 5 integer
matrix (built as P J P^-1 and then "forgotten") is analysed with that formula,
compared with SymPy's own jordan_form, and used to check the Cayley-Hamilton
theorem and the minimal polynomial exactly. A last pair of 4 x 4 matrices shows
that the characteristic and minimal polynomials alone do not determine the
Jordan form, while the ranks do.

All arithmetic is exact (rational), so each check is an exact verification for
these particular matrices; the general theorems are proved in the lesson.
"""

import sympy

X = sympy.Symbol("x")

def jordan_block(lam, size):
    """The size x size Jordan block with eigenvalue lam."""
    return sympy.Matrix(size, size, lambda i, j: lam if i == j else
                        (1 if j == i + 1 else 0))

def example_matrix():
    """A = P J P^-1 with J = J3(2) + J1(2) + J1(-1) and det P = 1."""
    p = sympy.Matrix([[1, 1, 0, 0, 0], [0, 1, 1, 0, 0], [1, 0, 1, 1, 0],
                      [0, 0, 0, 1, 1], [0, 1, 0, 0, 1]])
    j = sympy.diag(jordan_block(2, 3), jordan_block(2, 1), jordan_block(-1, 1))
    return p * j * p.inv()

def rank_sequence(a, lam):
    """[rank (A - lam I)^k for k = 0, 1, ...] until the ranks stop falling."""
    n = a.shape[0]
    shifted = a - lam * sympy.eye(n)
    ranks, power = [n], sympy.eye(n)
    while True:
        power = power * shifted
        ranks.append(power.rank())
        if ranks[-1] == ranks[-2]:
            return ranks

def block_sizes(ranks):
    """Jordan block sizes (largest first) from a rank sequence r_0, r_1, ...

    Blocks of size >= k number r_(k-1) - r_k, so blocks of size exactly k
    number r_(k-1) - 2 r_k + r_(k+1).
    """
    r = list(ranks) + [ranks[-1]]
    sizes = []
    for k in range(len(ranks) - 1, 0, -1):
        sizes += [k] * (r[k - 1] - 2 * r[k] + r[k + 1])
    return sizes

def jordan_data(a):
    """{eigenvalue: block sizes} computed with the rank formula."""
    roots = sympy.roots(a.charpoly(X).as_expr(), X)
    return {lam: block_sizes(rank_sequence(a, lam)) for lam in sorted(roots)}

def evaluate(poly_expr, a):
    """The matrix p(A) for a polynomial expression p in X (Horner's rule)."""
    result = sympy.zeros(*a.shape)
    for c in sympy.Poly(poly_expr, X).all_coeffs():
        result = result * a + c * sympy.eye(a.shape[0])
    return result

def blocks_of_jordan_matrix(j):
    """{eigenvalue: block sizes} read off a matrix already in Jordan form."""
    n, blocks, i = j.shape[0], {}, 0
    while i < n:
        k = 1
        while i + k < n and j[i + k - 1, i + k] == 1:
            k += 1
        blocks.setdefault(j[i, i], []).append(k)
        i += k
    return {lam: sorted(s, reverse=True) for lam, s in blocks.items()}

def minimal_polynomial(a):
    """prod (x - lambda)^(largest block for lambda), from the Jordan data."""
    return sympy.Mul(*[(X - lam) ** max(s) for lam, s in jordan_data(a).items()])

def main():
    a = example_matrix()
    print("A (a 5 x 5 integer matrix):")
    for i in range(5):
        print("   " + " ".join(f"{int(v):3d}" for v in a.row(i)))
    print("characteristic polynomial:", sympy.factor(a.charpoly(X).as_expr()))
    data = jordan_data(a)
    for lam, sizes in data.items():
        ranks = rank_sequence(a, lam)
        print(f"lambda = {lam}: ranks of (A - lambda I)^k, k = 0, 1, ...: "
              f"{ranks}")
        print(f"   -> Jordan block sizes {sizes}")
    _, j = a.jordan_form()
    print("SymPy's jordan_form gives the same blocks:",
          blocks_of_jordan_matrix(j) == data)
    m = minimal_polynomial(a)
    print("minimal polynomial:", m)
    chi = a.charpoly(X).as_expr()
    print("chi_A(A) = 0 (Cayley-Hamilton):", evaluate(chi, a).is_zero_matrix)
    print("m(A) = 0:", evaluate(m, a).is_zero_matrix)
    smaller = (X - 2) ** 2 * (X + 1)
    print("(x - 2)^2 (x + 1) kills A:", evaluate(smaller, a).is_zero_matrix)
    print()
    b = sympy.diag(jordan_block(0, 2), jordan_block(0, 2))
    c = sympy.diag(jordan_block(0, 2), jordan_block(0, 1), jordan_block(0, 1))
    print("B = J2(0) + J2(0) and C = J2(0) + J1(0) + J1(0):")
    print("   same characteristic polynomial:",
          b.charpoly(X) == c.charpoly(X), "  same minimal polynomial:",
          minimal_polynomial(b) == minimal_polynomial(c))
    print(f"   but rank B = {b.rank()} and rank C = {c.rank()}: "
          "not similar")
    print()
    print("Epistemic status: exact rational arithmetic on these specific "
          "matrices,\nso every 'True' above is an exact verification for them "
          "(trusting SymPy's\nimplementation). That the ranks determine the "
          "Jordan form of every\nmatrix, and that chi_A(A) = 0 always, are "
          "theorems proved in the lesson.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Exact arithmetic is essential here. The second program shows why: in floating point, the spectral theorem is beautifully stable — computed eigenvectors are orthonormal to $10^{-15}$ , and a perturbation of size $\varepsilon$ moves the eigenvalues of a symmetric matrix by at most $\varepsilon$ (Weyl's inequality) — but the Jordan form is not. Changing one entry of $J_8(0)$ by $\varepsilon = 10^{-10}$ moves its eigenvalues to modulus $\varepsilon^{1/8} \approx 0.056$ , because the characteristic polynomial becomes $x^8 - \varepsilon$ .

Spectral theorem in floating point; the fragility of JordanPythonNumerical approximationExperimental evidenceComputationally tested

"""The spectral theorem in floating point, and why numerical analysts fear Jordan.

1. A random real symmetric 6 x 6 matrix is diagonalised by numpy's eigh: the
   computed eigenvectors are orthonormal and A = Q diag(w) Q^T to rounding error.
2. The largest eigenvalue is the maximum of the Rayleigh quotient <Av, v>/<v, v>
   (the variational step in the lesson's proof): random sampling approaches it
   from below and never exceeds it.
3. A non-normal matrix has eigenvectors far from orthogonal.
4. Perturbing a symmetric matrix by size eps moves its eigenvalues by at most
   eps (Weyl's inequality), but perturbing one entry of the 8 x 8 Jordan block
   J8(0) by eps = 1e-10 moves its eigenvalues to modulus eps^(1/8) = 0.056,
   more than five hundred million times further.

All results are floating-point (numerical) evidence about specific matrices.
"""

import numpy as np

def random_symmetric(n, seed):
    """A seeded random real symmetric n x n matrix (M + M^T) / 2."""
    m = np.random.default_rng(seed).standard_normal((n, n))
    return (m + m.T) / 2

def spectral_residuals(a):
    """(max |Q^T Q - I|, max |A - Q diag(w) Q^T|) for numpy's eigh."""
    w, q = np.linalg.eigh(a)
    n = a.shape[0]
    return (np.abs(q.T @ q - np.eye(n)).max(),
            np.abs(a - q @ np.diag(w) @ q.T).max())

def rayleigh_max(a, samples, seed):
    """Largest Rayleigh quotient <Av, v>/<v, v> over random vectors v."""
    v = np.random.default_rng(seed).standard_normal((samples, a.shape[0]))
    return float(np.max(np.einsum("ij,jk,ik->i", v, a, v) /
                        np.einsum("ij,ij->i", v, v)))

def eigenvector_angle_degrees(a):
    """Angle between the two eigenvector lines of a 2 x 2 matrix."""
    _, vecs = np.linalg.eig(a)
    c = abs(vecs[:, 0] @ vecs[:, 1])
    c /= np.linalg.norm(vecs[:, 0]) * np.linalg.norm(vecs[:, 1])
    return float(np.degrees(np.arccos(min(1.0, c))))

def perturbed_jordan(n, eps):
    """The nilpotent Jordan block J_n(0) with eps in the bottom-left corner.

    Its characteristic polynomial is x^n - eps, so its eigenvalues are the
    n complex n-th roots of eps, all of modulus eps^(1/n).
    """
    j = np.diag(np.ones(n - 1), 1)
    j[n - 1, 0] = eps
    return j

def max_eigenvalue_shift_symmetric(a, eps, seed):
    """Largest change in sorted eigenvalues after a symmetric eps-perturbation."""
    e = random_symmetric(a.shape[0], seed)
    e *= eps / np.linalg.norm(e, 2)
    return float(np.abs(np.linalg.eigvalsh(a + e) -
                        np.linalg.eigvalsh(a)).max())

def main():
    a = random_symmetric(6, 2024)
    orth, recon = spectral_residuals(a)
    w = np.linalg.eigvalsh(a)
    print("1. A random symmetric 6 x 6 matrix A (seed 2024)")
    print("   eigenvalues:", " ".join(f"{x:.4f}" for x in w))
    print(f"   max |Q^T Q - I| = {orth:.1e},  max |A - Q D Q^T| = {recon:.1e}")
    print()
    r = rayleigh_max(a, 20000, 1)
    print("2. Rayleigh quotient over 20000 random vectors")
    print(f"   best found {r:.6f} <= largest eigenvalue {w[-1]:.6f}")
    print()
    print("3. Eigenvector angle (90 degrees for symmetric matrices)")
    for name, m in [("[[2, 1], [1, 2]]", [[2, 1], [1, 2]]),
                    ("[[1, 10], [0, 2]]", [[1, 10], [0, 2]])]:
        ang = eigenvector_angle_degrees(np.array(m, dtype=float))
        print(f"   {name:<18} angle = {ang:6.2f} degrees")
    print()
    eps = 1e-10
    print(f"4. Sensitivity to a perturbation of size eps = {eps:.0e}")
    shift = max_eigenvalue_shift_symmetric(a, eps, 5)
    print(f"   symmetric A + E: eigenvalues move by {shift:.1e} <= eps")
    for n in (2, 4, 8):
        mods = np.abs(np.linalg.eigvals(perturbed_jordan(n, eps)))
        print(f"   J{n}(0) + eps corner: |eigenvalues| = {mods.mean():.2e}"
              f"  (eps^(1/{n}) = {eps ** (1 / n):.2e})")
    print()
    print("Epistemic status: floating-point computations on specific matrices.\n"
          "They illustrate, but do not prove, the spectral theorem, the\n"
          "variational principle and Weyl's inequality (all theorems). The\n"
          "eps^(1/n) law for the Jordan block is exact algebra (x^n = eps); the\n"
          "computer only confirms it numerically.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The first program's checks are exact verifications for its matrices (trusting SymPy); the second is floating-point evidence. Neither proves the general theorems, which is what the proofs above are for. The moral, well known to numerical analysts since Golub and Wilkinson's 1976 survey: compute Schur forms and singular value decompositions, which are stable, and treat the Jordan form as a theoretical tool.

Explore

Explore: orthogonal axes, skewed axes, one axis

A symmetric matrix maps the unit circle to an ellipse whose axes are its eigenvector lines, and they are perpendicular. Drag the off-diagonal entries apart (making the matrix non-symmetric) and watch the dashed invariant lines stop being perpendicular. Then pick the shear preset: a Jordan block has a single invariant line.

Symmetric: perpendicular eigenvectors

Make the two off-diagonal entries different. When do the dashed lines stop being perpendicular?

Your own matrix

image of the grid
image of the unit square
image of the flag
before the transformation
invariant line

From the identity I to As = 1

A =

The columns of A are the images of e₁ = (1, 0) and e₂ = (0, 1): Ae₁ = (2, 1), Ae₂ = (1, 2)

det A = ad − bc = 3

The unit square (area 1) becomes a parallelogram of area |det A| = 3. Since det A > 0, orientation is preserved.

Invariant lines (real eigenvectors)

λ₁ = 3, v₁ = (1, 1)
λ₂ = 1, v₂ = (1, −1)

Vectors on the two dashed lines are only stretched, by the factors λ₁ = 3 and λ₂ = 1; every other direction is turned.

Here the matrix is upper triangular with distinct eigenvalues $1$ and $2$ : diagonalisable, but its eigenvectors meet at about $34°$ . Slide the top-right entry towards $0$ (the angle opens to $90°$ ) and towards large values (the eigenvectors nearly coincide — the matrix is close to a Jordan block in the numerical sense, and its eigenvectors become ill-conditioned).

Non-normal: skewed eigenvectors

Change the entries or pick a transformation. The columns of A are where e₁ and e₂ land; the gold square shows what happens to area.

Your own matrix

image of the grid
image of the unit square
image of the flag
before the transformation
invariant line

From the identity I to As = 1

A =

The columns of A are the images of e₁ = (1, 0) and e₂ = (0, 1): Ae₁ = (1, 0), Ae₂ = (1.5, 2)

det A = ad − bc = 2

The unit square (area 1) becomes a parallelogram of area |det A| = 2. Since det A > 0, orientation is preserved.

Invariant lines (real eigenvectors)

λ₁ = 2, v₁ = (1, 0.667)
λ₂ = 1, v₂ = (1, 0)

Vectors on the two dashed lines are only stretched, by the factors λ₁ = 2 and λ₂ = 1; every other direction is turned.

Exercises

1. Advanced linear algebra

Warm-upHuman

The symmetric matrix $A = \begin{pmatrix} 5 & 2 \\ 2 & 2 \end{pmatrix}$ is the matrix of $q(x, y) = 5x^2 + 4xy + 2y^2$ . What is the largest eigenvalue of $A$ , that is, the maximum of $q$ on the unit circle?

2. Advanced linear algebra

CoreHuman

Which of these matrices are unitarily (or, for real ones, orthogonally) diagonalisable over $\mathbb{C}$ ? (Choose all that apply.)

Choose all that apply

\begin{pmatrix} 2 & 1 \\ 1 & 2 \end{pmatrix}

\begin{pmatrix} 0 & -1 \\ 1 & 0 \end{pmatrix}

\begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}

\begin{pmatrix} 1 & i \\ i & -1 \end{pmatrix}

\begin{pmatrix} 1 & 10 \\ 0 & 2 \end{pmatrix}

3. Advanced linear algebra

CoreHuman

In the proof of the spectral theorem, $v_1$ is an eigenvector of the self-adjoint operator $T$ and $W = v_1^{\perp}$ . Why does $T$ map $W$ into $W$ ?

Choose one

For

w \in W

\langle v_1, Tw \rangle = \langle Tv_1, w \rangle = \lambda_1 \langle v_1, w \rangle = 0

.Because

T

is invertible, so it maps a hyperplane onto a hyperplane.Because

W

is an eigenspace of

T

.Because the eigenvalues of

T

are real.

4. Advanced linear algebra

CoreHuman

A nilpotent operator $N$ on a $5$ -dimensional space has $\operatorname{rank} N = 3$ , $\operatorname{rank} N^2 = 1$ and $N^3 = 0$ . What is the degree of its minimal polynomial?

5. Advanced linear algebra

CoreHuman

Let $V$ and $W$ be finite-dimensional. Which statements about $V \otimes W$ are true? (Choose all that apply.)

Choose all that apply

\dim(V \otimes W) = \dim V \cdot \dim W

.Every element is a finite sum of pure tensors

v \otimes w

.Every element is a pure tensor

v \otimes w

v \otimes w = 0

if and only if

v = 0

w = 0

(v_1 + v_2) \otimes (w_1 + w_2) = v_1 \otimes w_1 + v_2 \otimes w_2

6. Advanced linear algebra

StretchHuman

Let $V = W = \mathbb{R}$ and let $\eta : \mathbb{R} \to \mathbb{R}^*$ be the 'basis' isomorphism sending $1$ to the functional $1^*$ with $1^*(t) = t$ . Let $f : \mathbb{R} \to \mathbb{R}$ be $f(t) = 2t$ . Compute the number $\big(f^*(\eta(f(1)))\big)(1)$ . (Naturality would require it to equal $\eta(1)(1) = 1$ .)

7. Advanced linear algebra

CoreFormal

Which Lean statement correctly formalises Lemma 2 (eigenvectors of a symmetric operator for distinct eigenvalues are orthogonal)? In each, T : E →ₗ[ℝ] E on a real inner product space E.

Choose one

(hT : T.IsSymmetric) (hv : T v = a • v) (hw : T w = b • w) (hab : a ≠ b) : inner ℝ v w = 0(hT : T.IsSymmetric) (hv : T v = a • v) (hw : T w = b • w) : inner ℝ v w = 0(hv : T v = a • v) (hw : T w = b • w) (hab : a ≠ b) : inner ℝ v w = 0(hT : T.IsSymmetric) (h : inner ℝ v w = 0) : ∃ a b, a ≠ b ∧ T v = a • v ∧ T w = b • w

8. Advanced linear algebra

Warm-upHuman

What is $\dim\big(\mathbb{R}^3 \otimes \mathbb{R}^4 \otimes \mathbb{R}^2\big)$ ?

9. Advanced linear algebra

StretchComputational

Implement the uniqueness part of Theorem 12. Write block_sizes(ranks) where ranks = [r0, r1, r2, ...] lists $\operatorname{rank}(A - \lambda I)^k$ for $k = 0, 1, 2, \dots$ , ending once the ranks stop changing. Return the list of Jordan block sizes for $\lambda$ , largest first. (Blocks of size $\geq k$ number $r_{k-1} - r_k$ .)

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

" $V$ and $V^*$ are canonically the same." They have the same dimension, so they are isomorphic, but every isomorphism depends on a choice — a basis (sending $e_i$ to $e_i^*$ ) or an inner product. Proposition 15 makes this precise: no choice-free family of isomorphisms $V \to V^*$ is compatible with all isomorphisms. The double dual is different: $V \to V^{**}$ is natural (Theorem 14). The worked example of a dual basis shows the dependence concretely: $b_1 = e_1$ but $b_1^* \ne e_1^*$ .

Misconception

"Every element of $V \otimes W$ has the form $v \otimes w$ ." Pure tensors span $V \otimes W$ , but most elements are sums of them. $e_1 \otimes e_1 + e_2 \otimes e_2$ corresponds to the identity matrix of rank $2$ and is not pure (Proposition 17, and the Lean theorem not_pure_tensor). In quantum mechanics the non-pure tensors are the entangled states.

Misconception

"Symmetric matrices are diagonalisable over every field." The spectral theorem is about real symmetric matrices, or complex Hermitian ones, and its proof uses positivity of the inner product. The complex symmetric matrix $\begin{pmatrix} 1 & i \\ i & -1 \end{pmatrix}$ is non-zero with square $0$ , and over $\mathbb F_2$ the symmetric matrix $\begin{pmatrix} 1 & 1 \\ 1 & 1 \end{pmatrix}$ also squares to $0$ .

Misconception

" $\chi_A(A) = \det(AI - A) = 0$ proves Cayley–Hamilton." Substituting a matrix for $x$ inside a determinant is not legitimate: in $\det(xI - A)$ , $x$ multiplies scalar entries, and $AI - A$ would be a matrix with matrix entries. The theorem is true, but needs an argument such as the adjugate proof of Theorem 7.

Misconception

"The characteristic and minimal polynomials determine the matrix up to similarity." They do for $n \le 3$ , but not in general: $J_2(0) \oplus J_2(0)$ and $J_2(0) \oplus J_1(0) \oplus J_1(0)$ both have $\chi = x^4$ and $m = x^2$ , yet ranks $2$ and $1$ . The complete invariant is the list of ranks of $(A - \lambda I)^k$ — equivalently the Jordan form.

Misconception

"Eigenvectors are always orthogonal." Only for normal operators (Theorem 6). The eigenvectors $(1, 0)$ and $(10, 1)$ of $\begin{pmatrix} 1 & 10 \\ 0 & 2 \end{pmatrix}$ meet at under $6°$ , as the second experiment measures.

ViewpointsH

Many ways of seeing

Geometry— Ellipsoids, quadrics and the singular value decomposition

The spectral theorem is the principal axes theorem: every quadric $\mathbf x^{\mathsf T} A \mathbf x = 1$ in $\R^n$ becomes $\sum \lambda_i u_i^2 = 1$ in suitable orthonormal coordinates, so the signs of the eigenvalues classify ellipsoids and hyperboloids (Sylvester's law of inertia says the number of positive and negative $\lambda_i$ cannot be changed by any change of basis, orthogonal or not). For an arbitrary real matrix $M$ , applying the theorem to the symmetric matrix $M^{\mathsf T}M$ gives the singular value decomposition $M = U\Sigma V^{\mathsf T}$ : every linear map takes the unit sphere to an ellipsoid, rotating the sphere first and the ellipsoid afterwards, with semi-axes the singular values. In mechanics, the same theorem gives a rigid body's principal axes of inertia, about which it can spin without wobbling. See conic sections and matrix groups, where the orthogonal and unitary matrices $Q$ , $U$ become groups.

Topology— Similarity classes, closures and generic matrices

Similarity classes of complex $n \times n$ matrices are orbits of the group $GL_n(\C)$ acting on $\C^{n^2}$ by conjugation, and their topology mirrors the Jordan form. The orbit of $J_2(0)$ is not closed: $\begin{pmatrix} 0 & t \\ 0 & 0 \end{pmatrix}$ is similar to $J_2(0)$ for every $t \ne 0$ but tends to $0$ . In general the closure of the orbit of a nilpotent matrix is a union of orbits of "smaller" Jordan types (ordered by dominance of partitions). Conversely, matrices with distinct eigenvalues form an open dense set, so the map "matrix $\mapsto$ Jordan form" is wildly discontinuous — the topological face of the $\varepsilon^{1/n}$ phenomenon in the second experiment. On the other hand, the eigenvalues, as an unordered list, depend continuously on the matrix (roots of a polynomial depend continuously on its coefficients). This also gives an analyst's proof of Cayley–Hamilton over $\C$ : $A \mapsto \chi_A(A)$ is continuous, vanishes on diagonalisable matrices, and these are dense.

Analysis— Infinite dimensions: compact operators, Fourier series and the spectrum

On infinite-dimensional Hilbert spaces the spectral theorem survives for compact self-adjoint operators: there is an orthonormal basis of eigenvectors with real eigenvalues tending to $0$ (Hilbert and Schmidt, 1904–1907, in the study of integral equations). Fourier series are an instance: the functions $e^{inx}$ are eigenfunctions of $-d^2/dx^2$ on the circle, with eigenvalues $n^2$ , and expanding a function in Fourier series is diagonalising that operator (whose inverse on functions with mean zero is compact). For general bounded self-adjoint operators eigenvectors may not exist at all — multiplication by $x$ on $L^2[0, 1]$ has none — and the theorem becomes a statement about projection-valued measures (von Neumann, 1929). Duality also changes: for normed spaces one uses only continuous functionals, and a space with $V \to V^{**}$ onto is called reflexive ( $\ell^2$ is, $\ell^1$ is not). See functional analysis.

Algebra— Canonical forms are the structure theorem for modules over k[x]

An operator $T$ on $V$ makes $V$ into a module over the polynomial ring $k[x]$ , with $x$ acting as $T$ ; similar operators give isomorphic modules. Because $k[x]$ is a principal ideal domain, every finitely generated module is a direct sum of cyclic modules $k[x]/(p)$ — the same theorem that classifies finitely generated abelian groups as sums of $\Z/n$ . Choosing the invariant-factor decomposition $\bigoplus k[x]/(d_i)$ gives the rational canonical form (on $k[x]/(d)$ , $x$ acts by the companion matrix of $d$ ); choosing the elementary-divisor decomposition $\bigoplus k[x]/((x - \lambda)^m)$ over an algebraically closed field gives the Jordan form (on $k[x]/((x - \lambda)^m)$ with basis $(x - \lambda)^{m-1}, \dots, 1$ , $x$ acts as $J_m(\lambda)$ ). Cayley–Hamilton says $\chi_T$ lies in the annihilator ideal $(m_T)$ . See modules and rings.

Probability— Covariance matrices and principal components

The covariance matrix $\Sigma = \mathbb E[(X - \mu)(X - \mu)^{\mathsf T}]$ of a random vector $X$ in $\R^n$ is symmetric and positive semidefinite, since $\mathbf u^{\mathsf T}\Sigma\mathbf u = \operatorname{Var}(\mathbf u^{\mathsf T} X) \ge 0$ . By the spectral theorem its orthonormal eigenvectors are uncorrelated directions, and by the variational characterisation (Lemma 4) the top eigenvector is the direction of greatest variance. This is principal component analysis. The level sets of a multivariate normal density are the ellipsoids $(\mathbf x - \mu)^{\mathsf T}\Sigma^{-1}(\mathbf x - \mu) = c$ , whose axes are those eigenvectors. Random matrix theory studies the eigenvalues of large random symmetric matrices, whose histogram approaches Wigner's semicircle law. See statistics.

Physics— Observables, composite systems and entanglement

In quantum mechanics a measurable quantity is a self-adjoint operator on a complex Hilbert space; the possible outcomes of a measurement are its eigenvalues (real, by Lemma 1) and outcomes for different eigenvalues are perfectly distinguishable because the eigenvectors are orthogonal (Lemma 2). Two observables can be measured simultaneously exactly when the operators commute, which is when they share an orthonormal eigenbasis. The state space of a composite system is the tensor product of the state spaces of its parts, and a state that is not a pure tensor — such as the Bell state $\tfrac{1}{\sqrt2}(\lvert 00 \rangle + \lvert 11 \rangle)$ of the motivation, which corresponds to a rank-two matrix — is entangled. The rank in Proposition 17 is the Schmidt rank, a basic measure of entanglement. See quantum mechanics.

Category theory— Naturality, monoidal structure and the tensor–hom adjunction

Eilenberg and Mac Lane introduced categories, functors and natural transformations (1945) to make precise exactly the distinction in Theorem 14 and Proposition 15: $V \mapsto V^{**}$ is a covariant functor and $\mathrm{ev}$ is a natural isomorphism from the identity functor, while $V \mapsto V^*$ is contravariant, so a natural isomorphism to it cannot even be stated (see natural transformations). The universal property of $\otimes$ is an adjunction: $\Hom(V \otimes W, U) \cong \Hom(V, \Hom(W, U))$ , naturally in all three spaces. With $\otimes$ and unit $k$ , finite-dimensional vector spaces form a symmetric monoidal category in which every object has a dual, with $V^* \otimes W \cong \Hom(V, W)$ (Proposition 17); the trace is then a composite $V^* \otimes V \to k$ of structure maps. See monoidal categories.

History & global context

History and global context

Principal axes and secular equations. Euler (1765) found the principal axes of a rotating rigid body, and Lagrange and Laplace studied the "secular equation" $\det(A - \lambda I) = 0$ for the long-term (secular) perturbations of planetary orbits. Augustin-Louis Cauchy proved in 1829 that the roots of this equation are real for symmetric $A$ , and that the principal axes are orthogonal, in a paper on exactly that astronomical problem.
Inertia and matrices. James Joseph Sylvester proved his law of inertia for quadratic forms (1852) and coined the word matrix (1850). Arthur Cayley's Memoir on the theory of matrices (1858) stated the Cayley–Hamilton theorem, verified it for $2 \times 2$ matrices and reported checking $3 \times 3$ ; William Rowan Hamilton had proved an instance for linear functions of quaternions (1853). Ferdinand Georg Frobenius gave the first general proof (1878) and introduced the minimal polynomial.
Canonical forms. Karl Weierstrass (1868) developed elementary divisors for pairs of bilinear forms, and Camille Jordan's Traité des substitutions (1870) gave the canonical form, originally over finite fields, in his study of groups. Henry Smith's normal form for integer matrices (1861) is the $\Z$ -analogue.
Infinite dimensions. David Hilbert's work on integral equations (1904–1910) introduced the word spectrum into analysis, Erhard Schmidt developed the orthogonalisation now named after him and Gram, and John von Neumann proved the spectral theorem for unbounded self-adjoint operators (1929–1932) to put quantum mechanics on a rigorous footing.
Tensors. The tensor calculus of Gregorio Ricci-Curbastro and Tullio Levi-Civita (1900) was the language of Einstein's general relativity; Woldemar Voigt's crystal physics (1898) gave the word tensor its modern meaning. The algebraic tensor product of modules was introduced by Hassler Whitney (1938), and Bourbaki's Algèbre multilinéaire (1948) made the universal-property definition standard.
Naturality. Samuel Eilenberg and Saunders Mac Lane's General theory of natural equivalences (1945) began category theory, with the double dual as a guiding example.

Three questions a first course leaves open

Choosing coordinates well

Definitions

Examples and non-examples

The spectral theorem

Cayley–Hamilton, minimal polynomials and the Jordan form

Dual spaces: natural and unnatural isomorphisms

Tensor products and multilinear algebra

The theorems in Lean and Mathlib

Jordan forms exactly, spectra numerically

Explore: orthogonal axes, skewed axes, one axis

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading