Matroid 2-sum #
Here we study the 2-sum of matroids (starting with the 2-sum of matrices).
Shorthands for convenience #
All declarations in this section are private.
Definition #
def
matrixSum2
{R : Type u_1}
[Semiring R]
{Xₗ : Type u_2}
{Yₗ : Type u_3}
{Xᵣ : Type u_4}
{Yᵣ : Type u_5}
(Aₗ : Matrix Xₗ Yₗ R)
(r : Yₗ → R)
(Aᵣ : Matrix Xᵣ Yᵣ R)
(c : Xᵣ → 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 (c ⊗ r) Aᵣ
Instances For
noncomputable def
standardReprSum2
{α : Type u_1}
[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.
Instances For
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.
Instances For
Specifics about pivoting for the proof of 2-sum regularity #
All declarations in this section are private.
Total unimodularity after adjoining an outer product #
All declarations in this section are private.
Proof of regularity of the 2-sum #
theorem
standardReprSum2_hasTuSigning
{α : Type u_1}
[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)
:
theorem
Matroid.IsSum2of.isRegular
{α : Type u_1}
[DecidableEq α]
{M Mₗ Mᵣ : Matroid α}
(hMMM : M.IsSum2of Mₗ Mᵣ)
(hM : M.RankFinite)
(hMₗ : Mₗ.IsRegular)
(hMᵣ : 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.