Standard Representation

Here we study the standard representation of vector matroids.

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.

theorem Matroid.IsBase.not_ssubset_indep {α : Type} {M : Matroid α} {G I : Set α} (hMG : M.IsBase G) (hMH : M.Indep I) : ¬G ⊂ I

@[reducible, inline]

abbrev Equiv.leftCongr {α ι₁ ι₂ : Type} (e : ι₁ ≃ ι₂) : ι₁ ⊕ α ≃ ι₂ ⊕ α

Equations

• e.leftCongr = e.sumCongr (Equiv.refl α)

def StandardRepr.toFull {α : Type} [DecidableEq α] {R : Type} [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.toFull_indep_iff {α : Type} [DecidableEq α] {R : Type} [DivisionRing R] (S : StandardRepr α R) (I : Set α) : S.toFull.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)

theorem StandardRepr.toFull_indep_iff_elem {α : Type} [DecidableEq α] {R : Type} [DivisionRing R] (S : StandardRepr α R) (I : Set α) : S.toFull.toMatroid.Indep I ↔ ∃ (hI : I ⊆ S.X ∪ S.Y), LinearIndepOn R (Matrix.transpose fun (x : ↑S.X) => (1 ◫ S.B) x ∘ Subtype.toSum) hI.elem.range

theorem StandardRepr.ext {α R : Type} {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} [DecidableEq α] {R : Type} [DivisionRing R] {S₁ S₂ : StandardRepr α R} (hX : S₁.X = S₂.X) (hY : S₁.Y = S₂.Y) (hB : S₁.B = ⋯ ▸ ⋯ ▸ S₂.B) : S₁ = S₂

Kinda extensionality on StandardRepr but @[ext] cannot be here.

def StandardRepr.toMatroid {α : Type} [DecidableEq α] {R : Type} [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} [DecidableEq α] {R : Type} [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} [DecidableEq α] {R : Type} [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)

theorem StandardRepr.toMatroid_indep_iff_elem {α : Type} [DecidableEq α] {R : Type} [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} [DecidableEq α] {R : Type} [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

@[simp]

theorem StandardRepr.toMatroid_indep {α : Type} [DecidableEq α] {R : Type} [DivisionRing R] (S : StandardRepr α R) : S.toMatroid.Indep = fun (x : Set α) => ∃ (hI : x ⊆ S.X ∪ S.Y), LinearIndepOn R ((1 ◫ S.B).transpose ∘ Subtype.toSum) hI.elem.range

theorem Matrix.longTableauPivot_toMatroid {α : Type} [DecidableEq α] {R : Type} [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_isTotallyUnimodular {α : Type} [DecidableEq α] {R : Type} [Field R] {G : Set α} [Fintype ↑G] {X Y : Set α} (V : Matrix (↑X) (↑Y) R) (hVG : V.toMatroid.IsBase G) (hVA : V.IsTotallyUnimodular) : ∃ (S : StandardRepr α R), S.X = G ∧ S.toMatroid = V.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.

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

The identity matrix has linearly independent rows.

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

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

theorem ext_standardRepr_of_same_matroid_same_X {α : Type} [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 {α : Type} [DecidableEq α] {F₁ F₂ : Type} [Field F₁] [Field F₂] [DecidableEq F₁] [DecidableEq 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.