mathlib3 documentation

combinatorics.hall.basic

Hall's Marriage Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a list of finite subsets $X_1, X_2, \dots, X_n$ of some given set $S$, P. Hall in [Hal35] 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_bUnion_card_iff_exists_injective' in a separate module.

The theorem can be generalized to remove the constraint that ι be a fintype. As observed in [Hal66], 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 #

Todo #

Tags #

Hall's Marriage Theorem, indexed families

source
def hall_matchings_on {ι : Type u} {α : Type v} (t : ι → finset α) (ι' : finset ι) :
set (↥ι' → α)

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

Equations
Instances for ↥hall_matchings_on
source
def hall_matchings_on.restrict {ι : Type u} {α : Type v} (t : ι → finset α) {ι' ι'' : finset ι} (h : ι' ⊆ ι'') (f : ↥(hall_matchings_on t ι'')) :
↥(hall_matchings_on t ι')

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

Equations
source
theorem hall_matchings_on.nonempty {ι : Type u} {α : Type v} [decidable_eq α] (t : ι → finset α) (h : ∀ (s : finset ι), s.card ≤ (s.bUnion t).card) (ι' : finset ι) :
nonempty ↥(hall_matchings_on t ι')

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

source
def hall_matchings_functor {ι : Type u} {α : Type v} (t : ι → finset α) :
(finset ι)ᵒᵖ ⥤ Type (max u v)

This is the hall_matchings_on sets assembled into a directed system.

Equations
source
@[protected, instance]
def hall_matchings_on.finite {ι : Type u} {α : Type v} (t : ι → finset α) (ι' : finset ι) :
finite ↥(hall_matchings_on t ι')
source
theorem finset.all_card_le_bUnion_card_iff_exists_injective {ι : Type u} {α : Type v} [decidable_eq α] (t : ι → finset α) :
(∀ (s : finset ι), s.card ≤ (s.bUnion 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.bUnion t is the union of all the sets t i for i ∈ s.

This theorem is bootstrapped from finset.all_card_le_bUnion_card_iff_exists_injective', which has the additional constraint that ι is a fintype.

source
@[protected, instance]
def rel.image.fintype {α : Type u} {β : Type v} [decidable_eq β] (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
source
theorem fintype.all_card_le_rel_image_card_iff_exists_injective {α : Type u} {β : Type v} [decidable_eq β] (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})].

source
theorem fintype.all_card_le_filter_rel_iff_exists_injective {α : Type u} {β : Type v} [fintype β] (r : α → β → Prop) [Π (a : α), decidable_pred (r a)] :
(∀ (A : finset α), A.card ≤ (finset.filter (λ (b : β), ∃ (a : α) (H : 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.