Definition. — Let $T$ be a theory in a language $L$. One says that $T$ eliminates imaginaries (resp. weakly eliminates imaginaries) if for every model $M$ and every formula $f(x;a)$ with parameters $a\in M^p$, there exists a formula $g(x;y)$ such that $\{ b\in M^q\;;\; \forall x, f(x;a)\Leftrightarrow g(x;b)\}$ is a singleton (resp. is a non-empty finite set).
What does this mean? View the formula $f(x;y)$ as defining a family of definable subsets, where $f(x;a)$ is the slice given by the choice of parameters $a$. It may happen that many fibers are equal. The property of elimination of imaginaries asserts that one can define the same family of definable subsets via another formula $g(x;y)$, with different parameters, so that every definable set in the original family appears once and only once. For the case of weak elimination, every definable set of the initial family appears only finitely times.
There is an alternative, Galois theoretic style, description: a theory $T$ (weakly) eliminates imaginaries if and only if, for every formula $f(x;a)$ with parameters in a model $M$, there exists a finite subset $B\subset M$ such that for every elementary extension $N$ of $M$ and every automorphism $\sigma$ of $N$, then $\sigma$ preserves the formula (meaning $f(x;a)\leftrightarrow f(\sigma(x);a)$, or, equivalently, $\sigma$ leaves globally invariant the definable subset of $N^n$ defined by the formula $f(x;a)$) if and only if $\sigma$ leaves $B$ pointwise (resp. globally) invariant. One direction is obvious: take for $B$ the coordinates of the elements of the singleton (resp. the finite set) given by applying the definition. For the converse, elementary extensions must enter the picture because some models are too small to possess the necessary automorphisms that should exist; under “saturation hypotheses”, the model $M$ will witness them already.
This property is related to the possibility of representing equivalence classes modulo a definable equivalence relation. Namely, let $M$ be a model and let $E$ be an equivalence relation on $M^n$ whose graph is a definable subset of $M^n\times M^n$. Assume that the theory $T$ eliminates imaginaries and allows to define two distinct elements. Then there exists a definable map $f_E\colon M^n\to M^m$ such that for every $y,z\in M^n$, $y \mathrel{E} z$ if and only if $f_E(y)=f_E(z)$. In particular, the quotient set $M^n/E$ is represented by the image of the definable map $f_E$.
Conversely, let $f(x;a)$ be a formula with parameters $a\in M^p$ and consider the equivalence relation $E$ on $M^p$ given by $yEz$ if and only if $\forall x,\ f(x;y)\Leftrightarrow f(x;z)$. Its graph is obviously definable. Assume that there exists a definable map $f_E\colon M^p\to M^q$ such that $yEz$ if and only if $f_E(y)=f_E(z)$. Then an automorphism of (an elementary extension of) $M$ will fix the definable set defined by $f(x;a)$ if and only if it fixes $f_E(a)$, so that one has elimination of imaginaries.
Theorem (Poizat). — The theory of algebraically closed fields eliminates imaginaries.
This is more or less equivalent to Weil's theorem on the field of definition of a variety. It is my feeling, however, that this property is under-estimated in algebraic geometry. Indeed, it is closely related to a theorem of Rosenlicht that asserts that given a variety $X$ and an algebraic group $G$ acting on $X$, there exists a dense $G$-invariant open subset $U$ of $X$ such that a geometric quotient $U/G$ exists in the sense of Mumford's Geometric Invariant Theory.
Examples. — Let $K$ be an algebraically closed field.
a) Let $X$ be a Zariski closed subset of $K^n$ and let $G$ be a finite group of (regular) automorphisms of $X$. Let us consider the formula $f(x;y)=\bigwedge_{g\in G} (x=g\cdot y)$ which asserts that $x$ belongs to the orbit of $G$ under the given action, so that $f(x;y)$ parameterizes $G$-orbits. Since $G$ is finite, weak elimination of imaginaries is a trivial matter, but elimination of imaginaries is possible. Let indeed $A$ be the affine algebra of $X$; this is a $K$-algebra of finite type with an action of $G$ and the algebra $A^G$ is finitely generated. Consequently, there exists a Zariski closed subset $Y$ of some $K^m$ and a polynomial morphism $\phi\colon K^n\to K^m$ such that, for every $y,z\in X$, $\phi(y)=\phi(z)$ if and only if there exists $g\in G$ such that $z=g\cdot y$. Consequently, for $a\in X$, $b=\phi(a)$ is the only element such that the formula $f(x;a)$ be equivalent to the formula $g(x;b)=(b\in Y) \wedge (\exists y\in X)(\phi(y)=b) \wedge f(x;y))$.
The simplest instance would be the symmetric group $G=\mathfrak S_n$ acting on $K^n$ by permutation of coordinates. Then $G$-orbits are unordered $n$-tuples of elements of $K$, and it is a both trivial and fundamental fact that the orbit of $(x_1,\dots,x_n)$ is faithfully represented by the first $n$ elementary symmetric functions of $(x_1,\dots,x_n)$, equivalently, by the coefficients of the polynomial $\prod_{j=1}^n (T-x_j)$.
b) Let $X=K^{n^2}$ be the set of all $n\times n$ matrices under which the group $G=\mathop{\rm GL}(n,K)$ acts by conjugation. The Jordan decomposition gives a partition of $X$ into constructible sets, stable under the action of $G$, and on each of them, there exists a regular representation of the equivalence classes. For example, the set $U$ of all matrices with pairwise distinct eigenvalues is Zariski open — it is defined by the non-vanishing of the discriminant of the characteristic polynomial — and on this set $U$, the conjugacy class of a matrix is represented by its characteristic polynomial.
Theorem. — An o-minimal theory eliminates imaginaries. More precisely any surjective definable map $f\colon X\to Y$ between definable sets admits a definable section.
This follows from the fact that one can define a canonical point in every non-empty definable set. By induction on dimension, it suffices to prove this for a subset $A$ of the line. Then, let $J_A$ be the leftmost interval of $A$ (if the formula $f$ defines $f$, then $J_A$ is defined by the formula $y\leq \rightarrow f(y)$); let $u$ and $v$ be the “endpoints” of $J_A$; if $u=-\infty$ and $v=+\infty$, set $x_A=0$; if $u=-\infty$ and $v<\infty$, set $x_A=v-1$; if $-\infty<u\leq v<+\infty$, set $x_A=(u+v)/2$. It is easy to write down a formula that expresses $x_A$ in terms of a formula for $A$. Consequently, in a family $A_t\subset M$ of non-empty definable sets, the function $t\mapsto x_{A_t}$ is definable.
Theorem (Poizat). — The theory of differentially closed fields eliminates imaginaries in the language $\{+,-,\cdot,0,1,\partial\}$.
Examples. — Let $K$ be an algebraically closed differential field. Let $X$ be an algebraic variety with the action of an algebraic group $G$, all defined over the field of constants $C=K^\partial$. We can then endow $X(K)$ with the equivalence relation given by $x\sim y$ if and only if there exists $g\in G(C)$ such that $y=g\cdot x$. The following three special instances of elimination of imaginaries in DCF are classical results of function theory:
a) If $X=\mathbf A^1$ is the affine line and $G=\mathbf G_a$ is the additive group acting by translation, then the map $\partial\colon x\mapsto \partial (x)$ gives a bijection from $X(K)/G(C)$ to $K$. Indeed, two elements $x,y$ of $K$ differ by the addition of a constant element if and if $\partial(x)=\partial(y)$. (Moreover, every element of $K$ has a primitive.)
b) Let $X=\mathbf A^1\setminus\{0\}$ be the affine line minus the origin and let $G=\mathbf G_m$ be the multiplicative group acting by multiplication. Then the logarithmic derivative $\partial\log\colon x\mapsto \partial(x)/x$ gives a bijection from $X(K)/G(C)=K^\times/C^\times$ to $K$ — two elements $x,y$ of $K^\times$ differ by multiplication by a constant if and only if $\partial(x)/x=\partial(y)/y$, and every element of $K$ is a logarithmic derivative.
c) Let $X=\mathbf P^1$ be the projective line endowed with the action of the group $G=\operatorname{\rm PGL}(2)$. Then two points $x,y\in X(K)$ differ by an action of $G(C)$ if and only if their Schwarzian derivatives are equal, where the Schwarzian derivative of $x\in K$ is defined by
\[ S(x) = \partial\big(\partial^2 (x)/\partial (x)\big) -\frac12 \big(\partial^2(x)/\partial(x)\big). \]
Link to Part 5 — Algebraic differential equations from coverings
