1 Preliminaries
1.1 Total Unimodularity
Matrix is a function that takes a row index and returns a vector, which is a function that takes a column index and returns a value. The former aforementioned identity is definitional, the latter is syntactical. By abuse of notation \(\left(R^Y\right)^X \equiv R^{X \times Y}\) we do not curry functions in this text. When a matrix happens to be finite (that is, both \(X\) and \(Y\) are finite) and its entries are numeric, we like to represent it by a table of numbers.
Let \(A\) be a square matrix over a commutative ring. Determinant of \(A\) is the sum over all permutations, sign of the permutation times the product of ... . (Todo: complete definition).
Let \(R\) be a commutative ring. We say that a matrix \(A \in R^{X \times Y}\) is totally unimodular, or TU for short, if for every \(k \in \mathbb {N}\), every (not necessarily contiguous) \(k \times k\) submatrix \(T\) of \(A\) has \(\det T \in \{ 0, \pm 1\} \).
Let \(A\) be a TU matrix. Suppose rows of \(A\) are multiplied by \(\{ 0, \pm 1\} \) factors. Then the resulting matrix \(A'\) is also TU.
We prove that \(A'\) is TU by Definition 3. To this end, let \(T'\) be a square submatrix of \(A'\). Our goal is to show that \(\det T' \in \{ 0, \pm 1\} \). Let \(T\) be the submatrix of \(A\) that represents \(T'\) before pivoting. If some of the rows of \(T\) were multiplied by zeros, then \(T'\) contains zero rows, and hence \(\det T' = 0\). Otherwise, \(T'\) was obtained from \(T\) by multiplying certain rows by \(-1\). Since \(T'\) has finitely many rows, the number of such multiplications is also finite. Since multiplying a row by \(-1\) results in the determinant getting multiplied by \(-1\), we get \(\det T' = \pm \det T \in \{ 0, \pm 1\} \) as desired.
Let \(A\) be a TU matrix. Suppose columns of \(A\) are multiplied by \(\{ 0, \pm 1\} \) factors. Then the resulting matrix \(A'\) is also TU.
Apply Lemma 4 to \(A^{\top }\).
Given \(k \in \mathbb {N}\), we say that a matrix \(A\) is \(k\)-partially unimodular, or \(k\)-PU for short, if every (not necessarily contiguous, not necessarily injective) \(k \times k\) submatrix \(T\) of \(A\) has \(\det T \in \{ 0, \pm 1\} \).
A matrix \(A\) is TU if and only if \(A\) is \(k\)-PU for every \(k \in \mathbb {N}\).
Matrix made of 4 blocks (2x2).
1.2 Pivoting
Let \(A \in R^{X \times Y}\) be a matrix and let \((x, y) \in X \times Y\) be such that \(A (x, y) \neq 0\). A long tableau pivot in \(A\) on \((x, y)\) is the operation that maps \(A\) to the matrix \(A'\) where
Let \(A \in \mathbb {Q}^{X \times Y}\) be a TU matrix and let \((x, y) \in X \times Y\) be such that \(A (x, y) \neq 0\). Then performing the long tableau pivot in \(A\) on \((x, y)\) yields a TU matrix.
See implementation in Lean.
Let \(A \in R^{X \times Y}\) be a matrix and let \((x, y) \in X \times Y\) be such that \(A (x, y) \neq 0\). Perform the following sequence of operations.
Adjoin the identity matrix \(1 \in R^{X \times X}\) to \(A\), resulting in the matrix \(B = \begin{bmatrix} 1 & A \end{bmatrix} \in R^{X \times (X \oplus Y)}\).
Perform a long tableau pivot in \(B\) on \((x, y)\), and let \(C\) denote the result.
Swap columns \(x\) and \(y\) in \(C\), and let \(D\) be the resulting matrix.
Finally, remove columns indexed by \(X\) from \(D\), and let \(A'\) be the resulting matrix.
A short tableau pivot in \(A\) on \((x, y)\) is the operation that maps \(A\) to the matrix \(A'\) defined above.
Let \(A \in R^{X \times Y}\) be a matrix and let \((x, y) \in X \times Y\) be such that \(A (x, y) \neq 0\). Then the short tableau pivot in \(A\) on \((x, y)\) maps \(A\) to \(A'\) with
Follows by direct calculation.
Let \(B = \begin{bmatrix} B_{11} & 0 \\ B_{21} & B_{22} \end{bmatrix} \in \mathbb {Q}^{\{ X_{1} \cup X_{2}\} \times \{ Y_{1} \times Y_{2}\} }\). Let \(B' = \begin{bmatrix} B_{11}’ & B_{12}’ \\ B_{21}’ & B_{22}’ \end{bmatrix}\) be the result of performing a short tableau pivot on \((x, y) \in X_{1} \times Y_{1}\) in \(B\). Then \(B_{12}' = 0\), \(B_{22}' = B_{22}\), and \(\begin{bmatrix} B_{11}’ \\ B_{21}’ \end{bmatrix}\) is the matrix resulting from performing a short tableau pivot on \((x, y)\) in \(\begin{bmatrix} B_{11} \\ B_{21} \end{bmatrix}\).
This follows by a direct calculation. Indeed, because of the \(0\) block in \(B\), \(B_{12}\) and \(B_{22}\) remain unchanged, and since \(\begin{bmatrix} B_{11} \\ B_{21} \end{bmatrix}\) is a submatrix of \(B\) containing the pivot element, performing a short tableau pivot in it is equivalent to performing a short tableau pivot in \(B\) and then taking the corresponding submatrix.
Let \(k \in \mathbb {N}\), let \(A \in \mathbb {Q}^{k \times k}\), and let \(A'\) be the result of performing a short tableau pivot in \(A\) on \((x, y)\) with \(x, y \in \{ 1, \dots , k\} \) such that \(A (x, y) \neq 0\). Then \(A'\) contains a submatrix \(A''\) of size \((k - 1) \times (k - 1)\) with \(|\det A''| = |\det A| / |A (x, y)|\).
Let \(X = \{ 1, \dots , k\} \setminus \{ x\} \) and \(Y = \{ 1, \dots , k\} \setminus \{ y\} \), and let \(A'' = A' (X, Y)\). Since \(A''\) does not contain the pivot row or the pivot column, \(\forall (i, j) \in X \times Y\) we have \(A'' (i, j) = A (i, j) - \frac{A (i, y) \cdot A (x, j)}{A (x, y)}\). For \(\forall j \in Y\), let \(B_{j}\) be the matrix obtained from \(A\) by removing row \(x\) and column \(j\), and let \(B_{j}''\) be the matrix obtained from \(A''\) by replacing column \(j\) with \(A (X, y)\) (i.e., the pivot column without the pivot element). The cofactor expansion along row \(x\) in \(A\) yields
By reordering columns of every \(B_{j}\) to match their order in \(B_{j}''\), we get
By linearity of the determinant applied to \(\det A''\), we have
Therefore, \(|\det A''| = |\det A| / |A (x, y)|\).
Let \(A \in \mathbb {Q}^{X \times Y}\) be a TU matrix and let \((x, y) \in X \times Y\) be such that \(A (x, y) \neq 0\). Then performing the short tableau pivot in \(A\) on \((x, y)\) yields a TU matrix.
See implementation in Lean.
1.3 Vector Matroids
(Todo: Add definition of matroids)
Let \(R\) be a division ring, let \(X\) and \(Y\) be sets, and let \(A \in R^{X \times Y}\) be a matrix. The vector matroid of \(A\) is the matroid \(M = (Y, \mathcal{I})\) where a set \(I \subset Y\) is independent in \(M\) if and only if the columns of \(A\) indexed by \(I\) are linearly independent.
Let \(R\) be a division ring, let \(X\) and \(Y\) be disjoint sets, and let \(S \in R^{X \times Y}\) be a matrix. Let \(A = \begin{bmatrix} 1 & S \end{bmatrix} \in R^{X \times (X \cup Y)}\) be the matrix obtained from \(S\) by adjoining the identity matrix as columns, and let \(M\) be the vector matroid of \(A\). Then \(S\) is called the standard representation of \(M\).
Let \(S \in R^{X \times Y}\) be a standard representation of a vector matroid \(M\). Then \(X\) is a base in \(M\).
See implementation in Lean.
Adding extra zero rows to a full representation matrix of a vector matroid does not change the matroid.
See implementation in Lean.
Let \(A \in \mathbb {Q}^{X \times Y}\) be a TU matrix, let \(M\) be the vector matroid of \(A\), and let \(B\) be a base of \(M\). Then there exists a matrix \(S \in \mathbb {Q}^{B \times (Y \setminus B)}\) such that \(S\) is TU and \(S\) is a standard representation of \(M\).
See implementation in Lean.
Let \(R\) be a magma containing zero. The support of matrix \(A \in R^{X \times Y}\) is \(A^{\# } \in \{ 0, 1\} ^{X \times Y}\) given by
Transpose of a support matrix is equal to a support of the transposed matrix.
Definitional equality.
Submatrix of a support matrix is equal to a support matrix of the submatrix.
Definitional equality.
If \(A\) is a matrix over \(\mathbb {Z}_{2}\), then \(A^{\# } = A\).
Check elementwise equality.
If two standard representation matrices of the same matroid have the same base, then they have the same support.
See implementation in Lean.
A square matrix is invertible iff its determinant is invertible.
This result is proved in Mathlib.
Let \(A\) be a rational TU matrix with finite number of rows and finite number of columns. Its rows are linearly independent iff the rows of its support matrix are linearly independent.
See implementation in Lean.
Let \(A\) be a rational TU matrix with finite number of rows. Its rows are linearly independent iff the rows of its support matrix are linearly independent.
See implementation in Lean.
Let \(A\) be a rational TU matrix. Its rows are linearly independent iff the rows of its support matrix are linearly independent.
See implementation in Lean.
Let \(A\) be a TU matrix.
If a matroid is represented by \(A\), then it is also represented by \(A^{\# }\).
If a matroid is represented by \(A^{\# }\), then it is also represented by \(A\).
See implementation in Lean.
1.4 Regular Matroids
A matroid \(M\) is regular if there exists a TU matrix \(A \in \mathbb {Q}^{X \times Y}\) such that \(M\) is a vector matroid of \(A\).
We say that \(A' \in \mathbb {Q}^{X \times Y}\) is a TU signing of \(A \in \mathbb {Z}_{2}^{X \times Y}\) if \(A'\) is TU and
Let \(B \in \mathbb {Z}_{2}^{X \times Y}\) be a standard representation matrix of a matroid \(M\). Then \(M\) is regular if and only if \(B\) has a TU signing.
Suppose that \(M\) is regular. By Definition 32, there exists a TU matrix \(A \in \mathbb {Q}^{X \times Y}\) such that \(M\) is a vector matroid of \(A\). By Lemma 19, \(X\) (the row set of \(B\)) is a base of \(M\). By Lemma 21, \(A\) can be converted into a standard representation matrix \(B' \in \mathbb {Q}^{X \times Y}\) of \(M\) such that \(B'\) is also TU. Since \(B'\) and \(B\) are both standard representations of \(M\), by Lemma 26 the support matrices \((B')^{\# }\) and \(B^{\# }\) are the same. Lemma 25 gives \(B^{\# } = B\). Thus, \(B'\) is TU and \((B')^{\# } = B\), so \(B'\) is a TU signing of \(B\).
Suppose that \(B\) has a TU signing \(B' \in \mathbb {Q}^{X \times Y}\). Then \(A = [1 \mid B']\) is TU, as it is obtained from \(B'\) by adjoining the identity matrix. Moreover, by Lemma 31, \(A\) represents the same matroid as \(A^{\# } = [1 \mid B]\), which is \(M\). Thus, \(A\) is a TU matrix representing \(M\), so \(M\) is regular.