arXiv2025
Linear algebra's main concerns are sets of vectors, linear functions, subspaces, linear systems, matrices and concepts about those, such as whether the solution of linear system exists or is unique; a set of vectors is linearly independent or spans the whole space; a linear function has a right or a left inverse; a linear function is surjective or injective; and the kernel of a matrix is trivial or the its image is full. The Invertible Matrix Theorem ties all these ideas and many others together. Many modern linear algebra books use this theorem as a guiding principle to explain many connections in linear algebra. The main idea is to separately characterize whether the linear function is surjective or injective. The proof usually uses a matrix decomposition as the key step. However, the invertible matrix theorem deals with a single linear function, a single set of vectors, a single subspace, and a single matrix. In this work, we generalize part of the invertible matrix theorem to results about a pair of linear functions, a pair of sets of vectors, a pair of subspaces, and a single linear relation. The main idea is to separately characterize the linear relation's fundamental properties -- whether it is surjective, injective, deterministic and total. Our proof uses a decomposition of a linear relation as the key step. Unfortunately, reasoning with linear relations in classical notation requires applying many rules besides shuffling quantifiers and variables around, which can obscure the symmetries in the results. Therefore, this work employs graphical linear algebra, a two-dimensional diagrammatic syntax with the fundamental rules of linear relations built-in.