This file defines binary matroids and regular matroids. Basic API is provided.

structure StandardRepresentation (α : Type u_1) [DecidableEq α] : Type u_1

Data describing a binary matroid on the ground set X ∪ Y where X and Y are bundled.

• X : Set α

  Basis elements -> row indices of [1 | B]

• Y : Set α

  Nonbasis elements -> column indices of B

• decmemX : (a : α) → Decidable (a ∈ self.X)

  Necessary decidability

• decmemY : (a : α) → Decidable (a ∈ self.Y)

  Necessary decidability

• hXY : self.X ⫗ self.Y

  Basis and nonbasis elements are disjoint

• B : Matrix (↑self.X) (↑self.Y) Z2

  The standard representation matrix

theorem StandardRepresentation.hXY {α : Type u_1} [DecidableEq α] (self : StandardRepresentation α) : self.X ⫗ self.Y

Basis and nonbasis elements are disjoint

def Matrix.IndepCols {α : Type u_1} [DecidableEq α] {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (B : Matrix (↑X) (↑Y) Z2) (S : Set α) : Prop

Given matrix B, is the set of columns S in the (standard) representation [1 | B] Z2-independent?

Equations

• B.IndepCols S = ∃ (hs : S ⊆ X ∪ Y), LinearIndependent (ι := ↑S) Z2 ((Matrix.fromColumns 1 B).submatrix id (Subtype.toSum ∘ hs.elem)).transpose

theorem Matrix.IndepCols_empty {α : Type u_1} [DecidableEq α] {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {B : Matrix (↑X) (↑Y) Z2} : B.IndepCols ∅

The empty set of columns is linearly independent.

theorem Matrix.IndepCols_subset {α : Type u_1} [DecidableEq α] {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {B : Matrix (↑X) (↑Y) Z2} (I : Set α) (J : Set α) (hBJ : B.IndepCols J) (hIJ : I ⊆ J) : B.IndepCols I

A subset of a linearly independent set of columns is linearly independent.

theorem Matrix.IndepCols_augment {α : Type u_1} [DecidableEq α] {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {B : Matrix (↑X) (↑Y) Z2} (I : Set α) (J : Set α) (hBI : B.IndepCols I) (hBI' : ¬Maximal B.IndepCols I) (hBJ : Maximal B.IndepCols J) : ∃ x ∈ J \ I, B.IndepCols (x ᕃ I)

A nonmaximal linearly independent set of columns can be augmented with another linearly independent column.

theorem Matrix.IndepCols_maximal {α : Type u_1} [DecidableEq α] {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {B : Matrix (↑X) (↑Y) Z2} (S : Set α) : Matroid.ExistsMaximalSubsetProperty B.IndepCols S

Any set of columns has the maximal subset property.

def Matrix.toIndepMatroid {α : Type u_1} [DecidableEq α] {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (B : Matrix (↑X) (↑Y) Z2) : IndepMatroid α

Binary matroid generated by its standard representation matrix, expressed as IndepMatroid.

Equations

• B.toIndepMatroid = { E := X ∪ Y, Indep := B.IndepCols, indep_empty := ⋯, indep_subset := ⋯, indep_aug := ⋯, indep_maximal := ⋯, subset_ground := ⋯ }

def Matrix.toMatroid {α : Type u_1} [DecidableEq α] {X : Set α} {Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (B : Matrix (↑X) (↑Y) Z2) : Matroid α

Binary matroid generated by its standard representation matrix, expressed as Matroid.

Equations

• B.toMatroid = B.toIndepMatroid.matroid

def StandardRepresentation.toMatroid {α : Type u_1} [DecidableEq α] (M : StandardRepresentation α) : Matroid α

Convert StandardRepresentation to Matroid.

Equations

• M.toMatroid = M.B.toMatroid

@[simp]

theorem StandardRepresentation.E_eq {α : Type u_1} [DecidableEq α] (M : StandardRepresentation α) : M.toMatroid.E = M.X ∪ M.Y

@[simp]

theorem StandardRepresentation.indep_eq {α : Type u_1} [DecidableEq α] (M : StandardRepresentation α) : M.toMatroid.Indep = M.B.IndepCols

instance instCoeStandardRepresentationMatroid {α : Type u_1} [DecidableEq α] : Coe (StandardRepresentation α) (Matroid α)

Registered conversion from StandardRepresentation to Matroid.

Equations

• instCoeStandardRepresentationMatroid = { coe := StandardRepresentation.toMatroid }

def StandardRepresentation.IsRegular {α : Type u_1} [DecidableEq α] (M : StandardRepresentation α) : Prop

The binary matroid is regular iff the standard representation matrix has a totally unimodular signing.

Equations

• M.IsRegular = ∃ (B' : Matrix ↑M.X ↑M.Y ℚ), B'.TU ∧ ∀ (i : ↑M.X) (j : ↑M.Y), if M.B i j = 0 then B' i j = 0 else B' i j = 1 ∨ B' i j = -1

theorem StandardRepresentation.isRegular_iff {α : Type u_1} [DecidableEq α] (M : StandardRepresentation α) : M.IsRegular ↔ ∃ (B' : Matrix ↑M.X ↑M.Y ℚ), (Matrix.fromColumns 1 B').TU ∧ ∀ (i : ↑M.X) (j : ↑M.Y), if M.B i j = 0 then B' i j = 0 else B' i j = 1 ∨ B' i j = -1

The binary matroid is regular iff the entire matrix has a totally unimodular signing.

theorem StandardRepresentation_toMatroid_isRegular_iff {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} (hM : M₁.toMatroid = M₂.toMatroid) : M₁.IsRegular ↔ M₂.IsRegular