Transversal matroids

For a finite indexed family A : Fin t → Finset α, a finite set X is a partial transversal if its elements can be assigned injectively to indices whose sets contain them. The partial transversals are the independent sets of a matroid (Edmonds–Fulkerson, Mirsky–Perfect). The augmentation axiom is proved from Hall's theorem through tight sets: if an element cannot be added, a set of tight indices blocks it.

Main definitions

• Theorems.TransversalMatroid.IsPartialTransversal A X.
• Theorems.TransversalMatroid.transversalMatroid A: the matroid on α.

Main results

• partialTransversal_iff_hall: Hall's characterization of partial transversals.
• exists_tight_witness_of_not_insert: a tight obstruction to insertion.
• tight_union, tight_biUnion: unions of tight sets are tight.
• partialTransversal_augmentation: the augmentation axiom.
• transversalMatroid_indep: the independent sets of transversalMatroid A are the partial transversals.

References

• J. Edmonds, D. R. Fulkerson, Transversals and matroid partition, J. Res. Nat. Bur. Standards Sect. B 69B (1965) 147–153.
• J. Oxley, Matroid Theory, 2nd ed., Oxford University Press, 2011, §1.6.

def Theorems.Compatible {α : Type u_1} {t : ℕ} (A : Fin t → Set α) (x : α) (i : Fin t) : Prop

The compatibility relation of a set-system presentation.

Equations

• Theorems.Compatible A x i = (x ∈ A i)

theorem Theorems.compatible_iff {α : Type u_1} {t : ℕ} (A : Fin t → Set α) (x : α) (i : Fin t) : Compatible A x i ↔ x ∈ A i

The compatibility predicate is definitionally the membership condition in the presenting set system.

def Theorems.TransversalMatroid.compatibleSlots {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (x : α) : Finset (Fin t)

The available indices of sets in A that contain x.

Equations

• Theorems.TransversalMatroid.compatibleSlots A x = {i : Fin t | x ∈ A i}

def Theorems.TransversalMatroid.IsPartialTransversal {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (I : Finset α) : Prop

A finite set is a partial transversal when its elements can be assigned injectively to compatible indices in the presenting family.

Equations

• Theorems.TransversalMatroid.IsPartialTransversal A I = Nonempty ↑(hallMatchingsOn (Theorems.TransversalMatroid.compatibleSlots A) I)

theorem Theorems.TransversalMatroid.partialTransversal_empty {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) : IsPartialTransversal A ∅

The empty set is a partial transversal of every finite set system.

theorem Theorems.TransversalMatroid.partialTransversal_subset {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I J : Finset α} (hIJ : I ⊆ J) (hJ : IsPartialTransversal A J) : IsPartialTransversal A I

Restricting a partial transversal preserves its matching, hence preserves independence. This is the hereditary matroid axiom for the presentation.

theorem Theorems.TransversalMatroid.partialTransversal_card_le_slots {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I : Finset α} (hI : IsPartialTransversal A I) : I.card ≤ (I.biUnion (compatibleSlots A)).card

A partial transversal satisfies Hall's cardinal inequality for its full set of elements. The subset form and the augmentation theorem will build on this injection into the union of compatible slots.

theorem Theorems.TransversalMatroid.partialTransversal_hall {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I S : Finset α} (hSI : S ⊆ I) (hI : IsPartialTransversal A I) : S.card ≤ (S.biUnion (compatibleSlots A)).card

Every subset of a partial transversal satisfies Hall's cardinal inequality.

theorem Theorems.TransversalMatroid.hall_partialTransversal {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (I : Finset α) (h : ∀ S ⊆ I, S.card ≤ (S.biUnion (compatibleSlots A)).card) : IsPartialTransversal A I

Hall's inequalities on every subset of I construct a partial transversal of I. Together with partialTransversal_hall, this is the finite Hall characterization used by the augmentation proof.

theorem Theorems.TransversalMatroid.partialTransversal_iff_hall {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (I : Finset α) : IsPartialTransversal A I ↔ ∀ S ⊆ I, S.card ≤ (S.biUnion (compatibleSlots A)).card

Finite Hall characterization of partial transversals.

theorem Theorems.TransversalMatroid.not_partialTransversal_exists_hall_violation {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (I : Finset α) (hI : ¬IsPartialTransversal A I) : ∃ S ⊆ I, (S.biUnion (compatibleSlots A)).card < S.card

If a finite set has no partial transversal, Hall's condition has a concrete finite witness. This is the starting point for the tight-set argument in the augmentation axiom.

theorem Theorems.TransversalMatroid.hall_violation_insert_mem {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I S : Finset α} {e : α} (hI : IsPartialTransversal A I) (hSsub : S ⊆ insert e I) (hS : (S.biUnion (compatibleSlots A)).card < S.card) : e ∈ S

A Hall witness for the failure of insert e I must contain the inserted element when I is already a partial transversal.

theorem Theorems.TransversalMatroid.exists_tight_witness_of_not_insert {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I : Finset α} {e : α} (hI : IsPartialTransversal A I) (hnot : ¬IsPartialTransversal A (insert e I)) : ∃ R ⊆ I, e ∉ R ∧ (R.biUnion (compatibleSlots A)).card = R.card ∧ compatibleSlots A e ⊆ R.biUnion (compatibleSlots A)

If adding e to a partial transversal fails, there is a tight subset of the original transversal whose compatible slots already contain every slot compatible with e. This is the tight-set certificate used in the standard Hall proof of augmentation.

theorem Theorems.TransversalMatroid.tight_union {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I R S : Finset α} (hI : IsPartialTransversal A I) (hRI : R ⊆ I) (hSI : S ⊆ I) (hR : (R.biUnion (compatibleSlots A)).card = R.card) (hS : (S.biUnion (compatibleSlots A)).card = S.card) : ((R ∪ S).biUnion (compatibleSlots A)).card = (R ∪ S).card

The union of two Hall-tight subsets of a partial transversal is again Hall-tight. This is the submodularity step in the augmentation argument.

theorem Theorems.TransversalMatroid.tight_biUnion {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I : Finset α} (hI : IsPartialTransversal A I) (F : Finset (Finset α)) (hsub : ∀ R ∈ F, R ⊆ I) (htight : ∀ R ∈ F, (R.biUnion (compatibleSlots A)).card = R.card) : ((F.biUnion id).biUnion (compatibleSlots A)).card = (F.biUnion id).card

A finite union of Hall-tight subsets of a partial transversal is Hall-tight.

theorem Theorems.TransversalMatroid.card_sdiff_le_of_tight_cover {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I J : Finset α} (hI : IsPartialTransversal A I) (hJ : IsPartialTransversal A J) (F : Finset (Finset α)) (hFsub : ∀ R ∈ F, R ⊆ I) (hFtight : ∀ R ∈ F, (R.biUnion (compatibleSlots A)).card = R.card) (hcover : ∀ e ∈ J \ I, compatibleSlots A e ⊆ (F.biUnion id).biUnion (compatibleSlots A)) : (J \ I).card ≤ (I \ J).card

A finite family of tight subsets of I that covers the compatible slots of every element in J \ I forces |J \ I| ≤ |I \ J|.

theorem Theorems.TransversalMatroid.partialTransversal_augmentation {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {I J : Finset α} (hI : IsPartialTransversal A I) (hJ : IsPartialTransversal A J) (hcard : I.card < J.card) : ∃ e ∈ J \ I, IsPartialTransversal A (insert e I)

The augmentation axiom for finite partial transversals. This is the combinatorial core of Perfect's transversal-matroid theorem.

noncomputable def Theorems.TransversalMatroid.transversalMatroid {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) : Matroid α

The transversal matroid presented by the finite set system A. Elements outside every member of A are loops, so the ground set is all of α.

Equations

• Theorems.TransversalMatroid.transversalMatroid A = (IndepMatroid.ofFinset Set.univ (Theorems.TransversalMatroid.IsPartialTransversal A) ⋯ ⋯ ⋯ ⋯).matroid

theorem Theorems.TransversalMatroid.transversalMatroid_indep {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (I : Finset α) : (transversalMatroid A).Indep ↑I ↔ IsPartialTransversal A I

Perfect's transversal-matroid theorem for the finite presentation A: the independent finite sets of transversalMatroid A are exactly the partial transversals of A.