In the category of sets, we have a bijective correspondence (up to isomorphism) between surjective functions on and equivalence relations on , where a surjective function is taken to the equivalence relation gotten by pulling back the diagonal of , and an equivalence relation is taken to the function which projects onto the set of -classes. If we replace Set with the category of definable sets of a first-order theory , this correspondence generally fails, because when is a definable equivalence relation, there may not be a corresponding definable . That is to say, internal congruences in are not generally effective.
We say that:
has uniform elimination of imaginaries if the above correspondence does hold, that is, if internal congruences in are effective.
has elimination of imaginaries if for every definable set , there exists a formula and a tuple with the same sort as such that uniquely satisfies
Inside a saturated model , elimination of imaginaries is equivalent to the following statement: for every definable set , there exists a tuple such that for all , setwise if and only if pointwise. This is sometimes called the coding of definable sets.
Poizat noticed that having elimination of imaginaries allows one to develop a classical Galois theory classifying definably-closed extensions of small parameter sets in terms of the closed subgroups of a profinite automorphism group in any sufficiently saturated model of .
The imaginary elements of a theory are precisely -classes, where is a -definable equivalence relation on .
In the process of inventing stability theory, i.e. classifying theories according to the number of isomorphism classes of their models in each cardinality, Shelah found he needed to eliminate imaginaries in a universal way, so he found a way to conservatively interpret each theory in a theory which eliminated all the imaginaries of . The process just involves throwing in for each congruence on a new sort (type in type theory) for and a projection map .
satisfies the following universal property: any theory which interprets and eliminates imaginaries must uniquely interpret as theories under (in the -category of theories and interpretations.)
(Indeed, pretoposes are just toposes that might be missing some power objects. According to the next section, inside a Boolean pretopos these power objects will still be there, just generally only formally.)
If a first-order theory eliminates imaginaries, it interprets infinitely many constants. This is because it interprets at least two constants: a code for the diagonal relation and its complement. Taking binary sequences of these two constants in higher and higher Cartesian products of the model with itself produces infinitely many constants.
The following characterization is due to Moshe Kamensky, and can be found in his categorical internality paper.
Proposition. Let (T) be a first-order theory which interprets two constants. Then eliminates imaginaries if and only if for all and in , the presheaf is ind-representable.
Proof. Suppose first that the presheaves are ind-representable. Let be a definable equivalence relation on . Let classify . Let be the Yoneda embedding. Then has a product-exponential transpose . The Yoneda lemma says that , and by assumption for some a filtered diagram of definable sets. Since this is filtered, the colimit as a set can be computed as
where the equivalence relation identifies elements that are eventually sent to the same element by transition maps in the diagram. Hence, we can identify with its equivalence class of maps . Now, is the kernel pair of in , so . By compactness, we can replace with a finite subset . Since is filtered, there exists a weak coproduct to . Since the turn into a cone to , for each there is a transition map , so . Replacing each with , we see , and is definable.
On the other hand, suppose we have elimination of imaginaries. Fix and . For each and , we may form the equivalence relation on which says if and only if they define the same fiber of . The projection map induces a map
which is also a map of objects over .
Now, the category of elements of the presheaf has objects maps for ranging over , and morphisms from to the maps for such that . For each object , as above coequalizes all pairs of maps in into . Furthermore, the natural projection from by sending creates colimits, in particular finite coproducts, which by assumption exist in . So is filtered, and since for any presheaf , we have that
so is ind-representable.
Remark. In the above proof, complementation is required to characterize compactness as “every covering of a definable set by an infinite family of definable sets is finitely supported.” The same proof works if we replace inner homs with power objects.