Sums of matroids

The sum M of a collection M₁, M₂, .. of matroids is a matroid on the disjoint union of the ground sets of the summands, in which the independent sets are precisely the unions of independent sets of the summands.

We can ask for such a sum both for pairs and for arbitrary indexed collections of matroids, and we can also ask for the 'disjoint union' to be either set-theoretic or type-theoretic. To this end, we define five separate versions of the sum construction.

Main definitions

• For an indexed collection M : (i : ι) → Matroid (α i) of matroids on different types, Matroid.sigma M is the sum of the M i, as a matroid on the sigma type (Σ i, α i).

• For an indexed collection M : ι → Matroid α of matroids on the same type, Matroid.sum' M is the sum of the M i, as a matroid on the product type ι × α.

• For an indexed collection M : ι → Matroid α of matroids on the same type, and a proof h : Pairwise (Disjoint on fun i ↦ (M i).E) that they have disjoint ground sets, Matroid.disjointSigma M h is the sum of the M as a Matroid α with ground set ⋃ i, (M i).E.

• Matroid.sum (M : Matroid α) (N : Matroid β) is the sum of M and N as a matroid on α ⊕ β.

• If M N : Matroid α and h : Disjoint M.E N.E, then Matroid.disjointSum M N h is the sum of M and N as a Matroid α with ground set M.E ∪ N.E.

Implementation details

We only directly define a matroid for Matroid.sigma. All other versions of sum are defined indirectly, using Matroid.sigma and the API in Matroid.map.

def Matroid.sigma {ι : Type u_1} {α : ι → Type u_2} (M : (i : ι) → Matroid (α i)) : Matroid ((i : ι) × α i)

The sum of an indexed collection of matroids, as a matroid on the sigma-type.

Equations

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

@[simp]

theorem Matroid.sigma_indep_iff {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I : Set ((i : ι) × α i)} : (Matroid.sigma M).Indep I ↔ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)

@[simp]

theorem Matroid.sigma_base_iff {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {B : Set ((i : ι) × α i)} : (Matroid.sigma M).Base B ↔ ∀ (i : ι), (M i).Base (Sigma.mk i ⁻¹' B)

@[simp]

theorem Matroid.sigma_ground_eq {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} : (Matroid.sigma M).E = Set.univ.sigma fun (i : ι) => (M i).E

@[simp]

theorem Matroid.sigma_basis_iff {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {I : Set ((i : ι) × α i)} {X : Set ((i : ι) × α i)} : (Matroid.sigma M).Basis I X ↔ ∀ (i : ι), (M i).Basis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)

theorem Matroid.Finitary.sigma {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} (h : ∀ (i : ι), (M i).Finitary) : (Matroid.sigma M).Finitary

def Matroid.sum' {α : Type u_1} {ι : Type u_2} (M : ι → Matroid α) : Matroid (ι × α)

The sum of an indexed family M : ι → Matroid α of matroids on the same type, as a matroid on the product type ι × α.

Equations

• Matroid.sum' M = (Matroid.sigma M).mapEquiv (Equiv.sigmaEquivProd ι α)

@[simp]

theorem Matroid.sum'_indep_iff {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {I : Set (ι × α)} : (Matroid.sum' M).Indep I ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)

@[simp]

theorem Matroid.sum'_ground_eq {α : Type u_1} {ι : Type u_2} (M : ι → Matroid α) : (Matroid.sum' M).E = ⋃ (i : ι), Prod.mk i '' (M i).E

@[simp]

theorem Matroid.sum'_base_iff {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {B : Set (ι × α)} : (Matroid.sum' M).Base B ↔ ∀ (i : ι), (M i).Base (Prod.mk i ⁻¹' B)

@[simp]

theorem Matroid.sum'_basis_iff {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {I : Set (ι × α)} {X : Set (ι × α)} : (Matroid.sum' M).Basis I X ↔ ∀ (i : ι), (M i).Basis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)

theorem Matroid.Finitary.sum' {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} (h : ∀ (i : ι), (M i).Finitary) : (Matroid.sum' M).Finitary

def Matroid.disjointSigma {α : Type u_1} {ι : Type u_2} (M : ι → Matroid α) (h : Pairwise (Disjoint on fun (i : ι) => (M i).E)) : Matroid α

The sum of an indexed collection of matroids on α with pairwise disjoint ground sets, as a matroid on α

Equations

• Matroid.disjointSigma M h = (Matroid.sigma fun (i : ι) => (M i).restrictSubtype (M i).E).mapEmbedding (Function.Embedding.sigmaSet h)

@[simp]

theorem Matroid.disjointSigma_ground_eq {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Disjoint on fun (i : ι) => (M i).E)} : (Matroid.disjointSigma M h).E = ⋃ (i : ι), (M i).E

@[simp]

theorem Matroid.disjointSigma_indep_iff {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Disjoint on fun (i : ι) => (M i).E)} {I : Set α} : (Matroid.disjointSigma M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ (i : ι), (M i).E

@[simp]

theorem Matroid.disjointSigma_base_iff {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Disjoint on fun (i : ι) => (M i).E)} {B : Set α} : (Matroid.disjointSigma M h).Base B ↔ (∀ (i : ι), (M i).Base (B ∩ (M i).E)) ∧ B ⊆ ⋃ (i : ι), (M i).E

@[simp]

theorem Matroid.disjointSigma_basis_iff {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Disjoint on fun (i : ι) => (M i).E)} {I : Set α} {X : Set α} : (Matroid.disjointSigma M h).Basis I X ↔ (∀ (i : ι), (M i).Basis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ (i : ι), (M i).E

def Matroid.sum {α : Type u} {β : Type v} (M : Matroid α) (N : Matroid β) : Matroid (α ⊕ β)

The sum of two matroids as a matroid on the sum type.

Equations

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

@[simp]

theorem Matroid.sum_ground {α : Type u} {β : Type v} (M : Matroid α) (N : Matroid β) : (M.sum N).E = Sum.inl '' M.E ∪ Sum.inr '' N.E

@[simp]

theorem Matroid.sum_indep_iff {α : Type u} {β : Type v} (M : Matroid α) (N : Matroid β) {I : Set (α ⊕ β)} : (M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)

@[simp]

theorem Matroid.sum_base_iff {α : Type u} {β : Type v} {M : Matroid α} {N : Matroid β} {B : Set (α ⊕ β)} : (M.sum N).Base B ↔ M.Base (Sum.inl ⁻¹' B) ∧ N.Base (Sum.inr ⁻¹' B)

@[simp]

theorem Matroid.sum_basis_iff {α : Type u} {β : Type v} {M : Matroid α} {N : Matroid β} {I : Set (α ⊕ β)} {X : Set (α ⊕ β)} : (M.sum N).Basis I X ↔ M.Basis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.Basis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)

def Matroid.disjointSum {α : Type u_1} (M : Matroid α) (N : Matroid α) (h : Disjoint M.E N.E) : Matroid α

The sum of two matroids on α with disjoint ground sets, as a Matroid α.

Equations

• M.disjointSum N h = ((M.restrictSubtype M.E).sum (N.restrictSubtype N.E)).mapEmbedding (Function.Embedding.sumSet h)

@[simp]

theorem Matroid.disjointSum_ground_eq {α : Type u_1} {M : Matroid α} {N : Matroid α} {h : Disjoint M.E N.E} : (M.disjointSum N h).E = M.E ∪ N.E

@[simp]

theorem Matroid.disjointSum_indep_iff {α : Type u_1} {M : Matroid α} {N : Matroid α} {h : Disjoint M.E N.E} {I : Set α} : (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E

@[simp]

theorem Matroid.disjointSum_base_iff {α : Type u_1} {M : Matroid α} {N : Matroid α} {h : Disjoint M.E N.E} {B : Set α} : (M.disjointSum N h).Base B ↔ M.Base (B ∩ M.E) ∧ N.Base (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E

@[simp]

theorem Matroid.disjointSum_basis_iff {α : Type u_1} {M : Matroid α} {N : Matroid α} {h : Disjoint M.E N.E} {I : Set α} {X : Set α} : (M.disjointSum N h).Basis I X ↔ M.Basis (I ∩ M.E) (X ∩ M.E) ∧ N.Basis (I ∩ N.E) (X ∩ N.E) ∧ I ⊆ X ∧ X ⊆ M.E ∪ N.E

theorem Matroid.Indep.eq_union_image_of_disjointSum {α : Type u_1} {M : Matroid α} {N : Matroid α} {h : Disjoint M.E N.E} {I : Set α} (hI : (M.disjointSum N h).Indep I) : ∃ (IM : Set α) (IN : Set α), M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

theorem Matroid.Base.eq_union_image_of_disjointSum {α : Type u_1} {M : Matroid α} {N : Matroid α} {h : Disjoint M.E N.E} {B : Set α} (hB : (M.disjointSum N h).Base B) : ∃ (BM : Set α) (BN : Set α), M.Base BM ∧ N.Base BN ∧ Disjoint BM BN ∧ B = BM ∪ BN