Matroid partition theorem

TheoremEdmonds' matroid partition theorem, arbitrary ground set#✓fully proved

Let \(E\) be a finite set, let \(M\) be a matroid with ground set \(E(M) \subseteq E\), let \(S \subseteq E\) and let \(k\) be a natural number. Then \(S = J_1 \cup \dots \cup J_k\) for some sets \(J_1, \dots, J_k\) that are independent in \(M\) (not necessarily disjoint) if and only if \(|X| \le k \, r_M(X)\) for every \(X \subseteq S\), where \(r_M(X)\) denotes the rank in \(M\) of \(X \cap E(M)\).

theorem edmonds_matroid_partition'
    {E : Type*} [Finite E]
    {M : Matroid E}
    {S : Set E} {k : ℕ} :
    (∃ J : Fin k → Set E, (∀ i, M.Indep (J i)) ∧ S = ⋃ i, J i) ↔
      ∀ X : Set E, X ⊆ S → (X.ncard : ℕ∞) ≤ (k : ℕ∞) * M.eRk X

Uses 1 · Used by 1

Proof usesMatroid intersection for abstract rank functions

Used byEdmonds' matroid partition theorem

TheoremEdmonds' matroid partition theorem#✓fully proved

Let \(E\) be a finite set, let \(M\) be a matroid whose ground set is all of \(E\), let \(S \subseteq E\) and let \(k\) be a natural number. Then \(S = J_1 \cup \dots \cup J_k\) for some sets \(J_1, \dots, J_k\) that are independent in \(M\) (not necessarily disjoint) if and only if \(|X| \le k \, r_M(X)\) for every \(X \subseteq S\), where \(r_M\) is the rank function of \(M\).

theorem edmonds_matroid_partition
    {E : Type*} [Fintype E] [DecidableEq E]
    {M : Matroid E} (hM : M.E = Set.univ)
    {S : Set E} {k : ℕ} :
    (∃ J : Fin k → Set E, (∀ i, M.Indep (J i)) ∧ S = ⋃ i, J i) ↔
      ∀ X : Set E, X ⊆ S → (X.ncard : ℕ∞) ≤ (k : ℕ∞) * M.eRk X

Sources

• J. Edmonds, Minimum partition of a matroid into independent subsets, J. Res. Natl. Bur. Standards Sect. B 69B (1965), 67-72, DOI 10.6028/jres.069B.004.

Uses 1

Proof usesEdmonds' matroid partition theorem, arbitrary ground set

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.