@[reducible, inline]

abbrev Matrix_1sumComposition {α β : Type} [Zero β] {X₁ Y₁ X₂ Y₂ : Set α} (A₁ : Matrix (↑X₁) (↑Y₁) β) (A₂ : Matrix (↑X₂) (↑Y₂) β) : Matrix (↑X₁ ⊕ ↑X₂) (↑Y₁ ⊕ ↑Y₂) β

Matrix-level 1-sum for matroids defined by their standard representation matrices.

Equations

• Matrix_1sumComposition A₁ A₂ = Matrix.fromBlocks A₁ 0 0 A₂

def StandardRepr_1sumComposition {α : Type} [DecidableEq α] {S₁ S₂ : StandardRepr α Z2} (hXY : S₁.X ⫗ S₂.Y) (hYX : S₁.Y ⫗ S₂.X) : StandardRepr α Z2 × Prop

StandardRepr-level 1-sum of two matroids. It checks that everything is disjoint (returned as .snd of the output).

Equations

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

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

Matroid M is a result of 1-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₂
• hXY : self.S₁.X ⫗ self.S₂.Y
• hYX : self.S₁.Y ⫗ self.S₂.X
• IsSum : (StandardRepr_1sumComposition ⋯ ⋯).1 = self.S
• IsValid : (StandardRepr_1sumComposition ⋯ ⋯).2

theorem StandardRepr_1sumComposition_as_disjointSum {α : Type} [DecidableEq α] {S₁ S₂ : StandardRepr α Z2} {hXY : S₁.X ⫗ S₂.Y} {hYX : S₁.Y ⫗ S₂.X} (valid : (StandardRepr_1sumComposition hXY hYX).2) : (StandardRepr_1sumComposition hXY hYX).1.toMatroid = S₁.toMatroid.disjointSum S₂.toMatroid ⋯

Matroid constructed from a valid 1-sum of binary matroids is the same as disjoint sum of matroids constructed from them.

theorem StandardRepr_1sumComposition_comm {α : Type} [DecidableEq α] {S₁ S₂ : StandardRepr α Z2} {hXY : S₁.X ⫗ S₂.Y} {hYX : S₁.Y ⫗ S₂.X} (valid : (StandardRepr_1sumComposition hXY hYX).2) : (StandardRepr_1sumComposition hXY hYX).1.toMatroid = (StandardRepr_1sumComposition ⋯ ⋯).1.toMatroid

A valid 1-sum of binary matroids is commutative.

theorem StandardRepr_1sumComposition_hasTuSigning {α : Type} [DecidableEq α] {S₁ S₂ : StandardRepr α Z2} (hXY : S₁.X ⫗ S₂.Y) (hYX : S₁.Y ⫗ S₂.X) (hS₁ : S₁.HasTuSigning) (hS₂ : S₂.HasTuSigning) : (StandardRepr_1sumComposition hXY hYX).1.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 the first of the three parts of the easy direction of the Seymour's theorem.