@[reducible, inline]

abbrev Matrix_2sumComposition {α β : Type} [Semiring β] {X₁ Y₁ X₂ Y₂ : Set α} (A₁ : Matrix (↑X₁) (↑Y₁) β) (x : ↑Y₁ → β) (A₂ : Matrix (↑X₂) (↑Y₂) β) (y : ↑X₂ → β) : Matrix (↑X₁ ⊕ ↑X₂) (↑Y₁ ⊕ ↑Y₂) β

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

Equations

• Matrix_2sumComposition A₁ x A₂ y = Matrix.fromBlocks A₁ 0 (fun (i : ↑X₂) (j : ↑Y₁) => y i * x j) A₂

def StandardRepr_2sum {α : Type} [DecidableEq α] {a : α} {S₁ S₂ : StandardRepr α Z2} (ha : S₁.X ∩ S₂.Y = {a}) (hXY : S₂.X ⫗ S₁.Y) : StandardRepr α Z2 × Prop

StandardRepresentation-level 2-sum of two matroids. The second part checks legitimacy: the ground sets of M₁ and M₂ are disjoint except for the element a ∈ M₁.X ∩ M₂.Y, and the bottom-most row of M₁ and the left-most column of M₂ are each nonzero vectors.

Equations

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

structure Matroid.Is2sumOf {α : Type} [DecidableEq α] (M M₁ M₂ : Matroid α) : Type

Binary matroid M is a result of 2-summing M₁ and M₂ in some way.

• S : StandardRepr α Z2
• S₁ : StandardRepr α Z2
• S₂ : StandardRepr α Z2
• hM : self.S.toMatroid = M
• hM₁ : self.S₁.toMatroid = M₁
• hM₂ : self.S₂.toMatroid = M₂
• a : α
• ha : self.S₁.X ∩ self.S₂.Y = {self.a}
• hXY : self.S₂.X ⫗ self.S₁.Y
• IsSum : (StandardRepr_2sum ⋯ ⋯).1 = self.S
• IsValid : (StandardRepr_2sum ⋯ ⋯).2

theorem Matrix_2sumComposition_isTotallyUnimodular {α : Type} [DecidableEq α] {X₁ Y₁ X₂ Y₂ : Set α} {A₁ : Matrix ↑X₁ ↑Y₁ ℚ} {A₂ : Matrix ↑X₂ ↑Y₂ ℚ} (hA₁ : A₁.IsTotallyUnimodular) (hA₂ : A₂.IsTotallyUnimodular) (x : ↑Y₁ → ℚ) (y : ↑X₂ → ℚ) : (Matrix_2sumComposition A₁ x A₂ y).IsTotallyUnimodular

theorem StandardRepr_2sum_B {α : Type} [DecidableEq α] {S₁ S₂ : StandardRepr α Z2} {a : α} (ha : S₁.X ∩ S₂.Y = {a}) (hXY : S₂.X ⫗ S₁.Y) : ∃ (haX₁ : a ∈ S₁.X) (haY₂ : a ∈ S₂.Y), (StandardRepr_2sum ha hXY).1.B = (Matrix_2sumComposition (S₁.B ∘ ⋯.elem) (S₁.B ⟨a, haX₁⟩) (fun (x : ↑S₂.X) => S₂.B x ∘ ⋯.elem) fun (x : ↑S₂.X) => S₂.B x ⟨a, haY₂⟩).toMatrixUnionUnion

theorem StandardRepr_2sum_hasTuSigning {α : Type} [DecidableEq α] {S₁ S₂ : StandardRepr α Z2} {a : α} (ha : S₁.X ∩ S₂.Y = {a}) (hXY : S₂.X ⫗ S₁.Y) (hS₁ : S₁.HasTuSigning) (hS₂ : S₂.HasTuSigning) : (StandardRepr_2sum ha hXY).1.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 the middle of the three parts of the easy direction of the Seymour's theorem.