Totally unimodular matrices #
This file defines totally unimodular matrices and provides basic API for them.
Main definitions #
Matrix.IsTotallyUnimodular: a matrix is totally unimodular iff every square submatrix (not necessarily contiguous) has determinant0or1or-1.
Main results #
Matrix.isTotallyUnimodular_iff: a matrix is totally unimodular iff every square submatrix (possibly with repeated rows and/or repeated columns) has determinant0or1or-1.Matrix.IsTotallyUnimodular.apply: entry in a totally unimodular matrix is0or1or-1.
def
Matrix.IsTotallyUnimodular
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
(A : Matrix m n R)
:
A.IsTotallyUnimodular means that every square submatrix of A (not necessarily contiguous)
has determinant 0 or 1 or -1; that is, the determinant is in the range of SignType.cast.
Equations
- A.IsTotallyUnimodular = ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), Function.Injective f → Function.Injective g → (A.submatrix f g).det ∈ Set.range SignType.cast
Instances For
theorem
Matrix.isTotallyUnimodular_iff_fintype
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
(A : Matrix m n R)
:
A.IsTotallyUnimodular ↔ ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
(A.submatrix f g).det ∈ Set.range SignType.cast
theorem
Matrix.IsTotallyUnimodular.apply
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
{A : Matrix m n R}
(hA : A.IsTotallyUnimodular)
(i : m)
(j : n)
:
theorem
Matrix.IsTotallyUnimodular.submatrix
{m : Type u_1}
{m' : Type u_2}
{n : Type u_3}
{n' : Type u_4}
{R : Type u_5}
[CommRing R]
{A : Matrix m n R}
(f : m' → m)
(g : n' → n)
(hA : A.IsTotallyUnimodular)
:
(A.submatrix f g).IsTotallyUnimodular
theorem
Matrix.IsTotallyUnimodular.transpose
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
{A : Matrix m n R}
(hA : A.IsTotallyUnimodular)
:
theorem
Matrix.IsTotallyUnimodular.reindex
{m : Type u_1}
{m' : Type u_2}
{n : Type u_3}
{n' : Type u_4}
{R : Type u_5}
[CommRing R]
{A : Matrix m n R}
(em : m ≃ m')
(en : n ≃ n')
(hA : A.IsTotallyUnimodular)
:
((Matrix.reindex em en) A).IsTotallyUnimodular
theorem
Matrix.IsTotallyUnimodular.fromRows_unitlike
{m : Type u_1}
{m' : Type u_2}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq n]
{A : Matrix m n R}
{B : Matrix m' n R}
(hA : A.IsTotallyUnimodular)
(hB : Nonempty n → ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single j ↑s)
:
(A.fromRows B).IsTotallyUnimodular
If A is totally unimodular and each row of B is all zeros except for at most a single 1 or
a single -1 then fromRows A B is totally unimodular.
theorem
Matrix.fromRows_isTotallyUnimodular_iff_rows
{m : Type u_1}
{m' : Type u_2}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq n]
{A : Matrix m n R}
{B : Matrix m' n R}
(hB : Nonempty n → ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single j ↑s)
:
If A is totally unimodular and each row of B is all zeros except for at most a single 1,
then fromRows A B is totally unimodular.
theorem
Matrix.fromRows_one_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq n]
(A : Matrix m n R)
:
theorem
Matrix.one_fromRows_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq n]
(A : Matrix m n R)
:
theorem
Matrix.fromCols_one_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq m]
(A : Matrix m n R)
:
@[deprecated Matrix.fromCols_one_isTotallyUnimodular_iff (since := "2024-12-11")]
theorem
Matrix.fromColumns_one_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq m]
(A : Matrix m n R)
:
theorem
Matrix.one_fromCols_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq m]
(A : Matrix m n R)
:
@[deprecated Matrix.one_fromCols_isTotallyUnimodular_iff (since := "2024-12-11")]
theorem
Matrix.one_fromColumns_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq m]
(A : Matrix m n R)
:
theorem
Matrix.IsTotallyUnimodular.fromRows_one
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq n]
(A : Matrix m n R)
:
A.IsTotallyUnimodular → (A.fromRows 1).IsTotallyUnimodular
Alias of the reverse direction of Matrix.fromRows_one_isTotallyUnimodular_iff.
theorem
Matrix.IsTotallyUnimodular.one_fromRows
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq n]
(A : Matrix m n R)
:
A.IsTotallyUnimodular → (fromRows 1 A).IsTotallyUnimodular
Alias of the reverse direction of Matrix.one_fromRows_isTotallyUnimodular_iff.
theorem
Matrix.IsTotallyUnimodular.fromCols_one
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq m]
(A : Matrix m n R)
:
A.IsTotallyUnimodular → (A.fromCols 1).IsTotallyUnimodular
Alias of the reverse direction of Matrix.fromCols_one_isTotallyUnimodular_iff.
theorem
Matrix.IsTotallyUnimodular.one_fromCols
{m : Type u_1}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
[DecidableEq m]
(A : Matrix m n R)
:
A.IsTotallyUnimodular → (fromCols 1 A).IsTotallyUnimodular
Alias of the reverse direction of Matrix.one_fromCols_isTotallyUnimodular_iff.
@[deprecated Matrix.fromRows_replicateRow0_isTotallyUnimodular_iff (since := "2024-12-11")]
theorem
Matrix.fromRows_row0_isTotallyUnimodular_iff
{m : Type u_1}
{m' : Type u_2}
{n : Type u_3}
{R : Type u_5}
[CommRing R]
(A : Matrix m n R)
:
Alias of Matrix.fromRows_replicateRow0_isTotallyUnimodular_iff.
@[deprecated Matrix.fromCols_replicateCol0_isTotallyUnimodular_iff (since := "2024-12-11")]
theorem
Matrix.fromColumns_col0_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{n' : Type u_4}
{R : Type u_5}
[CommRing R]
(A : Matrix m n R)
:
Alias of Matrix.fromCols_replicateCol0_isTotallyUnimodular_iff.
@[deprecated Matrix.fromCols_replicateCol0_isTotallyUnimodular_iff (since := "2024-12-11")]
theorem
Matrix.fromCols_col0_isTotallyUnimodular_iff
{m : Type u_1}
{n : Type u_3}
{n' : Type u_4}
{R : Type u_5}
[CommRing R]
(A : Matrix m n R)
:
Alias of Matrix.fromCols_replicateCol0_isTotallyUnimodular_iff.