nLab Engeler's lemma

Contents

Contents

Idea

Engeler’s lemma is one of a number of set-theoretic propositions connected with choice principles and prime ideal/maximal ideal theorems. A key phrase for such set-theoretic propositions is “systems of finite character”; related results include the Teichmüller-Tukey lemma?.

Statement and proof

Theorem

(Engeler’s lemma) Let XX be a set, and let FF be a collection of partial functions f:X2={0,1}f: X \rightharpoonup 2 = \{0, 1\}:

XAf2X \hookleftarrow A \stackrel{f}{\to} 2

where A=dom(f)A = \dom(f) is the domain of ff. Suppose the following 3 conditions are satisfied:

  1. For every f:dom(f)2f: \dom(f) \to 2 in FF and finite subset Sdom(f)S \subseteq \dom(f), the restriction Res S(f):S2Res_S(f): S \to 2 belongs to FF;

  2. If f:X2f: X \rightharpoonup 2 is any partial function such that Res S(f)Res_S(f) belongs to FF for every finite subset Sdom(f)S \subseteq \dom(f), then ff belongs to FF;

  3. Every finite subset SXS \subseteq X is the domain of some fFf \in F.

Then, assuming the ultrafilter principle (UP), there exists a total function fFf \in F.

Proof

We abuse notation by identifying partial functions f:X{0,1}f: X \rightharpoonup \{0, 1\} with total functions X3={0,1,2}X \to 3 = \{0, 1, 2\}, defining dom(f)\dom(f) for f:X3f: X \to 3 in terms of the corresponding partial function: dom(f)={xX:f(x)2}\dom(f) = \{x \in X: f(x) \neq 2\}. For f:X3f: X \to 3, the notation Res S(f)Res_S(f) means we regard ff as a partial function, obtain another partial function by restriction, and consider this a function X3X \to 3.

Thus FF defines a subspace F3 XF \subseteq 3^X. Under UP, the product space 3 X3^X is compact Hausdorff. We claim FF is closed. For suppose f:X3f: X \to 3 is in the closure of FF. This means that for any finite AXA \subseteq X there exists gFg \in F with f| A=g| Af|_A = g|_A. In particular, for any finite Bdom(f)B \subseteq \dom(f) there exists gFg \in F such that f| B=g| Bf|_B = g|_B. In particular g(x)2g(x) \neq 2 for all xBx \in B, so Bdom(g)B \subseteq \dom(g), and so Res B(f)=Res B(g)Res_B(f) = Res_B(g) belongs to FF by condition 1. Since Res B(f)Res_B(f) belongs to FF for all finite Bdom(f)B \subseteq \dom(f), we have that fFf \in F by condition 2. Thus FF is closed, and therefore compact.

Now we claim that the set T={fF: xXf(x)2}T = \{f \in F: \forall_{x \in X} f(x) \neq 2\} is inhabited, which in the partial function interpretation means FF contains a total function. For, the family of closed sets C x=F{f3 X:f(x)2}C_x = F \cap \{f \in 3^X: f(x) \neq 2\} satisfies the finite intersection property, by condition 3. Thus T= xXC xT = \bigcap_{x \in X} C_x is inhabited by compactness of FF.

References

  • Marcel Erné, Prime Ideal Theorems and systems of finite character, Commentationes Mathematicae Universitatis Carolinae, Vol. 38, No. 3 (1997), 513-536. (web)

Created on July 13, 2015 at 03:23:40. See the history of this page for a list of all contributions to it.