Matroid 3-sum

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

Matrix-level 3-sum

Additional notation for convenience

We define the unsigned and the signed version of the special cases of the 3×3 submatrix in the intersection of the summands.

Definition

structure MatrixSum3 (Xₗ : Type u_1) (Yₗ : Type u_2) (Xᵣ : Type u_3) (Yᵣ : Type u_4) (R : Type u_5) : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

Structural data of 3-sum of matrices.

• Aₗ : Matrix (Xₗ ⊕ Unit) (Yₗ ⊕ Fin 2) R
• Dₗ : Matrix (Fin 2) Yₗ R
• D₀ₗ : Matrix (Fin 2) (Fin 2) R
• D₀ᵣ : Matrix (Fin 2) (Fin 2) R
• Dᵣ : Matrix Xᵣ (Fin 2) R
• Aᵣ : Matrix (Fin 2 ⊕ Xᵣ) (Unit ⊕ Yᵣ) R

@[reducible, inline]

noncomputable abbrev MatrixSum3.D {Xₗ : Type u_1} {Yₗ : Type u_2} {Xᵣ : Type u_3} {Yᵣ : Type u_4} {R : Type u_5} [CommRing R] (S : MatrixSum3 Xₗ Yₗ Xᵣ Yᵣ R) : Matrix (Fin 2 ⊕ Xᵣ) (Yₗ ⊕ Fin 2) R

The bottom-left block of 3-sum.

Equations

• S.D = ⊞ S.Dₗ S.D₀ₗ (S.Dᵣ * S.D₀ₗ⁻¹ * S.Dₗ) S.Dᵣ

noncomputable def MatrixSum3.matrix {Xₗ : Type u_1} {Yₗ : Type u_2} {Xᵣ : Type u_3} {Yᵣ : Type u_4} {R : Type u_5} [CommRing R] (S : MatrixSum3 Xₗ Yₗ Xᵣ Yᵣ R) : Matrix ((Xₗ ⊕ Unit) ⊕ Fin 2 ⊕ Xᵣ) ((Yₗ ⊕ Fin 2) ⊕ Unit ⊕ Yᵣ) R

The resulting matrix of 3-sum.

Equations

• S.matrix = ⊞ S.Aₗ 0 S.D S.Aᵣ

Conversion of summands

def blocksToMatrixSum3 {Xₗ : Type u_1} {Yₗ : Type u_2} {Xᵣ : Type u_3} {Yᵣ : Type u_4} {R : Type u_5} (Bₗ : Matrix ((Xₗ ⊕ Unit) ⊕ Fin 2) ((Yₗ ⊕ Fin 2) ⊕ Unit) R) (Bᵣ : Matrix (Unit ⊕ Fin 2 ⊕ Xᵣ) (Fin 2 ⊕ Unit ⊕ Yᵣ) R) : MatrixSum3 Xₗ Yₗ Xᵣ Yᵣ R

Constructs 3-sum from summands in block form.

Equations

• blocksToMatrixSum3 Bₗ Bᵣ = { Aₗ := Bₗ.toBlocks₁₁, Dₗ := Bₗ.toBlocks₂₁.toCols₁, D₀ₗ := Bₗ.toBlocks₂₁.toCols₂, D₀ᵣ := Bᵣ.toBlocks₂₁.toRows₁, Dᵣ := Bᵣ.toBlocks₂₁.toRows₂, Aᵣ := Bᵣ.toBlocks₂₂ }

Canonical signing of matrices

Definition

All declarations in this section are private.

General results

All declarations in this section are private.

Definition of re-signing in two special cases

All declarations in this section are private.

Lemmas about distinctness of row and column indices

All declarations in this section are private.

Canonical signing of 3-sum of matrices

Additional notation for special rows and columns and their properties

@[reducible, inline]

abbrev Function.IsParallelTo₃ {X : Type u_1} {R : Type u_2} [Zero R] [Neg R] (v c₀ c₁ c₂ : X → R) : Prop

Property of a vector to be in {0, c₀, -c₀, c₁, -c₁, c₂, -c₂}.

Equations

• Function.IsParallelTo₃ v c₀ c₁ c₂ = (v = 0 ∨ v = c₀ ∨ v = -c₀ ∨ v = c₁ ∨ v = -c₁ ∨ v = c₂ ∨ v = -c₂)

Auxiliary definitions

All declarations in this section are private.

Soundness of definitions

In this section we prove that MatrixSum3.HasCanonicalSigning.toCanonicalSigning satisfies IsCanonicalSigning.

Lemmas about extending bottom-right block with special columns and top-left block with special rows

All declarations in this section are private.

Properties of canonical signings of 3-sums

All declarations in this section are private.

Correctness

In this section we prove that MatrixSum3.HasCanonicalSigning.toCanonicalSigning is indeed a signing of the original 3-sum.

Family of 3-sum-like matrices

Definition

structure MatrixLikeSum3 (Xₗ : Type u_1) (Yₗ : Type u_2) (Xᵣ : Type u_3) (Yᵣ : Type u_4) (c₀ c₁ : Fin 2 ⊕ Xᵣ → ℚ) : Type (max (max (max u_1 u_2) u_3) u_4)

Structural data of 3-sum-like matrices.

• Aₗ : Matrix Xₗ Yₗ ℚ
• D : Matrix (Fin 2 ⊕ Xᵣ) Yₗ ℚ
• Aᵣ : Matrix (Fin 2 ⊕ Xᵣ) Yᵣ ℚ
• LeftTU : (self.Aₗ ⊟ self.D).IsTotallyUnimodular
• Parallels (j : Yₗ) : Function.IsParallelTo₃ (fun (x : Fin 2 ⊕ Xᵣ) => self.D x j) c₀ c₁ (c₀ - c₁)
• BottomTU : (▮c₀ ◫ ▮c₁ ◫ ▮(c₀ - c₁) ◫ self.Aᵣ).IsTotallyUnimodular
• AuxTU : (⊞ self.Aₗ 0 self.D.toRows₁ (▮![1, 1])).IsTotallyUnimodular
• Col₀ : c₀ ◩0 = 1 ∧ c₀ ◩1 = 0
• Col₁ : c₁ ◩0 = 0 ∧ c₁ ◩1 = -1 ∨ c₁ ◩0 = 1 ∧ c₁ ◩1 = 1

Pivoting

Auxiliary results about multiplying columns of the left block by 0, ±1 factors .

Total unimodularity

All declarations in this section are private.

Implications for canonical signing of 3-sum of matrices

In this section we prove that 3-sums of matrices belong to the family of 3-sum-like matrices.

Matroid-level 3-sum

Additional notation for convenience

All declarations in this section are private.

Removing bundled elements from sets

@[reducible, inline]

abbrev Set.drop1 {α : Type u_1} (Z : Set α) (z₀ : ↑Z) : Set α

Remove one bundled element from a set.

Equations

• Z.drop1 z₀ = Z \ {↑z₀}

@[reducible, inline]

abbrev Set.drop2 {α : Type u_1} (Z : Set α) (z₀ z₁ : ↑Z) : Set α

Remove two bundled elements from a set.

Equations

• Z.drop2 z₀ z₁ = Z \ (↑z₀ ᕃ {↑z₁})

@[reducible, inline]

abbrev Set.drop3 {α : Type u_1} (Z : Set α) (z₀ z₁ z₂ : ↑Z) : Set α

Remove three bundled elements from a set.

Equations

• Z.drop3 z₀ z₁ z₂ = Z \ (↑z₀ ᕃ ↑z₁ ᕃ {↑z₂})

def undrop3 {α : Type u_1} {Z : Set α} {z₀ z₁ z₂ : ↑Z} (i : ↑(Z.drop3 z₀ z₁ z₂)) : ↑Z

Equations

• undrop3 i = ⟨↑i, ⋯⟩

Membership in drop-sets

All declarations in this section are private.

Re-typing elements of the triplet intersection

All declarations in this section are private.

Conversion from union form to block form and vice versa

def Matrix.toBlockSummandₗ {α : Type u_1} {Xₗ Yₗ : Set α} {R : Type u_2} (Bₗ : Matrix (↑Xₗ) (↑Yₗ) R) (x₀ x₁ x₂ : ↑Xₗ) (y₀ y₁ y₂ : ↑Yₗ) : Matrix ((↑(Xₗ.drop3 x₀ x₁ x₂) ⊕ Unit) ⊕ Fin 2) ((↑(Yₗ.drop3 y₀ y₁ y₂) ⊕ Fin 2) ⊕ Unit) R

Equations

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

def Matrix.toBlockSummandᵣ {α : Type u_1} {Xᵣ Yᵣ : Set α} {R : Type u_2} (Bᵣ : Matrix (↑Xᵣ) (↑Yᵣ) R) (x₀ x₁ x₂ : ↑Xᵣ) (y₀ y₁ y₂ : ↑Yᵣ) : Matrix (Unit ⊕ Fin 2 ⊕ ↑(Xᵣ.drop3 x₀ x₁ x₂)) (Fin 2 ⊕ Unit ⊕ ↑(Yᵣ.drop3 y₀ y₁ y₂)) R

Equations

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

def Matrix.toMatrixDropUnionDrop {α : Type u_1} [DecidableEq α] {Xₗ Yₗ Xᵣ Yᵣ : Set α} {R : Type u_2} [(a : α) → Decidable (a ∈ Xₗ)] [(a : α) → Decidable (a ∈ Yₗ)] [(a : α) → Decidable (a ∈ Xᵣ)] [(a : α) → Decidable (a ∈ Yᵣ)] {x₀ₗ x₁ₗ x₂ₗ : ↑Xₗ} {y₀ₗ y₁ₗ y₂ₗ : ↑Yₗ} {x₀ᵣ x₁ᵣ x₂ᵣ : ↑Xᵣ} {y₀ᵣ y₁ᵣ y₂ᵣ : ↑Yᵣ} (A : Matrix ((↑(Xₗ.drop3 x₀ₗ x₁ₗ x₂ₗ) ⊕ Unit) ⊕ Fin 2 ⊕ ↑(Xᵣ.drop3 x₀ᵣ x₁ᵣ x₂ᵣ)) ((↑(Yₗ.drop3 y₀ₗ y₁ₗ y₂ₗ) ⊕ Fin 2) ⊕ Unit ⊕ ↑(Yᵣ.drop3 y₀ᵣ y₁ᵣ y₂ᵣ)) R) : Matrix (↑(Xₗ.drop2 x₀ₗ x₁ₗ ∪ Xᵣ.drop1 x₂ᵣ)) (↑(Yₗ.drop1 y₂ₗ ∪ Yᵣ.drop2 y₀ᵣ y₁ᵣ)) R

Equations

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

The 3-sum of standard representations

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

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

Equations

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

theorem standardReprSum3_X_eq {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {x₀ x₁ x₂ y₀ y₁ y₂ : α} {hXX : Sₗ.X ∩ Sᵣ.X = x₀ ᕃ x₁ ᕃ {x₂}} {hYY : Sₗ.Y ∩ Sᵣ.Y = y₀ ᕃ y₁ ᕃ {y₂}} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum3 hXX hYY hXY hYX = some S) : S.X = Sₗ.X ∪ Sᵣ.X

theorem standardReprSum3_Y_eq {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {x₀ x₁ x₂ y₀ y₁ y₂ : α} {hXX : Sₗ.X ∩ Sᵣ.X = x₀ ᕃ x₁ ᕃ {x₂}} {hYY : Sₗ.Y ∩ Sᵣ.Y = y₀ ᕃ y₁ ᕃ {y₂}} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hS : standardReprSum3 hXX hYY hXY hYX = some S) : S.Y = Sₗ.Y ∪ Sᵣ.Y

theorem standardReprSum3_hasTuSigning {α : Type u_1} [DecidableEq α] {Sₗ Sᵣ S : StandardRepr α Z2} {x₀ x₁ x₂ y₀ y₁ y₂ : α} {hXX : Sₗ.X ∩ Sᵣ.X = x₀ ᕃ x₁ ᕃ {x₂}} {hYY : Sₗ.Y ∩ Sᵣ.Y = y₀ ᕃ y₁ ᕃ {y₂}} {hXY : Sₗ.X ⫗ Sᵣ.Y} {hYX : Sₗ.Y ⫗ Sᵣ.X} (hSₗ : Sₗ.B.HasTuSigning) (hSᵣ : Sᵣ.B.HasTuSigning) (hS : standardReprSum3 hXX hYY hXY hYX = some S) : S.B.HasTuSigning

The 3-sum of matroids

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

Matroid M is a result of 3-summing Mₗ and Mᵣ in some way.

Equations

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

theorem Matroid.IsSum3of.E_eq {α : Type u_1} [DecidableEq α] (M Mₗ Mᵣ : Matroid α) (hMMM : M.IsSum3of Mₗ Mᵣ) : M.E = Mₗ.E ∪ Mᵣ.E

theorem Matroid.IsSum3of.isRegular {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum3of Mₗ Mᵣ) (hM : M.RankFinite) (hMₗ : Mₗ.IsRegular) (hMᵣ : Mᵣ.IsRegular) : M.IsRegular

Any 3-sum of two regular matroids is a regular matroid. This is the final part of the easy direction of the Seymour's theorem.