structure VectorMatroid (α R : Type) : Type

Data representing a vector matroid M[A] of matrix A.

• X : Set α

  Row indices.

• Y : Set α

  Col indices.

• A : Matrix (↑self.X) (↑self.Y) R

  Full representation matrix.

def VectorMatroid.IndepCols {α R : Type} [Semiring R] (M : VectorMatroid α R) (I : Set α) : Prop

A set S is independent in M[A] iff S ⊆ Y and S corresponds to a linearly independent submultiset of columns in A.

Equations

• M.IndepCols I = ∃ (hI : I ⊆ M.Y), LinearIndependent R fun (i : ↑I) (x : ↑M.X) => M.A x (hI.elem i)

theorem VectorMatroid.indepCols_iff_submatrix {α R : Type} [Semiring R] (M : VectorMatroid α R) (I : Set α) : M.IndepCols I ↔ ∃ (hI : I ⊆ M.Y), LinearIndependent (ι := ↑I) R (M.A.submatrix id hI.elem).transpose

theorem VectorMatroid.indepCols_empty {α R : Type} [Semiring R] (M : VectorMatroid α R) : M.IndepCols ∅

Empty set is independent.

theorem VectorMatroid.indepCols_subset {α R : Type} [Semiring R] (M : VectorMatroid α R) (I J : Set α) (hMJ : M.IndepCols J) (hIJ : I ⊆ J) : M.IndepCols I

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

theorem VectorMatroid.indepCols_aug {α R : Type} [Semiring R] (M : VectorMatroid α R) (I J : Set α) (hMI : M.IndepCols I) (hMI' : ¬Maximal M.IndepCols I) (hMJ : Maximal M.IndepCols J) : ∃ x ∈ J \ I, M.IndepCols (x ᕃ I)

A non-maximal linearly independent set of columns can be augmented with another linearly independent column.

theorem VectorMatroid.indepCols_maximal {α R : Type} [Semiring R] (M : VectorMatroid α R) (I : Set α) : Matroid.ExistsMaximalSubsetProperty M.IndepCols I

Every set of columns contains a maximal independent subset of columns.

def VectorMatroid.toIndepMatroid {α R : Type} [Semiring R] (M : VectorMatroid α R) : IndepMatroid α

VectorMatroid expressed as IndepMatroid.

Equations

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

def VectorMatroid.toMatroid {α R : Type} [Semiring R] (M : VectorMatroid α R) : Matroid α

VectorMatroid converted to Matroid.

Equations

• M.toMatroid = M.toIndepMatroid.matroid

@[simp]

theorem VectorMatroid.toMatroid_E {α R : Type} [Semiring R] (M : VectorMatroid α R) : M.toMatroid.E = M.Y

@[simp]

theorem VectorMatroid.toMatroid_indep {α R : Type} [Semiring R] (M : VectorMatroid α R) : M.toMatroid.Indep = M.IndepCols