Matroid intersection theorem

TheoremMatroid intersection for abstract rank functions#✓fully proved

Let \(E\) be a finite subset of a type \(\alpha\), let \(k\) be a natural number, and let \(r_1, r_2\) be functions from the finite subsets of \(\alpha\) to \(\mathbb{N}\) such that, for \(i = 1, 2\) and all finite \(X, Y \subseteq \alpha\), we have \(r_i(X) \le |X|\), \(r_i(X) \le r_i(Y)\) whenever \(X \subseteq Y\), and \(r_i(X \cap Y) + r_i(X \cup Y) \le r_i(X) + r_i(Y)\). If every \(X \subseteq E\) satisfies \(k \le r_1(X) + r_2(E \setminus X)\), then there is a set \(I \subseteq E\) with \(r_1(I) = r_2(I) = |I|\) and \(|I| \ge k\).

Proved by induction on \(E\), via deletion and contraction.

theorem exists_common_indep_of_cut_le
    {α : Type*} [DecidableEq α]
    (E : Finset α) (k : ℕ) (r₁ r₂ : Finset α → ℕ)
    (hle₁ : ∀ X, r₁ X ≤ X.card)
    (hle₂ : ∀ X, r₂ X ≤ X.card)
    (hmono₁ : ∀ X Y, X ⊆ Y → r₁ X ≤ r₁ Y)
    (hmono₂ : ∀ X Y, X ⊆ Y → r₂ X ≤ r₂ Y)
    (hsub₁ : ∀ X Y, r₁ (X ∩ Y) + r₁ (X ∪ Y) ≤ r₁ X + r₁ Y)
    (hsub₂ : ∀ X Y, r₂ (X ∩ Y) + r₂ (X ∪ Y) ≤ r₂ X + r₂ Y)
    (hcut : ∀ X, X ⊆ E → k ≤ r₁ X + r₂ (E \ X)) :
    ∃ I, I ⊆ E ∧ r₁ I = I.card ∧ r₂ I = I.card ∧ k ≤ I.card

Used by 2

Used byEdmonds' matroid intersection theorem · Edmonds' matroid partition theorem, arbitrary ground set

TheoremEdmonds' matroid intersection theorem#✓fully proved

Let \(M_1\) and \(M_2\) be matroids on a finite type \(\alpha\), with arbitrary ground sets, and let \(k\) be a natural number. There is a set \(I \subseteq \alpha\) independent in both \(M_1\) and \(M_2\) with \(|I| \ge k\) if and only if every \(X \subseteq \alpha\) satisfies \(k \le r_1(X) + r_2(\alpha \setminus X)\), where \(r_i(Y)\) is the largest size of a subset of \(Y\) independent in \(M_i\).

theorem edmonds_matroid_intersection'
    {α : Type*} [Finite α]
    {M₁ M₂ : Matroid α}
    {k : ℕ} :
    (∃ I : Finset α, M₁.Indep (I : Set α) ∧
      M₂.Indep (I : Set α) ∧ k ≤ I.card) ↔
    ∀ X : Set α, (k : ℕ∞) ≤ M₁.eRk X + M₂.eRk Xᶜ

Uses 1 · Used by 1

Proof usesMatroid intersection for abstract rank functions

Used byEdmonds' matroid intersection theorem for matroids on the whole type

TheoremEdmonds' matroid intersection theorem for matroids on the whole type#✓fully proved

Let \(M_1\) and \(M_2\) be matroids on a finite type \(\alpha\), each with ground set all of \(\alpha\), and let \(k\) be a natural number. There is a set \(I \subseteq \alpha\) independent in both \(M_1\) and \(M_2\) with \(|I| \ge k\) if and only if every \(X \subseteq \alpha\) satisfies \(k \le r_1(X) + r_2(\alpha \setminus X)\), where \(r_i\) is the rank function of \(M_i\).

The hypotheses on the ground sets are not needed; the general version drops them.

theorem edmonds_matroid_intersection
    {α : Type*} [Fintype α] [DecidableEq α]
    {M₁ M₂ : Matroid α}
    (h₁ : M₁.E = Set.univ) (h₂ : M₂.E = Set.univ)
    {k : ℕ} :
    (∃ I : Finset α, M₁.Indep (I : Set α) ∧
      M₂.Indep (I : Set α) ∧ k ≤ I.card) ↔
    ∀ X : Set α, (k : ℕ∞) ≤ M₁.eRk X + M₂.eRk Xᶜ

Sources

• J. Edmonds, Submodular Functions, Matroids, and Certain Polyhedra, Combinatorial Structures and Their Applications (1970), 69–87.

Uses 1

Proof usesEdmonds' matroid intersection theorem

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.