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_2} {R : Type u_3} [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_2} {R : Type u_3} [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_2} {R : Type u_3} [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_2} {R : Type u_3} [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} {n : Type u_2} {R : Type u_3} [CommRing R] {A : Matrix m n R} (hA : A.IsTotallyUnimodular) {k : ℕ} (f : Fin k → m) (g : Fin k → n) : (A.submatrix f g).IsTotallyUnimodular

theorem Matrix.IsTotallyUnimodular.transpose {m : Type u_1} {n : Type u_2} {R : Type u_3} [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_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) : A.transpose.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

theorem Matrix.mapEquiv_isTotallyUnimodular {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] {X' : Type u_4} {Y' : Type u_5} (A : Matrix m n R) (eX : X' ≃ m) (eY : Y' ≃ n) : Matrix.IsTotallyUnimodular ((fun (x : m) => A x ∘ ⇑eY) ∘ ⇑eX) ↔ A.IsTotallyUnimodular

theorem Matrix.fromRows_row0_isTotallyUnimodular_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) {m' : Type u_4} : (A.fromRows (Matrix.row m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

theorem Matrix.fromColumns_col0_isTotallyUnimodular_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix m n R) {n' : Type u_4} : (A.fromColumns (Matrix.col n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular