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

@[reducible, inline]

noncomputable abbrev Matrix_3sumComposition {α : Type u_1} {β : Type u_2} [CommRing β] {X₁ : Set α} {Y₁ : Set α} {X₂ : Set α} {Y₂ : Set α} (A₁ : Matrix (↑X₁) (↑Y₁ ⊕ Fin 2) β) (A₂ : Matrix (Fin 2 ⊕ ↑X₂) (↑Y₂) β) (z₁ : ↑Y₁ → β) (z₂ : ↑X₂ → β) (D : Matrix (Fin 2) (Fin 2) β) (D₁ : Matrix (Fin 2) (↑Y₁) β) (D₂ : Matrix (↑X₂) (Fin 2) β) : Matrix ((↑X₁ ⊕ Unit) ⊕ Fin 2 ⊕ ↑X₂) ((↑Y₁ ⊕ Fin 2) ⊕ Unit ⊕ ↑Y₂) β

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

Equations

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

noncomputable def StandardRepresentation_3sum {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {x₁ : α} {x₂ : α} {x₃ : α} {y₁ : α} {y₂ : α} {y₃ : α} (hXX : M₁.X ∩ M₂.X = x₁ ᕃ x₂ ᕃ {x₃}) (hYY : M₁.Y ∩ M₂.Y = y₁ ᕃ y₂ ᕃ {y₃}) (hXY : M₁.X ⫗ M₂.Y) (hYX : M₁.Y ⫗ M₂.X) : StandardRepresentation α × Prop

StandardRepresentation-level 3-sum of two matroids. The second part checks legitimacy (invertibility of a certain 2x2 submatrix and specific 1s and 0s on concrete positions).

Equations

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

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

Binary 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 StandardRepresentation.Is3sumOf.interXX {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is3sumOf M₁ M₂) : ∃ (x₁ : α) (x₂ : α) (x₃ : α), M₁.X ∩ M₂.X = x₁ ᕃ x₂ ᕃ {x₃}

theorem StandardRepresentation.Is3sumOf.interYY {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is3sumOf M₁ M₂) : ∃ (y₁ : α) (y₂ : α) (y₃ : α), M₁.Y ∩ M₂.Y = y₁ ᕃ y₂ ᕃ {y₃}

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

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

theorem StandardRepresentation.Is3sumOf.indep {α : Type u_1} [DecidableEq α] {M₁ : StandardRepresentation α} {M₂ : StandardRepresentation α} {M : StandardRepresentation α} (hM : M.Is3sumOf M₁ M₂) : ∃ (x₁ : α) (x₂ : α) (x₃ : α) (y₁ : α) (y₂ : α) (y₃ : α) (x₁inX₁ : x₁ ∈ M₁.X) (x₂inX₁ : x₂ ∈ M₁.X) (x₂inX₂ : x₂ ∈ M₂.X) (x₃inX₁ : x₃ ∈ M₁.X) (x₃inX₂ : x₃ ∈ M₂.X) (y₃inY₂ : y₃ ∈ M₂.Y) (y₂inY₁ : y₂ ∈ M₁.Y) (y₂inY₂ : y₂ ∈ M₂.Y) (y₁inY₁ : y₁ ∈ M₁.Y) (y₁inY₂ : y₁ ∈ M₂.Y), let A₁ := Matrix.of fun (i : ↑(M₁.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) (j : ↑(M₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃})) ⊕ Fin 2) => M₁.B ⟨↑i, ⋯⟩ (Sum.casesOn j (fun (j' : ↑(M₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => ⟨↑j', ⋯⟩) ![⟨y₂, y₂inY₁⟩, ⟨y₁, y₁inY₁⟩]); let A₂ := Matrix.of fun (i : Fin 2 ⊕ ↑(M₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) (j : ↑(M₂.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => M₂.B (Sum.casesOn i ![⟨x₂, x₂inX₂⟩, ⟨x₃, x₃inX₂⟩] fun (i' : ↑(M₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) => ⟨↑i', ⋯⟩) ⟨↑j, ⋯⟩; let z₁ := fun (j : ↑(M₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => M₁.B ⟨x₁, x₁inX₁⟩ ⟨↑j, ⋯⟩; let z₂ := fun (i : ↑(M₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) => M₂.B ⟨↑i, ⋯⟩ ⟨y₃, y₃inY₂⟩; let D_₁ := Matrix.of fun (i j : Fin 2) => M₁.B (![⟨x₂, x₂inX₁⟩, ⟨x₃, x₃inX₁⟩] i) (![⟨y₂, y₂inY₁⟩, ⟨y₁, y₁inY₁⟩] j); let D₁ := Matrix.of fun (i : Fin 2) (j : ↑(M₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => M₁.B (![⟨x₂, x₂inX₁⟩, ⟨x₃, x₃inX₁⟩] i) ⟨↑j, ⋯⟩; let D₂ := Matrix.of fun (i : ↑(M₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) (j : Fin 2) => M₂.B ⟨↑i, ⋯⟩ (![⟨y₂, y₂inY₂⟩, ⟨y₁, y₁inY₂⟩] j); (Matrix.of fun (i : ↑(M₁.X \ (x₁ ᕃ x₂ ᕃ {x₃}) ∪ M₂.X)) (j : ↑(M₁.Y ∪ M₂.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => Matrix_3sumComposition A₁ A₂ z₁ z₂ D_₁ D₁ D₂ (if hi₁ : ↑i ∈ M₁.X \ (x₁ ᕃ x₂ ᕃ {x₃}) then Sum.inl (Sum.inl ⟨↑i, hi₁⟩) else if hi₂ : ↑i ∈ M₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}) then Sum.inr (Sum.inr ⟨↑i, hi₂⟩) else if hx₁ : ↑i = x₁ then Sum.inl (Sum.inr ()) else if hx₂ : ↑i = x₂ then Sum.inr (Sum.inl 0) else if hx₃ : ↑i = x₃ then Sum.inr (Sum.inl 1) else ⋯.elim) (if hj₁ : ↑j ∈ M₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃}) then Sum.inl (Sum.inl ⟨↑j, hj₁⟩) else if hj₂ : ↑j ∈ M₂.Y \ (y₁ ᕃ y₂ ᕃ {y₃}) then Sum.inr (Sum.inr ⟨↑j, hj₂⟩) else if hy₁ : ↑j = y₁ then Sum.inl (Sum.inr 1) else if hy₂ : ↑j = y₂ then Sum.inl (Sum.inr 0) else if hy₃ : ↑j = y₃ then Sum.inr (Sum.inl ()) else ⋯.elim)).IndepCols = M.toMatroid.Indep

theorem StandardRepresentation.Is3sumOf.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.Is3sumOf M₁ M₂) (hM₁ : M₁.IsRegular) (hM₂ : M₂.IsRegular) : M.IsRegular

Any 3-sum of regular matroids is a regular matroid. This is the last of the three parts of the easy direction of the Seymour's theorem.

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

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

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

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