# Imaginaries in equicharacteristic zero henselian fields

Silvain Rideau-Kikuchi and Mariana Vicaría

###### Abstract

We prove an elimination of imaginaires results for (almost all) henselian
valued fields of equicharacteristic zero. To do so, we consider a mix of sorts
introduced in earlier works of the two authors and define a generalized
version of the k-linear sorts. Under technical assumptions on the value group
we prove that the imaginaries of such a valued field can be elimininated in
the field, the k-linear sorts and the imaginaries of the value group.

##  1 Introduction

In the model theory of valued fields, one of the most striking results is a
theorem by Ax, Kochen and, independently, Ershov which roughly states that the
first-order theory of an unramified henselian valued field is completely
determined by the first-order theory of its residue field $\mathrm{k}$ and of
its value group $\Gamma$. A natural philosophy follows from this theorem: the
model theory of a henselian valued field is controlled by its residue field
and its value group.

In this paper we show that this philosophy also applies to the question of
eliminating imaginaries — essentially, the classification of quotients of
definable sets by definable equivalence relations.

Over the past thirty years, the imaginaries in various henselian valued fields
have been classified, starting with the case of algebraically closed field
with a non-trivial valuation ($\mathrm{ACVF}$) in the foundational work by
Haskell, Hrushovski and Macpherson [HHM06]. This work laid the groundwork for
a “geometric model theory” of valued fields. They proved that $\mathrm{ACVF}$
eliminates imaginaries down to the _geometric sorts_ : the main field
$\mathrm{K}$, and, for all $n\in\mathbb{Z}_{>0}$, the space
$\mathrm{S}_{n}:=\mathrm{GL}_{n}(K)/\mathrm{GL}_{n}(\mathcal{O})$ of free rank
$n$ $\mathcal{O}$-submodules of $\mathrm{K}^{n}$ and the space
$\mathrm{T}_{n}=\bigsqcup_{R\in\mathrm{S}_{n}}R/\mathfrak{m}R$, where
$\mathcal{O}$ denotes the valuation ring and
$\mathfrak{m}\subseteq\mathcal{O}$ is the unique maximal ideal. These results
were later extended to other classes of (enriched) henselian fields [Mel06,
HMR18, HKR18, Rid19].

In the early 2000, Hrushovski asked if such results could be explained by
general result and proposed a classification reminiscent of the Ax-Kochen-
Ershov principle. This paper provides a positive answer to this question for a
broad class of henselian valued fields of equicharacteristic zero.

As can be expected, the natural obstruction to the elimination of imaginaries
in valued fields come in two flavors: those coming from the residue field,
studied in work of Hils and the first author [HR21], and those coming from the
value group, studied in work of the second author [Vic23].

###  1.1 Obstructions arising from the residue field

In [HR21], Hils and the first author assume the value group to be definably
complete — this only allows divisible ordered abelian groups and
$\mathbb{Z}$-groups — and classify the imaginaries that might arise. This
includes the imaginaries of the residue field $\mathrm{k}$, which might be
arbitrarily complicated, but also linearly twisted versions.

Given a free rank $n$ $\mathcal{O}$-submodule $R\subseteq K^{n}$, the quotient
module $R/\mathfrak{m}R$ is a $\mathrm{k}$-vector space of dimension $n$, on
which $\mathrm{k}$ induces a non-trivial structure. Once we name a basis,
$R/\mathfrak{m}R$ is definably isomorphic to $\mathrm{k}^{n}$, but without
that basis, imaginaries of $R/\mathfrak{m}R$ cannot be identified with
imaginaries of $\mathrm{k}$.

The structure $(\mathrm{k},R/\mathfrak{m}R)$ can be seen as a structure in the
language $\mathfrak{L}_{\mathrm{vect}}$ with two sorts:

  * •

a field sort $\mathrm{k}$ with the ring language,

  * •

a vector space sort $\mathrm{V}$ with the (additive) group language,

  * •

A function $\lambda:\mathrm{k}\times\mathrm{V}\rightarrow\mathrm{V}$
interpreted as scalar multiplication.

Given an $\emptyset$-interpretable set $X$ in the
$\mathfrak{L}_{\mathrm{vect}}$-theory of dimension $n$ vector spaces, the
interpretable sets $X^{(\mathrm{k},R/\mathfrak{m}R)}$ has to be accounted for.
To do so, one introduces

$\mathrm{T}_{n,X}=\bigsqcup_{R\in\mathrm{S}_{n}}X^{(k,R/\mathfrak{m}R)}$

and the _$\mathrm{k}$ -linear sorts_

$\mathrm{k}^{\mathrm{leq}}=\bigsqcup_{n,X}\mathrm{T}_{n,X}.$

In fact, it suffices to consider interpretable sets $X$ that are quotients of
$\mathrm{V}$ (and not some power of $\mathrm{V}$ and $\mathrm{k}$). Note that
if $X=\mathrm{V}$ then $\mathrm{T}_{n,X}=\mathrm{T}_{n}$, and if $X$ is the
one element quotient of $V$ then $\mathrm{T}_{n,X}\cong\mathrm{S}_{n}$.

One of the main result of [HR21], is that, under some hypothesis on
$\mathrm{k}$, these are the only obstructions to elimination of imaginaries:

######  Theorem 1.1 ([HR21, Theorem 6.1.1]).

Let $K$ be a henselian valued field of equicharacteristic zero such that:

  * •

The value group is definably complete;

  * •

The residue field eliminates $\exists^{\infty}$.

Then $K$ has weak elimination of imaginaries down to
$\mathrm{K}\cup\mathrm{k}^{\mathrm{leq}}\cup\Gamma$.

This result can be generalized to finite ramification and certain difference
valued fields and is resplendent in $\mathrm{k}$ and $\Gamma$.

###  1.2 Obstructions arising from the value group

In [Vic23], the second author studied imaginaries in equicharacteristic zero
henselian valued fields with algebraically closed residue field. The
complexity of the value group directly impacts the complexity of definable
$\mathcal{O}$-modules and this needs to be taken in account.

This can be done by introducing the _stabilizer sorts_ which provide codes for
all the definable $\mathcal{O}$-submodules of $\mathrm{K}^{n}$, for any $n$.
More precisely, let $\mathcal{C}=(\mathcal{C}_{c})_{c\in\mathrm{Cut}^{\star}}$
be a definable family of proper cuts in $\Gamma$ such that any definable
proper cut is of the of form $\gamma+\mathcal{C}_{c}$ for some unique
$\gamma\in\Gamma(K)$ and $c\in\mathrm{Cut}^{\star}(K)$. For every
$c\in\mathrm{Cut}^{\star}$, let $\mathrm{I}_{c}$ denote the
$\mathcal{O}$-submodule
$\\{x\in\mathrm{K}:\mathrm{v}(x)\in\mathcal{C}_{c}\\}$. and, for every tuple
$c\in\mathrm{Cut}^{\star}$, let $\Lambda_{c}$ be the module
$\sum_{i}I_{c_{i}}e_{i}$, where $(e_{i})_{i<n}$ is the canonical basis of
$\mathrm{K}^{n}$.

The group $\mathrm{B}_{n}$ of upper triangular matrices acts on the set of all
definable $\mathcal{O}$-submodules of $\mathrm{K}^{n}$, and we define

$\mathrm{Mod}_{c}=\mathrm{B}_{n}/\operatorname{Stab}(\Lambda_{c})\text{ and
}\mathrm{Mod}=\bigsqcup_{c}\mathrm{Mod}_{c}.$

In [Vic23], the second author proved that, under some hypothesis on the value
group, the stabilizer sorts are the only obstructions to elimination of
imaginaries:

######  Theorem 1.2 ([Vic23, Theorem 5.12]).

Let $K$ be a valued field of equicharacteristic zero, such that:

  * •

the residue field algebraically closed;

  * •

the value group of _bounded regular ranks_ — _i.e._ it has countably many
definable convex subgroups.

Then $K$ admits weak elimination of imaginaries down to
$\mathrm{K}\cup\mathrm{Mod}\cup\Gamma^{eq}$.

###  1.3 An imaginary Ax-Kochen-Ershov principle

In this paper, building on those previous works, we provide a common
generalization of both Theorems 1.1 and 1.2, obtaining a general Ax-Kochen-
Ershov principle for the classification of imaginaries, under a technical
assumption of the value group:

######  Definition 1.3.

We say that an (enriched) ordered group $G$ satisfies Property D if for every
finite set of formulas $\Delta(x,y)$ containing the formula $x<y_{0}$, any
$A=\mathrm{acl}(A)\subseteq G^{\mathrm{eq}}$ and any $\Delta$-type $p(x)$ that
is $A$-definable, there is an $A$-definable complete type $q(x)$ containing
$p$.

This is a stronger property than the density of definable types, and it holds
in ordered abelian groups of bounded regular rank.

We also introduce a version of the $\mathrm{k}$-linear sorts adapted to this
new setting where more $\mathcal{O}$-modules might arise. This also provides
an encoding of the stabilizer sorts which is more alike the geometric sorts of
[HHM06]. Let
$\mathrm{Cut}^{\star\star}=\mathrm{Cut}^{\star}\setminus\\{0^{+}\\}$ — unless
the value group is discrete, in which case
$\mathrm{Cut}^{\star\star}=\mathrm{Cut}^{\star}$. A module $R$ is said to be
$\mathfrak{m}$-avoiding if it is (coded) in $\mathrm{Mod}_{c}$, for some tuple
$c\in\mathrm{Cut}^{\star\star}$. The dimension of $R/\mathfrak{m}R$ only
depends on $c$ — it is equal to $r=|\\{i:\mathcal{C}_{c_{i}}=0^{-}\\}|$.

For every $\emptyset$-interpretable quotient $X$ of $\mathrm{V}$ in the
$\mathfrak{L}_{\mathrm{vect}}$-theory of dimension $r$ vector spaces, We
define

$\mathrm{T}_{c,X}=\bigsqcup_{R\in\mathrm{Mod}_{c}}X^{(\mathrm{k},R/\mathfrak{m}R)}$

and the _(generalized) $\mathrm{k}$-linear imaginaries_:

$\mathrm{k}^{\mathrm{leq}}=\bigsqcup_{c\in\mathrm{Cut}^{\star\star},X}\mathrm{T}_{c,X}.$

Among those, we denote
$\mathrm{S}=\bigsqcup_{c\in\mathrm{Cut}^{\star\star}}\mathrm{Mod}_{c}$ and
$\mathrm{T}=\bigsqcup_{c\in\mathrm{Cut}^{\star\star}}\mathrm{T}_{c,\mathrm{V}}$.
Along with $\mathrm{K}$, these form the _(generalized) geometric sorts_ , and
they encode all $\mathcal{O}$-definable submodules of $\mathrm{K}^{n}$, for
any $n$.

Our main results are the following:

######  Theorem (Theorem 6.5).

Let $M$ be a $\mathrm{k}$-$\Gamma$-expansion of a model of
$\mathrm{Hen}_{0,0}$ — that is a $\mathrm{k}$-expansion of a
$\Gamma$-expansion. Assume that:

  * •

the value group satisfies Property D,

  * •

_one_ of the following conditions holds:

    1. (a)

for every $n\in\mathbb{Z}_{\geq 0}^{\geq 2}$ one has $[\Gamma:n\Gamma]<\infty$
and the pre-image in $\mathrm{RV}$ of any coset of $n\Gamma$ contains a point
which is algebraic over $\emptyset$;

    2. (b)

or, the multiplicative group $k^{\times}$ is divisible.

Then $M$ has weak elimination of imaginaries in
$K\cup\mathrm{k}^{\mathrm{leq}}\cup\Gamma^{\mathrm{eq}}$.

Without condition (a) or (b), the short exact sequence

$1\to\mathrm{k}^{\star}\to\mathrm{K}^{\star}/(1+\mathfrak{m})\to\Gamma\to 0$

might not eliminate imaginaries, creating further obstructions. This is not an
issue in presence of an angular component, _i.e._ a section of this short
exact sequence.

######  Theorem (Theorem 6.6).

Let $M$ be a $\mathrm{k}$-$\Gamma$-expansion of a model of
$\mathrm{Hen}_{0,0}$ with an angular component. Assume that the value group
satisfies property D. Then $M$ weakly eliminates imaginaries in
$K\cup\mathrm{k}^{\mathrm{leq}}\cup\Gamma^{\mathrm{eq}}$.

###  1.4 Overview of the paper

In Section 2 we present background results on henselian valued fields of
equicharacteristic zero. In Section 3, we introduce the stabilizer sorts and
prove a unary decomposition (LABEL:decompsolv). We also show that modules can
be encoded in the (generalized) geometric sorts, and we classify
$\mathrm{k}$-internal sets in the geometric sorts (LABEL:almostk_int).

In Section 4, we show that definable types in the structure induced from the
maximal unramified algebraic extension are dense, _cf._ Theorem 4.1. This is
the first main step of the proof. Density of definable types is a cornerstone
of recent work on elimination of imaginaries, but it cannot hold in an
arbitrary (equicharacteristic zero) henselian field $K$ due to the complexity
of the residue field. However, the second author showed ([Vic23, Theorem 5.9])
that its holds in its maximal unramified algebraic extension $K^{\mathrm{ur}}$
(assuming Property D). In Section 4, we show that the definable types in
$K^{\mathrm{ur}}$ are also dense among the sets definable in $K$. The main new
challenge is to relate the germs of functions definable in $K$ to those of
functions definable in $K^{\mathrm{ur}}$ — see Section 4.3.

In Section 5, we show that partial definable types build in Section 4 have
completions that are invariant over $\mathrm{RV}$ and families of
$\mathrm{k}$-vector spaces of the form $R/\mathfrak{m}R$ for some
$\mathfrak{m}$-avoiding definable modules $R$. This is the second main step of
the proof. The bulk of the work (Proposition 5.16) revolves around showing
that geometric points can be lifted to the valued field by a sufficiently
invariant type. This, in turn, relies heavily on the computation of germs of
function into sets of the form $R/\mathfrak{m}R$ — _cf._ Proposition 5.4.

Finally, in Section 6, we wrap everything together and show our two main
theorems.

### Acknowledgments

S. Rideau-Kikuchi was partially supported by GeoMod AAPG2019 (ANR-DFG),
Geometric and Combinatorial Configurations in Model Theory. The authors also
wish to thank E. Hrushovski, T. Scanlon and P. Simon for many enlightening
discussions on this topic.

##  2 Equicharacteristic zero henselian fields

Throughout this text, whenever $X$ is a definable set and $A$ is a subset of a
structure, $X(A)$ denotes $X\cap A$. We change structures too often to not be
explicit with the definable closures at play.

Le $\mathrm{Hen}_{0,0}$ be the theory of residue characteristic zero valued
fields $(\mathrm{K},\mathrm{v})$ in some language $\mathfrak{L}$. The exact
language we use does not matter much since we really work in
$\mathfrak{L}^{\mathrm{eq}}$. In this section, we recall some useful results
about these structures. We denote by $\mathrm{RV}^{\star}$ the group
$\mathrm{K}^{\star}/(1+\mathfrak{m})$, where $\mathfrak{m}$ is the maximal
ideal of the valuation ring $\mathcal{O}\subseteq\mathrm{K}$ and
$\mathrm{rv}:\mathrm{K}\to\mathrm{RV}=\mathrm{RV}^{\star}\cup\\{0\\}$ the
canonical projection (extended by $\mathrm{rv}(0)=0$). Let
$M\models\mathrm{Hen}_{0,0}$ and $A\leq\mathrm{K}(M)$.

######  Theorem 2.1 ([Bas91, Theorem B]).

Every $A$-definable subset of $\mathrm{K}^{x}\times\mathrm{RV}^{y}$ is of the
form $\\{(x,y):(\mathrm{rv}(P(x)),y)\in X\\}$, for some tuple $P\in A[x]$ and
some $X\subseteq\mathrm{RV}^{n}$ which is $\mathrm{rv}(A)$-definable in the
short exact sequence

$1\to\mathrm{k}^{\star}\to\mathrm{RV}^{\star}\to\Gamma\setminus\\{\infty\\}\to
0.$

where $\mathrm{k}=\mathcal{O}/\mathfrak{m}$ is the residue ring and
$\Gamma=\mathrm{v}(\mathrm{K})$ is the ordered value group. Moreover, this
remains true in $\mathrm{RV}$-expansions.

From the result above, either by adding a section or proving a quantifier
elimination result for short exact sequences, we can deduce the following:

######  Proposition 2.2.

The sets $\mathrm{k}$ and $\Gamma$ are stably embedded (with respectively the
structure of a field and an ordered group) and they are orthogonal. In other
words, any $M$-definable subset of $\mathrm{k}^{x}\times\Gamma^{y}$ is a
finite union of products $X\times Y$ where $X$ is definable in the field
$\mathrm{k}$ and $Y$ is definable in the ordered group $\Gamma$.

Moreover, any $A$-definable $X\subseteq\Gamma^{n}$ is
$\mathrm{v}(A)$-definable. In particular,

$\Gamma^{\mathrm{eq}}(\mathrm{acl}(A))\subseteq\mathrm{acl}(\mathrm{v}(A)).$

These results remain true in $\mathrm{k}$-$\Gamma$-expansions.

Theorem 2.1 can also be refined for unary sets — showing that
$\mathrm{Hen}_{0,0}$ is 0-h-minimal.

######  Proposition 2.3 ([Fle11, Proposition 3.6]).

Let $X\subseteq\mathrm{K}\times\mathrm{RV}^{n}$ be $A$-definable. There exists
an $A$-definable finite set $C\subseteq\mathrm{K}$ such that for every
$\xi\in\mathrm{RV}^{n}$, $X_{\xi}=\\{x\in\mathrm{K}:(x,\xi)\in
X\\}=\mathrm{rv}_{C}^{-1}(\mathrm{rv}_{C}(X_{\xi}))$ where
$\mathrm{rv}_{C}(x)=(\mathrm{rv}(x-c))_{c\in C}$.

In other words, for any ball $b$ that does not intersect $C$, $b\cap
X_{\xi}=b$ or $b\cap X_{\xi}=\emptyset$.

######  Definition 2.4.

Let $a\in\mathrm{K}(M)$ and let $C$ be a cut in $\Gamma(M)$ — that is, an
upwards closed subset. We define the generalized ball $b_{C}(a)$ of cut $C$
around $a$ to be $\\{x\in\mathrm{K}:\mathrm{v}(x-a)\in C\\}$. A generalized
ball is open if its cut is not of the form $\Gamma_{\geq\gamma}$, for some
$\gamma\in\Gamma(M)$.

Let $\mathrm{B_{g}}$ denote the set of (codes for) generalized balls.

Note that, for every $\gamma\in\Gamma(M)$, $b_{\Gamma_{>\gamma}}(a)$ is the
open ball of radius $\gamma$ around $a$, $b_{\Gamma_{\geq\gamma}}(a)$ is the
closed ball of radius $\gamma$ around $a$ — $b_{\Gamma}(a)=\mathrm{K}$ is also
considered an open ball. Hence, a generalized ball is either a closed ball, an
open ball or an open generalized ball which is not a ball.

######  Corollary 2.5.

Let $A\leq\mathrm{K}(M)$ be a subfield and $b$ be an $A$-definable generalized
ball which is not an open ball. Then $b(\mathrm{dcl}(A))\neq\emptyset$.

###### Proof.

Let $C\subseteq\mathrm{K}(\mathrm{acl}(A))$ be such that, for any ball $d$
avoiding $C$, either $d\subseteq b$ or $d\cap b=\emptyset$. If $b\cap
C=\emptyset$, then $b$ is the largest ball around $b$ avoiding $C$, _i.e._ the
open ball around $b$ with radius $\min_{c\in C}\mathrm{v}(x-c)$, for any $x\in
b$. This contradicts the fact that $b$ is not an open ball. So $b\cap
C\neq\emptyset$.

Since we are in equicharacteristic zero, the average of $b\cap C$ is in $b$
and is $A$-definable. ∎

Finally, when the residue field is algebraically closed, Theorem 2.1 can be
further simplified:

######  Theorem 2.6 (_cf._ [Vic23, Corollary 2.33]).

Assume the residue field $\mathrm{k}(M)$ is algebraically closed. Every
$A$-definable subset of $\mathrm{K}^{x}$ is of the form $\mathrm{v}(P(x))\in
X$ where $P\in A[x]$ is a tuple and $X\subseteq\Gamma^{n}$ is
$\mathrm{v}(A)$-definable in the ordered group structure. Moreover, this
remains true in $\Gamma$-expansions.

##  3 Codes of $\mathcal{O}$-modules

###  3.1 The stabilizer sorts

Let $M$ be an (enriched) valued field.

######  Notation 3.1.

We fix an (ind-)definable family
$\mathcal{C}=(\mathcal{C}_{c})_{c\in\mathrm{Cut}}$ of cuts in $\Gamma$ such
that any $M$-definable cut is of the of form $\gamma+\mathcal{C}_{c}$ for some
unique $\gamma\in\Gamma(M)$ and $c\in\mathrm{Cut}(M)$. We will further assume
that $c$ is a canonical parameter for $\mathcal{C}_{c}$ and that $\Gamma_{\geq
0}$ and $\Gamma_{>0}$ are among the $\mathcal{C}_{c}$ — unless $\Gamma$ is
discrete, in which case, we only require $\Gamma_{\geq 0}$.

For every $c\in\mathrm{Cut}$, let $\mathrm{I}_{c}$ denote the
$\mathcal{O}$-submodule
$\\{x\in\mathrm{K}:\mathrm{v}(x)\in\mathcal{C}_{c}\\}$. Note that, by
hypothesis, any $\mathfrak{L}(M)$-definable $\mathcal{O}$-submodule of
$\mathrm{K}$ is of the form $a\mathrm{I}_{c}$ for some $a\in\mathrm{K}(M)$ and
some unique $c\in\mathrm{Cut}(M)$.

The following results are well-established and go back to Bauer’s work on
separated extensions.

######  Definition 3.2.

A definable valuation $v$ on an interpretable $\mathrm{K}$-vector space $V$ is
a map to some interpretable set $X$ with an order preserving action of
$\Gamma$ such that

  * •

for every $a\in\mathrm{K}$ and $x\in V$, $v(ax)=\mathrm{v}(a)+v(x)$;

  * •

for every $x,y\in V$, $v(x+y)\geq\min\\{v(x),v(y)\\}$.

######  Proposition 3.3.

Assume that $M$ is definably spherically complete — that is, the intersection
of any $M$-definable chain of balls is non empty.

  1. 1.

For every $M$-definable valuation $v$ on $\mathrm{K}^{n}$, there exists a
triangular basis $(a_{i})_{i<n}$ of $\mathrm{K}^{n}$ such that, for all $i$,
$v(a_{i})\in\mathrm{dcl}(\ulcorner v\urcorner)$ and for every
$\lambda_{i}\in\mathrm{K}$,

$v(\sum_{i}\lambda_{i}a_{i})=\max_{i}\mathrm{v}(\lambda_{i})\cdot v(e_{i}).$

  2. 2.

Any $M$-definable $\mathcal{O}$-submodule $R$ of $\mathrm{K}^{n}$ is of the
form $\sum_{i<n}\mathrm{I}_{c_{i}}a_{i}$, where $a_{i}$ is a triangular basis
of $\mathrm{K}^{n}(M)$ and $c_{i}\in\mathrm{Cut}(\ulcorner R\urcorner)$.

A basis as in the fist assertion is said to be separated. A module as in the
second assertion is said to be of type $c=(c_{i})_{i<n}$.

###### Proof.

If $M$ is (elementarily equivalent to a) maximally complete field, the first
assertion is [Vic23, Lemma 5.7]. If $M$ is only definably spherically
complete, the same proof works using [HR21, Claim 3.3.9] instead of [Vic23,
Fact 2.55].

Let us now prove the second assertion. For every $a\in\mathrm{K}^{n}$, we
define $v_{R}(a)=\\{v(x):xa\in R\\}$ a (non-empty) cut of $\Gamma$. We order
them by inclusion (so $\Gamma=v_{R}(0)$ is the maximal element and
$\\{\infty\\}$ is the minimal element). Note that, for every $x\in\mathrm{K}$,
$v_{R}(xa)=v_{R}(a)-\mathrm{v}(x)$ and for this action of $\Gamma$, $v_{R}$ is
an $M$-definable valuation.

By the first assertion, we can find a separated triangular basis $(a_{i})_{i}$
of $\mathrm{K}^{n}(M)$, such that $v_{R}(a_{i})\in\mathrm{dcl}(\ulcorner
R\urcorner)$. Then $\sum_{i}x_{i}a_{i}\in R$ if and only if
$0=\mathrm{v}(1)\in
v_{R}(\sum_{i}x_{i}a_{i})=\min_{i}v_{R}(a_{i})-\mathrm{v}(x_{i})$, _i.e._
$\mathrm{v}(x_{i})\in v_{R}(a_{i})$ for all $i$. Let
$c_{i}\in\mathrm{Cut}(\mathrm{dcl}{\ulcorner R\urcorner})$ and
$a_{i}\in\mathrm{K}$ be such that
$v_{R}(a_{i})=\mathrm{v}(a_{i})+\mathcal{C}_{c_{i}}$. We then have
$R=\sum_{i}a_{i}\mathrm{I}_{c_{i}}a_{i}$, as required. ∎

######  Notation 3.4.

  1. 1.

We write $B_{n}$ to denote the set of $n\times n$ upper triangular and
invertible matrices. We write $\mathrm{D}_{n}\leq\mathrm{B}_{n}$ for the
subgroup of diagonal matrices and $\mathrm{U}_{n}\leq\mathrm{B}_{n}$ for the
subgroup of unipotent matrices, that is upper triangular matrices with $1$’s
on the diagonal.

  2. 2.

For every $n$-tuple $c\in\mathrm{Cut}$, we define $\mathrm{Mod}_{c}$ to be the
interpretable set of modules of type $c$ and
$\Lambda_{c}=\sum\mathrm{I}_{c_{i}}e_{i}$, the canonical module of type $c$,
where $e_{i}$ is the canonical basis of $K^{n}$. Then
$\sum_{i<n}\mathrm{I}_{c_{i}}a_{i}=A\cdot\Lambda_{c}$ where
$A\in\mathrm{B}_{n}$ is the upper triangular matrix of the $a_{i}$. In other
words, $\mathrm{B}_{n}$ acts transitively on $\mathrm{Mod}_{c}$ and

$\mathrm{Mod}_{c}\simeq\mathrm{B}_{n}/\operatorname{Stab}(\Lambda_{c}).$

We will now identify $\mathrm{Mod}_{c}$ with this quotient of $\mathrm{B}_{n}$
and for every $s\in\mathrm{Mod}_{c}$, we write $R_{s}$ for the
$\mathcal{O}$-module of type $c$ coded by $s$.

If $\Delta\leq\Gamma$ is a (definable) convex subgroup, we write
$\mathcal{O}_{\Delta}=\\{x\in\mathrm{K}:\mathrm{v}(x)\in\Delta\\}$ for the
associated (definable) valuation ring. If $I,J\leq\mathrm{K}$ are two
(definable) $\mathcal{O}$-submodules, let $(I:J)$ denote the (definable)
$\mathcal{O}$-submodule $\\{x\in\mathrm{K}:xJ\subseteq I\\}$.

######  Proposition 3.5.

Let $c\in\mathrm{Cut}$ be a tuple. For every $i$, let
$\Delta_{i}=\\{\gamma\in\Gamma:\gamma+\mathcal{C}_{c_{i}}=\mathcal{C}_{c_{i}}\\}$
— this is a convex subgroup of $\Gamma$. For every $a\in\mathrm{B}_{n}$, we
have

$a\in\operatorname{Stab}(\Lambda_{c})\text{ if and only if
}\left\\{\begin{array}[]{cl}a_{i,i}\in\mathcal{O}_{\Delta_{i}}^{\times}&\text{for
all }i<n\text{, and}\\\
a_{i,j}\in(\mathrm{I}_{c_{i}}:\mathrm{I}_{c_{j}})&\text{for all i < j <
n.}\end{array}\right.$

###### Proof.

We proceed by induction on $n$. Write $a$ as
$\left(\begin{smallmatrix}a_{0,0}&b\\\ 0&e\end{smallmatrix}\right)$, with
$e\in\mathrm{B}_{n-1}$, and $c$ as $(c_{0},d)$, with $d\in\mathrm{Cut}^{n-1}$.
If $a\Lambda_{c}\subseteq\Lambda_{c}$, then, considering the action on
$\mathrm{I}_{c_{0}}$ and $\Lambda_{d}$, we see that
$a_{0,0}\mathrm{I}_{c_{0}}\subseteq\mathrm{I}_{c_{0}}$,
$b\Lambda_{d}\subseteq\mathrm{I}_{c_{0}}$ — so, considering the action on each
$\mathrm{I}_{c_{j}}$, for every $j>0$,
$a_{0,j}\mathrm{I}_{c_{j}}\subseteq\mathrm{I}_{c_{0}}$ — and
$e\Lambda_{d}\subseteq\Lambda_{d}$; and the converse also holds.

Since $a\Lambda_{c}=\Lambda_{c}$ if, moreover,
$a^{-1}\Lambda_{c}=\left(\begin{smallmatrix}a_{0,0}^{-1}&-a_{0,0}^{-1}be^{-1}\\\
0&e^{-1}\end{smallmatrix}\right)\Lambda_{c}\subseteq\Lambda_{c}$, it follows
that we must further have $a_{0,0}\mathrm{I}_{c_{0}}=\mathrm{I}_{c_{0}}$,
_i.e._ $\mathrm{v}(a_{0,0})\in\Delta_{0}$ and $e\Lambda_{d}=\Lambda_{d}$.
These conditions are sufficient since, in that case,
$a_{0,0}^{-1}be^{-1}\Lambda_{d}=a_{0,0}^{-1}b\Lambda_{d}\subseteq
a_{0,0}\mathrm{I}_{c_{0}}=\mathrm{I}_{c_{0}}$. The claim now follows by
induction. ∎

######  Definition 3.6.

Let $\mathrm{Cut}^{\star}=\mathrm{Cut}\setminus\\{\emptyset,\Gamma\\}$ and
$\mathrm{Mod}$ be the collection of all the $\mathrm{Mod}_{c}$ where $c$ is a
tuple in $\mathrm{Cut}^{\star}$.

######  Corollary 3.7.

Any $\mathfrak{L}(M)$-definable $\mathcal{O}$-submodule $R$ of
$\mathrm{K}^{n}$ is coded in $\mathrm{K}\cup\mathrm{Mod}$.

###### Proof.

Let $V\subseteq\mathrm{K}^{n}$ be the $\mathrm{K}$-span of $R$ and
$W=\\{x\in\mathrm{K}^{n}:\mathrm{K}x\subseteq R\\}$. Then $V/W$ is
$\mathrm{K}(\ulcorner R\urcorner)$-definably isomorphic to some
$\mathrm{K}^{r}$ and $R$ is entirely determined by its image in $V/W$. So we
may assume $V=\mathrm{K}^{r}$ and $W=0$ and hence that $R$ is of type $c$ with
$c\in\mathrm{Cut}^{\star}$. By definition, it is coded in $\mathrm{Mod}_{c}$.
∎

Let us now describe the structure of $\mathrm{Mod}$. The solvability of the
upper triangular invertible matrices will play a central role in this
description.

We go through the elements of an upper triangular matrix diagonal by diagonal
starting at the middle diagonal, and in each diagonal, we proceed from top to
bottom. In other words, we order pairs $(i,j)$ such that $i\leq j<n$ first by
$i-j$ and then by $i$. We will identify the set of such pairs with the set of
non-negative integers smaller than $n(n+1)/2$, according to that order.

For every pair $(i,j)$, let $p_{i,j}:\mathrm{B}_{n}\to\mathrm{K}$ be the
projection on coordinate $(i,j)$. Let also $\varepsilon_{i,j}=1$ if $i=j$ and
$0$ otherwise. For every pair $\ell$, let
$G_{\ell}=\\{a\in\mathrm{B}_{n}:p_{k}(a)=\varepsilon_{k},\ \forall k<\ell\\}$.
Then $G_{0}=\mathrm{B}_{n}$, $G_{n}=\mathrm{U}_{n}$ and
$G_{n(n+1)/2}=\\{\mathrm{id}\\}$. By choice of the order, for every $\ell$,
$G_{\ell+1}\triangleleft G_{\ell}$ and $p_{\ell}$ induces an isomorphism from
$G_{\ell}/G_{\ell+1}$ to $\mathbb{G}_{\mathrm{m}}$, if $\ell<n$, and to
$\mathbb{G}_{\mathrm{a}}$ otherwise. Note also that $H_{\ell}=\\{a\in
G_{\ell}:p_{k}(a)=\varepsilon_{k},\ \forall k>\ell\\}$, is a section of
$p_{\ell}$ restricted to $G_{\ell}$ and hence $G_{\ell}=G_{\ell-1}\rtimes
H_{\ell}$.

Furthermore, we have $G_{n}=\mathrm{U}_{n}$,
$\mathrm{B}_{n}=\mathrm{U}_{n}\rtimes\mathrm{D}_{n}$ and, for every $\ell\geq
n$, $G_{\ell}$ is central in $G_{n}$ module $G_{\ell+1}$ — actually modulo the
next upper triangular group $G_{0,j}$, if $\ell$ is a pair $(i,i+j-1)$. In
particular $G_{\ell}\trianglelefteq\mathrm{U}_{n}$.

We can now prove the following unary decomposition.

######  Proposition 3.8.

Let $s\in\mathrm{Mod}_{c}$. There exists a finite tuple
$b=(b_{\ell})_{\ell}\in M^{\mathrm{eq}}$ (identified with a subset of some
$\mathrm{K}^{r_{\ell}}$) and $cb_{<\ell}$-interpretable sets $X_{\ell}$ such
that:

  * •

for every $\ell$, $b_{\ell}\in X_{\ell}$;

  * •

$\mathrm{dcl}(s)=\mathrm{dcl}(cb)$;

  * •

if $\ell<n$, then $X_{\ell}=\Gamma/\Delta_{\ell}$, for some $c$-definable
convex subgroup $\Delta_{\ell}\leq\Gamma$;

  * •

if $\ell\geq n$, then $X_{\ell}$ has a $cb_{<\ell}$-definable
$\mathrm{K}/\mathrm{I}_{\ell}$-torsor structure where $\mathrm{I}_{\ell}$ is a
$cb_{<\ell}$-definable multiple of $(\mathrm{I}_{c_{i}}:\mathrm{I}_{c_{j}})$
if $\ell=(i,j)$.

Moreover, for any choice of $a_{k}\in b_{k}$ there is a (uniformly)
$ca_{<\ell}$-definable isomorphism
$f_{\ell}:X_{\ell}\to\mathrm{K}/\mathrm{I}_{\ell}$ and a
$ca_{<\ell}$-definable function $g_{\ell}:f_{\ell}(b_{\ell})\to b_{\ell}$.

###### Proof.

Let $F=\operatorname{Stab}(\Lambda_{c})$, we identify $s$ with a coset $gF$
for some $g\in\mathrm{B}_{n}$. Let $d\in\mathrm{D}_{n}$ and
$u\in\mathrm{U}_{n}$ be such that $g=ud$. Note that, by Proposition 3.5,
$F=F_{\mathrm{U}}\rtimes F_{\mathrm{D}}$ where
$F_{\mathrm{U}}=F\cap\mathrm{U}_{n}$ and $F_{\mathrm{D}}=F\cap\mathrm{D}_{n}$,
so, by (the proof of) [HHM08, Lemma 11.10],
$\mathrm{dcl}(s)=\mathrm{dcl}(\ulcorner dF_{\mathrm{D}}\urcorner,\ulcorner
uF_{\mathrm{U}}^{d}\urcorner)$, where
$F_{\mathrm{U}}^{d}=dFd^{-1}\cap\mathrm{U}_{n}$. Then, by Proposition 3.5,
$\mathrm{D}_{n}/F_{\mathrm{D}}\simeq\prod_{\ell<n}\mathrm{K}^{\star}/\mathcal{O}^{\star}_{\Delta_{\ell}}\simeq\prod_{\ell<n}\Gamma/\Delta_{i}$
and, for every $\ell<n$, we chose $b_{\ell}=v_{\Delta_{\ell}}(d_{\ell})$ to be
the $\ell$th coordinate in this product.

Now, for every $\ell\geq n$, note that
$F_{\mathrm{U}}^{d}G_{\ell}=G_{\ell}F_{\mathrm{U}}^{d}$ is a subgroup, since
$G_{\ell}$ is normal in $\mathrm{U}_{n}$ and moreover,
$F_{\mathrm{U}}^{d}G_{\ell+1}\trianglelefteq F_{\mathrm{U}}^{d}G_{\ell}$ since
for every $g\in G_{\ell}$, $(F_{\mathrm{U}}^{d})^{g}\subseteq
F_{\mathrm{U}}^{d}G_{\ell+1}$ by centrality of the sequence. For every
$\ell\geq n$,Let
$X_{\ell}=uF_{\mathrm{U}}^{d}G_{\ell}/F_{\mathrm{U}}^{d}G_{\ell+1}$ for the
right regular action and $b_{\ell}=uF_{\mathrm{U}}^{d}G_{\ell+1}\in X_{\ell}$.
Note that $X_{\ell}$ is a torsor for the group
$F_{\mathrm{U}}^{d}G_{\ell}/F_{\mathrm{U}}^{d}G_{\ell+1}\simeq
G_{\ell}/(F_{\mathrm{U}}^{d}\cap
G_{\ell})G_{\ell+1}\simeq\mathrm{K}/p_{\ell}(F_{\mathrm{U}}^{d}\cap
G_{\ell})\simeq\mathrm{K}/d_{i}d_{j}^{-1}(\mathrm{I}_{c_{i}}:\mathrm{I}_{c_{j}})$,
by Proposition 3.5, if we have $\ell=(i,j)$. Let
$\mathrm{I}_{\ell}=d_{i}d_{j}^{-1}(\mathrm{I}_{c_{i}}:\mathrm{I}_{c_{j}})$.

Now, any choice of $a_{\ell-1}\in b_{\ell-1}=G_{\ell}F_{\mathrm{U}}^{d}$ gives
rise to an element of $X_{\ell}$ and hence to a $cda_{\ell-1}$-definable
isomorphism $f_{\ell}:X_{\ell}\simeq\mathrm{K}/\mathrm{I}_{\ell}$ given by
left multiplication by $a_{\ell-1}^{-1}$. Let $s:\mathrm{K}\to H_{\ell}$ be
the section of $p_{\ell}$. Then for every $x\in f_{\ell}(b_{\ell})$, we have
$s(x)\in a_{\ell-1}^{-1}uF_{\mathrm{U}}^{d}G_{\ell+1}$ and hence
$a_{\ell-1}s(x)\in b_{\ell}$. ∎

######  Remark 3.9.

Looking at the proof, all the operation applied to any upper triangular matrix
representation of $s$ are actually field operations. It follows that
Proposition 3.8 can be refined as follows. If $A\leq\mathrm{K}(M)$ is a
subfield, and $s\in\mathrm{B}_{n}(A)\operatorname{Stab}(\Lambda_{c})$, then
for every $i$, $b_{i}(A)\neq\emptyset$. Furthermore, if $a_{i}\in b_{i}(A)$,
then $f_{i}(b_{i})(A)\neq\emptyset$ and $g_{i}$ sends $f(b_{i})(A)$ to
$b_{i}(A)$.

###  3.2 The geometric sorts

The goal of this section is to further simplify the codes of modules to
something more akin to the geometric sorts of [HHM06], when the value group is
non discrete. This will be crucial to classify $\mathrm{k}$-internal sets in
Corollary 6.7.

Let $M$ be an (enriched) valued field with non-discrete valued group.

######  Definition 3.10.

  1. 1.

Let $\mathrm{Cut}^{\star\star}$ denote
$\mathrm{Cut}^{\star}\setminus\\{0^{+}\\}$ — unless $\Gamma$ is discrete, in
which case, $\mathrm{Cut}^{\star\star}=\mathrm{Cut}^{\star}$. Any module of
type a tuple $c\in\mathrm{Cut}^{\star\star}$ is said to be
$\mathfrak{m}$-avoiding. Let $\mathrm{S}$ be the collection codes for all
$\mathfrak{m}$-avoiding modules; that is
$\mathrm{S}=\bigsqcup_{c\in\mathrm{Cut}^{\star\star}}\mathrm{Mod}_{c}$.

  2. 2.

For every $\mathcal{O}$-module $R$, let $\operatorname{red}(R)$ denote the
$\mathrm{k}$-vector space $R/\mathfrak{m}R$ and let
$\operatorname{red}_{R}:R\to\operatorname{red}(R)$ denote the canonical
projection. We also define
$\mathrm{T}=\bigsqcup_{s\in\mathrm{S}}\operatorname{red}(R_{s})$.

  3. 3.

Let $\mathcal{G}=\mathrm{K}\cup\mathrm{S}\cup\mathrm{T}$ be the (generalized)
geometric sorts.

######  Remark 3.11.

For every $c\in\mathrm{Cut}^{\star}$, we have
$\mathfrak{m}\mathrm{I}_{c}=\mathrm{I}_{c}$ if and only if
$\mathcal{C}_{c}\neq\Gamma_{\geq 0}$. Indeed, for every $x\in\mathrm{I}_{c}$,
if $\mathcal{C}_{c}\neq\Gamma_{\geq 0}$, there exists $a\in\mathrm{I}_{c}$
such that $\mathrm{v}(a)<\mathrm{v}(x)$. Then $xa^{-1}\in\mathfrak{m}$ and
hence $x=xa^{-1}a\in\mathfrak{m}\mathrm{I}_{c}$.

It follows that if $c\in\mathrm{Cut}^{\star}$ is some tuple and $R$ is an
$\mathcal{O}$-module of type $c$. Then $\operatorname{red}(R)$ has dimension
$|\\{i:\mathcal{C}_{c_{i}}=\Gamma_{\geq 0}\\}|$ over $\mathrm{k}$.

######  Lemma 3.12.

Let $R\subseteq\mathrm{K}^{n}$ be an $\mathcal{O}$-module of type $c$ for some
tuple $c\in\mathrm{Cut}^{\star}$. Then there exists an $\ulcorner
R\urcorner$-definable $\mathfrak{m}$-avoiding module $\overline{R}$ containing
$R$ and such that $\mathfrak{m}R=\mathfrak{m}\overline{R}$. In particular,
$\operatorname{red}(R)\subseteq\operatorname{red}(\overline{R})$ is a subspace
and $\mathrm{dcl}(\ulcorner
R\urcorner)=\mathrm{dcl}(\ulcorner\overline{R}\urcorner,\ulcorner\operatorname{red}(R)\urcorner)$.

###### Proof.

Let $v_{R}$ be the valuation defined in the proof of Proposition 3.3. Recall
that $R=\\{x\in\mathrm{K}^{n}:\Gamma_{\geq 0}\subseteq v_{R}(x)\\}$ and let
$\overline{R}=\\{x\in\mathrm{K}^{n}:\Gamma_{>0}\subseteq v_{R}(x)\\}$. If
$e_{i}$ is a (triangular) basis such that $R=\sum_{i}\mathrm{I}_{c_{i}}e_{i}$,
then $\overline{R}=\sum_{i}\overline{I}_{c_{i}}e_{i}$. Since
$\overline{\mathfrak{m}}=\mathcal{O}$ and
$\overline{I}_{c_{i}}=\mathrm{I}_{c_{i}}$ otherwise, then, by Remark 3.11,
$\mathfrak{m}\overline{\mathcal{O}}=\mathfrak{m}\mathcal{O}=\mathfrak{m}=\mathfrak{m}\overline{\mathfrak{m}}$
and
$\mathfrak{m}\overline{I}_{c_{i}}=I_{c_{i}}=\mathfrak{m}\mathrm{I}_{c_{i}}$,
otherwise. It follows that $\mathfrak{m}\overline{R}=\mathfrak{m}R$.

The last assertion follows from the fact that
$\operatorname{red}_{\overline{R}}^{-1}(\operatorname{red}(R))=R$. ∎

Let us now recall, following [HHM08, Lemma 2.6.4], how to code definable
subspaces of $\operatorname{red}(\overline{R})$. The following abstract
conditions were isolated in [Hru12].

######  Proposition 3.13.

Let $T$ be some theory, $\mathrm{k}$ be some $\emptyset$-definable field and
$\bigsqcup_{s\in\mathrm{S}}V_{s}$ be a collection of finite dimensional
$\emptyset$-definable $\mathrm{k}$-vector spaces which

  1. 1.

is closed under tensors: for every $s,r\in\mathrm{S}$, there is an
$\emptyset$-definable injection from the interpretable set $V_{s}\otimes
V_{s}$ into some $V_{t}$, with $t\in\mathrm{S}$;

  2. 2.

is closed under duals: for every $s\in\mathrm{S}$, there is an
$\emptyset$-definable injection from the interpretable set $V_{s}^{\vee}$ into
some $V_{t}$, with $t\in\mathrm{S}$;

  3. 3.

has flags: For every $s\in\mathrm{S}$, there exists $r,t\in\mathrm{S}$ and a
$\emptyset$-definable exact sequence $0\to V_{r}\to V_{s}\to V_{t}\to 0$, with
$\dim(V_{r})=1$.

Then any definable subspace $W\subseteq V_{s}$, for some $s\in\mathrm{S}$, is
coded in $\bigcup_{s\in\mathrm{S}}V_{s}$.

###### Proof.

By (the proof of) [Hru12, Proposition 5.2], $W$ is coded in the projective
space $\mathbb{P}(V_{r})$, for some $r\in\mathrm{S}$. By [Hru12, Lemma 5.6],
given that the family has flags, $\mathbb{P}(V_{r})$ is coded in
$\bigcup_{s\in\mathrm{S}}V_{s}$. ∎

We consider once again an (enriched) valued field $M$.

######  Definition 3.14.

For every $A\subseteq M^{\mathrm{eq}}$, let
$\mathrm{Lin}_{A}=\bigsqcup_{s\in\mathrm{S}(\mathrm{acl}(A))}\operatorname{red}(R_{s})$.

Before we prove that Proposition 3.13 can be applied to $\mathrm{Lin}_{A}$,
let us prove the following useful computation:

######  Lemma 3.15.

Let $I,J\leq\mathrm{K}$ be ($M$-definable) $\mathcal{O}$-submodule. If
$(I:J)=\mathfrak{m}$, then $I=a\mathfrak{m}$ and $J=a\mathcal{O}$, for some
$a\in\mathrm{K}$.

###### Proof.

We first argue that $\mathrm{v}(I)\subsetneq\mathrm{v}(J)$. If
$\mathrm{v}(J)\subseteq\mathrm{v}(I)$, then $J\subseteq I$ so
$\operatorname{Stab}(J)\subseteq(I:J)$, where $\operatorname{Stab}(J)=\\{x\in
K\ |\ xJ=J\\}$. Since $\operatorname{Stab}(J)=\mathcal{O}_{\Delta}^{\times}$
for some definable convex subgroup $\Delta$ of the value group, and
$\mathfrak{m}$ does not contain $\mathcal{O}_{\Delta}^{\times}$ then
$\mathrm{v}(I)\subsetneq\mathrm{v}(J)$.

We aim to show that $\mathrm{v}(J)$ has a minimal element. Otherwise, given
$\gamma\in\mathrm{v}(J)\backslash\mathrm{v}(I)$ there is some
$\beta\in\mathrm{v}(J)$ such that $\beta<\gamma$, thus $\gamma=\beta+\delta$
where $\delta=\gamma-\beta>0$. Take $x\in\mathfrak{m}$ and $y\in J$ such that
$v(x)=\delta$ and $v(y)=\beta$. Consequently, $xy\notin I$ since
$v(xy)=\gamma$, so $(I:J)\neq\mathfrak{m}$. Let $\gamma_{0}$ be the minimal
element of $\mathrm{v}(J)$ and $a\in K$ such that $v(a)=\gamma_{0}$ thus
$J=a\mathcal{O}$. To show that $I=a\mathfrak{m}$ it is sufficient to argue
that $\mathrm{v}(J)\backslash\mathrm{v}(I)=\\{\gamma_{0}\\}$. If there is some
$\beta\in\mathrm{v}(J)\backslash\mathrm{v}(I)$ such that
$\beta\neq\gamma_{0}$, then $\beta-\gamma_{0}>0$. Take $x\in\mathfrak{m}$ such
that $v(x)=\beta-\gamma_{0}$, then $x\in\mathfrak{m}$ but $ax\notin I$, hence
$(J:I)\neq\mathfrak{m}$. Thus, $I=a\mathfrak{m}$, as required. ∎

######  Proposition 3.16.

For every $A\subseteq M^{\mathrm{eq}}$, $\mathrm{Lin}_{A}$ is a collection of
finite dimensional $\mathrm{k}$-vector spaces which is closed under tensors,
duals and has flags.

###### Proof.

Let $R_{1}\subseteq\mathrm{K}^{n}$ and $R_{2}\subseteq\mathrm{K}^{m}$ be two
$\mathrm{acl}(A)$-definable $\mathfrak{m}$-avoiding $\mathcal{O}$-modules. Let
$f:\mathrm{K}^{n}\otimes\mathrm{K}^{n}\to\mathrm{K}^{nm}$ be the
$\emptyset$-definable isomorphism induced by the canonical basis. By Lemma
3.12, we find an $A$-definable $\mathfrak{m}$-avoiding $\mathcal{O}$-module
$R=\overline{f(R_{1}\otimes R_{2})}$ inducing an inclusion
$\operatorname{red}(f(R_{1}\otimes R_{2}))\subseteq\operatorname{red}(R)$.
Since $\operatorname{red}(R_{1})\otimes\operatorname{red}(R_{2})$ is
$A$-definably isomorphic to $\operatorname{red}(R_{1}\otimes R_{2})$, we
conclude that $\mathrm{Lin}_{A}$ is closed under tensors.

As for duals, for every $\mathcal{O}$-submodule $I\subseteq\mathrm{K}$, let
$I^{\vee}=(\mathcal{O}:I)=\\{x\in\mathrm{K}:xI\subseteq\mathcal{O}\\}$. By
Lemma 3.15, $I^{\vee}\neq\mathfrak{m}$. Let
$g:(\mathrm{K}^{n})^{\vee}\to\mathrm{K}^{n}$ be the $\emptyset$-definable
isomorphism induced by the canonical basis. Then, if
$R=\sum_{i}\mathrm{I}_{c_{i}}a_{i}$ for some triangular basis $a_{i}$, then
$g(\mathrm{Hom}_{\mathcal{O}}(R_{1},\mathcal{O}))=\sum_{i}\mathrm{I}_{c_{i}}^{\vee}g(a_{i})$,
which is $\mathfrak{m}$-avoiding. This induces an $A$-definable isomorphism
$\operatorname{red}(\mathrm{Hom}_{\mathcal{O}}(R_{1},\mathcal{O}))\simeq\operatorname{red}(g(\mathrm{Hom}_{\mathcal{O}}(R_{1},\mathcal{O})))$
which shows that $\mathrm{Lin}_{A}$ is closed under duals.

Finally, regarding flags, let
$R=\sum_{i}\mathrm{I}_{c_{i}}a_{i}\subset\mathrm{K}^{n}$ be an
$\mathrm{acl}(A)$-definable $\mathfrak{m}$-avoiding $\mathcal{O}$-module, with
$a$ triangular. We find a flag for $\operatorname{red}(R)$ by induction on
$n$. Let $\pi$ be the projection on the last $n-1$ variables. Then, we have an
$A$-definable short exact sequence

${0}$${\mathrm{I}_{c_{0}}a_{0}}$${R}$${\pi(R)}$${0}$

which induces the following $A$-definable short exact sequence

${0}$${\mathrm{I}_{c_{0}}a_{0}/\mathfrak{m}\mathrm{I}_{c_{0}}a_{0}}$${R/\mathfrak{m}R}$${\pi(R)/\mathfrak{m}\pi(R)}$${0.}$

If $\mathrm{I}_{c_{0}}=\mathfrak{m}\mathrm{I}_{c_{0}}$, then
$\operatorname{red}(R)\simeq\operatorname{red}(\pi(R))$ and we conclude by
induction on $n$. If not,
$\mathrm{I}_{c_{0}}a_{0}/\mathfrak{m}\mathrm{I}_{c_{0}}a_{0}$ is a dimension
one $\mathrm{k}$-vector space, and the above short exact sequence is a flag
for $\operatorname{red}(R)$. ∎

######  Remark 3.17.

Fix some $A\leq M^{\mathrm{eq}}$.

  1. 1.

$\mathrm{Lin}_{A}$ is stably embedded and its $A$-induced structure is
definable in the structure with the field on $\mathrm{k}$ and the vector space
structure on each sort $R_{s}/\mathfrak{m}R_{s}$. In fact,
$\mathrm{Lin}_{A}\cup\mathrm{RV}$ is stably embedded. Indeed, once we name a
basis of every vector space in $\mathrm{Lin}_{A}$, every definable subset in
$\mathrm{Lin}_{A}\cup\mathrm{RV}$ can be identified with a definable subset in
$\mathrm{RV}$, which is stably embedded.

  2. 2.

Whenever $\mathrm{k}$ is algebraically closed, combining [Hru12, Lemma 5.6]
with Proposition 3.16, $\mathrm{Lin}_{A}$, with its $A$-induced structure,
eliminates imaginaries

We can now improve Corollary 3.7:

######  Corollary 3.18.

Any $\mathfrak{L}(M)$-definable $\mathcal{O}$-submodule $R$ of type
$c\in\mathrm{Cut}^{\star}$ is coded in $\mathcal{G}$.

###### Proof.

By Lemma 3.12, $R$ is coded by $\ulcorner\overline{R}\urcorner\in\mathrm{S}$
for some $\mathfrak{m}$-avoinding module containing $R$ and such that
$\mathfrak{m}R=\mathfrak{m}\overline{R}$ and
$\ulcorner\operatorname{red}(R)\urcorner$ which is a subspace of
$\operatorname{red}(\overline{R})$. By Propositions 3.13 and 3.16,
$\operatorname{red}(R)$ is coded in $\mathrm{Lin}_{\ulcorner
R\urcorner}\subseteq\mathrm{T}$. ∎

One of the main reason for isolating the $\mathfrak{m}$-avoiding modules is
the following result. Assume that $M$ is an $\mathrm{RV}$-expansion of a model
of $\mathrm{Hen}_{0,0}$ and that $\Gamma(M)$ is dense.

######  Proposition 3.19.

Any $M$-definable $X\subseteq\mathrm{S}$ which is orthogonal to $\Gamma$ is
finite.

###### Proof.

Let us first consider the case of some $M$-definable
$X\subseteq\mathrm{K}/\mathrm{I}_{c}$ for some
$c\in\mathrm{Cut}^{\star\star}$. Let $Y\subseteq\mathrm{K}$ be the preimage of
$X$. By LABEL:Henprep, there exists a (non-empty) finite set
$C\subseteq\mathrm{K}(M)$ such that, any ball $b$ disjoint from $C$, is either
contained in $Y$ or is disjoint from it. If $X$ is infinite, then there exists
some $a\in Y$ such that $a+I$ is disjoint from $C$. Let $b$ be the maximal
ball around $a$ that is disjoint from $C$ — _i.e._ the ball $a+(\min_{c\in
C}\mathrm{v}(a-c))\mathfrak{m}$. Then $b\subseteq Y$. Since
$\mathrm{I}_{c}\neq\mathfrak{m}$, the function $f:x\mapsto\mathrm{v}(x-a)$
induces a well-defined function on $b/I\subseteq X$ with infinite image, so
$X$ is not orthogonal to $\Gamma$.

Let us now fix some $e\in X\subseteq\mathrm{S}$, in some elementary extension
of $M$. Let $b_{\ell}$ be as in Proposition 3.8 and let us prove, by induction
on $\ell$, that $b_{\ell}\in M^{\mathrm{eq}}$. For all $\ell<n$, we have
$b_{\ell}\in\Gamma/\Delta_{\ell}$, for some convex subgroup $\Delta_{\ell}$.
Since $e\in X$ and $X$ is orthogonal to $\Gamma$ and
$b_{\ell}\in\mathrm{dcl}(e)$, we must have $b_{\ell}\in M^{\mathrm{eq}}$. Let
now $\ell\geq n$ and let us assume that $b_{<\ell}\in M$. We have $b_{\ell}\in
X_{\ell}$ which is an $M$-definable torsor for some
$\mathrm{K}/\mathrm{I}_{\ell}$ where, by Lemma 3.15, $\mathrm{I}_{\ell}$ is
not a multiple of $\mathfrak{m}$. Since $b_{i}\in\mathrm{dcl}(e)$, it is
contained is an $M$-definable subset of $\mathrm{K}/\mathrm{I}_{\ell}$ which
is orthogonal to $\Gamma$, and hence, by the first paragraph, finite. So
$b_{\ell}\in M^{\mathrm{eq}}$.

Since $e\in\mathrm{dcl}(Mb)$, it follows that $e\in M^{\mathrm{eq}}$. As this
holds for any $e\in X$ is some elementary extension, $X$ is finite. ∎

Recall that a definable set $X$ is (resp. almost) internal to another
definable set $Y$ if, over a model, $X$ admits a one-to-one (resp. finite-to-
one) map to $Y^{\mathrm{eq}}$.

######  Corollary 3.20.

Let $A=\mathrm{acl}(A)\subseteq M^{\mathrm{eq}}$ and let $X$ be an almost
$\mathrm{k}$-internal $A$-definable subset of $\mathcal{G}$, then
$X\subseteq\mathrm{K}(A)\cup\mathrm{S}(A)\cup\mathrm{Lin}_{A}$.

###### Proof.

Any almost $\mathrm{k}$-internal set is orthogonal to $\Gamma$. By Proposition
2.3, any infinite definable subset of $\mathrm{K}$ contains a ball and hence
is not orthogonal to $\Gamma$, so if $X\subseteq\mathrm{K}$, then
$X\subseteq\mathrm{K}(A)$. By Proposition 3.19, if $X\subseteq\mathrm{S}$,
then $X\subseteq\mathrm{S}(A)$. Finally, if $X\subseteq\mathrm{T}$, then the
projection of $X$ to $\mathrm{S}$ is finite and hence
$X\subset\bigsqcup_{s\in\mathrm{S}(A)}\operatorname{red}(R_{s})/\mathfrak{m}R_{s}=\mathrm{Lin}_{A}$.
∎

##  4 Density of quantifier free definable types

Let $M$ be an $\mathrm{RV}$-expansion of a model of $\mathrm{Hen}_{0,0}$. Let
$M_{1}=M^{\mathrm{ur}}$ be its maximal algebraic unramified extension (with
the full induced structure on $\Gamma$) and $M_{0}=M^{\mathrm{a}}$ be its
algebraic closure (as a pure valued field). In what follows, whenever, we want
to refer to the structure in $M_{0}=M^{\mathrm{a}}$ (resp.
$M_{1}=M^{\mathrm{ur}}$, resp. $M$), we will indicate this by a $0$ (resp.
$1$, resp. nothing): _e.g._ $\mathrm{acl}_{0}$, $\mathrm{acl}_{1}$ or
$\mathrm{acl}$ for the algebraic closure and $\mathrm{S}^{0}(M)$ or
$\mathrm{S}^{1}(M)$ for the space of types over $M$. We also assume that the
language $\mathfrak{L}_{i}$ of $M_{i}$ is Morleyized, and we restrict
ourselves to quantifier free $\mathfrak{L}_{i}$-formulas when interpreting
them in a substructure.

Let $A=\mathrm{acl}(A)\subseteq M$ and $X\subseteq\mathrm{K}$ be
$\mathfrak{L}(A)$-definable.

The goal of this section is to prove the following density result:

######  Theorem 4.1.

Assume that $\Gamma(M)$ satisfies Property D. Then there exists an
$\mathfrak{L}_{1}(\mathcal{G}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable type
$p\in\mathrm{S}^{1}(M^{\mathrm{ur}})$ consistent with $X$ — in the pair
$(M^{\mathrm{ur}},M)$.

This statement was proved in [Vic23, Theorem 5.9] when $M=M^{\mathrm{ur}}$ and
$\Gamma$ is an abelian ordered group of bounded regular rank. It also
generalizes [HR21, Theorem 3.1.3] in two ways. The first is that it provides a
definable type in a stronger reduct (_i.e._ a type in $M^{\mathrm{ur}}$ and
not just in $M^{\mathrm{a}}$). The second is that there is no hypothesis on
the residue field — it is not required that the residue field eliminates
$\exists^{\infty}$.

###  4.1 Codes of definable types

We start by proving the following useful fact allowing to compare
$\mathfrak{L}_{1}$-types over $M$, $M_{1}=M^{\mathrm{ur}}$ and
$M_{0}=M^{\mathrm{a}}$:

######  Proposition 4.2.

Let $A=\mathrm{dcl}(A)\subseteq M$ and $p(x)\in\mathcal{S}^{\varepsilon}(M)$
be $\mathfrak{L}(A)$-definable, for $\varepsilon=0$ or $1$. Then $p$ has a
unique extension
$q_{\varepsilon}\in\mathcal{S}^{\varepsilon}(M_{\varepsilon})$.

Moreover, $q_{1}$ is
$\mathfrak{L}_{1}(\mathcal{G}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable and
$q_{0}$ is definable in an expansion $M_{0}^{\prime}$ of
$M_{0}=M^{\mathrm{a}}$ by cuts of the value group and $\ulcorner
q_{0}\urcorner\in\mathcal{G}(A)$.

As we will see in the proof, in $M_{0}^{\prime}$, we only add cuts whose trace
in $\Gamma(M)$ is $\mathcal{G}(A)$-definable. We can therefore identify the
set $\mathcal{G}(M)$ in $M_{0}^{\prime}$ with a subset of $\mathcal{G}(M)$ in
$M$.

We follow the proof of [Vic23, Theorem 5.9], _mutatis mutandis_.

###### Proof.

The uniqueness of $q_{\varepsilon}$ follows from [HR21, Lemma 3.3.8]; note
that $q_{\varepsilon}$ is finitely satisfiable in $M$.

For every integer $d\geq 0$, let $V_{d}\simeq\mathrm{K}^{\ell}$ be the space
of polynomials in $\mathrm{K}(M)[x]_{\leq d}$ of degree less or equal than $d$
(in each $x_{i}$). It comes with an $\mathfrak{L}(A)$-definable valuation
defined by $v(P)\leq v(Q)$ if
$p(x)\vdash\mathrm{v}(P(x))\leq\mathrm{v}(Q(x))$.

By Proposition 3.3 there exists a separated basis $(P_{i})_{i\leq\ell}\in
V_{d}$ such that, for every $i$, $\gamma_{i}=v(P_{i})\in\ulcorner
v\urcorner\subseteq A$. By [HR21, Claim 3.3.5], $(P_{i})_{i}$ is also a
separated basis of $V_{d}^{\varepsilon}=\mathrm{K}(M_{\varepsilon})[x]_{\leq
d}$ with the valuation $v_{\varepsilon}(P)\leq v(Q)$ if
$q_{\varepsilon}(x)\vdash\mathrm{v}(P(x))\leq\mathrm{v}(Q(x))$. It follows
that $v_{1}(V_{d}^{1})=v(V_{d})=\bigsqcup_{i}\gamma_{i}+\Gamma(M)$ and hence
that $v_{1}$ is $\mathfrak{L}_{1}(M)$-definable. Similarly,
$v_{0}(V_{d}^{0})=\bigcup_{i}\gamma_{i}+\Gamma(M^{\mathrm{a}})$ and $v_{0}$ is
definable (over $M$) in the expansion by the cuts
$C_{i,j}=\\{x\in\Gamma(M_{0}):\gamma_{i}+x\geq\gamma_{j}\\}$, for every pair
$i,j$. Let $\mathrm{Mod}^{0}$ be the set of codes fir definable modules in
this $\Gamma$-expansion.

By Corollary 3.7 the definable $\mathcal{O}$-modules
$R_{i}^{\varepsilon}=\\{P\in
V_{d}^{\varepsilon}:v_{\varepsilon}(P)\geq\gamma_{i}\\}$ are coded by some
tuple $e^{\varepsilon}_{i}\in\mathrm{Mod}^{\varepsilon}(M)$. We identify
$e^{\varepsilon}_{i}$ with the code $e_{i}\in\mathrm{Mod}(A)$ of
$R^{\varepsilon}_{i}\cap V_{d}$. Furthermore, the $R_{i}^{\varepsilon}$
entirely determine $v_{\varepsilon}$ which is therefore coded in
$\mathcal{G}(A)$ (_cf._ Corollary 3.18), as is $q_{\varepsilon}$.

Finally, let us prove the definability of $q_{1}$. By Theorem 2.6, any
$\mathfrak{L}_{1}$-formula $\phi(x,y)$ (with variables in $\mathrm{K}$) is
equivalent to one of the form $\psi(\mathrm{v}(P(x,y)))$, where
$P\in\mathbb{Z}[x,y]$ is a tuple. Let $X_{\phi}=\\{v_{1}(P(x,a))\in
v_{1}(V_{d}^{1}):q_{1}(x)\vdash\phi(\mathrm{v}(P(x,a)))\\}$. Note that if
$v_{1}(P(x,b))=v_{1}(P(x,a))$, then
$q_{1}(x)\models\mathrm{v}(P(x,b))=\mathrm{v}(P(x,a))$ and hence
$v_{1}(P(x,b))\in X_{\phi}$ if and only if $v_{1}(P(x,a))\in X_{\phi}$. So
$q_{1}$ is entirely determined by the $X_{\phi}$ over $\mathcal{G}(A)$.
Moreover, since $v_{1}(V_{d}^{1})=v(V_{d})=\bigcup_{i}\gamma_{i}+\Gamma(M)$
and $\gamma_{i}\in\mathcal{G}(A)$, this set can be identified, over $G(A)$, to
a disjoint union of copies of $Vg(M)$. It follows that $X_{\phi}$ is
$\mathfrak{L}_{1}(\mathcal{G}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable, and
hence so is $q_{1}$. ∎

From now on, we will identify $\mathfrak{L}(A)$-definable types in
$\mathcal{S}^{1}(M)$ with their unique extensions to $M_{1}=M^{\mathrm{ur}}$
and $M_{0}=M^{\mathrm{a}}$.

###  4.2 Unary sets

We first consider the case of Theorem 4.1 when $X\subseteq\mathrm{K}$ is
unary. The proof proceeds exactly as in [Vic23, Theorem 5.3] where, in the
unary case, the hypothesis that $M=M^{\mathrm{ur}}$ is not used. We first
build a definable type in $M^{\mathrm{a}}$ consistent with $X$:

######  Lemma 4.3.

There exists an $\mathfrak{L}_{1}(\mathrm{B_{g}}(A))$-definable type
$p_{0}\in\mathrm{S}^{0}(M^{\mathrm{ur}})$ consistent with $X$.

This follows from [HR21, Section 3] which states a relative version of that
statement. However, since the machinery set up for the relative version of the
statement is rather heavy, let us sketch a proof. A detailed version of this
proof can also be found in [Vic23, Theorem 5.5].

###### Proof.

Let $\mathrm{B}(M^{\mathrm{ur}})$ be the set of all open and closed balls
(including points and $\mathrm{K}$ itself) in $M^{\mathrm{ur}}$. Given
$b_{1},b_{2}\in\mathrm{B}$ we write $b_{1}\trianglelefteqslant b_{2}$ if
$b_{1}\cap X\subseteq b_{2}\cap X$. This is a preorder with associated
equivalence $\equiv$ and the associated order is a tree $\mathcal{T}$ if we
remove the class $E_{\emptyset}$ of balls that don’t intersect $X$.

Note that any $\equiv$-class $E\neq E_{\emptyset}$, the generalized ball
$b_{E}=\bigcap_{b\in E}b$ is defined by knowing a point in $b_{E}$ and the set
$\\{\mathrm{v}(x-y):x,y\in B\\}$ which is definable in
$\Gamma(M)=\Gamma(M^{\mathrm{ur}})$. So $b_{E}$ is
$\mathfrak{L}_{1}(M)$-definable. It follows that $E$ is coded in
$\mathrm{B_{g}}(M)$ and that the generic type
$\eta_{E}(x)\in\mathcal{S}^{0}(M^{\mathrm{ur}})$ generated by

$\\{x\in b:b\in E\\}\cup\\{x\nin\bigcup_{i}b_{i}:b_{i}\in\mathrm{B}\text{ and
}\forall b\in E,\ b_{i}\subset b\\}$

is $\mathfrak{L}_{1}(\ulcorner E\urcorner)$-definable. If the type $\eta_{E}$
is not consistent with $X$, by compactness, $E$ has finitely many direct
predecessors for $\trianglelefteqslant$, each of them in
$\mathrm{acl}(A,\ulcorner E\urcorner)$. So either the lemma holds or the tree
$\mathcal{T}$ has an initial discrete finitely branching tree of
$\mathfrak{L}_{1}(\mathrm{B_{g}}(A))$-definable $\equiv$-classes.

By Proposition 2.3, there exists a finite set $C\subseteq\mathrm{K}(M)$
preparing $X$ and, we can find an $\equiv$-class $E$ in the initial discrete
tree such that $b_{E}\cap C=\emptyset$. Then $b_{E}\subseteq X$ and hence $X$
is consistent with the $\mathfrak{L}_{1}(\mathrm{B_{g}}(A))$-definable type
$\eta_{E}$. ∎

The type $p_{0}=\eta_{E}$ can then be completed to a type
$\mathfrak{L}_{1}(\mathrm{B_{g}}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable
type $p_{1}\in\mathcal{S}^{1}(M^{\mathrm{ur}})$ consistent with $X$:

######  Lemma 4.4.

Assume that $\Gamma(M)$ satisfies Property D. Let $A=\mathrm{dcl}(A)\subseteq
M^{\mathrm{eq}}$ be such that: Then for every $\mathfrak{L}(A)$-definable
generalized ball $b$, there exists an
$\mathfrak{L}_{1}(\mathrm{B_{g}}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable
type $p\in\mathcal{S}^{1}(M^{\mathrm{ur}})$ containing $\eta_{b}$.

###### Proof.

For any $a\in b(M)$ and $c\models\eta_{b}$, $\gamma=\mathrm{v}(c-a)$ does not
depend on $a$. If $\gamma\in\Gamma(M)$, then $\eta_{b}$ generates a complete
type in $\mathrm{S}^{1}(M^{\mathrm{ur}})$. If not, let $C$ be the
$\mathfrak{L}_{1}(A)$-definable cut of $\gamma$ over $\Gamma(A)$ and
$Y_{a}=\mathrm{v}(X-a)$, for every $a\in B$. Note that $\gamma\in Y_{a}\cap
C$. By hypothesis, there exists an $\mathfrak{L}(A)$-definable type
$q\in\mathcal{S}(\Gamma(M))$ consistent with $C$ and $Y_{a}$. Then, the type
$p_{1}(x)=p_{0}(x)\wedge q(\mathrm{v}(x-a))$ is complete by Theorem 2.6, and
it is
$\mathfrak{L}_{1}(\mathrm{B_{g}}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable. ∎

######  Corollary 4.5.

Suppose that the value group satisfies Property D. Let
$A=\mathrm{acl}(A)\subseteq M^{\mathrm{eq}}$ then any
$\mathfrak{L}(A)$-definable subset of $\Gamma^{n}$ is consistent with an
$\mathfrak{L}(A)$-definable type $p\in\mathrm{S}^{1}(M)$.

###  4.3 Germs of functions

To prove density of definable types in general, we now wish to proceed by
transitivity. However, since we are working with definable
$\mathfrak{L}_{1}$-types, we first need to address the potential difference
between $\mathrm{acl}$ and $\mathrm{acl}_{1}$.

######  Lemma 4.6.

Let $A\subseteq M^{\mathrm{eq}}$ and assume that

  1. 1.

For every $\mathfrak{L}(A)$-definable convex subgroup $\Delta\leq\Gamma$,
$\Gamma/\Delta(\mathrm{dcl}(A))\subseteq v_{\Delta}(\mathrm{K}(A))$.

  2. 2.

For every $b\in\mathrm{B_{g}}(\mathrm{dcl}(A))$, $b(A)\neq\emptyset$.

Then
$\mathcal{G}(A)\subseteq\mathrm{dcl}_{1}(\mathrm{Cut}(\mathrm{dcl}(A)),\mathrm{K}(A))$.

###### Proof.

Let $s\in\mathrm{Mod}_{c}(\mathrm{dcl}(A))$ — in particular
$c\in\mathrm{Cut}(\mathrm{dcl}(A))$ — and $b=(b_{\ell})_{\ell}$ be as in
Proposition 3.8 applied in $M_{1}$. Let us show, by induction on $\ell$, that
$b_{\ell}(\mathrm{K}(\mathrm{dcl}_{1}(A)))\neq emptyset$. For $\ell<n$, since
$b_{\ell}\in\Gamma/\Delta_{\ell}$, this follows from the first assumption. If
$\ell\geq n$, by induction, $b_{\ell}$ is
$\mathcal{L}_{1}(c\mathrm{K}(A))$-interdefinable with some
$b^{\prime}_{\ell}\in\mathrm{K}/\mathrm{I}_{\ell}$. By Remark 3.9,
$b^{\prime}_{\ell}(M)\neq\emptyset$, so $b^{\prime}_{\ell}$ is an
$\mathfrak{L}(A)$-definable generalized ball in $M$ and hence
$b^{\prime}_{\ell}(A)\neq\emptyset$ by the second assumption. By Remark 3.9,
we also have $b_{\ell}(\mathrm{dcl}_{1}(A))\neq\emptyset$. It follows that,
for every $\ell$, $b_{i}\in\mathrm{dcl}_{1}(c\mathrm{K}(A))$ and hence
$s\in\mathrm{dcl}_{1}(cb)\subseteq\mathrm{dcl}_{1}(c\mathrm{K}(A))$. ∎

For every tuple $a\in M$, let $a_{\mathrm{K}}$ enumerate $\mathrm{K}(a)$.

######  Proposition 4.7.

Assume that $\Gamma$ has property D. Let $X$ be
pro-$\mathfrak{L}(A)$-definable and $p(x)\in\mathcal{S}^{1}(M)$ be
$\mathfrak{L}(A)$-definable and consistent with $X$. Assume that for any
$a\models p$, $a\subseteq\mathrm{acl}_{1}(Ma_{\mathrm{K}})$. Then, for every
$\mathfrak{L}(A)$-definable one-to-finite correspondence $F$ into
$\mathcal{G}\cup\Gamma^{\mathrm{eq}}$ (defined at realizations of $p$), there
exists an $\mathfrak{L}(A)$-definable $q(xy)\in\mathcal{S}^{1}(M)$ containing
$p(x)$ and $ac\models q$ with $a\in X$,
$c\in\mathrm{acl}_{1}(Ma_{\mathrm{K}}c_{\mathrm{K}})$ and
$F(a)\cap\mathrm{dcl}_{1}(ac)\neq\emptyset$.

###### Proof.

We first consider the case where $F$ is almost definable in $M_{1}$.

######  Claim 4.7.1.

If there exists an $\mathfrak{L}_{1}(M)$-definable one-to-finite
correspondence $G$ such that $p(x)\wedge x\in X\vdash F(x)\subseteq G(x)$,
then the proposition holds.

###### Proof.

Since $p\in\mathrm{S}^{1}(M)$, $|G(x)|$ is constant when $x$ varies over
realizations of $p$; and we may assume that it is minimal. Then for every
other such $G^{\prime}$, $p(x)\wedge x\in X\models F(x)\subseteq G(x)\cap
G^{\prime}(x)$ and hence $p(x)\wedge x\in X\vdash G(x)=G^{\prime}(x)$. In
other words, for some (and hence for every) $a\models p$,
$G(a)=G^{\prime}(a)$. This holds in particular of any $G^{\prime}=\sigma(G)$,
where $\sigma\in\mathrm{Aut}(M/A)$ and hence $[G]_{p}\in\mathrm{dcl}(A)=A$.
Let $G_{0}\subseteq G$ be minimal $\mathfrak{L}_{1}(M)$-definable such that
$p(x)\vdash\emptyset\neq G_{0}(x)\subseteq G(x)$. Then
$[G_{0}]_{p}\in\mathrm{acl}(A)=A$. So the type $q(xy)=p(x)\wedge y\in
G_{0}(x)$ is $\mathfrak{L}(A)$-definable and, by construction, for any
$ac\models q$, $c\in
G_{0}(a)\subseteq\mathrm{acl}_{1}(Aa)\subseteq\mathrm{acl}_{1}(Ma_{K})$.
Moreover, if $q(xy)$ is not consistent with $x\in X\wedge y\in F(x)$, then
$p(x)\wedge x\in X\vdash F(x)\subseteq G(x)\setminus G_{0}(x)$, contradicting
the minimality of $G$. So the type $q$ is as required. ∎

Let us now assume that the codomain of $F$ is $\Gamma^{\mathrm{eq}}$. By
Proposition 2.2, for every $a\models p$,

$\Gamma^{\mathrm{eq}}(\mathrm{acl}(Aa))\subseteq\Gamma^{\mathrm{eq}}(\mathrm{acl}(Ma_{\mathrm{K}}))\subseteq\mathrm{acl}_{1}(\mathrm{v}(M(a_{\mathrm{K}})))$

and hence, by compactness, there exists an $\mathfrak{L}_{1}(M)$-definable
one-to-finite correspondence $G$ such that $p(x)\vdash F(x)\subseteq G(x)$. We
now conclude with 4.7.1. Iterating this case of the proposition, we may assume
that $a$ contains all of $\Gamma^{\mathrm{eq}}(\mathrm{acl}(Aa))$.

######  Claim 4.7.2.

Let $f:p\to\mathrm{B_{g}}$ be $\mathfrak{L}_{1}$-definable. Then, there exists
an $\mathfrak{L}(A)$-definable $q(xy)\in\mathcal{S}^{1}(M)$ containing
$\int_{p(x)}\eta_{f(x)}(y)$ — that is, the $\mathfrak{L}_{0}$-type of tuples
$ac$ such that $a\models p$ and $c\models\eta_{f(a)}$.

###### Proof.

Let $a\models p$ and $b=f(a)$. Since
$\Gamma^{\mathrm{eq}}(\mathrm{acl}(b))\subseteq\Gamma^{\mathrm{eq}}(\mathrm{acl}(Aa))\subseteq
a$, by Lemma 4.4, there exists an $\mathfrak{L}_{1}(a)$-definable type
$r_{a}(y)$ containing $\eta_{b}(y)$. Then $\int_{p(x)}r_{x}(y)$ is as
required. ∎

Iterating 4.7.2, we can further assume that for every
$\mathfrak{L}(Aa)$-definable convex subgroup $\Delta\leq\Gamma$,
$\Gamma/\Delta(\mathrm{acl}(Aa))\subseteq v_{\Delta}(a_{\mathrm{K}})$.

If the codomain of $F$ is $\mathrm{k}$, let $\eta_{k}(y)\in\mathcal{S}^{1}(M)$
be the $\mathfrak{L}$-definable generic of $\mathrm{k}$ — that is, the only
non-algebraic type concentrating on $\mathrm{k}$. If
$p(x)\otimes\eta_{\mathrm{k}}(y)$ is not consistent with $x\in X\wedge y\in
G(y)$, then there exists an $\mathfrak{L}_{1}(M)$-definable one-to-finite
correspondence $G$ such that $p(x)\wedge x\in X\vdash F(x)\subseteq G(x)$.
Once again, we conclude with 4.7.1. On the other hand, if
$p(x)\otimes\eta_{\mathrm{k}}(y)$is consistent with $x\in X\wedge y\in F(y)$,
let $q(xz)=p(x)\otimes\eta_{\mathcal{O}}(y)$, then, by hypothesis, $q(xz)$ is
consistent with $x\in X\wedge\mathrm{res}(z)\in F(y)$. Applying 4.7.2 and
iterating, we can thus assume that
$\mathrm{k}(\mathrm{acl}(Aa))\subseteq\mathrm{res}(a_{\mathrm{K}})$. Then, we
also have $\mathrm{RV}(\mathrm{acl}(Aa))\subseteq\mathrm{rv}(a_{K})$.

Let us now assume that the codomain of $F$ is the set of generalized balls
that are not open balls. For any $a\models p$ and $b\in
F(a)\subseteq\mathrm{acl}(Aa)\subseteq\mathrm{acl}_{1}(Ma_{\mathrm{K}})$, by
Corollary 2.5, we have $b(\mathrm{acl}_{1}(Ma_{\mathrm{K}}))\neq\emptyset$.
Moreover,
$\mathrm{cut}(b)\in\Gamma^{\mathrm{eq}}(\mathrm{acl}(Aa))\subseteq\mathrm{dcl}_{1}(a)$,
by Proposition 2.2. Hence $b\in\mathrm{acl}_{1}(Ma)$ and we conclude with
4.7.1. So we may assume that $b\in a$. Applying 4.7.2 and iterating, we may
assume that any generalized ball $b\in\mathrm{acl}(Aa)$, which is not an open
ball, has a point in $a$.

Now, if $b\in\mathrm{acl}(Aa)$ is an open ball, the smallest closed ball
around $b$ has a point $c\in a$ and
$b-c\in\mathrm{RV}(\mathrm{acl}(Aa))\subseteq\mathrm{rv}(a_{\mathrm{K}})$ also
has a point in $a$, hence so does $b$. Recall that we already assumed that,
for every $\mathrm{acl}(Aa)$-definable convex subgroup $\Delta\leq\Gamma$,
$\Gamma/\Delta(\mathrm{acl}(Aa))\subseteq v_{\Delta}(a_{\mathrm{K}})$. By
Lemma 4.6, it follows that
$\mathcal{G}(\mathrm{acl}(Aa))\subseteq\mathrm{dcl}_{1}(a)$, concluding the
proof of the proposition. ∎

######  Corollary 4.8.

There exists $a\models p$ in $X$ such that

$\operatorname{tp}_{1}(\mathcal{G}(\mathrm{acl}(Aa))\cup\Gamma^{\mathrm{eq}}(\mathrm{acl}(Aa))/M)$

is $\mathfrak{L}(A)$-definable.

The proof of Theorem 4.1 is now a standard induction.

###### Proof of Theorem 4.1.

Recall that, by Proposition 4.2, we can identify $\mathfrak{L}(A)$-definable
types in $\mathcal{S}^{1}(M)$, with their unique
$\mathfrak{L}(\mathcal{G}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable extension
to $M^{\mathrm{ur}}$.

We may assume that $X\subseteq\mathrm{K}^{n}$ and we proceed by induction on
$n$. Let $\pi:\mathrm{K}^{n}\to\mathrm{K}$ be the projection on the first
coordinate. By LABEL:unarydens, there exists an
$\mathfrak{L}_{1}(\mathcal{G}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable type
$p\in\mathcal{S}^{1}(M^{\mathrm{ur}})$ consistent with $\pi(X)$. Let $a\models
p(x)\wedge x\in X$, $c$ enumerate
$\mathcal{G}(\mathrm{acl}(Aa))\cup\Gamma^{\mathrm{eq}}(\mathrm{acl}(Aa))$ and
$X_{a}=\\{y\in\mathrm{K}^{n-1}:(a,y)\in X\\}$. By Corollary 4.8, we may assume
that $q(y)=\operatorname{tp}_{1}(c/M^{\mathrm{ur}})$ is
$\mathfrak{L}_{1}(\mathcal{G}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable. By
induction, there exists an $\mathfrak{L}_{1}(c)$-definable $r_{c}(z)$
consistent with $X_{a}$. The type $\int_{q(y)}r_{y}(z)$ is then as required. ∎

In the case $M=M^{\mathrm{ur}}$, we can deduce a slight generalization of
[Vic23, Theorem 5.12]: To conclude we

######  Corollary 4.9.

Assume that

  * •

$\Gamma(M)$ satisfies Property D;

  * •

$\mathrm{k}(M)$ is algebraically closed.

Then $M$ weakly eliminates imaginaries down to
$\mathcal{G}\cup\Gamma^{\mathrm{eq}}$.

##  5 Invariant Extensions

In this section, we will consider the invariance of types over large subsets
of our model (which are points of some stably embedded definable set _e.g._
$\mathrm{RV}$). This gives rise to several notions of invariance isolated in
[HR21, Section 4.2].

Whenever $D=\bigcup_{i}D_{i}$ is an ind-definable, we denote by
$D^{\mathrm{eq}}$ the ind-definable union of all interpretable sets $X$ that
admit a definable surjection $\prod_{j}D_{i_{j}}\rightarrow X$.

######  Definition 5.1.

Let $M$ be an $\mathfrak{L}$-structure, $C\subseteq M$, $D$ be an
(ind-)definable set and $p$ be a partial type over $M$. We say that:

  1. 1.

$p$ is $\mathrm{Aut}(M/C)$-invariant if for every
$\sigma\in\mathrm{Aut}(M/C)$, $p=\sigma(p)$;

  2. 2.

$p$ has $\mathrm{Aut}(M/C)$-invariant $D$-germs if it is
$\mathrm{Aut}(M/C)$-invariant and so is the $p$-germ of every $M$-definable
map $f:p\rightarrow D^{\mathrm{eq}}$;

  3. 3.

$p$ is $\mathrm{Aut}(M/D)$-invariant if it has
$\mathrm{Aut}(M/D(M))$-invariant $D$-germs.

A nice property of the stronger notion is that it is transitive — _cf._ [HR21,
Lemma 2.4.2]:

######  Lemma 5.2.

Let $M\prec N$ be $\mathfrak{L}$-structures with $N$ saturated and
sufficiently large, let $C\subseteq M$ be potentially large, let $D$ be an
(ind-)$\mathfrak{L}$-definable stably embedded set, let $p\in S(M)$ have
$\mathrm{Aut}(M/C)$-invariant $D$-germs, let $a\vDash p$ in $N$ and let $q\in
S(N)$ be $\mathrm{Aut}(N/CD(N)a)$-invariant. Then $q|_{M}$ is
$\mathrm{Aut}(M/C)$-invariant.

Moreover, if $q$ has $\mathrm{Aut}(N/CD(N)a)$-invariant $E$-germs, for some
(ind-)$\mathfrak{L}$-definable set $E$, then $q|_{M}$ has
$\mathrm{Aut}(M/C)$-invariant $E$-germs.

The main goal of this section is to prove the following statement:

######  Theorem 5.3.

Let $M$ be an $\mathrm{RV}$-expansion model of $\mathrm{Hen}_{0,0}$ which is
sufficiently saturated and homogeneous and let $M_{0}=M^{\mathrm{a}}$. Let
$A\subseteq\mathcal{G}(M)$ and $a\in N\succ M$ a tuple such that
$\operatorname{tp}_{0}(a/M)$ is $\mathrm{Aut}(M/A)$-invariant. Then
$\operatorname{tp}(a/M)$ is
$\mathrm{Aut}(M/A\mathrm{RV}(M)\mathrm{Lin}_{A}(M))$-invariant.

We follow the general strategy of [HR21, Section 4]. The main new challenge is
to prove the equivalent (Proposition 5.16) of [HR21, Corollary 4.4.6] in the
present setting since the geometric sorts are now larger.

###  5.1 Germs of functions into the linear sorts

Let $M$ be (a $\Gamma$-expansion of) a model of $\mathrm{Hen}_{0,0}$, with
algebraically closed residue field and $\mathrm{NIP}$ value group. One
important ingredient of the proof of Proposition 5.16 is a description of
germs of functions into the linear sorts:

######  Proposition 5.4.

Let $A\subseteq M^{\mathrm{eq}}$. Let $p(x)\in\mathcal{S}(M)$ be $A$-definable
concentrating on $\mathrm{K}^{n}$ for some $n$. Let $f$ be an $M$-definable
function with domain $\mathrm{K}^{n}$. Assume that for every $a\models p$,
$f(a)\in\mathrm{Lin}_{Aa}$, then $[f]_{p}$ lies in a $\mathrm{k}$-internal
$A$-definable set.

We follow the ideas underlying the proof of [HHM08, Proposition 6.9]. A key
ingredient of this proof is that there cannot be large $\mathrm{dcl}$-closed
chains inside $\mathrm{Lin}_{A}$ — see Corollary 5.8. We start by describing
the growth of $\mathrm{dcl}$ in $\mathrm{Lin}_{A}$.

######  Lemma 5.5.

Let $a$ be a finite tuple in $M^{\mathrm{eq}}$ and $A$ any base structure.
There is some set $Z_{a}\subseteq\mathrm{acl}(A)$ such that $|Z_{a}|\leq|T|$
and $\operatorname{tp}(a/\mathrm{acl}(A))$ is
$\mathrm{dcl}(A,Z_{a})$-invariant.

###### Proof.

The structure $M$ is $\mathrm{NIP}$, _e.g._ see [JS20, Theorem 3.3]. The
statement then follows immediately from [She90, Chapter III, Theorem 7.5]. ∎

######  Lemma 5.6.

Let $U$ be an open $Ac$-$\infty$-definable generalized ball. Let $a$ be a
generic element of $U$ over $Ac$. Then
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aac))\subseteq\mathrm{acl}(Ab)$.

###### Proof.

Let $f:U\to\mathrm{Lin}_{A}$ be some $Ac$-definable function and let
$\mathrm{cut}(U)$ be the cut of $U$. Fix some $e\in U(M)$. For now, we work
over $M$, so we can assume that $e=0$ and we can identify the sorts in
$\mathrm{Lin}_{A}$ with some $\mathrm{k}^{n}$. For every
$\gamma\in\mathrm{cut}(U)$ and $d\in\mathrm{Lin}_{A}$, let
$X_{d,\gamma}=\\{x\in U:\mathrm{v}(x)=\gamma$ and $f(x)=d\\}$. Then by
Proposition 2.3, there exists a finite set $C\subseteq U(M)$ which does not
depend on $\gamma$ or $d$, such that for every ball $b$, if $b\cap
C\neq\emptyset$, then $b\cap X_{d,\gamma}\neq\emptyset$ implies that
$b\subseteq X_{d,\gamma}$.

If $a\in U$ is not in the smallest ball $b$ containing $C$ and $0$, then the
open ball of radius $\mathrm{v}(a)$ around $a$ — that is $\mathrm{rv}(a)$ — is
entirely contained in $X_{f(a),\mathrm{v}(a)}$. In other words, $f$ induces a
well-defined function $\bar{f}:\mathrm{rv}(U\setminus b)\to\mathrm{k}^{n}$.

######  Claim 5.6.1.

Let $f:\mathrm{RV}\to\mathrm{k}$ be $M$-definable. Then there are finitely
many $\gamma_{i}\in\Gamma(M)$ such that
$f(\\{x\in\mathrm{RV}:\mathrm{v}(x)\neq\gamma_{i}\\})$ is finite.

###### Proof.

For any choice of $\alpha\in\mathrm{k}$ and $\gamma\in\Gamma$ (in some $N\succ
M$), we find an automorphism
$\sigma\in\mathrm{Aut}(\mathrm{RV}(N)/\mathrm{RV}(M),\mathrm{k}(N))$ such
that, if $\mathrm{v}(x)=\gamma$, then $\sigma(x)=x+\alpha$. First, we find a
group morphism $f:\Gamma\to\mathrm{k}$ sending $\gamma$ to $\alpha$ and
$\Gamma(M)$ to $0$. Indeed, $\gamma\nin\mathbb{Q}\otimes\Gamma(M)$ and hence,
it suffices to choose images for $n^{-1}\gamma$, for every
$n\in\mathbb{Z}_{>0}$, which we can do (coherently) because $\mathrm{k}$ is
algebraically closed. This $f$ induces an automorphism
$\sigma\in\mathrm{Aut}(\mathrm{RV}(N)/\mathrm{RV}(M),\mathrm{k}(N))$ defined
by $\sigma(x)=x+f(\mathrm{v}(x))$.

Let $x,y\in\mathrm{RV}$ be such that
$\mathrm{v}(x)=\mathrm{v}(y)\nin\Gamma(M)$. Then, by the above paragraph,
there is an automorphism $\sigma$ fixing $\mathrm{k}$ and $M$, and hence $f$,
and such that $\sigma(x)=\sigma(y)$. It follows that
$f(x)=\sigma(f(x))=f(\sigma(x))=f(y)$. By compactness, it follows that there
are finitely many $\gamma_{i}\in\Gamma(M)$ such that $f$ induces a function
$\Gamma\setminus\bigcup_{i}\gamma_{i}\to\mathrm{k}$. This function has finite
image by orthogonality of $\mathrm{k}$ and $\Gamma$. ∎

Thus we have found an $\mathfrak{L}(M)$-definable closed ball $b\subset U$
such that $f(U\setminus b)$ is finite. Let us conclude the proof by showing
that $b$ can be replaced by a generalized $\mathfrak{L}(Ac)$-definable ball.
If there are two such $\mathfrak{L}(M)$-definable closed balls with empty
intersection, then $f(U)$ is finite. If not, they form a chain and their
intersection is an $\mathfrak{L}(Ac)$-definable generalized subball $B$ of $U$
such that $f(U\setminus B)$ is finite. In both cases, if $a$ is generic in $U$
over $Ac$, $f(a)$ is in a finite $\mathfrak{L}(Ac)$-definable set. In other
words, $\mathrm{Lin}_{A}(\mathrm{dcl}(Aac))\subseteq\mathrm{acl}(Ac)$. ∎

######  Proposition 5.7.

Let $a\in K^{n}(M)$ and $A=\mathrm{dcl}(A)$ be a set of parameters. Then there
is some set $Z\subseteq\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))$ such that
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{dcl}(A,Z)$ and
$|Z|\leq|T|$.

###### Proof.

We adapt the proof of [HHM08, Corollary 9.6] and start by proving the
following claim:

######  Claim 5.7.1.

There is a countable tuple $c\in\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))$ such that
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{acl}(Ac)$.

###### Proof.

By backwards induction, we construct an increasing sequence of tuples
$d_{n}\subseteq\dots\subseteq d_{1}$ in $\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))$
such that, for every $i\leq n$, we have
$d_{i}\in\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{\leq i},d_{>i}))$ and
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{\leq
i},d_{>i}))\subseteq\mathrm{acl}(\mathrm{Lin}_{A}(a_{<i},d_{i}))$. Fix $i\leq
n$ and suppose $d_{>i}$ has been constructed. Let $W=\\{B\ |\ a_{i}\in B$ and
$B$ is a $Aa_{<i}d_{>i}$-definable generalized ball$\\}$. Then $a_{i}$ is
generic in the $\infty$-$Aa_{<i}d_{>i}$-definable generalized ball

$U=\bigcap_{b\in W}b.$

If $U$ is open, let $d_{i}=d_{i+1}$. Then, by Lemma 5.6,

$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{\leq
i},d_{i>}))=\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{\leq
i},d_{i+1}))\subseteq\mathrm{Lin}_{A}(\mathrm{acl}(a_{<i},d_{i})).$

If $U$ is closed, let
$y_{0}=\mathrm{res}_{U}(a_{i})\in\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{\leq
i},d_{>i}))$. Let $U_{0}$ be intersection of all
$Aa_{<i}d_{>i}y_{0}$-definable generalized ball containing $a_{i}$. Either
$U_{0}$ is open, or we set
$y_{1}=\mathrm{res}_{U_{0}}(a_{i})\in\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{\leq
i},d_{>i}))$. We continue this process unless $U_{i}$ is open and we set
$U_{\omega}=\bigcap_{j}U_{j}$. Then $a_{i}$ is generic in the
$Aa_{<i}d_{i>i}y_{\geq 0}$-definable open generalized ball $U_{\omega}$. By
Lemma 5.6, $\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{\leq
i},d_{i}))\subseteq\mathrm{acl}(\mathrm{Lin}_{A}(\mathrm{dcl}(Aa_{<i},d_{>i},y_{\geq
0})))$, so we set $d_{i}=d_{>i}y_{\geq 0}$. Taking $c=d_{1}$, we have
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{acl}(Ab)$. ∎

We might replace $A$ by $\mathrm{dcl}(Ac)$ and assume that
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{acl}(A)$. By Lemma 5.5,
there is $Z_{a}\subseteq\mathrm{acl}(A)$ such that $|Z_{a}|\leq|T|$ and
$\operatorname{tp}(a/\mathrm{acl}(A))$ is $\mathrm{dcl}(A,Z_{a})$-invariant.
In particular,

$\mathrm{dcl}(Aa)\cap\mathrm{acl}(A)\subseteq\mathrm{dcl}(A,Z_{a}).$ (1)

For any tuple $z\in Z_{a}$,
$\operatorname{tp}(z/A\mathrm{Lin}_{A}(\mathrm{dcl}(Aa)))$ is isolated,
because $z\in\mathrm{acl}(A)$. So there is some
$z^{\prime}\in\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))$ such that
$\operatorname{tp}(z/A,z^{\prime})\vdash\operatorname{tp}(z/A,\mathrm{Lin}_{A}(\mathrm{dcl}(Aa)))$.
Let $Z=\\{z^{\prime}|z\in Z_{a}^{m},m=1,2,\dots\\}$. By construction
$Z\subseteq\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))$, $|Z|\leq|T|$ and
$\operatorname{tp}(Z_{a}/A,Z)\vdash\operatorname{tp}(Z_{a}/A,\mathrm{Lin}_{A}(\mathrm{dcl}(Aa)))$.
Because $\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{acl}(A)$, by Eq.
1,
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{dcl}(Aa)\cap\mathrm{acl}(A)\subseteq\mathrm{dcl}(A,Z_{a})$.
Consequently, $\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{dcl}(A,Z)$,
as required. ∎

######  Corollary 5.8.

Let $\mathrm{dcl}(A)=A\subseteq M$ be a small set of parameters. Let $e\in
M^{eq}$, then there is no strictly ascending chain of length $(2^{|T|})^{+}$
of sets $B=\mathrm{dcl}(B)\cap\mathrm{Lin}_{A}$ between $\mathrm{Lin}_{A}$ and
$\mathrm{Lin}_{A}(\mathrm{dcl}(Ae))$.

###### Proof.

The proof follows ideas from [HHM08, Lemma 6.5], replacing $St_{C}$ by
$\mathrm{Lin}_{A}$ and applying Proposition 5.7. We include details for sake
of completeness.

Let $a\in K$ be a tuple such that $e\in\mathrm{dcl}(a)$. By Proposition 5.7
there is some subset $Z\subseteq\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))$ such that
$|Z|\leq|T|$ and
$\mathrm{Lin}_{A}(\mathrm{dcl}(Aa))\subseteq\mathrm{dcl}(A,Z)$. Let
$(B_{\alpha}\ |\ \alpha\in(2^{|T|})^{+})$ be an increasing chain of definably
closed subsets of
$\mathrm{Lin}_{A}(\mathrm{dcl}(Ae))\subseteq\mathrm{dcl}(A,Z)$ ordered by
inclusion with $B_{0}=A$. Since the residue field is algebraically closed,
$\mathrm{Lin}_{A}$ is stable. Thus
$\operatorname{tp}(Z/\bigcup_{\alpha\in(2^{|T|})^{+}}B_{\alpha})$ is
definable. By local character, it is definable over $B_{\mu}$ for some $\mu$.
Let $c\in B_{\mu+1}$. Then there is an $A$-definable function and a tuple
$z\in Z$ such that $c=f(z)$. Because $\operatorname{tp}(Z/AB_{\mu+1})$ is
$B_{\mu}$-definable then $\\{x\in AB_{\mu+1}\ |\ f(z)=x\\}$ is
$B_{\mu}$-definable and is a singleton. Since $B_{\mu}$ is definably closed
$c\in B_{\mu}$ and the chain stabilizes. ∎

###### Proof of Proposition 5.4.

We work in a sufficiently saturated and homogeneous elementary extension of
$M$. Let $f_{d}$ be an $A$-definable family of functions such that, for all
$d$ and $a\models p$, $f_{d}(a)$ is defined and in $\mathrm{Lin}_{Aa}$. Let
$\Theta$ be the $A$-interpretable set of all $[f_{m}]_{p}$.

We first argue that for a given $d$, there is an $n\in\mathbb{Z}_{\geq 0}$ and
$A$-definable function $\gamma$ such that for any realization $a_{<n}\models
p^{\otimes n-1}|_{Ad}$ we have $\gamma(a_{<n},b_{<n})=[f_{d}]_{p}$ where
$b_{i}=f_{d}(a_{i})$.

Let $I$ be a linear order without endpoints. Take a Morley sequence in $p$ of
order type $I$ over $Ad$, i.e. $a_{i}\vDash p|_{Ada_{<i}}$. Let
$D=A(a_{i})_{i\in I}$ and $b_{i}=f_{d}(a_{i})$, for $i\in I$. If $I$ is
sufficiently large, we can find an increasing strict sequence of initial
segments $(I_{\alpha})_{\alpha\in(2^{|T|})^{+}}$. For each
$\alpha\in(2^{|T|})^{+}$ we let
$E_{\alpha}=\mathrm{Lin}_{D}(\mathrm{dcl}(D(b_{i})_{i\in
I_{\alpha}}))\subseteq\mathrm{Lin}_{D}(\mathrm{dcl}(Dd))$. By Corollary 5.8
(applied to $\mathrm{Lin}_{D}(Dd)$) the sequence
$(E_{\alpha})_{\alpha\in(2^{|T|})^{+}}$ is eventually constant, thus there is
some $\ell\in I$ such that $b_{\ell}\in\mathrm{dcl}(Db_{<\ell})$.

######  Claim 5.8.1.

There is some $n\in\mathbb{Z}_{>0}$ such that for any $i_{1}<\dots<i_{n}$ in
$I$, we have
$b_{i_{n}}\in\mathrm{dcl}(A,a_{i_{1}},\dots,a_{i_{n}},b_{i_{1}},\dots,b_{i_{n-1}})$.

###### Proof.

Since the sequence $(a_{i})_{i\in I}$ is $Ad$-indiscernible there are
$n,m\in\mathbb{Z}_{>0}$ such that $i_{1}<\dots<i_{n}<j_{1}<\dots<j_{m}$ and:

$b_{i_{n}}\in\mathrm{dcl}(Aa_{i_{1}},\dots,a_{i_{n}},b_{i_{1}},\dots,b_{i_{n-1}},a_{j_{1}},\dots,a_{j_{m}}).$

To simplify the notation we write $I_{\leq s}$ for $i_{1}<\dots<i_{s}$, and
$J_{\leq k}$ for $j_{1}<\dots<j_{k}$. Let
$b^{\prime}_{i_{n}}\equiv_{Aa_{I_{\leq n}}b_{I_{<n}}}b_{i_{n}}$, we aim to
show that $b_{i_{n}}^{\prime}\equiv_{Aa_{I_{\leq n}},b_{I_{<n}}a_{J_{\leq
n}}}b_{i_{n}}$, and therefore $b_{i_{n}}\in\mathrm{dcl}(Aa_{I_{\leq
n}}b_{I_{<n}})$. For each $k\leq m$, we can assume $a_{j_{k}}\vDash
p|_{Aa_{I}b_{I_{<n}}b_{i_{n}}b^{\prime}_{i_{n}}a_{J_{\leq k-1}}}$. Suppose
that there is a formula $\phi(x,a_{I_{\leq n}},b_{I_{\leq n-1}},a_{J_{\leq
m}})$ such that $\phi(b_{i_{n}},a_{I_{\leq n}},b_{I_{\leq n-1}},a_{J_{\leq
m}})$ holds while $\neg\phi(b^{\prime}_{i_{n}},a_{I_{\leq n}},b_{I_{\leq
n-1}},a_{J_{\leq m}})$ holds. Since $p$ is $A$ definable, so it is $p^{\otimes
n+m}$ thus there is a $A$-formula $\psi(x,y)$ such that
$\psi(b_{i_{n}},b_{I_{\leq n-1}})$ holds while
$\psi(b^{\prime}_{i_{n}},b_{I_{\leq n-1}})$ does not. This contradicts that
$b_{i_{n}}$ and $b^{\prime}_{i_{n}}$ elements have the same type over
$Aa_{I_{\leq n}}b_{I_{<n}}$. ∎

By indiscernability over $Ad$, for any $a_{\leq n}\models p^{\otimes n}|_{Ad}$
and $b_{i}=f_{d}(a_{i})$, we have $b_{n}\in\mathrm{dcl}(Aa_{\leq n}b_{<n})$.
so there is an $Aa_{<n}b_{<n}$-definable function $h_{a_{<n}b_{<n}}$ sending
$a_{n}$ to $b_{n}$. Note that $a_{n}\vDash p|_{Ada_{<n}b_{<n}}$, since
$a_{n}\vDash p|_{Aa_{<n}d}$ and $b_{<n}\in\mathrm{dcl}(Ada_{<n})$.
Summarizing, we have that $h_{a_{<n}b_{<n}}(a_{n})=b_{n}$,
$f_{d}(a_{n})=b_{n}$ and $a_{n}\vDash p|_{Ada_{<n}b_{<n}}$, consequently
$[h_{a_{<n}b_{<n}}]_{p}=[f_{d}]_{p}$. Let $\gamma$ be an $A$-definable
function such that $\gamma(a_{<n},b_{<n})=[h_{a_{<n}b_{<n}}]_{p}$.

For each fixed realization $a_{<n}\vDash p^{<n}$ let
$\Theta_{a_{<n}}=\\{\gamma(a_{<n},b_{<n}^{\prime})\ |\ \text{for all choices
of $b_{<n}^{\prime}$}\\}$, which is internal to the residue field as it is
$\mathrm{Lin}_{Aa_{<n}}$-internal. In particular $\Theta_{a_{<n}}$ is stable.
Given $d\in M$, if $a_{<n}\vDash p^{\otimes n-1}|_{Ad}$ then
$[f_{d}]_{p}=\gamma(a_{<n},b_{<n})\in\Theta_{a_{<n}}$. Then
$\Theta(M)\subseteq\Theta_{a_{<n}}$ and $\Theta$ is stable.

######  Claim 5.8.2.

Finitely many $\Theta_{a}$ cover $\Theta$.

###### Proof.

We proceed by contradiction. By induction we construct $a_{i}$ and $e_{i}$
such that:

  * •

$a_{i+1}\vDash p^{\otimes n-1}|_{Aa_{\leq i}e_{\leq i}}$.

  * •

$e_{i}\in\Theta\backslash(\Theta_{a_{0}}\cup\dots\cup\Theta_{a_{i}})$.

Then $e_{i}\in\Theta_{a_{j}}$ if and only if $j>i$, but this contradicts the
stability of $\Theta$. ∎

Since each $\Theta_{a_{j}}$ is internal to the residue field, $\Theta$ also
is. ∎

###  5.2 Divisible ordered abelian groups with cuts

Proposition 5.4 is particularly useful if $\mathrm{k}$-internal sets in $M$
are entirely classified. By Corollary 3.20, this is the case if $\Gamma(M)$ is
dense and $M$ eliminates imaginaries down to $\mathcal{G}$ and
$\Gamma^{\mathrm{eq}}$. But this is not very helpful to understand imaginaries
in $M$, _a priori_. What we can do, however, is use these results in a well-
chosen extension of $M$, namely its algebraic closure in which we have named
certain cuts on the valued group to preserve definability of the types we are
interested in.

We will now study its value group. All other required results will follow by
standard methods — mostly the resplendence of every result involved.

######  Definition 5.9.

Let $\mathfrak{L}$ be the language of ordered groups with unary predicates
$(\mathcal{C}_{i})_{i\in I}$ and, for every $i$ in some $I_{0}\subseteq I$,
constants $a_{i}$. Let $T$ be a theory of ordered abelian groups such that:

  1. 1.

for every $i\in I$, the $\mathcal{C}_{i}$ are distinct cuts which are not
translates of $0^{+}$;

  2. 2.

for some fixed $i\in I$, $\mathcal{C}_{i}=0^{-}$;

  3. 3.

for every $i\in I$, $\mathcal{C}_{i}$ is a translate of $0^{-}$ if and only if
$i\in I_{0}$, and, in that case $\mathcal{C}_{i}=a_{i}^{-}$.

  4. 4.

for every $i,j\in I$, for some fixed $\ell$,
$\mathcal{C}_{\ell}=\mathcal{C}_{i}+\mathcal{C}_{j}=\\{x+y:x\in\mathcal{C}_{i},\
y\in\mathcal{C}_{j}\\}$;

  5. 5.

For every $i$, for some fixed $\ell$,
$\mathcal{C}_{\ell}=-\mathcal{C}_{i}=\\{y:\forall
x\in\mathcal{C}_{i}\\}\,y>-x$ — unless $i\in I_{0}$, in which case
$\mathcal{C}_{\ell}=-\mathcal{C}_{i}\cup\\{-a_{i}\\}$.

######  Proposition 5.10.

The theory $T$ eliminates quantifiers.

###### Proof.

Let $G,H\models T$ with $H$ $|G|^{+}$-saturated, let $A\leq G$ and let $f:A\to
H$ be an embedding. For every $g\in G$ we have to show that $f$ extends to
$g$.

First, if $g\in\mathbb{Q}\otimes A$, let $n>0$ be minimal such that $ng\in A$.
Then, for every $a\in A$, $g\geq a$ if and only if $ng\geq na$ and
$g\in\mathcal{C}_{i}$ if and only if $ng\in n\mathcal{C}_{i}$. So $f$ extends
(uniquely) by defining $f(g)=n^{-1}f(ng)$.

If $g\nin\mathbb{Q}\otimes A$, let $L$ be the set of triples $(n,a,i)$, with
$n\in\mathbb{Z}$, $a\in A$ and $i\in I$, such that $ng\in a+\mathcal{C}_{i}$.
Since $ng\in a+\mathcal{C}_{i}$ if and only if $nmg\in ma+m\mathcal{C}_{i}$,
in order for the set $\Sigma=\\{nx\in a+\mathcal{C}_{i}:(n,a,i)\in
L\\}\cup\\{nx\nin a+\mathcal{C}_{i}:(n,a,i)\nin L\\}$ to be satisfied in $H$,
it suffices to check that, if
$(a+\mathcal{C}_{i})\setminus(b+\mathcal{C}_{j})\neq\emptyset$ (because it
contains $ng$, for some $n\in\mathbb{Z}$), then
$(f(a)+\mathcal{C}_{i})\setminus(f(b)+\mathcal{C}_{j})\neq\emptyset$. But
$a+\mathcal{C}_{i}\subseteq b+\mathcal{C}_{j}$ if and only if
$a-b\in\mathcal{C}_{i}-\mathcal{C}_{j}$, so $a+\mathcal{C}_{i}\subseteq
b+\mathcal{C}_{j}$ (in $G$) if and only if $f(a)+\mathcal{C}_{i}\subseteq
f(b)+\mathcal{C}_{j}$ (in $H$). Consequently, $\Sigma$ is realized by some
$h\in H$, and we can extend $f$ by sending $g$ to $h$. ∎

######  Remark 5.11.

It follows that $T$ is weakly o-minimal and hence $\mathrm{NIP}$.

######  Corollary 5.12.

Models of $T$ have Property D.

###### Proof.

Given $G\models T$, it follows from Proposition 5.10 that any definable cut of
$G$ is of the form $g+n^{-1}\mathcal{C}_{i}$ for some $g\in G$, $n>0$ and
$i\in I$. It follows that any definable $<$-type over $G$ has most two
completions which are both definable. ∎

###  5.3 Invariant resolutions

We are now fully equipped to prove Proposition 5.16, of which Theorem 5.3 will
follow as in [HR21, Section 4].

Let $M$ be an $\mathrm{RV}$-expansion of a model of $\mathrm{Hen}_{0,0}$ which
is sufficiently saturated and homogeneous and $A\subseteq\mathcal{G}(M)$. By
Proposition 4.2 there exists a $\Gamma$-expansion $M_{0}^{\prime}$ of
$M_{0}=M^{\mathrm{a}}$ (in the language $\mathfrak{L}_{0}^{\prime}$) such
that, the unique extension to $M_{0}$ of any $\mathfrak{L}(A)$-definable type
in $\mathcal{S}^{0}(M)$ is $\mathfrak{L}^{\prime}_{0}(A)$-definable —
effectively, this extends every $\mathfrak{L}(A)$-definable cut to
$M_{0}=M^{\mathrm{a}}$ in a way that is compatible with the coding of types.

Recall that we identify the set $\mathcal{G}(M)$ in $M_{0}^{\prime}$ with a
subset of $\mathcal{G}(M)$ in $M$. By Proposition 5.10, we can also identify
the set $\Gamma^{\mathrm{eq}}(M)$ in $M_{0}^{\prime}$ with a subset of
$\Gamma^{\mathrm{eq}}(M)$ in $M$. We do, however, have to code the imaginaries
of $M$ that $M_{0}^{\prime}$ believes to be geometric:

######  Lemma 5.13.

For every $e\in\mathrm{dcl}_{0}^{\prime}(M)$, there is an
$\varepsilon\in\mathcal{G}(M)\cup\Gamma^{\mathrm{eq}}(M)$ such that
$e\in\mathrm{dcl}_{0}^{\prime}(\varepsilon)$ and
$\varepsilon\in\mathrm{acl}_{0}^{\prime}(e)$.

###### Proof.

If $e\in\mathrm{dcl}_{0}^{\prime}(M)$, there exists an
$\mathfrak{L}_{0}^{\prime}$-definable map and $m\in\mathrm{K}(M)$ a tuple,
such that $e=f(m)$. Let $X=f^{-1}(e)$ and
$E=\mathcal{G}(\mathrm{acl}_{0}^{\prime}(e))$. By Theorem 4.1 in
$M_{0}^{\prime}$, there exists an $\mathfrak{L}_{0}^{\prime}(E)$-definable
type $p$ such that $p\models f(x)=e$. By Proposition 4.2, $p$ is the unique
extension of its restriction to $M$, whose code
$\varepsilon\in\mathcal{G}(M)\cup\Gamma^{\mathrm{eq}}(M)$, is also a code of
$p$. Then $\varepsilon\in E\subseteq\mathrm{acl}_{0}^{\prime}(e)$ and, since
$p\models f(x)=e$, $e\in\mathrm{dcl}_{0}^{\prime}(\varepsilon)$. ∎

Our goal, to prove Proposition 5.16, is to find a subset of $\mathrm{K}$ which
generates $A$ and “canonical” generators of $\mathrm{rv}(M(C))$. By the
following lemma, this will imply that $\operatorname{tp}(C/M)$ is invariant
over some large (stably embedded definable) set:

######  Lemma 5.14.

Let $N\succ M$, let $D\subseteq M$ be potentially large, let
$a\in\mathrm{K}(M)$ be a tuple and let $\rho$ be a
pro-$\mathfrak{L}_{0}^{\prime}(M)$-definable map. Assume that
$\mathrm{rv}(M(a))\subseteq\mathrm{dcl}_{0}^{\prime}(D\rho(a))$ and that
$p_{0}=\operatorname{tp}_{0}^{\prime}(a/M)$ and $[\rho]_{p_{0}}$ are
$\mathrm{Aut}(M/D)$-invariant. Then $p=\operatorname{tp}(a/M)$ has
$\mathrm{Aut}(M/D)$-invariant $\mathrm{RV}$-germs.

This is essentially [HR21, Lemma 4.2.5] in a slightly different context and
the proof is identical. The main ingredient is elimination of quantifier down
to $\mathrm{RV}$ — see Theorem 2.1.

###### Proof.

Let $N_{0}^{\prime}$ a large saturated elementary extension of
$M_{0}^{\prime}$ containing $N$. Fix $\sigma\in\mathrm{Aut}(M/D)$. Since
$p=\operatorname{tp}_{0}^{\prime}(a/M)$ is $\mathrm{Aut}(M/D)$ invariant,
there is an $\mathfrak{L}_{0}^{\prime}$-elementary embedding
$\tau:M(a)\rightarrow M(a)$ extending $\sigma$. Because $[\rho]_{p_{0}}$ is
$\mathrm{Aut}(M/D)$-invariant, we have $\rho(a)=\sigma(\rho)(a)$.
Consequently, since $rv(M(a))\subseteq\mathrm{dcl}_{0}^{\prime}(D,\rho(a))$,
$\tau|_{rv(M(a))}$ is the identity map. By Theorem 2.1 in $N_{0}^{\prime}$,
extending $\tau$ by the identity on $\mathrm{RV}(N_{0}^{\prime})$ yields an
$\mathfrak{L}_{0}^{\prime}$-elementary embedding. Since $\mathrm{RV}$ is
stably embedded, this embedding further extends to an element $\tau$ of
$\mathrm{Aut}(N_{0}/D,\mathrm{RV}(N_{0}^{\prime}),a)$ — _cf._ [TZ12, Lemma
10.1.5].

By Theorem 2.1 (in $M$ now), $\tau|_{M(a)\cup\mathrm{RV}(N)}$ is
$\mathfrak{L}$-elementary. Consequently,
$\operatorname{tp}(a,M)=\operatorname{tp}(a,\sigma(M))$ and we conclude that
$\sigma(p)=p$, as required. Lastly, we argue that $\operatorname{tp}(a/M)$ has
$\mathrm{Aut}(M/C)$-invariant $\mathrm{RV}$-germs. Let
$X\subseteq\mathrm{RV}^{n}$ be $\mathfrak{L}(Ma)$-definable. Then, by Theorem
2.1, it is $\mathfrak{L}(\mathrm{rv}(M(a)))$-definable and hence
$X(N)=\tau(X(N))=\tau(X)(N)$. Equivalently, $\sigma$ fixes the $p$-germ of any
$\mathfrak{L}(M)$-definable function
$f:p\rightarrow\mathrm{RV}^{\mathrm{eq}}$. ∎

Let us now describe how $\mathrm{RV}$ grows when adding one field element:

######  Lemma 5.15.

Let $a\in N\succ M$ be such that $q=\operatorname{tp}_{0}^{\prime}(a/M)$ is
$\mathfrak{L}_{0}^{\prime}(A)$-definable. Let $b(a)$ be an
$\mathfrak{L}_{0}^{\prime}(Aa)$-definable generalized ball. Let
$c\models\eta_{b(a)}|Ma$ and $p=\operatorname{tp}_{0}^{\prime}(ac/M)$. Then
there is a (pro-)$\mathfrak{L}_{0}^{\prime}(M)$-definable map $\rho$ such that
$[\rho]_{p}\in\mathrm{dcl}_{0}^{\prime}(A,\mathrm{Lin}_{A}(M),\Gamma(M))$ and
$\mathrm{rv}(M(ac))\subseteq\mathrm{dcl}_{0}^{\prime}(\mathrm{rv}(M(a)),\rho(ac))$.

###### Proof.

We proceed by cases. If $b(a)$ is an open generalized ball, by [HR21, Lemma
4.3.10] there is a (pro-)$\mathfrak{L}_{0}^{\prime}(M)$-definable map $\rho$
whose $p$-germ is $\mathrm{Aut}(M/A)$-invariant and such that
$\mathrm{rv}(M(ac))\subseteq\mathrm{dcl}_{0}(\mathrm{rv}(M(a)),\rho(ac))$.
Note that, in equicharacteristic zero, condition (2) of [HR21, Lemma 4.3.10]
is verified as soon as $b(a)$ is not a closed ball.

If $b(a)$ is a closed ball, by Corollary 2.5 there is an
$\mathfrak{L}_{0}^{\prime}(M)$ definable function $g$ such that $g(a)\in
b(a)$. By [HR21, Lemma 4.3.13], we have

$\mathrm{rv}(M(ac))\subseteq\mathrm{dcl}_{0}(\mathrm{rv}(M(a)),\mathrm{res}_{b(a)}(c),\mathrm{res}_{b(a)}(g(a))).$

Let $h(a)=\mathrm{res}_{b(a)}(g(a))\in\mathrm{Lin}_{Aa}$. By Proposition 5.4
applied in $M_{0}^{\prime}$, $[h]_{q}$ lies in an
$\mathfrak{L}_{0}^{\prime}(A)$-definable $\mathrm{k}$-internal set. By Lemma
5.13, there exists $\varepsilon\in\mathcal{G}(M)\cup\Gamma^{\mathrm{eq}}(M)$
such that $\varepsilon\in\mathrm{acl}_{0}([h]_{q})$ and
$[h]_{q}\in\mathrm{dcl}_{0}^{\prime}(\varepsilon)$. Then $\varepsilon$ lies in
an $\mathfrak{L}_{0}^{\prime}(A)$-definable almost $\mathrm{k}$-internal set.
Since $\Gamma(M_{0})=\Gamma(M^{\mathrm{a}})$ is dense, by Corollary 3.20,
$\varepsilon\in A\cup\mathrm{Lin}_{A}(M)$.

Let $\rho(ac)=(\mathrm{res}_{b(a)}(c),\mathrm{res}_{b(a)}(g(a)))$. Since
$\mathrm{res}_{b(a)}(c)\in\mathrm{dcl}_{0}^{\prime}(Aac)$, we indeed have
$[\rho]_{p}\in\mathrm{dcl}_{0}^{\prime}(A,\mathrm{Lin}_{A}(M))$ and
$\mathrm{rv}(M(ac))\subseteq\mathrm{dcl}_{0}(\mathrm{rv}(M(a)),\rho(ac))$. ∎

We can now prove the existence of sufficiently invariant resolutions of
geometric points:

######  Proposition 5.16.

There exists $C\subseteq\mathrm{K}(N)$, for some $N\succ M$, such that
$\operatorname{tp}(C/M)$ has
$\mathrm{Aut}(M/A,RV(M),\mathrm{Lin}_{A}(M))$-invariant $\mathrm{RV}$-germs
and $A\subseteq\mathrm{dcl}_{0}^{\prime}(C)$.

###### Proof.

Replacing $A$ by $A\cup\Gamma(M)$, we may assume that
$\mathrm{Cut}(\mathrm{dcl}_{0}^{\prime}(A))\subseteq\mathrm{dcl}_{0}^{\prime}(\Gamma(A))$.
By iterating Lemma 5.15, we construct an
$\mathfrak{L}_{0}^{\prime}(A)$-definable type
$p_{0}=\operatorname{tp}_{0}^{\prime}(c/M)$ and an
$\mathfrak{L}_{0}^{\prime}(M)$-definable function $\rho$ such that

  * •

$\mathrm{rv}(M(c))\subseteq\mathrm{dcl}_{0}^{\prime}(A,\mathrm{RV}(M),\rho(c))$;

  * •

$[\rho]_{p_{0}}\in\mathrm{dcl}_{0}^{\prime}(A,\mathrm{Lin}_{A}(M),\Gamma(M))$;

  * •

any $\mathfrak{L}_{0}^{\prime}(Ac)$-definable generalized ball $b$ has a point
in $C$;

  * •

for every $\mathfrak{L}_{0}^{\prime}(Ac)$-definable convex subgroup
$\Delta\leq\Gamma$, $\Gamma/\Delta(\mathrm{acl}_{0}^{\prime}(Ac))\subseteq
v_{\Delta}(\mathrm{K}(C))$.

Then, by Lemma 4.6,
$A=\mathcal{G}(A)\subseteq\mathrm{dcl}_{0}^{\prime}(\mathrm{Cut}(\mathrm{dcl}_{0}^{\prime}(A)),C)\subseteq\mathrm{dcl}_{0}^{\prime}(\Gamma(A),C)\subseteq\mathrm{dcl}_{0}^{\prime}(C)$.
Also, by Lemma 5.14, $\operatorname{tp}(C/M)$ has
$\mathrm{Aut}(M/A,\mathrm{RV}(M),\mathrm{Lin}_{A}(M))$-invariant
$\mathrm{RV}$-germs. ∎

We now deduce Theorem 5.3 from Proposition 5.16 and the machinery of [HR21,
Section $4$].

###### Proof of Theorem 5.3.

Fix $A\subseteq\mathcal{G}(M)$ and $a$ in some elementary extension of $M$
such that $p=\operatorname{tp}_{0}(a/M)$ is $\mathrm{Aut}(M/A)$-invariant.

  * •

By Proposition 5.16, we find $C\subseteq\mathrm{K}(N_{1})$, for some
$N_{1}\succ M$ (sufficiently saturated and homogeneous), such that
$\operatorname{tp}(C/M)$ has
$\mathrm{Aut}(M/A,\mathrm{RV}(M),\mathrm{Lin}_{A}(M))$-invariant
$\mathrm{RV}$-germs and $A\subseteq\mathrm{dcl}_{0}^{\prime}(C)$.

  * •

By [HR21, Corollary 4.4.3], we find $\widehat{C}\prec N_{2}$, for some
$N_{2}\succ N_{1}$ (sufficiently saturated and homogeneous), such that
$\widehat{C}$ contains a realization of every type over $C$ and such that
$\operatorname{tp}(\widehat{C}/N_{1})$ is
$\mathrm{Aut}(N_{1}/C,\mathrm{RV})$-invariant — _i.e._ has
$\mathrm{Aut}(N_{1}/C,\mathrm{RV}(M))$-invariant $\mathrm{RV}$-germs.

  * •

We may assume that $a\models p|_{M_{2}}$ — _cf._ [HR21, Claim 4.4.7]. Since
$A\subseteq\mathrm{dcl}(C)\subseteq\widehat{C}$,
$\operatorname{tp}_{0}(a/N_{1})=p|_{M_{2}}$ is
$\mathrm{Aut}(N_{1}/\widehat{C})$-invariant. By [HR21, Corollary 4.3.17],
$\operatorname{tp}(a/N_{2})$ is
$\mathrm{Aut}(N_{2}/\widehat{C},\mathrm{RV})$-invariant.

By repeated use of transitivity (Lemma 5.2), $\operatorname{tp}(a/N_{1})$ is
$\mathrm{Aut}(N_{1}/C,\mathrm{RV})$-invariant and hence
$\operatorname{tp}(a/M)$ is
$\mathrm{Aut}(M/A,\mathrm{RV}(M),\mathrm{Lin}_{A}(M))$-invariant. ∎

##  6 Eliminating imaginaries

Following the general strategy of [HR21, Theorem 6.1.1], we can now deduce
elimination of imaginaries.

######  Proposition 6.1.

Let $M$ be an $\mathrm{RV}$-expansion of a model of $\mathrm{Hen}_{0,0}$.
Assume that the value group satisfies Property D. Let $e\in M^{\mathrm{eq}}$
and $A=\mathrm{acl}(e)$. Then

$e\in\mathrm{dcl}(\mathcal{G}(A),(\mathrm{RV}\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}(A)).$

###### Proof.

Let $M_{1}=M^{\mathrm{ur}}$ and assume $M$ is sufficiently saturated and
homogeneous. There is an $\mathfrak{L}$-definable map $f$ and a tuple $m\in
K(M)$ such that $f(m)=e$. Let $X=f^{-1}(e)$. By Theorem 4.1 we can find a type
$p\in\mathcal{S}^{1}(M)$ such that:

  * •

$p\cup X$ is consistent;

  * •

$p$ is
$\mathfrak{L}_{1}(\mathcal{G}(A)\cup\Gamma^{\mathrm{eq}}(A))$-definable.

Take $a\vDash p\cup X$. Then $\operatorname{tp}_{0}(a/M)$ is
$\mathfrak{L}(\mathcal{G}(A))$-definable. By Theorem 5.3, the type
$q=\operatorname{tp}(a/M)$ is
$\mathrm{Aut}(M/\mathcal{G}(A),\mathrm{RV}(M),\mathrm{Lin}_{\mathcal{G}(A)}(M))$-invariant.

######  Claim 6.1.1.

For every automorphism
$\sigma\in\mathrm{Aut}(M/\mathcal{G}(A),\mathrm{RV}(M),\mathrm{Lin}_{\mathcal{G}(A)}(M))$,
one has $\sigma(e)=e$.

###### Proof.

We have $\sigma(q)=q\vdash f(x)=e$, but we also have $q=\sigma(q)\vdash
f(x)=\sigma(e)$. It follows that $e=\sigma(e)$, proving the claim. ∎

Since $\mathrm{RV}\cup\mathrm{Lin}_{A}$ is stably embedded (_cf._ Remark
3.17), if follows — _e.g._ see [HR21, Lemma 4.2.3] — that

$e\in\mathrm{dcl}(\mathcal{G}(A),\mathrm{RV}(M),\mathrm{Lin}_{\mathcal{G}(A)}(M)).$

So there is a $\mathfrak{L}(\mathcal{G}(A))$-definable function $g$ and a
tuple $c\in\mathrm{RV}^{m}(M)\times\mathrm{Lin}_{\mathcal{G}(A)}^{n}(M)$ such
that $g(c)=e$. Let $Y=g^{-1}(e)$. This is an $A$-definable subset of
$\mathrm{RV}^{m}\times\mathrm{Lin}_{\mathcal{G}(A)}^{n}$. Consequently,
$\ulcorner
Z\urcorner\in(\mathrm{RV}\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}(A)$
and

$e\in\mathrm{dcl}(\mathcal{G}(A),\ulcorner
Z\urcorner)\subseteq\mathrm{dcl}(\mathcal{G}(A)\cup(RV\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}(A)),$

as required. ∎

We now want to describe the imaginaries in $\mathrm{RV}\cup\mathrm{Lin}_{A}$.
This amounts to describing imaginaries in short exact sequences (with
auxiliary sorts) as in [HR21, Proposition 5.2.1]. Let us first proof a version
of that result under alternative finiteness assumptions that focuses on
$\mathrm{A}$.

######  Proposition 6.2.

Let $\mathcal{L}$ be a language with sorts
$\mathcal{A}\sqcup\\{\mathrm{B},\mathrm{C}\\}$. Let $R$ be an integral domain.
Let $M$ be an $\mathcal{L}$-structure which is an
$\mathcal{A}$-$\mathrm{C}$-enrichment — that is an expansion by predicates on
powers of $C$ and predicates on products of sorts in $\mathcal{A}$ — of the
pure (in the sense of model theory) sequence of $R$-modules

$0\rightarrow\mathrm{A}\rightarrow\mathrm{B}\xrightarrow{v}\mathrm{C}\rightarrow
0$ (2)

where $\mathrm{A}\in\mathcal{A}$ and $\mathrm{C}\in\mathcal{C}$. Assume that
the following properties hold:

  1. 1.

$\mathrm{A}$ is a pure $R$-submodule of $\mathrm{B}$ (in the sense of module
theory),

  2. 2.

$\mathrm{C}$ is a torsion free $R$-module,

  3. 3.

For any $l\in R\setminus\\{0\\}$, $A=lA$.

Let $e\in M^{\mathrm{eq}}$, $E=\mathrm{acl}(e)$ and $\Delta=\mathrm{C}(E)$.
Then

$e\in\mathrm{dcl}(\mathrm{C}^{\mathrm{eq}}(E)\cup(\mathcal{A}\cup\mathrm{B}_{\Delta})^{\mathrm{eq}}(E)),$

where $\mathrm{B}_{\Delta}$ denotes the union of all $\mathrm{B}_{\delta}$ for
$\delta\in\Delta$.

###### Proof.

We follow the proof of [HR21, Theorem 5.1.5] with slight modifications. Note
that $\mathcal{A}$ and $\mathrm{C}$ are orthogonal in this structure.

Let $X\subseteq\mathrm{B}^{n}$ be $\mathcal{L}(M)$-definable,
$E=\mathrm{acl}(\ulcorner X\urcorner)$ and $\Delta=\mathrm{C}(E)$. We proceed
by induction on $r=\dim_{R}(X)$, see [HR21, p. 59]. By [HR21, Lemma 5.1.3] we
may assume that there exists an $R$-linear map
$L:\mathrm{B}^{r}\to\mathrm{B}^{n-r}$, $\delta\in\mathrm{C}^{n-r}(E)$ and
$m\in R\setminus\\{0\\}$ such that for every $(x^{\prime},x^{\prime\prime})\in
X$, with $|x^{\prime}|=r$, we have
$mv(x^{\prime\prime})=L(v(x^{\prime}))+\delta$. Let
$X_{m}=\\{(x^{\prime},x^{\prime\prime}):((x^{\prime})^{m},x^{\prime\prime})\in
X$ and $|x^{\prime}|=r\\}$, then $\ulcorner X_{m}\urcorner=\ulcorner
X\urcorner$ and for every $(x^{\prime},x^{\prime\prime})\in X_{m}$ with
$|x^{\prime}|=r$, we have $v(x^{\prime\prime})=L(v(x^{\prime}))+\delta/m$. So
we may assume that $m=1$.

We consider the action of $\mathrm{A}^{r}$ on $\mathrm{B}^{n}$ given by
$a\cdot(x^{\prime},x^{\prime\prime})=(x^{\prime}+a,x^{\prime\prime}+L(a))$. By
[HR21, Claim 5.1.6], and since $l\mathrm{A}=\mathrm{A}$, for every $l\in
R\setminus\\{0\\}$, we may assume that $\mathrm{A}^{r}\cdot X=X$. For every
$c\in\mathrm{C}^{r}$ and $x^{\prime}\in\mathrm{B}^{r}$ with $v(x^{\prime})=c$,
let
$Y_{c}=X_{x^{\prime}}+L(x^{\prime})=\\{x^{\prime\prime}-L(x^{\prime}):(x^{\prime},x^{\prime\prime})\in
X\\}\subseteq B_{\delta}$. This set $Y_{c}$ does not depend on the choice of
$x^{\prime}$. Indeed, if $v(y^{\prime})=c$ and
$(x^{\prime},x^{\prime\prime})\in X$, then
$a=y^{\prime}-x^{\prime}\in\mathrm{A}^{r}$ and hence
$a\cdot(x^{\prime},x^{\prime\prime})=(y^{\prime},x^{\prime\prime}-L(x^{\prime})+L(y^{\prime}))\in
X$. So $x^{\prime\prime}-L(x^{\prime})\in X_{y^{\prime}}-L(y^{\prime})$ and
hence, by symmetry,
$X_{x^{\prime}}-L(x^{\prime})=X_{y^{\prime}}-L(y^{\prime})$. Then $X$ and
$Y=\\{(c,b):b\in Y_{c}\\}\subseteq\mathrm{C}\times\mathrm{B}_{\delta}$ are
inter-definable, and we conclude by orthogonality of $\mathrm{B}_{\Delta}$ and
$\mathrm{C}$.

Now, if $X\subseteq\mathrm{A}^{\prime}\times\mathrm{B}^{n}$ where
$\mathrm{A}^{\prime}$ is a product of sorts in $\mathcal{A}$, for every $a\in
A^{\prime}$, the fiber $X_{a}\subseteq\mathrm{B}^{n}$ is coded in
$\mathrm{C}^{\mathrm{eq}}\cup(\mathcal{A}\cup\mathrm{B}_{\Delta})^{\mathrm{eq}}$
where $\Delta=\mathrm{C}(\mathrm{acl}(\ulcorner X\urcorner
a))=\mathrm{C}(\mathrm{acl}(\ulcorner X\urcorner))$, by orthogonality. It
follows, by orthogonality again, that the graph of the function
$a\mapsto\ulcorner X_{a}\urcorner$, and hence $X$ itself, is coded also in
$\mathrm{C}^{\mathrm{eq}}\cup(\mathcal{A}\cup\mathrm{B}_{\Delta})^{\mathrm{eq}}$.
∎

We deduce the following variant of [HR21, Proposition 5.3.1]. This covers new
cases since there are no conditions on $\Gamma$ when $\mathrm{k}^{\star}$ is
divisible.

######  Corollary 6.3.

Let $M$ be a $\mathrm{k}$-$\Gamma$-expansion of a model of
$\mathrm{Hen}_{0,0}$. Assume that _one_ of the following conditions holds:

  1. (a)

For every $n\in\mathbb{Z}_{\geq 0}^{\geq 2}$ one has $[\Gamma:n\Gamma]<\infty$
and the pre-image in $\mathrm{RV}$ of any coset of $n\Gamma$ contains a point
which is algebraic over $\emptyset$,

  2. (b)

The group $\mathrm{k}^{\star}$ is divisible.

Let $A\subseteq M^{\mathrm{eq}}$ and
$e\in(\mathrm{RV}\cup\mathrm{Lin}_{A})^{\mathrm{eq}}(M)$ and
$E=\mathrm{acl}(e)$. Then

$e\in\mathrm{dcl}(\Gamma^{\mathrm{eq}}(E)\cup(\mathrm{Lin}_{A}\cup\mathrm{RV}_{\Gamma(E)})^{\mathrm{eq}}(E)).$

In particular for $A=\mathrm{acl}(A)\subseteq M^{\mathrm{eq}}$,

$(\mathrm{RV}\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}(A)\subseteq\mathrm{dcl}(\Gamma^{\mathrm{eq}}(A)\cup\mathrm{Lin}_{\mathcal{G}(A)}^{\mathrm{eq}}(A)).$

###### Proof.

This is a direct consequence of Proposition 6.2 with $R=\mathbb{Z}$. Note that
$\Gamma$ is torsion free, as it is an ordered abelian group. ∎

Before proving our main theorem, let us relate
$\mathrm{Lin}^{\mathrm{eq}}_{A}$ to $\mathrm{k}^{\mathrm{leq}}$:

######  Lemma 6.4.

Let $M\vDash\mathrm{Hen}_{0,0}$ and $A=\mathrm{acl}(A)\subseteq M$. Then
$\mathrm{Lin}_{\mathcal{G}(A)}^{\mathrm{eq}}(A)\subseteq\mathrm{dcl}(\mathrm{k}^{\mathrm{leq}}(A))$.

###### Proof.

Recall that $\mathrm{Lin}_{A}$ is a stably embedded collection of
$\mathrm{k}$-vector spaces — see Remark 3.17. Take
$e\in\mathrm{Lin}_{\mathcal{G}(A)}^{\mathrm{eq}}(A)$. Then $e$ is the code of
a definable set $X_{a}\subseteq\prod_{i}\operatorname{red}(R_{i})$ where
$a\in\prod_{j}\operatorname{red}(R^{\prime}_{j})$ and $R_{i}$ and
$R^{\prime}_{j}$ are $A$-definable $\mathfrak{m}$-avoiding module. Then
$R=\prod R_{i}\times\prod_{j}R^{\prime}_{j}$ is an $A$-definable
$\mathfrak{m}$-avoiding module, and, adding zero coordinates, we may assume
that we have $X_{a}\subseteq\operatorname{red}(R)$ and
$a\in\operatorname{red}(R)$. Let $aEa^{\prime}$ be the equivalence relation
defined by $X_{a}=X_{a}^{\prime}$ and $c$ be the type of $R$. Then
$e\in\mathrm{dcl}(\mathrm{T}_{c,V/E})$. ∎

We can now prove our main results:

######  Theorem 6.5.

Let $M$ be a $\mathrm{k}$-$\Gamma$-expansion of a model of
$\mathrm{Hen}_{0,0}$. Assume that:

  * •

the value group satisfies Property D,

  * •

_one_ of the following conditions holds:

    1. (a)

for every $n\in\mathbb{Z}_{\geq 0}^{\geq 2}$ one has $[\Gamma:n\Gamma]<\infty$
and the pre-image in $\mathrm{RV}$ of any coset of $n\Gamma$ contains a point
which is algebraic over $\emptyset$;

    2. (b)

or, the multiplicative group $k^{\times}$ is divisible.

Then $M$ has weak elimination of imaginaries in
$K\cup\mathrm{k}^{\mathrm{leq}}\cup\Gamma^{\mathrm{eq}}$.

###### Proof.

Let $e\in M^{\mathrm{eq}}$ and $A=\mathrm{acl}(A)$. By Proposition 6.1, we
have

$e\in\mathrm{dcl}(\mathcal{G}(A)\cup(\mathrm{RV}\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}(A)).$

By Corollary 6.3, we have

$(\mathrm{RV}\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}(A)\subseteq\mathrm{dcl}(\Gamma^{\mathrm{eq}}(A),\mathrm{Lin}^{\mathrm{eq}}_{\mathcal{G}(A)}(A))\subseteq\mathrm{dcl}(\Gamma^{\mathrm{eq}}(A),\mathrm{k}^{\mathrm{leq}}(A)),$

where the last inclusion follows from Lemma 6.4. ∎

######  Theorem 6.6.

Let $M$ be a $\mathrm{k}$-$\Gamma$-expansion of a model of
$\mathrm{Hen}_{0,0}$ with angular components. Assume that the value group
satisfies property D. Then $M$ weakly eliminates imaginaries in
$K\cup\mathrm{k}^{\mathrm{leq}}\cup\Gamma^{\mathrm{eq}}$.

###### Proof.

Let $e\in M^{\mathrm{eq}}$ and $A=\mathrm{acl}(A)$. By Proposition 6.1,
$e\in\mathrm{dcl}(\mathcal{G}(A)\cup(\mathrm{RV}\cup\mathrm{Lin}^{\mathrm{eq}}_{\mathcal{G}(A)})(A))$.
Since $\mathrm{RV}$ is $\emptyset$-definably isomorphic to
$\mathrm{k}^{\times}\times\Gamma$, then
$(\mathrm{RV}\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}\subseteq(\Gamma\cup\mathrm{Lin}_{\mathcal{G}(A)})^{\mathrm{eq}}$.
The statement now follows from orthogonality of $\Gamma$ and
$\mathrm{Lin}_{A}$ and Lemma 6.4. x∎

As an illustration (and since it came up earlier), we conclude this paper with
the complete classification of (almost) $\mathrm{k}$-internal sets, when the
value group is dense.

######  Corollary 6.7.

Let $M$ be as in Theorem 6.5 or Theorem 6.6 and assume that $\Gamma(M)$ is
dense. Let $A\subseteq M^{\mathrm{eq}}$ and $X$ be $A$-definable. The
following statements are equivalent:

  1. 1.

$X$ is $\mathrm{k}$-internal;

  2. 2.

$X$ is almost $\mathrm{k}$-internal;

  3. 3.

$X$ is orthogonal to $\Gamma$;

  4. 4.

$X\subseteq\mathrm{dcl}(\mathrm{acl}(A)\cup\mathrm{Lin}_{A}^{\mathrm{eq}})$.

###### Proof.

The fourth statement is a particular case of the first statement. The second
statement is a particular case of the first, and it implies the third since
$\mathrm{k}$ and $\Gamma$ are orthogonal. There remains to prove that if $X$
is orthogonal to $\Gamma$ then it is a subset of
$(^{\mathrm{eq}}\mathrm{Lin}_{A})$. By Theorems 6.5 and 6.6, any element $a\in
X$ is weakly coded in by some tuple $\eta\in\mathrm{K}\cup
K^{\mathrm{leq}}\cup\Gamma^{\mathrm{eq}}$. Then $\eta$ also lies on a
$A$-definable set orthogonal to $\Gamma$. Since $X$ is orthogonal to $\Gamma$,
if $\eta\in\mathrm{K}\cup\Gamma^{\mathrm{eq}}$, then $\eta\in\mathrm{acl}(A)$.
If $\eta\in\mathrm{S}$, then, by Proposition 3.19, $\eta\in\mathrm{acl}(A)$.
Finally, if $\eta\in\operatorname{red}(R_{s})$, for some $s\in\mathrm{S}$,
then $s\in\mathrm{acl}(A)$ and hence $\eta\in\mathrm{Lin}_{A}$. It follows
that $e$ is weakly coded in $\mathrm{acl}(A)\cup\mathrm{Lin}_{A}$, as
required. ∎

## References

  * [Bas91] Şerban A. Basarab  “Relative elimination of quantifiers for Henselian valued fields”  In _Ann. Pure Appl. Logic_ 53.1, 1991, pp. 51–74
  * [Fle11] Joseph Flenner  “Relative decidability and definability in Henselian valued fields”  In _J. Symb. Log._ 76.4, 2011, pp. 1240–1260
  * [HHM06] Deirdre Haskell, Ehud Hrushovski and Dugald Macpherson  “Definable sets in algebraically closed valued fields: elimination of imaginaries”  In _J. Reine Angew. Math._ 597, 2006, pp. 175–236
  * [HHM08] Deirdre Haskell, Ehud Hrushovski and Hugh Dugald Macpherson  “Stable domination and independence in algebraically closed valued fields” 30, Lect. Notes Log.  Cambridge Univ. Press, 2008
  * [HKR18] Martin Hils, Moshe Kamensky and Silvain Rideau  “Imaginaries in separably closed valued fields”  In _Proc. Lond. Math. Soc. (3)_ 116.6, 2018, pp. 1457–1488
  * [HR21] Martin Hils and Silvain Rideau-Kikuchi  “Un principe d’Ax-Kochen-Ershov imaginaire” arXiv:2109.12189, 2021
  * [Hru12] Ehud Hrushovski  “Groupoids, imaginaries and internal covers”  In _Turkish J. Math._ 36.2, 2012, pp. 173–198
  * [HMR18] Ehud Hrushovski, Ben Martin and Silvain Rideau  “Definable equivalence relations and zeta functions of groups” With an appendix by Raf Cluckers  In _J. Eur. Math. Soc. (JEMS)_ 20.10, 2018, pp. 2467–2537
  * [JS20] Franziska Jahnke and Pierre Simon  “NIP Henselian valued fields”  In _Arch. Math. Logic_ 59.1-2, 2020, pp. 167–178
  * [Mel06] Tim Mellor  “Imaginaries in real closed valued fields”  In _Ann. Pure Appl. Logic_ 139, 2006, pp. 230–279
  * [Rid19] Silvain Rideau  “Imaginaries and invariant types in existentially closed valued differential fields”  In _J. Reine Angew. Math._ 2019.750, 2019, pp. 157–196
  * [She90] Saharon Shelah  “Classification theory and the number of non-isomorphic models” 92, Stud. Logic Found. Math.  Amsterdam etc.: North-Holland, 1990
  * [TZ12] Katrin Tent and Martin Ziegler  “A Course in Model Theory”, Lect. Notes Log. 40  Cambridge Univ. Press, 2012
  * [Vic23] Mariana Vicaría  “Elimination of imaginaries in $\mathbb{C}((\Gamma))$”  In _J. Lond. Math. Soc., II. Ser._ 108.2, 2023, pp. 482–544