Contents

(…)

# Contents

## Idea

In linear algebra, what is known as the rank-nullity theorem (e.g. 3.22 in Axler (2015), who calls it the fundamental theorem of linear maps) is the statement that for any linear map $f \colon V \to W$ out of a finite-dimensional vector space, the sum of

• the rank $rk(f) \coloneqq dim\big(im(f)\big)$, i.e. the dimension of the image;

with

• the nullity $nl(f) \coloneqq dim\big( ker(f) \big)$, i.e. the dimension of the kernel

equals

• the dimension $d_V \coloneqq dim(V)$ of the domain space $V$:
$d_V \;=\; rk(f) + nl(f) \,.$

This rank-nullity theorem is the decategorification (under the dimension functor $dim \colon FinDimVect \to \mathbb{Z}$) of the stronger statement that $V$ itself is the direct sum of its kernel and image vector spaces:

$V \;\simeq\; im(f) \oplus ker(f) \,.$

This may be understood as an instance of the splitting lemma for vector spaces, or more precisely of the statement (here) that every short exact sequence of vector spaces, such as

$0 \to ker(f) \longrightarrow V \longrightarrow im(f) \to 0$

is a split exact sequence, hence of the form

$0 \to ker(f) \longrightarrow ker(f) \oplus im(f) \longrightarrow im(f) \to 0 \,.$

Textbook accounts:

A formal proof of the rank-nullity theorem in the Isabelle proof assistant: