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 determinant 0 or 1 or -1.

Main results

• Matrix.isTotallyUnimodular_iff: a matrix is totally unimodular iff every square submatrix (possibly with repeated rows and/or repeated columns) has determinant 0 or 1 or -1.
• Matrix.IsTotallyUnimodular.apply: entry in a totally unimodular matrix is 0 or 1 or -1.

def Matrix.IsTotallyUnimodular {m : Type u_1} {n : Type u_3} {R : Type u_5} [CommRing R] (A : Matrix m n R) : Prop

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

theorem Matrix.isTotallyUnimodular_iff {m : Type u_1} {n : Type u_3} {R : Type u_5} [CommRing R] (A : Matrix m n R) : A.IsTotallyUnimodular ↔ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

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) : A i j ∈ Set.range SignType.cast

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) : A.transpose.IsTotallyUnimodular

theorem Matrix.transpose_isTotallyUnimodular_iff {m : Type u_1} {n : Type u_3} {R : Type u_5} [CommRing R] (A : Matrix m n R) : A.transpose.IsTotallyUnimodular ↔ 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.reindex_isTotallyUnimodular {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') : ((Matrix.reindex em en) A).IsTotallyUnimodular ↔ 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) : (A.fromRows B).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

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) : (A.fromRows 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

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) : (Matrix.fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

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) : (A.fromColumns 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

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) : (Matrix.fromColumns 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

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 → (Matrix.fromRows 1 A).IsTotallyUnimodular

Alias of the reverse direction of Matrix.one_fromRows_isTotallyUnimodular_iff.

theorem Matrix.IsTotallyUnimodular.fromColumns_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.fromColumns 1).IsTotallyUnimodular

Alias of the reverse direction of Matrix.fromColumns_one_isTotallyUnimodular_iff.

theorem Matrix.IsTotallyUnimodular.one_fromColumns {m : Type u_1} {n : Type u_3} {R : Type u_5} [CommRing R] [DecidableEq m] (A : Matrix m n R) : A.IsTotallyUnimodular → (Matrix.fromColumns 1 A).IsTotallyUnimodular

Alias of the reverse direction of Matrix.one_fromColumns_isTotallyUnimodular_iff.

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) : (A.fromRows (Matrix.row m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

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) : (A.fromColumns (Matrix.col n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular