This file contains everything about 2-sum of binary matroids.

@[reducible, inline]

abbrev Matrix_2sumComposition {α : Type u_1} {β : Type u_2} [Semiring β] {X₁ : Set α} {Y₁ : Set α} {X₂ : Set α} {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 StandardRepresentation_2sum {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {a : α} (ha : M₁.X ∩ M₂.Y = {a}) (hXY : M₂.X ⫗ M₁.Y) : StandardRepresentation α × 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.

def StandardRepresentation.Is2sumOf {α : Type u_1} [DecidableEq α] (M : StandardRepresentation α) (M₁ : StandardRepresentation α) (M₂ : StandardRepresentation α) : Prop

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

Equations

• M.Is2sumOf M₁ M₂ = ∃ (a : α) (ha : M₁.X ∩ M₂.Y = {a}) (hXY : M₂.X ⫗ M₁.Y), let M₀ := StandardRepresentation_2sum ha hXY; M.toMatroid = M₀.1.toMatroid ∧ M₀.2

theorem StandardRepresentation.Is2sumOf.disjoXX {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is2sumOf M₁ M₂) : M₁.X ⫗ M₂.X

theorem StandardRepresentation.Is2sumOf.disjoYY {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is2sumOf M₁ M₂) : M₁.Y ⫗ M₂.Y

theorem StandardRepresentation.Is2sumOf.interXY {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is2sumOf M₁ M₂) : ∃ (a : α), M₁.X ∩ M₂.Y = {a}

theorem StandardRepresentation.Is2sumOf.disjoYX {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is2sumOf M₁ M₂) : M₁.Y ⫗ M₂.X

theorem StandardRepresentation.Is2sumOf.indep {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is2sumOf M₁ M₂) : ∃ (a : α) (ha : M₁.X ∩ M₂.Y = {a}), let A₁ := M₁.B ∘ ⋯.elem; let A₂ := fun (x : ↑M₂.X) => M₂.B x ∘ ⋯.elem; let x := M₁.B ⟨a, ⋯⟩; let y := fun (x : ↑M₂.X) => M₂.B x ⟨a, ⋯⟩; (Matrix_2sumComposition A₁ x A₂ y).toMatrixUnionUnion.IndepCols = M.toMatroid.Indep

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

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

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

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

theorem StandardRepresentation_2sum_isRegular {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {a : α} (ha : M₁.X ∩ M₂.Y = {a}) (hXY : M₂.X ⫗ M₁.Y) (hM₁ : M₁.IsRegular) (hM₂ : M₂.IsRegular) : (StandardRepresentation_2sum ha hXY).1.IsRegular

theorem StandardRepresentation_2sum_isRegular_left {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {a : α} (ha : M₁.X ∩ M₂.Y = {a}) (hXY : M₂.X ⫗ M₁.Y) (hM : (StandardRepresentation_2sum ha hXY).1.IsRegular) : M₁.IsRegular

theorem StandardRepresentation_2sum_isRegular_right {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {a : α} (ha : M₁.X ∩ M₂.Y = {a}) (hXY : M₂.X ⫗ M₁.Y) (hM : (StandardRepresentation_2sum ha hXY).1.IsRegular) : M₂.IsRegular

theorem StandardRepresentation.Is2sumOf.isRegular {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} [Fintype ↑M₁.X] [Fintype ↑M₁.Y] [Fintype ↑M₂.X] [Fintype ↑M₂.Y] (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.

theorem StandardRepresentation.Is2sumOf.isRegular_left {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hMsum : M.Is2sumOf M₁ M₂) (hMreg : M.IsRegular) : M₁.IsRegular

If a regular matroid is a 2-sum, then the left summand of the 2-sum is regular.

theorem StandardRepresentation.Is2sumOf.isRegular_right {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hMsum : M.Is2sumOf M₁ M₂) (hMreg : M.IsRegular) : M₂.IsRegular

If a regular matroid is a 2-sum, then the right summand of the 2-sum is regular.