compact element

Compact/finite elements


Let PP be a poset such that every directed subset of PP has a join; that is, PP is a dcpo. A compact element, or finite element, of PP is a compact object in PP regarded as a thin category; that is, homs out of it commute with these directed joins.

In other words, cPc \in P is compact precisely if for every directed subset {d i}\{d_i\} of PP we have

(c id i) i(cd i). (c \leq \bigvee_i d_i ) \Leftrightarrow \exists_i (c \leq d_i) \,.

Of course, the \Leftarrow part of this is automatic, so the real condition is the \Rightarrow part. In more elementary terms:

In the case where PP has a top element 11, we say that PP is compact if 11 is a compact element.