Rado's theorem on independent transversals

TheoremRado's theorem on independent transversals, arbitrary ground set#✓fully proved

Let \(I\) and \(E\) be finite sets, let \(M\) be a matroid with ground set \(E(M) \subseteq E\), and let \((A_i)_{i \in I}\) be a family of subsets of \(E\). Then there is an injective map \(f : I \to E\) such that \(f(i) \in A_i\) for every \(i \in I\) and the image \(f(I)\) is independent in \(M\), if and only if \(|J| \le r_M\bigl(\bigcup_{i \in J} A_i\bigr)\) for every \(J \subseteq I\), where \(r_M(X)\) denotes the rank in \(M\) of \(X \cap E(M)\).

theorem rado_matroidal_marriage' {I E : Type*} [Finite I] [Finite E] {M : Matroid E}
    (A : I → Set E) :
    (∃ f : I → E, Function.Injective f ∧ (∀ i, f i ∈ A i) ∧
      M.Indep (Set.range f)) ↔
    ∀ J : Finset I, (J.card : ℕ∞) ≤ M.eRk (⋃ i ∈ J, A i)

Used by 1

Used byRado's theorem on independent transversals

TheoremRado's theorem on independent transversals#✓fully proved

Let \(I\) and \(E\) be finite sets, let \(M\) be a matroid whose ground set is all of \(E\), and let \((A_i)_{i \in I}\) be a family of subsets of \(E\). Then there is an injective map \(f : I \to E\) such that \(f(i) \in A_i\) for every \(i \in I\) and the image \(f(I)\) is independent in \(M\), if and only if \(|J| \le r_M\bigl(\bigcup_{i \in J} A_i\bigr)\) for every \(J \subseteq I\), where \(r_M\) is the rank function of \(M\).

The hypothesis that the ground set of \(M\) is all of \(E\) is not needed.

theorem rado_matroidal_marriage
    {I E : Type*} [Fintype I] [DecidableEq I] [Fintype E] [DecidableEq E]
    {M : Matroid E} (hM : M.E = Set.univ) (A : I → Set E) :
    (∃ f : I → E, Function.Injective f ∧ (∀ i, f i ∈ A i) ∧
      M.Indep (Set.range f)) ↔
    ∀ J : Finset I, (J.card : ℕ∞) ≤ M.eRk (⋃ i ∈ J, A i)

Sources

• R. Rado, Quart. J. Math. os-13 (1942), DOI 10.1093/qmath/os-13.1.83.

Uses 1

Proof usesRado's theorem on independent transversals, arbitrary ground set

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.