Matroid 2-sum

Here we study the 2-sum of matroids (starting with the 2-sum of matrices).

Shorthands for convenience

Definition

@[reducible, inline]

abbrev matrixSum2 {R : Type} [Semiring R] {Xₗ Yₗ Xᵣ Yᵣ : Type} (Aₗ : Matrix Xₗ Yₗ R) (r : Yₗ → R) (Aᵣ : Matrix Xᵣ Yᵣ R) (c : Xᵣ → R) : Matrix (Xₗ ⊕ Xᵣ) (Yₗ ⊕ Yᵣ) R

Matrix-level 2-sum for matroids defined by their standard representation matrices; does not check legitimacy.

Equations

• matrixSum2 Aₗ r Aᵣ c = ⊞ Aₗ 0 ((fun {X Y α : Type} [Mul α] (c : X → α) (r : Y → α) => Matrix.of fun (i : X) (j : Y) => c i * r j) c r) Aᵣ

noncomputable def standardReprSum2 {α : Type} [DecidableEq α] {Sₗ Sᵣ : StandardRepr α Z2} {x y : α} (hXX : Sₗ.X ∩ Sᵣ.X = {x}) (hYY : Sₗ.Y ∩ Sᵣ.Y = {y}) (hXY : Sₗ.X ⫗ Sᵣ.Y) (hYX : Sₗ.Y ⫗ Sᵣ.X) : Option (StandardRepr α Z2)

StandardRepr-level 2-sum of two matroids. Returns the result only if valid.

Equations

• One or more equations did not get rendered due to their size.

def Matroid.Is2sumOf {α : Type} [DecidableEq α] (M Mₗ Mᵣ : Matroid α) : Prop

Binary matroid M is a result of 2-summing Mₗ and Mᵣ in some way.

Equations

• One or more equations did not get rendered due to their size.

Specifics about pivoting for the proof of 2-sum regularity

Total unimodularity after adjoining an outer product

Proof of regularity of the 2-sum

theorem standardReprSum2_X {α : Type} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {x y : α} {hx : Sₗ.X ∩ Sᵣ.X = {x}} {hy : Sₗ.Y ∩ Sᵣ.Y = {y}} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum2 hx hy hXY hYX = some S) : S.X = Sₗ.X ∪ Sᵣ.X

theorem standardReprSum2_Y {α : Type} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {x y : α} {hx : Sₗ.X ∩ Sᵣ.X = {x}} {hy : Sₗ.Y ∩ Sᵣ.Y = {y}} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum2 hx hy hXY hYX = some S) : S.Y = Sₗ.Y ∪ Sᵣ.Y

theorem standardReprSum2_hasTuSigning {α : Type} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {x y : α} {hx : Sₗ.X ∩ Sᵣ.X = {x}} {hy : Sₗ.Y ∩ Sᵣ.Y = {y}} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hSₗ : Sₗ.B.HasTuSigning) (hSᵣ : Sᵣ.B.HasTuSigning) (hS : standardReprSum2 hx hy hXY hYX = some S) : S.B.HasTuSigning

theorem Matroid.Is2sumOf.isRegular {α : Type} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hM : M.Is2sumOf Mₗ Mᵣ) (hMₗ : Mₗ.IsRegular) (hMᵣ : Mᵣ.IsRegular) : M.IsRegular

Any 2-sum of regular matroids is a regular matroid. This is part two (of three) of the easy direction of the Seymour's theorem.