The canonical obstruction for a partial transversal

Call R ⊆ I tight when the indices compatible with R are exactly #R many. The tight subsets of a partial transversal I are closed under union and intersection, so there is a largest one, maxTight A I. An element e ∉ I can be added to I exactly when its compatible indices are not contained in those of maxTight A I; this describes the closure of I in the transversal matroid.

Main definitions

• Theorems.TransversalMatroid.IsTight A R, Theorems.TransversalMatroid.maxTight A I.

Main results

• tight_union_and_inter: tight subsets form a lattice.
• maxTight_isTight, subset_maxTight: maxTight A I is the largest tight subset.
• insert_iff_not_subset_maxTight, not_insert_iff_subset_maxTight: the insertion criterion.
• mem_closure_iff_subset_maxTight: the matroid closure of I.

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

The compatible slots of a whole finite set: N(S).

Equations

• Theorems.TransversalMatroid.slotsOf A S = S.biUnion (Theorems.TransversalMatroid.compatibleSlots A)

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

A finite set is tight when it exactly saturates its compatible slots.

Equations

• Theorems.TransversalMatroid.IsTight A R = ((Theorems.TransversalMatroid.slotsOf A R).card = R.card)

@[instance_reducible]

instance Theorems.TransversalMatroid.decidableIsTight {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) : DecidablePred (IsTight A)

Equations

• Theorems.TransversalMatroid.decidableIsTight A R = (Theorems.TransversalMatroid.slotsOf A R).card.decEq R.card

theorem Theorems.TransversalMatroid.slotsOf_union {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (R S : Finset α) : slotsOf A (R ∪ S) = slotsOf A R ∪ slotsOf A S

theorem Theorems.TransversalMatroid.slotsOf_inter_subset {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (R S : Finset α) : slotsOf A (R ∩ S) ⊆ slotsOf A R ∩ slotsOf A S

theorem Theorems.TransversalMatroid.slotsOf_mono {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) {R S : Finset α} (h : R ⊆ S) : slotsOf A R ⊆ slotsOf A S

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

Hall's inequality, phrased with slotsOf.

theorem Theorems.TransversalMatroid.tight_union_and_inter {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I R S : Finset α} (hI : IsPartialTransversal A I) (hRI : R ⊆ I) (hSI : S ⊆ I) (hR : IsTight A R) (hS : IsTight A S) : IsTight A (R ∪ S) ∧ IsTight A (R ∩ S)

The tight sets are a lattice. Both the union and the intersection of two tight subsets of a partial transversal are tight. The two halves are one submodular squeeze: |N(R∪S)| + |N(R∩S)| ≤ |N(R)| + |N(S)| = |R| + |S| = |R∪S| + |R∩S|, and Hall bounds each left-hand term from below, so both inequalities are forced to equalities.

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 : IsTight A R) (hS : IsTight A S) : IsTight A (R ∪ S)

theorem Theorems.TransversalMatroid.tight_inter {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I R S : Finset α} (hI : IsPartialTransversal A I) (hRI : R ⊆ I) (hSI : S ⊆ I) (hR : IsTight A R) (hS : IsTight A S) : IsTight A (R ∩ S)

Tight subsets of a partial transversal are closed under intersection. This is the half the augmentation proof never needs, and the half that makes the family a lattice.

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

The empty set is tight.

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

The tight subsets of I, as a finite family.

Equations

• Theorems.TransversalMatroid.tightSubsets A I = Finset.filter (Theorems.TransversalMatroid.IsTight A) I.powerset

theorem Theorems.TransversalMatroid.mem_tightSubsets {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I R : Finset α} : R ∈ tightSubsets A I ↔ R ⊆ I ∧ IsTight A R

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

The canonical obstruction of I: the union of every tight subset of I.

Equations

• Theorems.TransversalMatroid.maxTight A I = (Theorems.TransversalMatroid.tightSubsets A I).biUnion id

theorem Theorems.TransversalMatroid.maxTight_subset {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) (I : Finset α) : maxTight A I ⊆ I

theorem Theorems.TransversalMatroid.subset_maxTight {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I R : Finset α} (hRI : R ⊆ I) (hR : IsTight A R) : R ⊆ maxTight A I

Every tight subset of I is contained in maxTight A I: it is the maximum, not merely a maximal, tight set.

theorem Theorems.TransversalMatroid.maxTight_isTight {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I : Finset α} (hI : IsPartialTransversal A I) : IsTight A (maxTight A I)

The maximum tight set is itself tight.

theorem Theorems.TransversalMatroid.not_insert_of_tight_cover {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I R : Finset α} {e : α} (hRI : R ⊆ I) (heR : e ∉ R) (hR : IsTight A R) (hcover : compatibleSlots A e ⊆ slotsOf A R) : ¬IsPartialTransversal A (insert e I)

A tight subset avoiding e and already owning every slot of e blocks the insertion. This is the converse of exists_tight_witness_of_not_insert: the tight certificate is not just necessary, it is sufficient.

theorem Theorems.TransversalMatroid.exists_tight_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 ∧ IsTight A R ∧ compatibleSlots A e ⊆ slotsOf A R

The existence lemma of the base development, restated with IsTight.

theorem Theorems.TransversalMatroid.not_insert_iff_exists_tight {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I : Finset α} {e : α} (hI : IsPartialTransversal A I) (heI : e ∉ I) : ¬IsPartialTransversal A (insert e I) ↔ ∃ R ⊆ I, IsTight A R ∧ compatibleSlots A e ⊆ slotsOf A R

Failure is exactly a tight cover. For a partial transversal I and an element e ∉ I, the insertion fails if and only if some tight subset of I already owns every slot compatible with e.

theorem Theorems.TransversalMatroid.insert_iff_not_subset_maxTight {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I : Finset α} {e : α} (hI : IsPartialTransversal A I) (heI : e ∉ I) : IsPartialTransversal A (insert e I) ↔ ¬compatibleSlots A e ⊆ slotsOf A (maxTight A I)

One set decides every insertion. For a partial transversal I and e ∉ I, the set insert e I is a partial transversal if and only if e has a compatible slot outside the neighbourhood of the single canonical obstruction maxTight A I.

theorem Theorems.TransversalMatroid.not_insert_iff_subset_maxTight {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I : Finset α} {e : α} (hI : IsPartialTransversal A I) (heI : e ∉ I) : ¬IsPartialTransversal A (insert e I) ↔ compatibleSlots A e ⊆ slotsOf A (maxTight A I)

The contrapositive of insert_iff_not_subset_maxTight: the insertion fails exactly when the canonical obstruction already owns every slot of e. Stated positively for readability; it makes no claim about the matroid's closure operator (for that, see mem_closure_iff_subset_maxTight).

@[simp]

theorem Theorems.TransversalMatroid.transversalMatroid_ground {α : Type u_1} [DecidableEq α] {t : ℕ} (A : Fin t → Finset α) : (transversalMatroid A).E = Set.univ

The ground set of the transversal matroid is all of α: an element lying in no presenting set is a loop, not an absentee.

theorem Theorems.TransversalMatroid.mem_closure_iff_subset_maxTight {α : Type u_1} [DecidableEq α] {t : ℕ} {A : Fin t → Finset α} {I : Finset α} {e : α} (hI : IsPartialTransversal A I) (heI : e ∉ I) : e ∈ (transversalMatroid A).closure ↑I ↔ compatibleSlots A e ⊆ slotsOf A (maxTight A I)

The canonical obstruction computes the closure. For a partial transversal I and e ∉ I, the element e lies in the closure of I in the matroid transversalMatroid A exactly when the single finite set maxTight A I already owns every slot compatible with e.

This is the statement in Mathlib's own matroid vocabulary: Matroid.closure is a genuine matroid invariant, and the theorem says that on independent sets it is decided by one containment test against one canonical set, with no search over subsets and no matching recomputed.