Regularity

Here we study regular matroids.

Primary definition of regularity (LI & TU over ℚ)

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

Matroid is regular iff it can be constructed from a rational TU matrix.

Equations

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

Secondary definition of regularity (LI over Z2 while TU over ℚ)

def Matrix.IsTuSigningOf {X Y : Type} (A : Matrix X Y ℚ) (U : Matrix X Y Z2) : Prop

Rational matrix A is a TU signing of U (matrix of the same size but different type) iff A is TU and its entries are the same as entries in U on respective positions up to signs. Do not ask U.IsTotallyUnimodular ... see Matrix.overZ2_isTotallyUnimodular for example!

Equations

• A.IsTuSigningOf U = (A.IsTotallyUnimodular ∧ A.IsSigningOf U)

def Matrix.HasTuSigning {X Y : Type} (U : Matrix X Y Z2) : Prop

Matrix U has a TU signing iff there is a rational TU matrix whose entries are the same as those in U up to signs.

Equations

• U.HasTuSigning = ∃ (A : Matrix X Y ℚ), A.IsTuSigningOf U

Auxiliary stuff

theorem Matrix.IsTotallyUnimodular.isTuSigningOf_support {X Y : Type} {A : Matrix X Y ℚ} (hA : A.IsTotallyUnimodular) : A.IsTuSigningOf A.support

theorem Matrix.isTuSigningOf_iff {X Y : Type} (A : Matrix X Y ℚ) (U : Matrix X Y Z2) : A.IsTuSigningOf U ↔ A.IsTotallyUnimodular ∧ A.support = U

@[simp]

theorem Matroid.isRegular_mapEquiv_iff {α β : Type} (M : Matroid α) (e : α ≃ β) : (M.mapEquiv e).IsRegular ↔ M.IsRegular

Regularity of matroids is preserved under remapping.

Main results of this file

theorem Matroid.IsRegular.isBinary {α : Type} [DecidableEq α] {M : Matroid α} (hM : M.IsRegular) : ∃ (X : Set α) (Y : Set α) (A : Matrix (↑X) (↑Y) Z2), A.toMatroid = M

Every regular matroid is binary.

theorem StandardRepr.toMatroid_isRegular_iff_hasTuSigning {α : Type} [DecidableEq α] (S : StandardRepr α Z2) [Finite ↑S.X] : S.toMatroid.IsRegular ↔ S.B.HasTuSigning

Binary matroid constructed from a standard representation is regular iff the binary matrix has a TU signing.