nLab elimination of imaginaries




In the category of sets, we have a bijective correspondence (up to isomorphism) between surjective functions on XX and equivalence relations on XX, where a surjective function π:XY\pi \colon X \to Y is taken to the equivalence relation E πE_{\pi} gotten by pulling back the diagonal of YY, and an equivalence relation EE is taken to the function f Ef_E which projects XX onto the set of EE-classes. If we replace Set with the category of definable sets Def(T)\mathbf{Def}(T) of a first-order theory TT, this correspondence generally fails, because when EE is a definable equivalence relation, there may not be a corresponding definable f Ef_E. That is to say, internal congruences in Def(T)\mathbf{Def}(T) are not generally effective.


We say that:

  1. TT has uniform elimination of imaginaries if the above correspondence does hold, that is, if internal congruences in Def(T)\mathbf{Def}(T) are effective.

  2. TT has elimination of imaginaries if for every definable set X={m𝕄 | φ(m,b)}X = \{m \in \mathbb{M} \operatorname{ | } \varphi(m,b)\}, there exists a formula ψ(x,y)\psi(x,y) and a tuple cc with the same sort as yy such that cc uniquely satisfies X={mM | ψ(m,c)}.X = \{m \in M \operatorname{ | } \psi(m,c)\}.

Inside a saturated model 𝕄T\mathbb{M} \models T, elimination of imaginaries is equivalent to the following statement: for every definable set XX, there exists a tuple cc such that for all σAut(𝕄)\sigma \in \operatorname{Aut}(\mathbb{M}), σ(X)=X\sigma(X) = X setwise if and only if σ(c)=c\sigma(c) = c pointwise. This is sometimes called the coding of definable sets.

Poizat noticed that TT 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 TT.

The imaginary elements of a theory TT are precisely EE-classes, where EE is a 00-definable equivalence relation on TT.

The () eq(-)^{\operatorname{eq}} construction

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 TT in a theory T eqT^{\operatorname{eq}} which eliminated all the imaginaries of TT. The process just involves throwing in for each congruence EE on XX a new sort (type in type theory) for X/EX/E and a projection map XX/EX \twoheadrightarrow X/E.

T eqT^{\operatorname{eq}} satisfies the following universal property: any theory which interprets TT and eliminates imaginaries must uniquely interpret T eqT^{\operatorname{eq}} as theories under TT (in the 22-category of theories and interpretations.)

Makkai realized not long after that the () eq(-)^{\operatorname{eq}} construction corresponded to the pretopos completion of the syntactic category of TT.

(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.)

Relation to ind-representable power objects

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.

In particular, when TT eliminates imaginaries, its syntactic category has finite coproducts. In particular, 2\mathbf{2} exists, and all definable subsets have definable classifying maps.

The following characterization is due to Moshe Kamensky, and can be found here.


Let (T) be a first-order theory which interprets two constants. Then TT eliminates imaginaries if and only if for all XX and YY in Def(T)\mathbf{Def}(T), the presheaf ZHom Def(T)(Z×X,Y)Z \mapsto \operatorname{Hom}_{\mathbf{Def}(T)}(Z \times X, Y) is ind-representable.


Suppose first that the presheaves Y X=dfZHom Def(T)(Z×X,Y)Y^X \overset{\operatorname{df}}{=}Z \mapsto \operatorname{Hom}_{\mathbf{Def}(T)}(Z \times X,Y) are ind-representable. Let EtsXE \overset{s}{\underset{t}{\rightrightarrows}} X be a definable equivalence relation on XX. Let ϕ E:X×X2\phi_E : X \times X \to 2 classify E(s,t)X×XE \overset{(s,t)}{\hookrightarrow} X \times X. Let y:Def(T)Def(T)^\mathbf{y} : \mathbf{Def}(T) \hookrightarrow \widehat{\mathbf{Def}(T)} be the Yoneda embedding. Then yϕ E\mathbf{y} \phi_E has a product-exponential transpose yϕ E¯:yX2 X\overline{\mathbf{y} \phi_E} : \mathbf{y}X \to 2^X. The Yoneda lemma says that Hom Def(T)^(yX,2 X)2 X(X)\operatorname{Hom}_{\widehat{\mathbf{Def}(T)}}(\mathbf{y}X, 2^X) \simeq 2^X(X), and by assumption 2 X(X)limHom(X,J(i))2^X(X) \simeq \underset{\longrightarrow}{\lim}\operatorname{Hom}(X,J(i)) for some J:IDef(T)J : I \to \mathbf{Def}(T) a filtered diagram of definable sets. Since this is filtered, the colimit as a set can be computed as

iIJ(i)/,\bigsqcup_{i \in I} J(i) / \sim,

where the equivalence relation \sim identifies elements that are eventually sent to the same element by transition maps in the diagram. Hence, we can identify yϕ E¯\overline{\mathbf{y}\phi_E} with its equivalence class of maps {ϕ i:XJ(i)} iI\{\phi_i : X \to J(i)\}_{i \in I}. Now, yE\mathbf{y}E is the kernel pair of yϕ E¯\overline{\mathbf{y} \phi_E} in Def(T)^\widehat{\mathbf{Def}(T)}, so E= iIker(ϕ i)E = \bigvee_{i \in I} \ker(\phi_i). By compactness, we can replace II with a finite subset I 0II_0 \subseteq I. Since II is filtered, there exists a weak coproduct jj to I 0I_0. Since the {ϕ i} iI\{\phi_i\}_{i \in I} turn XX into a cone to JJ, for each iI 0i \in I_0 there is a transition map h ij:J(i)J(j)h_{ij} : J(i) \to J(j), so ker(ϕ j)=ker(h ijϕ i)ker(ϕ i)\ker(\phi_j) = \ker(h_{ij} \circ \phi_i) \supseteq \ker(\phi_i). Replacing each ker(ϕ i)\ker(\phi_i) with ker(ϕ j)\ker(\phi_j), we see E=ker(ϕ j)E = \ker(\phi_j), and ϕ j\phi_j is definable.

On the other hand, suppose we have elimination of imaginaries. Fix XX and YY. For each ZZ and f:Z×XYf : Z \times X \to Y, we may form the equivalence relation E fE_f on ZZ which says z 1 E fz 2z_1 \sim_{E_f} z_2 if and only if they define the same fiber of Γ(f)\Gamma(f). The projection map induces a map

(/E f)×X:Z×XZ/E f×X(-/E_f) \times X : Z \times X \to Z/E_f \times X

which is also a map ff/E ff \to f/E_f of objects over YY.

Now, the category of elements Pt(1,Y X)\operatorname{Pt}(1, Y^X) of the presheaf Hom(×X,Y)\operatorname{Hom}(- \times X, Y) has objects maps f:Z×XYf : Z \times X \to Y for ZZ ranging over Def(T)\mathbf{Def}(T), and morphisms from f 1:Z 1×XYf_1 : Z_1 \times X \to Y to f 2:Z 2×XYf_2 : Z_2 \times X \to Y the maps g×X:Z 1×XZ 2×Xg \times X : Z_1 \times X \to Z_2 \times X for g:Z 1Z 2g : Z_1 \to Z_2 such that f 1=f 2gf_1 = f_2 \circ g. For each object fPt(1,Y X)f \in \operatorname{Pt}(1, Y^X), /E f×X-/ E_f \times X as above coequalizes all pairs of maps in Pt(1,Y X)\operatorname{Pt}(1, Y^X) into ff. Furthermore, the natural projection pp from Pt(1,Y X)Def(T)\operatorname{Pt}(1, Y^X) \to \mathbf{Def}(T) by sending f:Z×XYZf : Z \times X \to Y \mapsto Z creates colimits, in particular finite coproducts, which by assumption exist in Def(T)\mathbf{Def}(T). So Pt(1,Y X)\operatorname{Pt}(1, Y^X) is filtered, and since for any presheaf PP, we have that

Plim(Pt(1,P)pDef(T)yDef(T)^),P \simeq \underset{\longrightarrow}{\lim}\left(\operatorname{Pt}(1,P) \overset{p}{\to} \mathbf{Def}(T) \overset{\mathbf{y}}{\hookrightarrow} \widehat{\mathbf{Def}(T)}\right),

so Y XY^X is ind-representable.


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.

Imaginaries and automorphisms

Let MTM \models T be a model. If a formula φ(x 1,x 2)\varphi(x_1, x_2) is a 00-definable equivalence relation EE (i.e. an internal congruence in Def(T)\mathbf{Def}(T)) on a definable set XX, any automorphism σ\sigma of MM must preserve and reflect EE-equivalence, so that σ\sigma extends along XX/EX \twoheadrightarrow X/E to a permutation on X/EX/E. So automorphisms of models “already see” imaginaries. This can be stated rigorously as: the expansion of a monster model 𝕄\mathbb{M} of TT to a monster model 𝕄 eq\mathbb{M}^{\operatorname{eq}} of T eqT^{\operatorname{eq}} will have the same automorphism group as 𝕄\mathbb{M}.

To make things concrete, let’s consider the structure (,+)(\mathbb{Z}, +). Since there is an automorphism which switches signs, the only constant is 00. So the theory of this structure cannot eliminate imaginaries, since such theories must interpret infinitely many distinct constants.

However, we can tell that this structure has many imaginaries by its rigidity: the above automorphism is the only nontrivial one. This is because any such automorphism of (,+)(\mathbb{Z},+) must also act on the internal congruences E nE_n which say

x E nyxy(modn)()[xy=+ (n times) +],x \sim_{E_n} y \iff x \equiv y (\operatorname{mod} n) \iff (\exists \ell)\left[x - y = \ell + \dots \text{ (n times) } \dots + \ell\right],

that is, must extend along the abelian group epimorphisms /n\mathbb{Z} \twoheadrightarrow \mathbb{Z}/n\mathbb{Z} for each nn, so that kkk \mapsto -k is the only one that works.

(It’s essentially for this reason that the automorphism group of the forgetful functor GrpSet\mathbf{Grp} \to \mathbf{Set} is also /2\mathbb{Z}/2 \mathbb{Z}.)


  • Bruno Poizat, Une théorie de Galois imaginaire, J. Symbolic Logic 48 (1984), no.4, 1151-1170, MR85e:03083, doi

  • wikipedia imaginary element

  • Anand Pillay, Some remarks on definable equivalence relations in O-minimal structures, J. Symbolic Logic 51 (1986), 709-714, MR87h:03046, doi

  • Jan Holly, Definable operations on sets and elimination of imaginaries, Proc. Amer. Math. Soc. 117 (1993), no. 4, 1149–1157, MR93e:03052, doi, pdf

  • Ehud Hrushovski, Groupoids, imaginaries and internal covers, arxiv/math.LO/0603413; On finite imaginaries, arxiv/0902.0842

  • D. Haskell, E. Hrushovski, H.D.Macpherson, Definable sets in algebraically closed valued fields: elimination of imaginaries, J. reine und angewandte Mathematik 597 (2006)

  • Saharon Shelah, Classification theory and the number of non-isomorphic models, Studies in Logic and the Foundations of Mathematics 92, North Holland, Amsterdam 1978

  • Moshe Kamensky, A categorical approach to internality

Last revised on June 9, 2017 at 23:25:20. See the history of this page for a list of all contributions to it.