Graphicness

Here we study graphic and cographic matroids.

def IsIncidenceMatrixColumn {m : Type u_1} [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 : Type u_1} {n : Type u_2} [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 Matrix.IsGraphic.elem_in_signTypeCastRange {m : Type u_1} {n : Type u_2} [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 Matrix.IsGraphic.col_zero_or_two_nonzeros {m : Type u_1} {n : Type u_2} [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 : Type u_1} {n : Type u_2} [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.

def Matroid.IsGraphic {α : Type u_1} [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 u_1} [DecidableEq α] (M : Matroid α) : Prop

Matroid is cographic iff its dual is graphic.

Equations

• M.IsCographic = M✶.IsGraphic

theorem Matrix.IsGraphic.isTotallyUnimodular {α : Type u_1} [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 u_1} [DecidableEq α] {M : Matroid α} (hM : M.IsGraphic) : M.IsRegular

Graphic matroid is regular.