Combinatorial compactness and the Rado selection lemma

This file contains compactness arguments for constructing infinite objects from finite approximations. The main result is a formalization of Rado's selection principle, as an application of compactness to combinatorics.

We give four versions, depending on whether the "partial" functions are defined locally or globally, and whether we use Finset or Set.Finite. The precise formulation of the lemma is therefore Finset.rado_selection_subtype or Set.Finite.rado_selection_subtype, but the versions avoiding subtypes are easier to prove and often easier to apply, so they are provided too.

Main results

• Finset.rado_selection: Given functions g : Finset α → α → β where β is finite, there exists a single function χ : α → β which is constructed out of g. More precisely, for each finite set s, there exists a larger set t ⊇ s such that χ and g t agree on s. In fact, we can more generally allow each g s to be a dependent function, as (a : α) → β a, so the type of g will be Finset α → (a : α) → β a.

• Finset.rado_selection_subtype: A variant where g takes elements in the subtype.

• Set.Finite.rado_selection: A variant using Set.Finite.

• Set.Finite.rado_selection: A variant using Set.Finite and where g takes elements in the subtype.

Implementation notes

The proof uses the fact that the product of finite discrete spaces is compact (by Tychonoff's theorem). The closed sets corresponding to "agreeing with g s on s" have the finite intersection property, so their intersection is nonempty.

References

• de Bruijn, N. G.; Erdős, P. (1951). "A colour problem for infinite graphs and a problem in the theory of relations".
• Rado, R. (1949). "Axiomatic treatment of rank in infinite sets".

theorem Finset.rado_selection {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : Finset α → (a : α) → β a) : ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α), s ⊆ t ∧ ∀ x ∈ s, χ x = g t x

Given a (dependent) function g s : (a : α) → β a for each finset s of α, provided that each β a is finite, we can find another function χ : (a : α) → β a such that on every s, there is some larger t such that χ agrees with g t on s. Informally, we are stitching together the local functions g s into a global χ such that on each s, χ can be expressed in terms of one of the g.

theorem Finset.rado_selection_subtype {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Finset α) → (a : ↥s) → β ↑a) : ∃ (χ : (a : α) → β a), ∀ (s : Finset α), ∃ (t : Finset α) (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g t (Set.inclusion hst x)

Given a (dependent) function g s : (a : s) → β a for each finset s of α, provided that each β a is finite, we can find another function χ : (a : α) → β a such that on every s, there is some larger t such that χ agrees with g t on s. Informally, we are stitching together the local functions g s into a global χ such that on each s, χ can be expressed in terms of one of the g.

theorem Set.Finite.rado_selection {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Set α) → s.Finite → (a : α) → β a) : ∃ (χ : (a : α) → β a), ∀ (s : Set α), s.Finite → ∃ (t : Set α) (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x

Given a (dependent) function g s : (a : α) → β a for each finite set s of α, provided that each β a is finite, we can find another function χ : (a : α) → β a such that on every s, there is some larger t such that χ agrees with g t on s. Informally, we are stitching together the local functions g s into a global χ such that on each s, χ can be expressed in terms of one of the g.

theorem Set.Finite.rado_selection_subtype {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Set α) → s.Finite → (a : ↑s) → β ↑a) : ∃ (χ : (a : α) → β a), ∀ (s : Set α), s.Finite → ∃ (t : Set α) (ht : t.Finite) (hst : s ⊆ t), ∀ (x : ↑s), χ ↑x = g t ht (inclusion hst x)

Given a (dependent) function g s : (a : s) → β a for each finite set s of α, provided that each β a is finite, we can find another function χ : (a : α) → β a such that on every s, there is some larger t such that χ agrees with g t on s. Informally, we are stitching together the local functions g s into a global χ such that on each s, χ can be expressed in terms of one of the g.