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

Matrix A is a TU signing of U iff A is TU and its entries are the same as in U up to signs. Do not ask U.IsTotallyUnimodular ... see Matrix.overZ2_isTotallyUnimodular for example!

Equations

• A.IsTuSigningOf U = (A.IsTotallyUnimodular ∧ ∀ (i : X) (j : Y), |A i j| = ↑(U i j).val)

def Matrix.HasTuSigning {X Y : Type} {n : ℕ} (U : Matrix X Y (ZMod n)) : Prop

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

Equations

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

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

The main definition of regularity: M is regular iff it is constructed from a VectorMatroid with a rational TU matrix.

Equations

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

theorem Matroid.IsRegular.isBinary {α : Type} [DecidableEq α] {M : Matroid α} [Finite ↑M.E] (hM : M.IsRegular) : ∃ (V : VectorMatroid α Z2), V.toMatroid = M

Every regular matroid is binary.

theorem Matroid.IsRegular.isBinaryStd {α : Type} [DecidableEq α] {M : Matroid α} [Finite ↑M.E] (hM : M.IsRegular) : ∃ (S : StandardRepr α Z2), S.toMatroid = M

Every regular matroid has a standard binary representation.

@[reducible, inline]

abbrev StandardRepr.HasTuSigning {α : Type} [DecidableEq α] (S : StandardRepr α Z2) : Prop

Matroid M that can be represented by a matrix over Z2 with a TU signing

Equations

• S.HasTuSigning = S.B.HasTuSigning

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

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