Support Matrix

This file defines the support matrix and provides some API about them.

def Matrix.support {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Zero R] [DecidableEq R] (A : Matrix X Y R) : Matrix X Y Z2

Auxiliary Z2-valued matrix that has 1 on the position of all nonzero elements.

Equations

• A.support = Matrix.of fun (x1 : X) (x2 : Y) => if A x1 x2 = 0 then 0 else 1

theorem Matrix.support_transpose {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Zero R] [DecidableEq R] (A : Matrix X Y R) : A.support.transpose = A.transpose.support

theorem Matrix.support_submatrix {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Zero R] [DecidableEq R] (A : Matrix X Y R) {X' : Type u_4} {Y' : Type u_5} (f : X' → X) (g : Y' → Y) : A.support.submatrix f g = (A.submatrix f g).support

theorem Matrix.support_Z2 {X : Type u_1} {Y : Type u_2} (A : Matrix X Y Z2) : A.support = A

theorem Matrix.IsTotallyUnimodular.abs_eq_support_val {X : Type u_1} {Y : Type u_2} {A : Matrix X Y ℚ} (hA : A.IsTotallyUnimodular) (i : X) (j : Y) : |A i j| = ↑(ZMod.val (A.support i j))

theorem Matrix.IsTotallyUnimodular.abs_cast_eq_support {X : Type u_1} {Y : Type u_2} {A : Matrix X Y ℚ} (hA : A.IsTotallyUnimodular) (i : X) (j : Y) : ↑|A i j| = A.support i j

theorem Matrix.IsTotallyUnimodular.apply_abs_eq_one {X : Type u_1} {Y : Type u_2} {A : Matrix X Y ℚ} (hA : A.IsTotallyUnimodular) {i : X} {j : Y} (hAij : A.support i j = 1) : |A i j| = 1