Vector Matroids

Here we study vector matroids with emphasis on binary matroids.

def Matrix.IndepCols {α R : Type} {X Y : Set α} [Semiring R] (A : Matrix (↑X) (↑Y) R) (I : Set α) : Prop

A set is independent in a vector matroid iff it corresponds to a linearly independent submultiset of columns.

Equations

• A.IndepCols I = (I ⊆ Y ∧ LinearIndepOn R A.transpose (Subtype.val ⁻¹' I))

theorem Matrix.indepCols_iff_elem {α R : Type} {X Y : Set α} [Semiring R] (A : Matrix (↑X) (↑Y) R) (I : Set α) : A.IndepCols I ↔ ∃ (hI : I ⊆ Y), LinearIndepOn R A.transpose hI.elem.range

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

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

theorem Matrix.indepCols_empty {α R : Type} {X Y : Set α} [Semiring R] (A : Matrix (↑X) (↑Y) R) : A.IndepCols ∅

Empty set is independent.

theorem Matrix.indepCols_subset {α R : Type} {X Y : Set α} [Semiring R] (A : Matrix (↑X) (↑Y) R) (I J : Set α) (hAJ : A.IndepCols J) (hIJ : I ⊆ J) : A.IndepCols I

A subset of an independent set of columns is independent.

theorem Matrix.indepCols_aug {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) (I J : Set α) (hAI : A.IndepCols I) (hAI' : ¬Maximal A.IndepCols I) (hAJ : Maximal A.IndepCols J) : ∃ x ∈ J \ I, A.IndepCols (x ᕃ I)

A non-maximal independent set of columns can be augmented with another independent column. To see why DivisionRing is necessary, consider (!![0, 1, 2, 3; 1, 0, 3, 2] : Matrix (Fin 2) (Fin 4) (ZMod 6)) as a counterexample. The set {0} is nonmaximal independent. The set {2, 3} is maximal independent. However, neither of the sets {0, 2} or {0, 3} is independent.

theorem linearIndepOn_sUnion_of_directedOn {α R : Type} {X Y : Set α} [Semiring R] {A : Matrix (↑Y) (↑X) R} {s : Set (Set α)} (hs : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (hA : ∀ a ∈ s, LinearIndepOn R A (Subtype.val ⁻¹' a)) : LinearIndepOn R A (Subtype.val ⁻¹' ⋃₀ s)

theorem Matrix.indepCols_maximal {α R : Type} {X Y : Set α} [Semiring R] (A : Matrix (↑X) (↑Y) R) (I : Set α) : Matroid.ExistsMaximalSubsetProperty A.IndepCols I

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

def Matrix.toIndepMatroid {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) : IndepMatroid α

Matrix (interpreted as a full representation) converted to IndepMatroid.

Equations

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

def Matrix.toMatroid {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) : Matroid α

Matrix (interpreted as a full representation) converted to Matroid.

Equations

• A.toMatroid = A.toIndepMatroid.matroid

@[simp]

theorem Matrix.toMatroid_E {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) : A.toMatroid.E = Y

theorem Matrix.toMatroid_indep {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) : A.toMatroid.Indep = A.IndepCols

theorem Matrix.toMatroid_indep_iff {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) (I : Set α) : A.toMatroid.Indep I ↔ I ⊆ Y ∧ LinearIndepOn R A.transpose (Subtype.val ⁻¹' I)

@[simp]

theorem Matrix.toMatroid_indep_iff_elem {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) (I : Set α) : A.toMatroid.Indep I ↔ ∃ (hI : I ⊆ Y), LinearIndepOn R A.transpose hI.elem.range

theorem Matrix.toMatroid_indep_iff_submatrix {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) (I : Set α) : A.toMatroid.Indep I ↔ ∃ (hI : I ⊆ Y), LinearIndependent (ι := ↑I) R (A.transpose.submatrix hI.elem id)

theorem Matrix.fromRows_zero_reindex_toMatroid {α R : Type} {X Y : Set α} [DivisionRing R] {G : Set α} [Fintype ↑G] [(a : α) → Decidable (a ∈ G)] [(a : α) → Decidable (a ∈ Y)] (A : Matrix (↑G) (↑G ⊕ ↑(Y \ G)) R) (hGY : G ⊆ Y) {Z : Type} (e : ↑G ⊕ Z ≃ ↑X) : (of fun (i : ↑G) => A i ∘ Subtype.toSum).toMatroid = (of ((reindex e hGY.equiv) (A ⊟ 0))).toMatroid

theorem Matrix.toMatroid_isFinitary {α R : Type} {X Y : Set α} [DivisionRing R] (A : Matrix (↑X) (↑Y) R) : A.toMatroid.Finitary

Every vector matroid is finitary.