Matroid Duality

Here we study the duals of matroids given by their standard representation.

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

The dual of standard representation (transpose the matrix and flip its signs).

Equations

• S✶ = { X := S.Y, Y := S.X, hXY := ⋯, B := -S.B.transpose, decmemX := S.decmemY, decmemY := S.decmemX }

def «term_✶» : Lean.TrailingParserDescr

Equations

• «term_✶» = Lean.ParserDescr.trailingNode `«term_✶» 1024 1024 (Lean.ParserDescr.symbol "✶")

theorem StandardRepr.dual_dual {α : Type u_1} {R : Type u_2} [DecidableEq α] [DivisionRing R] (S : StandardRepr α R) : S✶✶ = S

The dual of dual is the original standard representation.

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

@[simp]

theorem StandardRepr.dual_ground {α : Type u_1} {R : Type u_2} [DecidableEq α] [DivisionRing R] (S : StandardRepr α R) : S✶.toMatroid.E = S.toMatroid.E