Matroid R10

This file studies the R10 matroid.

def matrixR10auxZ2 : Matrix (Fin 5) (Fin 5) Z2

Equations

• matrixR10auxZ2 = !![1, 0, 0, 1, 1; 1, 1, 0, 0, 1; 0, 1, 1, 0, 1; 0, 0, 1, 1, 1; 1, 1, 1, 1, 1]

def matrixR10auxRat : Matrix (Fin 5) (Fin 5) ℚ

Equations

• matrixR10auxRat = matrixR10auxZ2.map fun (x : Z2) => ↑(ZMod.val x)

theorem matrixR10auxRat_isTotallyUnimodular : matrixR10auxRat.IsTotallyUnimodular

def matrixR10Z2 : Matrix (↑{x : Fin 10 | ↑x < 5}) (↑{x : Fin 10 | 5 ≤ ↑x}) Z2

Equations

• matrixR10Z2 = matrixR10auxZ2.submatrix (fun (i : ↑{x : Fin 10 | ↑x < 5}) => ⟨↑↑i, ⋯⟩) fun (j : ↑{x : Fin 10 | 5 ≤ ↑x}) => ⟨↑↑j - 5, ⋯⟩

def matrixR10Rat : Matrix ↑{x : Fin 10 | ↑x < 5} ↑{x : Fin 10 | 5 ≤ ↑x} ℚ

Equations

• matrixR10Rat = matrixR10Z2.map fun (x : Z2) => ↑(ZMod.val x)

theorem matrixR10Rat_eq_coe_matrixR10auxRat : matrixR10Rat = matrixR10auxRat.submatrix (fun (i : ↑{x : Fin 10 | ↑x < 5}) => ⟨↑↑i, ⋯⟩) fun (j : ↑{x : Fin 10 | 5 ≤ ↑x}) => ⟨↑↑j - 5, ⋯⟩

def matroidR10 : StandardRepr (Fin 10) Z2

Matroid R10 (see Klaus Truemper, 9.2.13).

Equations

• matroidR10 = { X := {x : Fin 10 | ↑x < 5}, Y := {x : Fin 10 | 5 ≤ ↑x}, hXY := matroidR10.proof_1, B := matrixR10Z2, decmemX := fun (x : Fin 10) => (↑x).decLt 5, decmemY := Fin.decLe 5 }

@[simp]

theorem matroidR10_X_eq : matroidR10.X = {x : Fin 10 | ↑x < 5}

@[simp]

theorem matroidR10_Y_eq : matroidR10.Y = {x : Fin 10 | 5 ≤ ↑x}

@[simp]

theorem matroidR10_B_eq : matroidR10.B = matrixR10Z2

@[simp]

theorem matroidR10.isRegular : matroidR10.toMatroid.IsRegular