- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
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 \(A\) be a square matrix of the form \(A = \begin{bmatrix} A_{11} & A_{12} \\ 0 & A_{22} \end{bmatrix}\). Then \(\det A = \det A_{11} \cdot \det A_{22}\).
Adding extra zero rows to a full representation matrix of a vector matroid does not change the matroid.
Let \(X\) and \(Y\) be sets with \(\{ x_{2}, x_{1}, x_{0}\} \subseteq X\) and \(\{ y_{0}, y_{1}, y_{2}\} \subseteq Y\). Let \(Q \in \mathbb {Q}^{X \times Y}\) be a TU signing of \(Q_{0} \in \mathbb {Z}_{2}^{X \times Y}\) such that \(Q_{0} (\{ x_{2}, x_{1}, x_{0}\} , \{ y_{0}, y_{1}, y_{2}\} ) = S\) (from Definition 49). Then the canonical re-signing \(Q'\) of \(Q\) (from Definition 51) is a TU signing of \(Q_{0}\) and \(Q' (\{ x_{2}, x_{1}, x_{0}\} , \{ y_{0}, y_{1}, y_{2}\} ) = S'\) (from Definition 49).
Let \(Q\) be a TU signing of \(S\) (from Definition 49). Let \(u \in \{ 0, \pm 1\} ^{\{ x_{2}, x_{1}, x_{0}\} }\), \(v \in \{ 0, \pm 1\} ^{\{ y_{0}, y_{1}, y_{2}\} }\), and \(Q'\) be defined as follows:
Then \(Q' = S'\) (from Definition 49).
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\} \).
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 rational TU matrix. Its rows are linearly independent iff the rows of its support matrix are linearly independent.
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.
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.
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.
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.
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.
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.
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\).
A matrix \(A\) is TU if and only if \(A\) is \(k\)-PU for every \(k \in \mathbb {N}\).
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 \(D_{0} \in \mathbb {Z}_{2}^{\{ x_{1}, x_{0}\} \times \{ y_{0}, y_{1}\} }\) be an invertible matrix. Then, up to reindexing of rows and columns, either \(D_{0} = \begin{bmatrix} 1 & 0 \\ 0 & 1 \\ \end{bmatrix}\) or \(D_{0} = \begin{bmatrix} 1 & 1 \\ 0 & 1 \\ \end{bmatrix}\).
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 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
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}\).
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
Let \(X\) and \(Y\) be sets with \(\{ x_{2}, x_{1}, x_{0}\} \subseteq X\) and \(\{ y_{0}, y_{1}, y_{2}\} \subseteq Y\). Let \(Q \in \mathbb {Q}^{X \times Y}\) be a TU matrix. Define \(u \in \{ 0, \pm 1\} ^{X}\), \(v \in \{ 0, \pm 1\} ^{Y}\), and \(Q'\) as follows:
We call \(Q'\) the canonical re-signing of \(Q\).
We call \(D_{0}' \in \mathbb {Q}^{\{ x_{1}, x_{0}\} \times \{ y_{0}, y_{1}\} }\) the canonical signing of \(D_{0} \in \mathbb {Z}_{2}^{\{ x_{1}, x_{0}\} \times \{ y_{0}, y_{1}\} }\) if
Similarly, we call \(S' \in \mathbb {Q}^{\{ x_{2}, x_{1}, x_{0}\} \times \{ y_{0}, y_{1}, y_{2}\} }\) the canonical signing of \(S \in \mathbb {Z}_{2}^{\{ x_{2}, x_{1}, x_{0}\} \times \{ y_{0}, y_{1}, y_{2}\} }\) if
To simplify notation, going forward we use \(D_{0}\), \(D_{0}'\), \(S\), and \(S'\) to refer to the matrices of the form above. Observe that the canonical signing \(S'\) of \(S\) (from Definition 49) is TU.
Let \(X_{\ell }'\), \(Y_{\ell }'\), \(X_{r}'\), \(Y_{r}'\) be sets and let \(x_{0}\) and \(x_{1}\) be distinct elements contained neither in \(X_{\ell }'\) nor \(X_{r}'\). Additionally, let \(c_{0}, c_{1} \in \mathbb {Q}^{X_{r}' \cup \{ x_{1}, x_{0}\} }\) be column vectors. We define \(\mathcal{C} (X_{\ell }', Y_{\ell }', X_{r}', Y_{r}'; c_{0}, c_{1})\) to be the family of matrices of the form \(\begin{bmatrix} A_{\ell } & 0 \\ D & A_{r} \end{bmatrix}\) such that:
\(A_{\ell } \in \mathbb {Q}^{X_{\ell }' \times Y_{\ell }'}\), \(A_{r} \in \mathbb {Q}^{(X_{r}' \cup \{ x_{1}, x_{0}\} ) \times Y_{r}'}\), and \(D \in \mathbb {Q}^{(X_{r}' \cup \{ x_{1}, x_{0}\} ) \times Y_{\ell }'}\);
\(\begin{bmatrix} A_{\ell } \\ D \end{bmatrix}\) is TU;
for every \(j \in Y_{\ell }'\), \(D (X_{r}', j) \in \{ 0, \pm c_{0}, \pm c_{1}, \pm (c_{0} - c_{1})\} \);
\(\begin{bmatrix} c_{0} & c_{1} & c_{0} - c_{1} & A_{r} \end{bmatrix}\) is TU;
\(\begin{bmatrix} A_{\ell } & 0 \\ D (x_{0}, Y_{\ell }’) & 1 \\ D (x_{1}, Y_{\ell }’) & 1 \end{bmatrix}\) is TU;
\(c_{0} (x_{0}) = 1\) and \(c_{0} (x_{1}) = 0\);
either \(c_{1} (x_{0}) = 0\) and \(c_{1} (x_{1}) = -1\), or \(c_{1} (x_{0}) = 1\) and \(c_{1} (x_{1}) = 1\).
Let \(C \in \mathcal{C} (X_{\ell }', Y_{\ell }', X_{r}', Y_{r}'; c_{0}, c_{1})\) from Definition 58. Let \(x \in X_{\ell }'\) and \(y \in Y_{\ell }'\) be such that \(A_{\ell } (x, y) \neq 0\), and let \(C'\) be the result of performing a short tableau pivot in \(C\) on \((x, y)\). Then \(C' \in \mathcal{C} (X_{\ell }', Y_{\ell }', X_{r}', Y_{r}'; c_{0}, c_{1})\).
Suppose that \(B_{r}\) from Definition 46 has a TU signing \(B_{r}'\). Let \(B_{r}''\) be the canonical re-signing (from Definition 51) of \(B_{r}'\). Let \(c_{0}'' = B_{r}'' (X_{r}, y_{0})\), \(c_{1}'' = B_{r}'' (X_{r}, y_{1})\), and \(c_{2}'' = c_{0}'' - c_{1}''\). Then the following statements hold.
For every \(i \in X_{r}\), \(\begin{bmatrix} c_{0}” (i) & c_{1}” (i) \end{bmatrix} \in \{ 0, \pm 1\} ^{\{ y_{0}, y_{1}\} } \setminus \left\{ \begin{bmatrix} 1 & -1 \end{bmatrix}, \begin{bmatrix} -1 & 1 \end{bmatrix} \right\} \).
For every \(i \in X_{r}\), \(c_{2}'' (i) \in \{ 0, \pm 1\} \).
\(\begin{bmatrix} c_{0}” & c_{2}” & A_{r}” \end{bmatrix}\) is TU.
\(\begin{bmatrix} c_{1}” & c_{2}” & A_{r}” \end{bmatrix}\) is TU.
\(\begin{bmatrix} c_{0}” & c_{1}” & c_{2}” & A_{r}” \end{bmatrix}\) is TU.
Suppose that \(B_{\ell }\) from Definition 46 has a TU signing \(B_{\ell }'\). Let \(B_{\ell }''\) be the canonical re-signing (from Definition 51) of \(B_{\ell }'\). Let \(d_{0}'' = B_{\ell }'' (x_{0}, Y_{\ell })\), \(d_{1}'' = B_{\ell }'' (x_{1}, Y_{\ell })\), and \(d_{2}'' = d_{0}'' - d_{1}''\). Then the following statements hold.
For every \(j \in Y_{\ell }\), \(\begin{bmatrix} d_{0}” (i) \\ d_{1}” (j) \end{bmatrix} \in \{ 0, \pm 1\} ^{\{ x_{1}, x_{0}\} } \setminus \left\{ \begin{bmatrix} 1 \\ -1 \end{bmatrix}, \begin{bmatrix} -1 \\ 1 \end{bmatrix} \right\} \).
For every \(j \in Y_{\ell }\), \(d_{2}'' (j) \in \{ 0, \pm 1\} \).
\(\begin{bmatrix} A_{\ell }” \\ d_{0}” \\ d_{2}” \end{bmatrix}\) is TU.
\(\begin{bmatrix} A_{\ell }” \\ d_{1}” \\ d_{2}” \end{bmatrix}\) is TU.
\(\begin{bmatrix} A_{\ell }” \\ d_{0}” \\ d_{1}” \\ d_{2}” \end{bmatrix}\) is TU.
Let \(B''\) be from Definition 53. Let \(c_{0}'' = B'' (X_{r}, y_{0})\), \(c_{1}'' = B'' (X_{r}, y_{1})\), and \(c_{2}'' = c_{0}'' - c_{1}''\). Similarly, let \(d_{0}'' = B'' (x_{0}, Y_{\ell })\), \(d_{1}'' = B'' (x_{1}, Y_{\ell })\), and \(d_{2}'' = d_{0}'' - d_{1}''\). Then the following statements hold.
For every \(i \in X_{r}\), \(c_{2}'' (i) \in \{ 0, \pm 1\} \).
If \(D_{0}'' = \begin{bmatrix} 1 & 0 \\ 0 & -1 \end{bmatrix}\), then \(D'' = c_{0}'' \otimes d_{0}'' - c_{1}'' \otimes d_{1}''\). If \(D_{0}'' = \begin{bmatrix} 1 & 1 \\ 0 & 1 \end{bmatrix}\), then \(D'' = c_{0}'' \otimes d_{0}'' - c_{0}'' \otimes d_{1}'' + c_{1}'' \otimes d_{1}''\).
For every \(j \in Y_{\ell }\), \(D'' (X_{r}, j) \in \{ 0, \pm c_{0}'', \pm c_{1}'', \pm c_{2}''\} \).
For every \(i \in X_{r}\), \(D'' (i, Y_{\ell }) \in \{ 0, \pm d_{0}'', \pm d_{1}'', \pm d_{2}''\} \).
\(\begin{bmatrix} A_{\ell }” \\ D” \end{bmatrix}\) is TU.
Let \(B''\) be from Definition 53. Then \(B'' \in \mathcal{C} (X_{\ell }', Y_{\ell }', X_{r}', Y_{r}'; c_{0}'', c_{1}'')\) with \(X_{\ell }' = X_{\ell } \setminus \{ x_{1}, x_{0}\} \), \(X_{r}' = X_{r} \setminus \{ x_{2}, x_{1}, x_{0}\} \), \(Y_{\ell }' = Y_{\ell } \setminus \{ y_{2}\} \), \(Y_{r}' = Y_{r} \setminus \{ y_{0}, y_{1}\} \), \(x_{0}\) and \(x_{1}\) are the same, \(c_{0}'' = B'' (X_{r}', y_{0})\), and \(c_{1}'' = B'' (X_{r}', y_{1})\).
Suppose that \(B_{\ell }\) and \(B_{r}\) from Definition 46 have TU signings \(B_{\ell }'\) and \(B_{r}'\), respectively. Let \(B_{\ell }''\) and \(B_{r}''\) be the canonical re-signings (from Definition 51) of \(B_{\ell }'\) and \(B_{r}'\), respectively. Let \(A_{\ell }''\), \(A_{r}''\), \(D_{\ell }''\), \(D_{r}''\), and \(D_{0}''\) be blocks of \(B_{\ell }''\) and \(B_{r}''\) analogous to blocks \(A_{\ell }\), \(A_{r}\), \(D_{\ell }\), \(D_{r}\), and \(D_{0}\) of \(B_{\ell }\) and \(B_{r}\). The canonical signing \(B''\) of \(B\) is defined as
Note that \(D_{0}''\) is non-singular by construction, so \(D_{\ell r}''\) and hence \(B''\) are well-defined.
Any graphic matroid is good. Any cographic matroid is good. Any matroid isomorphic to R10 is good. Any 1-sum (in the sense of Definition 36) of good matroids is a good matroid. Any 2-sum (in the sense of Definition 41) of good matroids is a good matroid. Any 3-sum (in the sense of Definition 47) of good matroids is a good matroid. TODO some dependencies are missing in the blueprint.
Any good matroid is regular. This is a corollary of the easy direction of the Seymour theorem. TODO some dependencies are missing in the blueprint.
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\).
Let \(M\) be a \(1\)-sum of regular matroids \(M_{\ell }\) and \(M_{r}\). Then \(M\) is also regular.
Let \(M\) be a \(2\)-sum of regular matroids \(M_{\ell }\) and \(M_{r}\). Then \(M\) is also regular.
Let \(M\) be a \(3\)-sum of regular matroids \(M_{\ell }\) and \(M_{r}\). Then \(M\) is also regular.
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 \(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\).
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.
Let \(R\) be a magma containing zero (we will use \(R = \mathbb {Z}_{2}\) and \(R = \mathbb {Q}\)). Let \(B_{\ell } \in R^{X_{\ell } \times Y_{\ell }}\) and \(B_{r} \in R^{X_{r} \times Y_{r}}\) be matrices where \(X_{\ell }, Y_{\ell }, X_{r}, Y_{r}\) are pairwise disjoint sets. The \(1\)-sum \(B = B_{\ell } \oplus _{1} B_{r}\) of \(B_{\ell }\) and \(B_{r}\) is
Let \(R\) be a semiring (we will use \(R = \mathbb {Z}_{2}\) and \(R = \mathbb {Q}\)). Let \(B_{\ell } \in R^{X_{\ell } \times Y_{\ell }}\) and \(B_{r} \in R^{X_{r} \times Y_{r}}\) where \(X_{\ell } \cap X_{r} = \{ x\} \), \(Y_{\ell } \cap Y_{r} = \{ y\} \), \(X_{\ell }\) is disjoint with \(Y_{\ell }\) and \(Y_{r}\), and \(X_{r}\) is disjoint with \(Y_{\ell }\) and \(Y_{r}\). Additionally, let \(A_{\ell } = B_{\ell } (X_{\ell } \setminus \{ x\} , Y_{\ell })\) and \(A_{r} = B_{r} (X_{r}, Y_{r} \setminus \{ y\} )\), and suppose \(r = B_{\ell } (x, Y_{\ell }) \neq 0\) and \(c = B_{r} (X_{r}, y) \neq 0\). Then the \(2\)-sum \(B = B_{\ell } \oplus _{2, x, y} B_{r}\) of \(B_{\ell }\) and \(B_{r}\) is defined as
Here \(D \in R^{X_{r} \times Y_{\ell }}\), and the indexing is consistent everywhere.
Let \(B_{\ell }\) and \(B_{r}\) be matrices from Definition 40. Let \(B_{\ell }'\) and \(B'\) be the matrices obtained by performing a short tableau pivot on \((x_{\ell }, y_{\ell }) \in X_{\ell } \times Y_{\ell }\) in \(B_{\ell }\) and \(B\), respectively. Then \(B' = B_{\ell }' \oplus _{2, x, y} B_{r}\).
Let \(X_{\ell }\), \(Y_{\ell }\), \(X_{r}\), and \(Y_{r}\) be sets satisfying the following properties:
\(X_{\ell } \cap X_{r} = \{ x_{2}, x_{1}, x_{0}\} \) for some distinct \(x_{0}\), \(x_{1}\), and \(x_{2}\);
\(Y_{\ell } \cap Y_{r} = \{ y_{0}, y_{1}, y_{2}\} \) for some distinct \(y_{0}\), \(y_{1}\), and \(y_{2}\);
\(X_{\ell }\) is disjoint with \(Y_{r}\); and
\(Y_{\ell }\) is disjoint with \(X_{r}\).
Let \(B_{\ell } \in \mathbb {Z}_{2}^{X_{\ell } \times Y_{\ell }}\) and \(B_{r} \in \mathbb {Z}_{2}^{X_{r} \times Y_{r}}\) be matrices of the form
where \(D_{0}\) is invertible. Then the \(3\)-sum \(B = B_{\ell } \oplus _{3} B_{r}\) of \(B_{\ell }\) and \(B_{r}\) is defined as
Here the indexing is consistent between all the matrices, \(D_{0} \in \mathbb {Z}_{2}^{\{ x_{1}, x_{0}\} \times \{ y_{0}, y_{1}\} }\), and the submatrix
is indexed by \(\{ x_{2}, x_{1}, x_{0}\} \times \{ y_{0}, y_{1}, y_{2}\} \) in \(B_{\ell }\), \(B_{r}\), and \(B\).
If two standard representation matrices of the same matroid have the same base, then they have the same support.
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 \(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\).