Graphicness

Here we study graphic and cographic matroids.

def IsIncidenceMatrixColumn {m : Type} [DecidableEq m] (v : m → ℚ) : Prop

Column of a node-edge incidence matrix is either all 0, or has exactly one +1 entry, exactly one -1 entry, and all other elements 0.

Equations

• IsIncidenceMatrixColumn v = (v = 0 ∨ ∃ (i₁ : m) (i₂ : m), i₁ ≠ i₂ ∧ v i₁ = 1 ∧ v i₂ = -1 ∧ ∀ (i : m), i ≠ i₁ → i ≠ i₂ → v i = 0)

def Matrix.IsGraphic {m n : Type} [DecidableEq m] (A : Matrix m n ℚ) : Prop

Matrix is called graphic iff it is a node-edge incidence matrix of a (directed) graph.

Equations

• A.IsGraphic = ∀ (y : n), IsIncidenceMatrixColumn fun (x : m) => A x y

theorem IsIncidenceMatrixColumn.eq_if_mem {m : Type} [DecidableEq m] {v : m → ℚ} (hv : IsIncidenceMatrixColumn v) : v = 0 ∨ ∃ (i₁ : m) (i₂ : m), i₁ ≠ i₂ ∧ v = fun (i : m) => if i ∈ [i₁, i₂].toFinset then if i = i₁ then 1 else -1 else 0

The column function can be defined as an if statement with membership. We write it in this form to satisfy Fintype.sum_ite_mem.

theorem IsIncidenceMatrixColumn.elem_in_signTypeCastRange {m : Type} [DecidableEq m] {v : m → ℚ} (hv : IsIncidenceMatrixColumn v) (i : m) : v i ∈ SignType.cast.range

Every element of a column of a node-edge incidence matrix is 1, 0, or -1.

theorem IsIncidenceMatrixColumn.sum_zero {m : Type} [Fintype m] [DecidableEq m] {v : m → ℚ} (hv : IsIncidenceMatrixColumn v) : ∑ i : m, v i = 0

The sum of a column of an incidence matrix is 0.

theorem Matrix.IsGraphic.elem_in_signTypeCastRange {m n : Type} [DecidableEq m] {A : Matrix m n ℚ} (hA : A.IsGraphic) (i : m) (j : n) : A i j ∈ SignType.cast.range

Every element of a graphic matrix is 1, 0, or -1.

theorem IsIncidenceMatrixColumn.zero_or_two_nonzeros {m : Type} [DecidableEq m] {v : m → ℚ} (hv : IsIncidenceMatrixColumn v) : v = 0 ∨ ∃ (i₁ : m) (i₂ : m), i₁ ≠ i₂ ∧ ∀ (i : m), i ≠ i₁ → i ≠ i₂ → v i = 0

Column of a node-edge incidence matrix has either zero or two non-zero entries.

theorem Matrix.IsGraphic.col_zero_or_two_nonzeros {m n : Type} [DecidableEq m] {A : Matrix m n ℚ} (hA : A.IsGraphic) (y : n) : (fun (x : m) => A x y) = 0 ∨ ∃ (i₁ : m) (i₂ : m), i₁ ≠ i₂ ∧ ∀ (i : m), i ≠ i₁ → i ≠ i₂ → (fun (x : m) => A x y) i = 0

Column of a node-edge incidence matrix has either zero or two non-zero entries.

theorem Matrix.IsGraphic.cols_sum_zero {m n : Type} [Fintype n] [Fintype m] [DecidableEq m] {A : Matrix m n ℚ} (hA : A.IsGraphic) : ∑ x : m, A x = 0

The sum of the columns in a graphic matrix is 0.

theorem Matrix.IsGraphic.submatrix_one_if_not_graphic {l m o n : Type} [DecidableEq l] [DecidableEq m] {A : Matrix m n ℚ} (hA : A.IsGraphic) {f : l → m} {g : o → n} (hf : Function.Injective f) (hAfg : ¬(A.submatrix f g).IsGraphic) : ∃ (y : o) (x : l), (A.submatrix f g x y = 1 ∨ A.submatrix f g x y = -1) ∧ ∀ (i : l), i ≠ x → A.submatrix f g i y = 0

A nongraphic submatrix of a graphic matrix is only nongraphic iff there exists a column in it that only has one non-zero entry

def Matroid.IsGraphic {α : Type} [DecidableEq α] (M : Matroid α) : Prop

Matroid is graphic iff it can be represented by a graphic matrix.

Equations

• M.IsGraphic = ∃ (X : Set α) (Y : Set α) (A : Matrix ↑X ↑Y ℚ), A.IsGraphic ∧ A.toMatroid = M

def Matroid.IsCographic {α : Type} [DecidableEq α] (M : Matroid α) : Prop

Matroid is cographic iff its dual is graphic.

Equations

• M.IsCographic = M✶.IsGraphic

theorem Matrix.IsGraphic.isTotallyUnimodular {α : Type} [DecidableEq α] {X Y : Set α} {A : Matrix ↑X ↑Y ℚ} (hA : A.IsGraphic) : A.IsTotallyUnimodular

Node-edge incidence matrix is totally unimodular.

theorem Matroid.IsGraphic.isRegular {α : Type} [DecidableEq α] {M : Matroid α} (hM : M.IsGraphic) : M.IsRegular

Graphic matroid is regular.