Standard Representation

Here we study the standard representation of vector matroids.

Definition and API

structure StandardRepr (α : Type u_1) (R : Type u_2) [DecidableEq α] : Type (max u_1 u_2)

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.toFull {α : Type u_1} [DecidableEq α] {R : Type u_2} [Zero R] [One R] (S : StandardRepr α R) : Matrix (↑S.X) (↑(S.X ∪ S.Y)) R

Convert standard representation of a vector matroid to a full representation.

Equations

• S.toFull x✝ = (1 ◫ S.B) x✝ ∘ Subtype.toSum

theorem StandardRepr.ext {α : Type u_1} {R : Type u_2} {inst✝ : DecidableEq α} {x y : StandardRepr α R} (X : x.X = y.X) (Y : x.Y = y.Y) (B : HEq x.B y.B) (decmemX : HEq x.decmemX y.decmemX) (decmemY : HEq x.decmemY y.decmemY) : x = y

theorem standardRepr_eq_standardRepr_of_B_eq_B {α : Type u_1} [DecidableEq α] {R : Type u_2} [DivisionRing R] {S₁ S₂ : StandardRepr α R} (hX : S₁.X = S₂.X) (hY : S₁.Y = S₂.Y) (hB : S₁.B = ⋯ ▸ ⋯ ▸ S₂.B) : S₁ = S₂

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

Construct a matroid from a standard representation.

Equations

• S.toMatroid = S.toFull.toMatroid

@[simp]

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

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

theorem StandardRepr.toMatroid_indep_iff {α : Type u_1} [DecidableEq α] {R : Type u_2} [DivisionRing R] (S : StandardRepr α R) (I : Set α) : S.toMatroid.Indep I ↔ I ⊆ S.X ∪ S.Y ∧ LinearIndepOn R (Matrix.transpose fun (x : ↑S.X) => (1 ◫ S.B) x ∘ Subtype.toSum) (Subtype.val ⁻¹' I)

@[simp]

theorem StandardRepr.toMatroid_indep_iff_elem {α : Type u_1} [DecidableEq α] {R : Type u_2} [DivisionRing R] (S : StandardRepr α R) (I : Set α) : S.toMatroid.Indep I ↔ ∃ (hI : I ⊆ S.X ∪ S.Y), LinearIndepOn R ((1 ◫ S.B).transpose ∘ Subtype.toSum) hI.elem.range

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

theorem StandardRepr.toMatroid_indep_X {α : Type u_1} [DecidableEq α] {R : Type u_2} [DivisionRing R] (S : StandardRepr α R) : S.toMatroid.Indep S.X

The set of all rows of a standard representation is an independent set in the resulting matroid.

theorem StandardRepr.toMatroid_isBase_X {α : Type u_1} [DecidableEq α] {R : Type u_2} [Field R] (S : StandardRepr α R) [Fintype ↑S.X] : S.toMatroid.IsBase S.X

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

theorem StandardRepr.finite_X_of_toMatroid_rankFinite {α : Type u_1} [DecidableEq α] {R : Type u_2} [DivisionRing R] (S : StandardRepr α R) (hS : S.toMatroid.RankFinite) : Finite ↑S.X

theorem StandardRepr.toMatroid_rankFinite_of_finite_X {α : Type u_1} [DecidableEq α] {R : Type u_2} [Field R] (S : StandardRepr α R) [Fintype ↑S.X] : S.toMatroid.RankFinite

theorem StandardRepr.toMatroid_rankFinite_iff_finite_X {α : Type u_1} [DecidableEq α] {R : Type u_2} [Field R] (S : StandardRepr α R) : S.toMatroid.RankFinite ↔ Finite ↑S.X

Guaranteeing that a standard representation of desired properties exists

theorem Matrix.longTableauPivot_toMatroid {α : Type u_1} [DecidableEq α] {R : Type u_2} [Field R] {X Y : Set α} (A : Matrix (↑X) (↑Y) R) {x : ↑X} {y : ↑Y} (hAxy : A x y ≠ 0) : (A.longTableauPivot x y).toMatroid = A.toMatroid

theorem Matrix.exists_standardRepr_isBase {α : Type u_1} [DecidableEq α] {R : Type u_2} [DivisionRing R] {X Y G : Set α} (A : Matrix (↑X) (↑Y) R) (hAG : A.toMatroid.IsBase G) : ∃ (S : StandardRepr α R), S.X = G ∧ S.toMatroid = A.toMatroid

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

theorem Matrix.exists_standardRepr {α : Type u_1} [DecidableEq α] {R : Type u_2} [DivisionRing R] {X Y : Set α} (A : Matrix (↑X) (↑Y) R) : ∃ (S : StandardRepr α R), S.toMatroid = A.toMatroid

Every vector matroid has a standard representation.

theorem Matrix.exists_standardRepr_isBase_isTotallyUnimodular {α : Type u_1} [DecidableEq α] {R : Type u_2} [Field R] {X Y G : Set α} [Fintype ↑G] (A : Matrix (↑X) (↑Y) R) (hAG : A.toMatroid.IsBase G) (hA : A.IsTotallyUnimodular) : ∃ (S : StandardRepr α R), S.X = G ∧ S.toMatroid = A.toMatroid ∧ S.B.IsTotallyUnimodular

Every vector matroid whose full representation matrix is totally unimodular has a standard representation whose rows are a given base and the standard representation matrix is totally unimodular. Unlike Matrix.exists_standardRepr_isBase this lemma does not allow infinite G and does not allow R to have noncommutative multiplication.

Conditional uniqueness of standard representation

theorem ext_standardRepr_of_same_matroid_same_X {α : Type u_1} [DecidableEq α] {S₁ S₂ : StandardRepr α Z2} [Fintype ↑S₁.X] (hSS : S₁.toMatroid = S₂.toMatroid) (hXX : S₁.X = S₂.X) : S₁ = S₂

If two standard representations of the same binary matroid have the same base, they are identical.

theorem support_eq_support_of_same_matroid_same_X {F₁ : Type u₁} {F₂ : Type u₂} {α : Type (max u₁ u₂ v)} [DecidableEq α] [DecidableEq F₁] [DecidableEq F₂] [Field F₁] [Field F₂] {S₁ : StandardRepr α F₁} {S₂ : StandardRepr α F₂} [Fintype ↑S₂.X] (hSS : S₁.toMatroid = S₂.toMatroid) (hXX : S₁.X = S₂.X) : let hYY := ⋯; hXX ▸ hYY ▸ S₁.B.support = S₂.B.support

If two standard representations of the same matroid have the same base, then the standard representation matrices have the same support.