linear algebra, higher linear algebra
(…)
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
with
equals
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:
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
is a split exact sequence, hence of the form
Textbook accounts:
A formal proof of the rank-nullity theorem in the Isabelle proof assistant:
See also:
Created on April 4, 2023 at 08:19:19. See the history of this page for a list of all contributions to it.