Hall's Marriage Theorem

Given a list of finite subsets $X_1, X_2, \dots, X_n$ of some given set $S$, P. Hall in [Hall1935] gave a necessary and sufficient condition for there to be a list of distinct elements $x_1, x_2, \dots, x_n$ with $x_i\in X_i$ for each $i$: it is when for each $k$, the union of every $k$ of these subsets has at least $k$ elements.

Rather than a list of finite subsets, one may consider indexed families t : ι → Finset α of finite subsets with ι a Fintype, and then the list of distinct representatives is given by an injective function f : ι → α such that ∀ i, f i ∈ t i, called a matching. This version is formalized as Finset.all_card_le_biUnion_card_iff_exists_injective' in a separate module.

The theorem can be generalized to remove the constraint that ι be a Fintype. As observed in [Halpern1966], one may use the constrained version of the theorem in a compactness argument to remove this constraint. The formulation of compactness we use is that inverse limits of nonempty finite sets are nonempty (nonempty_sections_of_finite_inverse_system), which uses the Tychonoff theorem. The core of this module is constructing the inverse system: for every finite subset ι' of ι, we can consider the matchings on the restriction of the indexed family t to ι'.

Main statements

• Finset.all_card_le_biUnion_card_iff_exists_injective is in terms of t : ι → Finset α.
• Fintype.all_card_le_rel_image_card_iff_exists_injective is in terms of a relation r : α → β → Prop such that Rel.image r {a} is a finite set for all a : α.
• Fintype.all_card_le_filter_rel_iff_exists_injective is in terms of a relation r : α → β → Prop on finite types, with the Hall condition given in terms of finset.univ.filter.

Todo

• The statement of the theorem in terms of bipartite graphs is in preparation.

Tags

Hall's Marriage Theorem, indexed families

def hallMatchingsOn {ι : Type u} {α : Type v} (t : ι → Finset α) (ι' : Finset ι) : Set ({ x : ι // x ∈ ι' } → α)

The set of matchings for t when restricted to a Finset of ι.

Equations

• hallMatchingsOn t ι' = {f : { x : ι // x ∈ ι' } → α | Function.Injective f ∧ ∀ (x : { x : ι // x ∈ ι' }), f x ∈ t ↑x}

def hallMatchingsOn.restrict {ι : Type u} {α : Type v} (t : ι → Finset α) {ι' : Finset ι} {ι'' : Finset ι} (h : ι' ⊆ ι'') (f : ↑(hallMatchingsOn t ι'')) : ↑(hallMatchingsOn t ι')

Given a matching on a finset, construct the restriction of that matching to a subset.

Equations

• hallMatchingsOn.restrict t h f = { val := fun (i : { x : ι // x ∈ ι' }) => ↑f { val := ↑i, property := ⋯ }, property := ⋯ }

theorem hallMatchingsOn.nonempty {ι : Type u} {α : Type v} [DecidableEq α] (t : ι → Finset α) (h : ∀ (s : Finset ι), s.card ≤ (Finset.biUnion s t).card) (ι' : Finset ι) : Nonempty ↑(hallMatchingsOn t ι')

When the Hall condition is satisfied, the set of matchings on a finite set is nonempty. This is where Finset.all_card_le_biUnion_card_iff_existsInjective' comes into the argument.

def hallMatchingsFunctor {ι : Type u} {α : Type v} (t : ι → Finset α) : CategoryTheory.Functor (Finset ι)ᵒᵖ (Type (max u v))

This is the hallMatchingsOn sets assembled into a directed system.

Equations

• One or more equations did not get rendered due to their size.

instance hallMatchingsOn.finite {ι : Type u} {α : Type v} (t : ι → Finset α) (ι' : Finset ι) : Finite ↑(hallMatchingsOn t ι')

Equations

• ⋯ = ⋯

theorem Finset.all_card_le_biUnion_card_iff_exists_injective {ι : Type u} {α : Type v} [DecidableEq α] (t : ι → Finset α) : (∀ (s : Finset ι), s.card ≤ (Finset.biUnion s t).card) ↔ ∃ (f : ι → α), Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

This is the version of Hall's Marriage Theorem in terms of indexed families of finite sets t : ι → Finset α. It states that there is a set of distinct representatives if and only if every union of k of the sets has at least k elements.

Recall that s.biUnion t is the union of all the sets t i for i ∈ s.

This theorem is bootstrapped from Finset.all_card_le_biUnion_card_iff_exists_injective', which has the additional constraint that ι is a Fintype.

instance instFintypeElemImageToSet {α : Type u} {β : Type v} [DecidableEq β] (r : α → β → Prop) [(a : α) → Fintype ↑(Rel.image r {a})] (A : Finset α) : Fintype ↑(Rel.image r ↑A)

Given a relation such that the image of every singleton set is finite, then the image of every finite set is finite.

Equations

• instFintypeElemImageToSet r A = let_fun h := ⋯; Eq.mpr ⋯ (FinsetCoe.fintype (Finset.biUnion A fun (a : α) => Set.toFinset (Rel.image r {a})))

theorem Fintype.all_card_le_rel_image_card_iff_exists_injective {α : Type u} {β : Type v} [DecidableEq β] (r : α → β → Prop) [(a : α) → Fintype ↑(Rel.image r {a})] : (∀ (A : Finset α), A.card ≤ Fintype.card ↑(Rel.image r ↑A)) ↔ ∃ (f : α → β), Function.Injective f ∧ ∀ (x : α), r x (f x)

This is a version of Hall's Marriage Theorem in terms of a relation between types α and β such that α is finite and the image of each x : α is finite (it suffices for β to be finite; see Fintype.all_card_le_filter_rel_iff_exists_injective). There is a transversal of the relation (an injective function α → β whose graph is a subrelation of the relation) iff every subset of k terms of α is related to at least k terms of β.

Note: if [Fintype β], then there exist instances for [∀ (a : α), Fintype (Rel.image r {a})].

theorem Fintype.all_card_le_filter_rel_iff_exists_injective {α : Type u} {β : Type v} [Fintype β] (r : α → β → Prop) [(a : α) → DecidablePred (r a)] : (∀ (A : Finset α), A.card ≤ (Finset.filter (fun (b : β) => ∃ a ∈ A, r a b) Finset.univ).card) ↔ ∃ (f : α → β), Function.Injective f ∧ ∀ (x : α), r x (f x)

This is a version of Hall's Marriage Theorem in terms of a relation to a finite type. There is a transversal of the relation (an injective function α → β whose graph is a subrelation of the relation) iff every subset of k terms of α is related to at least k terms of β.

It is like Fintype.all_card_le_rel_image_card_iff_exists_injective but uses Finset.filter rather than Rel.image.