nLab choice object

Choice objects

Choice objects

Definitions and terminology

As it is used here, and by (at least some) topos theorists, a choice object is an object BB such that the axiom of choice holds when making choices from BB.

By contrast, a projective object is an object AA such that AC holds when making choices indexed by AA.

Confusingly, some constructivists use “choice set” to mean what we call a “projective set”.


One way to state the axiom of choice is that every entire relation from AA to BB (so that every element of AA is related to some element of BB) contains (the graph of) a function ABA\to B. With this terminology, we may say that

  • AA is projective iff every entire relation from AA to BB, for any BB, contains a function ABA\to B, while
  • BB is choice iff every entire relation from AA to BB, for any AA, contains a function ABA\to B.

Equivalently (at least, in a topos) BB is choice iff it has a choice function: a function c:P +BBc\colon P^+B \to B such that c(x)xc(x)\in x for all xP +Bx\in P^+B. Here P +BP^+B is the object of all inhabited subsets of BB. We can also say that an object is choice if and only if it is classically well-orderable (that is, it admits a total order where every inhabited subset has a least element); see D4.5.13 in the Elephant.

In constructive mathematics, the principle of excluded middle is equivalent to the statement that the set 2={ab}2 = \{a \ne b\} is a choice set.


Last revised on September 25, 2020 at 14:48:01. See the history of this page for a list of all contributions to it.