Documentation

Mathlib.Combinatorics.Hall.Basic

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 #

TODO #

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
Instances For
    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
    Instances For
      theorem hallMatchingsOn.nonempty {ι : Type u} {α : Type v} [DecidableEq α] (t : ιFinset α) (h : ∀ (s : Finset ι), s.card (s.biUnion t).card) (ι' : Finset ι) :

      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 α) :

      This is the hallMatchingsOn sets assembled into a directed system.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        instance hallMatchingsOn.finite {ι : Type u} {α : Type v} (t : ιFinset α) (ι' : Finset ι) :
        Equations
        • =
        theorem Finset.all_card_le_biUnion_card_iff_exists_injective {ι : Type u} {α : Type v} [DecidableEq α] (t : ιFinset α) :
        (∀ (s : Finset ι), s.card (s.biUnion 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 instFintypeElemImageToSetOfDecidableEqOfSingletonSet {α : 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
        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 : β) => aA, 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.