@[reducible, inline]
noncomputable abbrev
Matrix_3sumComposition
{α β : Type}
[CommRing β]
{X₁ Y₁ X₂ 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-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.
Instances For
noncomputable def
StandardRepr_3sum
{α : Type}
[DecidableEq α]
{S₁ S₂ : StandardRepr α Z2}
{x₁ x₂ x₃ y₁ y₂ y₃ : α}
(hXX : S₁.X ∩ S₂.X = x₁ ᕃ x₂ ᕃ {x₃})
(hYY : S₁.Y ∩ S₂.Y = y₁ ᕃ y₂ ᕃ {y₃})
(hXY : S₁.X ⫗ S₂.Y)
(hYX : S₁.Y ⫗ S₂.X)
:
StandardRepr α Z2 × 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.
Instances For
theorem
StandardRepr_3sum_B
{α : Type}
[DecidableEq α]
{S₁ S₂ : StandardRepr α Z2}
{x₁ x₂ x₃ y₁ y₂ y₃ : α}
(hXX : S₁.X ∩ S₂.X = x₁ ᕃ x₂ ᕃ {x₃})
(hYY : S₁.Y ∩ S₂.Y = y₁ ᕃ y₂ ᕃ {y₃})
(hXY : S₁.X ⫗ S₂.Y)
(hYX : S₁.Y ⫗ S₂.X)
:
(StandardRepr_3sum hXX hYY hXY hYX).1.B = let_fun hxxx₁ := ⋯;
let_fun hxxx₂ := ⋯;
let_fun hyyy₁ := ⋯;
let_fun hyyy₂ := ⋯;
let_fun x₁inX₁ := ⋯;
let_fun x₂inX₁ := ⋯;
let_fun x₂inX₂ := ⋯;
let_fun x₃inX₁ := ⋯;
let_fun x₃inX₂ := ⋯;
let_fun y₃inY₂ := ⋯;
let_fun y₂inY₁ := ⋯;
let_fun y₂inY₂ := ⋯;
let_fun y₁inY₁ := ⋯;
let_fun y₁inY₂ := ⋯;
let A₁ :=
Matrix.of fun (i : ↑(S₁.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) (j : ↑(S₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃})) ⊕ Fin 2) =>
S₁.B ⟨↑i, ⋯⟩ (Sum.casesOn j (fun (j' : ↑(S₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => ⟨↑j', ⋯⟩) ![⟨y₂, y₂inY₁⟩, ⟨y₁, y₁inY₁⟩]);
let A₂ :=
Matrix.of fun (i : Fin 2 ⊕ ↑(S₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) (j : ↑(S₂.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) =>
S₂.B (Sum.casesOn i ![⟨x₂, x₂inX₂⟩, ⟨x₃, x₃inX₂⟩] fun (i' : ↑(S₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) => ⟨↑i', ⋯⟩) ⟨↑j, ⋯⟩;
let z₁ := fun (j : ↑(S₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => S₁.B ⟨x₁, x₁inX₁⟩ ⟨↑j, ⋯⟩;
let z₂ := fun (i : ↑(S₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) => S₂.B ⟨↑i, ⋯⟩ ⟨y₃, y₃inY₂⟩;
let D_₁ := Matrix.of fun (i j : Fin 2) => S₁.B (![⟨x₂, x₂inX₁⟩, ⟨x₃, x₃inX₁⟩] i) (![⟨y₂, y₂inY₁⟩, ⟨y₁, y₁inY₁⟩] j);
let D₁ :=
Matrix.of fun (i : Fin 2) (j : ↑(S₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))) => S₁.B (![⟨x₂, x₂inX₁⟩, ⟨x₃, x₃inX₁⟩] i) ⟨↑j, ⋯⟩;
let D₂ :=
Matrix.of fun (i : ↑(S₂.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) (j : Fin 2) => S₂.B ⟨↑i, ⋯⟩ (![⟨y₂, y₂inY₂⟩, ⟨y₁, y₁inY₂⟩] j);
((Matrix_3sumComposition A₁ A₂ z₁ z₂ D_₁ D₁ D₂).submatrix
((Equiv.sumAssoc (↑(S₁.X \ (x₁ ᕃ x₂ ᕃ {x₃}))) Unit (Fin 2 ⊕ ↑(S₂.X \ (x₁ ᕃ x₂ ᕃ {x₃})))).invFun ∘ Sum.map id fun (i : ↑S₂.X) =>
if hx₁ : ↑i = x₁ then Sum.inl ()
else
if hx₂ : ↑i = x₂ then Sum.inr (Sum.inl 0)
else if hx₃ : ↑i = x₃ then Sum.inr (Sum.inl 1) else Sum.inr (Sum.inr ⟨↑i, ⋯⟩))
((Equiv.sumAssoc (↑(S₁.Y \ (y₁ ᕃ y₂ ᕃ {y₃})) ⊕ Fin 2) Unit ↑(S₂.Y \ (y₁ ᕃ y₂ ᕃ {y₃}))).toFun ∘ Sum.map
(fun (j : ↑S₁.Y) =>
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 () else Sum.inl (Sum.inl ⟨↑j, ⋯⟩))
id)).toMatrixUnionUnion
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₂
- x₁ : α
- x₂ : α
- x₃ : α
- y₁ : α
- y₂ : α
- y₃ : α
- hXY : self.S₁.X ⫗ self.S₂.Y
- hYX : self.S₁.Y ⫗ self.S₂.X
- IsSum : (StandardRepr_3sum ⋯ ⋯ ⋯ ⋯).1 = self.S
- IsValid : (StandardRepr_3sum ⋯ ⋯ ⋯ ⋯).2
Instances For
theorem
Matroid.Is3sumOf.isRegular
{α : Type}
[DecidableEq α]
{M M₁ M₂ : Matroid α}
(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 final of the three parts of the easy direction of the Seymour's theorem.