Matroid 1-sum

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

@[reducible, inline]

abbrev matrixSum1 {R : Type} [Zero R] {Xₗ Yₗ Xᵣ Yᵣ : Type} (Aₗ : Matrix Xₗ Yₗ R) (Aᵣ : Matrix Xᵣ Yᵣ R) : Matrix (Xₗ ⊕ Xᵣ) (Yₗ ⊕ Yᵣ) R

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

Equations

• matrixSum1 Aₗ Aᵣ = ⊞ Aₗ 0 0 Aᵣ

noncomputable def standardReprSum1 {α : Type} [DecidableEq α] {Sₗ Sᵣ : StandardRepr α Z2} (hXY : Sₗ.X ⫗ Sᵣ.Y) (hYX : Sₗ.Y ⫗ Sᵣ.X) : Option (StandardRepr α Z2)

StandardRepr-level 1-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.Is1sumOf {α : Type} [DecidableEq α] (M Mₗ Mᵣ : Matroid α) : Prop

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

Equations

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

theorem standardReprSum1_X {α : Type} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) : S.X = Sₗ.X ∪ Sᵣ.X

theorem standardReprSum1_Y {α : Type} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum1 hXY hYX = some S) : S.Y = Sₗ.Y ∪ Sᵣ.Y

theorem standardReprSum1_hasTuSigning {α : Type} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hSₗ : Sₗ.B.HasTuSigning) (hSᵣ : Sᵣ.B.HasTuSigning) (hS : standardReprSum1 hXY hYX = some S) : S.B.HasTuSigning

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

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