structure StandardRepr (α R : Type) [DecidableEq α] : Type

Standard matrix representation of a vector matroid.

• X : Set α

  Row indices.

• Y : Set α

  Col indices.

• hXY : self.X ⫗ self.Y

  Basis and nonbasis elements are disjoint

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

  Standard representation matrix.

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

  The computer can determine whether certain element is a row.

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

  The computer can determine whether certain element is a col.

def StandardRepr.toVectorMatroid {α R : Type} [DecidableEq α] [Zero R] [One R] (S : StandardRepr α R) : VectorMatroid α R

Vector matroid constructed from the standard representation.

Equations

• S.toVectorMatroid = { X := S.X, Y := S.X ∪ S.Y, A := fun (x : ↑S.X) => S.B.prependId x ∘ Subtype.toSum }

@[simp]

theorem StandardRepr.toVectorMatroid_E {α R : Type} [DecidableEq α] [Semiring R] (S : StandardRepr α R) : S.toVectorMatroid.toMatroid.E = S.X ∪ S.Y

Ground set of a vector matroid is union of row and column index sets of its standard matrix representation.

@[simp]

theorem StandardRepr.toVectorMatroid_A {α R : Type} [DecidableEq α] [Semiring R] (S : StandardRepr α R) : S.toVectorMatroid.A = fun (x : ↑S.X) => S.B.prependId x ∘ Subtype.toSum

Full representation matrix of vector matroid is [1 | B].

theorem StandardRepr.toVectorMatroid_indep_iff {α R : Type} [DecidableEq α] [Semiring R] (S : StandardRepr α R) (I : Set α) : S.toVectorMatroid.toMatroid.Indep I ↔ ∃ (hI : I ⊆ S.X ∪ S.Y), LinearIndependent R fun (i : ↑I) (x : ↑S.X) => S.B.prependId x (Subtype.toSum (hI.elem i))

Set is independent in the vector matroid iff the corresponding multiset of columns of [1 | B] is linearly independent over R.

theorem VectorMatroid.exists_standardRepr {α R : Type} [DecidableEq α] [Semiring R] (M : VectorMatroid α R) : ∃ (S : StandardRepr α R), S.toVectorMatroid = M

Every vector matroid has a standard representation.

theorem VectorMatroid.exists_standardRepr_base {α R : Type} [DecidableEq α] [Semiring R] {B : Set α} (M : VectorMatroid α R) (hMB : M.toMatroid.Base B) (hBY : B ⊆ M.Y) : ∃ (S : StandardRepr α R), M.X = B ∧ S.toVectorMatroid = M

Every vector matroid has a standard representation whose rows are a given base.

def StandardRepr.toMatroid {α R : Type} [DecidableEq α] [Semiring R] (S : StandardRepr α R) : Matroid α

Construct a matroid from standard representation.

Equations

• S.toMatroid = S.toVectorMatroid.toMatroid

@[simp]

theorem StandardRepr.toMatroid_E {α R : Type} [DecidableEq α] [Semiring R] (S : StandardRepr α R) : S.toMatroid.E = S.X ∪ S.Y

Ground set of a vector matroid is union of row and column index sets of its standard matrix representation.

@[simp]

theorem StandardRepr.toMatroid_indep_iff {α R : Type} [DecidableEq α] [Semiring R] (S : StandardRepr α R) (I : Set α) : S.toMatroid.Indep I ↔ ∃ (hI : I ⊆ S.X ∪ S.Y), LinearIndependent R fun (i : ↑I) (x : ↑S.X) => S.B.prependId x (Subtype.toSum (hI.elem i))

Set is independent in the resulting matroid iff the corresponding multiset of columns of [1 | B] is linearly independent over R.

theorem StandardRepr.toMatroid_indep_iff_submatrix {α R : Type} [DecidableEq α] [Semiring R] (S : StandardRepr α R) (I : Set α) : S.toMatroid.Indep I ↔ ∃ (hI : I ⊆ S.X ∪ S.Y), LinearIndependent (ι := ↑I) R (S.B.prependId.submatrix id (Subtype.toSum ∘ hI.elem)).transpose

theorem Matrix.one_linearIndependent {α R : Type} [DecidableEq α] [Ring R] : LinearIndependent R 1

The identity matrix has linearly independent rows.

theorem StandardRepr.toMatroid_base {α R : Type} [DecidableEq α] [Ring R] (S : StandardRepr α R) : S.toMatroid.Base (Set.range (Subtype.val ∘ Sum.toUnion ∘ Sum.inl))

The image of all rows of a standard representation is a base in the resulting matroid.