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) :

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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) :

(A.fromCols 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

source

@[deprecated Matrix.fromCols_one_isTotallyUnimodular_iff]

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.fromCols 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Alias of Matrix.fromCols_one_isTotallyUnimodular_iff.

source

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) :

(Matrix.fromCols 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

source

@[deprecated Matrix.one_fromCols_isTotallyUnimodular_iff]

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.fromCols 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Alias of Matrix.one_fromCols_isTotallyUnimodular_iff.

source

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.

source

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.

source

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.

source

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

Alias of the reverse direction of Matrix.one_fromCols_isTotallyUnimodular_iff.

source

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

source

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) :

(A.fromCols (Matrix.col n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

source

@[deprecated Matrix.fromCols_col0_isTotallyUnimodular_iff]

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

Alias of Matrix.fromCols_col0_isTotallyUnimodular_iff.

Documentation

Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Totally unimodular matrices #

Main definitions #

Main results #