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

Matroid is graphic iff it is represented by an incidence matrix of a graph.

Equations

• A.IsGraphic = ∀ (y : n), ∃ (x₁ : m) (x₂ : m), A x₁ y = 1 ∧ A x₂ y = -1 ∧ ∀ (x : m), x ≠ x₁ → x ≠ x₂ → A x y = 0

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

Matroid is graphic iff it is represented by an incidence matrix of a graph.

Equations

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

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

Matroid is cographic iff its dual is represented by an incidence matrix of a graph.

Equations

• M.IsCographic = M✶.IsGraphic

theorem Matrix.IsGraphic.isTotallyUnimodular_of_represents {α : Type} {X Y : Set α} {A : Matrix ↑X ↑Y ℚ} {M : Matroid α} (hA : A.IsGraphic) (hAM : { X := X, Y := Y, A := A }.toMatroid = M) : A.IsTotallyUnimodular

Graphic matroid can be represented only by a TU matrix.

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

Graphic matroid is regular.

theorem Matroid.IsCographic.isRegular {α : Type} {M : Matroid α} (hM : M.IsCographic) : M.IsRegular

Cographic matroid is regular.