\documentclass[draft,reqno]{asl}
%\renewcommand{\baselinestretch}{1.5}
%\date{\today}
\thanks{Version of \today.}
\subjclass[2000]{03C10 (03C60, 12H05)}
\title{Fields with several commuting derivations}
\author{David Pierce}
\revauthor{Pierce, David}
\address{Mathematics Department\\
Middle East Technical University\\
Ankara 06531, Turkey}
\email{dpierce@metu.edu.tr}
\urladdr{http://www.math.metu.edu.tr/\urltilde dpierce}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
% More packages %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amscd} % commutative diagram
\usepackage{pstricks,pst-node}
\usepackage[mathscr]{euscript}
\usepackage{stmaryrd} % for \trianglelefteqslant
\usepackage{bm}
\usepackage[all]{xy}
%\usepackage{showlabels} % this doesn't work well with the asl class
%\usepackage[notref,notcite,color]{showkeys} % this does work
%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Stylistic preferences %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\theenumi}{\roman{enumi}}
\renewcommand{\labelenumi}{(\theenumi)}
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}
\renewcommand{\phi}{\varphi}
\renewcommand{\emptyset}{\varnothing}
%\renewcommand{\qedsymbol}{\circ} % This didn't work
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Typographical conventions %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\myboxed}[2]{$#1$#2} % for symbolism (#1) being
% defined; #2 is the following
% punctuation. (I was originally
% going to put a box around #1.)
\newcommand{\defn}[2]{\textbf{#1#2}} % for terms (#1) being defined;
% #2 is punctuation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Theorem-like environments %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
%%%%%%%%%%%%
% Logic %
%%%%%%%%%%%%
\newcommand{\qsep}{\;} % follows a quantified variable
\newcommand{\Forall}[1]{\forall{#1}\qsep }
\newcommand{\Exists}[1]{\exists{#1}\qsep }
\newcommand{\Iff}{\iff}
\newcommand{\tuple}[1]{\bm{#1}}
%%%%%%%%%%%%%%%%%%
% Model-theory %
%%%%%%%%%%%%%%%%%%
\newcommand{\str}[1]{\mathfrak{#1}} % structure
\newcommand{\diag}[1]{\operatorname{diag}(#1)} % (Robinson) diagram of
\newcommand{\robfn}[1]{\widehat{#1}} % ``Robinson function''
\newcommand{\Th}[1]{\operatorname{Th}(#1)} % theory of
\newcommand{\Mod}[1]{\operatorname{Mod}(#1)} % class of models of
\newcommand{\proves}{\vdash}
\newcommand{\thy}[1]{\mathrm{#1}} % for the following:
\newcommand{\ACF}{\thy{ACF}} % algebraically closed fields
\newcommand{\SCF}{\thy{SCF}} % separably closed fields
\newcommand{\DF}{\thy{DF}} % differential fields
\newcommand{\DPF}{\thy{DPF}} % differentially perfect fields
\newcommand{\ACFA}{\thy{ACFA}} % fields with generic autom.
\newcommand{\mDF}{\text{$m$-$\thy{DF}$}} % fields with m derivations
\newcommand{\DCF}{\thy{DCF}} % differentially closed fields
\newcommand{\mDCF}{\text{$m$-$\thy{DCF}$}} % differentially closed fields
% with m derivations
%%%%%%%%%%%%%%%%
% Set-theory %
%%%%%%%%%%%%%%%%
\newcommand{\included}{\subseteq} % inclusion
\newcommand{\pincluded}{\subset} % proper inclusion
\newcommand{\size}[1]{\lvert#1\rvert}
\usepackage{txfonts} % needed for \omegaup in the following
\newcommand{\vnn}{\omegaup} % von Neumann natural numbers
\newcommand{\tleq}{\trianglelefteqslant} % the total ordering of \vnn^m
\newcommand{\tl}{\vartriangleleft} % the strict total ordering of \vnn^m
\newcommand{\ichar}{\bm i} % char. fn of {i} in \vnn^m
\newcommand{\jchar}{\bm j} % char. fn of {j} in \vnn^m
\newcommand{\kchar}{\bm k} % char. fn of {k} in \vnn^m
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% (Differential) Algebra %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Char}[1]{\operatorname{char}(#1)} % characteristic of a field
\newcommand{\sep}[1]{#1^{\mathrm{sep}}} % separable closure
\newcommand{\alg}[1]{#1^{\mathrm{alg}}} % algebraic closure
\newcommand{\Aff}{\mathbb{A}} % affine space
\newcommand{\lrv}{E} % a Lie-ring of vectors
\DeclareMathOperator{\dee}{d} % derivation into the dual of this
\begin{document}
\begin{abstract}
The existentially closed models of the theory of fields (of arbitrary
characteristic) with a given finite number of commuting
derivations can be characterized geometrically, in several ways.
In each case, the
existentially closed models are those models that contain
points of certain differential varieties, which are
determined by certain ordinary varieties.
\end{abstract}
\maketitle
% \tableofcontents
How can we tell whether a given system of partial differential equations
has a solution? An answer given in this paper is that, if we
differentiate the equations enough times, and no contradiction arises,
then it never will, and the system is soluble. Here, the meaning of
`enough times'
can be expressed \emph{uniformly;} this is one way of showing that the
theory, $\mDF$, of fields with a
finite number $m$ of commuting derivations has a model-companion.
In fact, this theorem is worked out here (as Corollary~\ref{cor:dcf},
of Theorem~\ref{thm:dcf}), not in terms of polynomials, but
in terms of the varieties that they define, and the function-fields of
these: in a word, the treatment is \emph{geometric.}
The model-companion of $\mDF_0$ (in
characteristic~$0$) has been axiomatized before, explicitly in terms
of differential polynomials: see \S~\ref{sect:several}. I
attempted in \cite{MR2000487} to characterize its models (namely, the
existentially closed
models of $\mDF_0$) in terms of
differential forms, but I made a mistake. Here I correct the mistake,
but also work in arbitrary characteristic. The existence
of a model-companion of $\mDF$ (with no specified characteristic) appears to
be a new result when $m>1$ (despite a remark by Saharon Shelah
\cite[p.~315]{MR0344116}: `I am
quite sure that for characteristic $p$ as well, [making $m$ greater
than $1$] does not make any essential
difference').
The theory of model-companions and model-completions was worked out
decades ago; perhaps for that very reason, it may be worthwhile to
review the theory here, as I do in \S~\ref{sect:mt}. I try
to give the original references, when
I have been able to consult them.
In \S~\ref{sect:one}, I review the various known characterizations of
existentially closed fields with single derivations. Then
\S\S~\ref{sect:several} and~\ref{sect:resolution} consider how those
characterizations can be
generalized to allow for several commuting derivations.
\section{Model-theoretic background}\label{sect:mt}
Let $\str M$ be an arbitrary (first-order) structure; its
theory is
\myboxed{\Th{\str M}}.
Let $T$ be an
arbitrary consistent (first-order) theory; its models compose the
class
\myboxed{\Mod T}.
Every class $\bm K$ of structures in some signature has a theory,
\myboxed{\Th{\bm K}}. Then $\bm K\included\Mod{\Th{\bm K}}$; in case of
equality, $\bm K$ is \defn{elementary}. Always, $\Th{\Mod T}=T$.
The structure $\str M$ has the universe $M$. The structure denoted by
$\str M_M$ is the expansion of $\str M$ that has a name for every
element of $M$.
Then $\str M$ embeds in $\str N$ if and only if $\str M_M$ embeds in
an expansion of $\str N$. However, although the class of
structures in
which $\str M$ embeds need not be elementary, the class of
structures in which $\str M_M$ embeds \emph{is} elementary. The
theory of the latter class is the \defn{diagram}{} of $\str M$, or
\myboxed{\diag{\str M}}: it is
axiomatized by the quantifier-free sentences in $\Th{\str M_M}$
\cite[Thm 2.1.3, p.~24]{MR0153570}.
The class of structures in which $\str M_M$
embeds \emph{elementarily}
is also elementary, and its theory is just \myboxed{\Th{\str M_M}}.
The class of
substructures of models of $T$ is elementary, and its theory is
denoted by \myboxed{T_{\forall}}: this is axiomatized by the universal
sentences of $T$ \cite[Thm 3.3.2, p.~71]{MR0153570}.
By a \defn{system over}{} $\str M$, I mean a finite conjunction of
atomic and negated atomic formulas in the signature of $\str M_M$;
likewise, a system \defn{over}{} $T$ is in the signature
of $T$. A structure $\str M$ \defn{solves}{} a system $\phi(\tuple x)$
if $\str M\models\Exists{\tuple x}\phi(\tuple x)$. Note well here that
$\tuple x$, in boldface, is a \emph{tuple} of variables, perhaps
$(x^0,\dots,x^{n-1})$. By an
\defn{extension}{} of a model of $T$, I mean another model of $T$ of
which the first is a substructure. Two systems over a model $\str M$
of $T$ are \defn{equivalent}{} if they are soluble in the same extensions.
An \defn{existentially closed}{} model of $T$ is a model of $T$ that
solves every system over
itself that is soluble in some extension. So a model $\str M$ of $T$ is
existentially closed if and only if
$T\cup\diag{\str M}\proves\Th{\str M_M}_{\forall}$, that is, every
extension of $\str M$ is a substructure of an elementary extension
(\cite[\S~7]{MR0277372} or \cite[\S~2]{MR51:12518}).
A theory is \defn{model-complete}{} if its every
model is existentially closed. An equivalent formulation explains the
name: $T$ is model-complete if and only if $T\cup\diag{\str M}$ is
complete whenever $\str M\models T$
\cite[Ch.~2]{MR0472504}.
Suppose every model of $T$ has an existentially closed extension.
Such is the case when $T$ is \defn{inductive}, that is, $\Mod{T}$ is
closed under unions of chains \cite[Thm~7.12]{MR0277372}: equivalently,
$T=T_{\forall\exists}$ \cite{MR0089813,MR0103812}. Suppose further
that we have a uniform
first-order way to tell when systems over models of $T$ are soluble in
extensions: more precisely, suppose there is a function
\begin{equation}\label{eqn:fn}
\phi(\tuple x,\tuple y)\longmapsto
\robfn{\phi}(\tuple x,\tuple y),
\end{equation}
where
$\phi(\tuple x,\tuple y)$ ranges over the systems over $T$ (with
variables analyzed as shown),
such that, for every model $\str
M$ of $T$ and every tuple $\tuple a$ of parameters from $M$, the
system $\phi(\tuple x,\tuple a)$ is soluble in some extension of $\str
M$ just in case $\robfn{\phi}(\tuple x,\tuple a)$ is soluble in $\str M$.
Then the existentially closed
models of $T$ compose an elementary class, whose theory $T^*$ is
axiomatized by $T$ together with the sentences
\begin{equation}\label{eqn:sen}
\Forall{\tuple y}(\Exists{\tuple x}\robfn{\phi}(\tuple x,\tuple
y)\to
\Exists{\tuple x}\phi(\tuple x,\tuple y)).
\end{equation}
Immediately, $T^*$ is model-complete, so $T^*\cup\diag{\str M}$ is
complete when $\str M\models T^*$. What is more,
$T^*\cup\diag{\str M}$ is complete whenever $\str M\models
T$ \cite[Thm 5.5.1]{MR0153570}.
In general, $T^*$ is a \defn{model-completion}{} of $T$ if
$T^*{}_{\forall}\included T\included T^*$
and
$T^*\cup\diag{\str M}$ is
complete whenever $\str M\models T$. Model-completions are unique
\cite[(2.8)]{MR0091922}. We have sketched the proof of part of the
following (the rest is \cite[(3.5)]{MR0091922}):
\begin{lemma}[Robinson's Criterion]
\label{lem:rob-crit}
Let $T$ be inductive. Then $T$ has a model-comple\-tion if and
only if a function $\phi(\tuple x,\tuple
y)\mapsto\robfn{\phi}(\tuple x,\tuple y)$ exists as
in~\eqref{eqn:fn}.
In this case, the model-completion is axiomatized \emph{modulo} $T$ by
the sentences in~\eqref{eqn:sen}.
\end{lemma}
If $T_{\forall}=T^*{}_{\forall}$ and $T^*$ is model-complete, then
$T^*$ is a \defn{model-companion}{} of~$T$
(\cite[\S~5]{MR0272613}; \emph{cf.}~\cite[\S~2]{MR0277372}).
Model-completions are model-companions, and model-companions are
unique \cite[Thm 5.3]{MR0272613}.
If $T$ has a
model-companion, then its models are just the existentially closed
models of $T$ \cite[Prop.~7.10]{MR0277372}.
Conversely, if $T$ is inductive,
and the class of existentially closed models
of $T$ is elementary, then the theory of this class is the
model-companion of $T$ \cite[Cor.~7.13]{MR0277372}.
\section{Fields with one derivation}\label{sect:one}
Let \myboxed{\DF}{} be the theory of fields with a derivation, and let
\myboxed{\DPF}{} be
the theory of models of $\DF$ that, for each prime $\ell$, satisfy also
\begin{equation*}
\Forall x\Exists y(\underbrace{1+\dotsb+1}_{\ell}=0\land
Dx=0\to\underbrace{y\dotsb y}_{\ell}=x).
\end{equation*}
So models of $\DPF$ are \defn{differentially perfect}. A
subscript on the name of one of these theories will indicate a
required characteristic for the field. In particular, we have $\DPF_0$,
which is the same as $\DF_0$.
Abraham Seidenberg
\cite{MR0082487} shows the existence of the function
in Lemma~\ref{lem:rob-crit} in case
$T$ is $\DPF_p$, where $p$ is prime or $0$. Consequently:
\begin{theorem}[Robinson]
$\DF_0$ has a model-completion, called \myboxed{\DCF_0}.
\end{theorem}
\begin{theorem}[Wood \cite{MR48:8227}]
If $p$ is prime, then $\DF_p$ has a model-companion,
\myboxed{\DCF_p}, which is the model-completion of $\DPF_p$.
\end{theorem}
\subsection{Single variables}\label{subsect:one-var}
Since it involves \emph{all} systems over a given theory,
Robinson's criterion yields the crudest possible axiomatization for a
model-completion. By contrast, though the theory \myboxed{\ACF}{} of
algebraically closed fields is the model-completion of the theory of
fields, its axioms (\emph{modulo} the latter theory) can involve only
systems in one variable (indeed, single equations in one variable).
A generalization of this observation is the following, which can be
extracted from the proof of \cite[Thm~17.2, pp.~89--91]{MR0398817}
(see also \cite{MR0491149}):
\begin{lemma}[Blum's Criterion]\label{lem:blum}
Say $T^*{}_{\forall}\included T\included T^*$.
\begin{enumerate}
\item
The theory $T^*$ is the model-completion of $T$ if and only if the
commutative diagram
\begin{equation*}
\xymatrix{
\str M &\\
\str A \ar[u] \ar[r] & \str B \ar@{.>}[ul]
}
\end{equation*}
of structures and embeddings
can be completed as indicated when
$\str A$ and $\str B$ are models of $T$ and $\str M$ is a
$\size{B}^+$-saturated model of $T^*$.
\item\label{item:blum2}
If $T=T_{\forall}$, it is enough to assume that $\str B$ is generated
over $\str A$
by a single element.
\end{enumerate}
\end{lemma}
This allows a refinement of Lemma~\ref{lem:rob-crit} in a special
case:
\begin{lemma}
Suppose $T=T_{\forall}$. Then Lemma~\ref{lem:rob-crit} still holds
when $\phi(\tuple x,\tuple y)$ is replaced with
$\phi(x,\tuple y)$ (where $x$ is a single variable).
\end{lemma}
From Lemma~\ref{lem:blum},
Lenore Blum obtains Theorem~\ref{thm:dcf-1} below in characteristic
$0$, in which case the first two numbered conditions amount to
$K\models\ACF$ (\cite[pp.~298~ff.]{MR0398817} or~\cite{MR0491149}).
If $p>0$, then $\DF_p$ is not universal, so
part~\eqref{item:blum2} of Blum's criterion does
\emph{not} apply; Carol Wood instead uses a
primitive-element theorem of Seidenberg \cite{MR0049174} to obtain new
axioms for $\DCF_p$ \cite{MR50:9577}. These can be combined with
Blum's axioms for $\DCF_0$ to yield the following. (Here \myboxed{\SCF}{} is
the theory of separably closed fields.)
\begin{theorem}[Blum, Wood]\label{thm:dcf-1}
A model $(K,D)$ of $\DF$ is existentially closed if and only if
\begin{enumerate}
\item
$K\models\SCF$;
\item
$(K,D)\models\DPF$;
\item
$(K,D)\models\Exists x(f(x,Dx,\dots,D^{n+1}x)=0\land
g(x,Dx,\dots,D^nx)\neq0)$ whenever $f$ and $g$ are ordinary
polynomials over $K$ in tuples $(x^0,\dots, x^{n+1})$ and
$(x^0,\dots,x^n)$ of variables
respectively such that $g\neq0$ and
$\partial f/\partial x^{n+1}\neq0$.
\end{enumerate}
Hence $\DF$ has a model-companion, \myboxed{\DCF}.
\end{theorem}
There is a similar characterization of the existentially closed
\emph{ordered} differential fields \cite{MR495120}.
\subsection{First derivatives}\label{sect:first-der}
Alternative simplified axioms for $\DCF$ are parallel to
those found for the model-companion \myboxed{\ACFA}{} of the theory of fields
with an automorphism \cite{MR99c:03046,MR2000f:03109}. Suppose
$(K,D)\models\DPF$ and $K\models\SCF$.
Every system
over $(K,D)$ can be written as
\begin{equation}\label{eqn:sys}
\bigwedge_ff(\tuple x,D\tuple x,\dots,D^n\tuple x)=0\land g(\tuple
x,D\tuple x,\dots,D^n\tuple x)\neq0,
\end{equation}
where $g$ and the $f$ are ordinary polynomials over $K$. This system is
equivalent to one that involves only first derivatives, namely
\begin{multline*}
\bigwedge_ff(\tuple x_0,\dots,\tuple x_{n-1},\tuple y_{n-1})=0\land
g(\tuple x_0,\dots,\tuple x_{n-1},\tuple y_{n-1})\neq0\land{}\\
{}\land\bigwedge_{i+1}{{}*!/-5pt/@{>}}
\xymatrix{
U \ar@{ >->}[r] \ar@{-->>}[dr]
& W \ar@{ >->}[r] \ar@{-->>}[d] & T_D(V) \ar@{-->>}[dl]^{(\tuple
x,\tuple y)\mapsto\tuple x}\\
& V&
}
\end{equation*}
In characteristic $0$, the model $(K,D)$ of $\DF$ is existentially
closed if and only if, in every such geometric situation, $U$ contains
a $K$-rational point $(\tuple c,D\tuple c)$; this yields the so-called
geometric axioms for $\DCF_0$ found with Anand Pillay
\cite{MR99g:12006}. In positive characteristic, it is still true
that, if $(\tuple a,\tuple b)$ is a generic point of $V$, then $D$
extends to $K(\tuple a)$ so that $D\tuple a=\tuple b$. However, an
additional condition is needed to ensure that $D$ extends to all of
$K(\tuple a,\tuple b)$; it is enough to require that the projection of
$T_D(W)$ onto $T_D(V)$ contain a generic point of $W$; this yields
Piotr Kowalski's geometric axioms for $\DCF_p$ \cite{MR2119125}.
In an alternative geometric approach to $\DCF$, instead
of~\eqref{eqn:sys}, it is enough to look
at an arbitrary system of \emph{equations,}
$\bigwedge_ff(\tuple x,D\tuple x,\dots,D^n\tuple x)=0$.
As before, we can take the derivations out of the polynomials,
this time getting the equivalent system
\begin{equation*}
\bigwedge_ff(\tuple x_0,\dots,\tuple
x_n)=0\land\bigwedge_{i}{a}{b}
\Cnode(0,-1){c}
\uput[l](0,-1){$(1,0)$}
\ncline{->}{b}{c}
\Cnode(2,0){d}
\uput[ur](2,0){$(0,2)$}
\ncline{->}{c}{d}
\Cnode(1,-1){e}
\uput[dr](1,-1){$(1,1)$}
\ncline{->}{d}{e}
\Cnode(0,-2){f}
\uput[d](0,-2){$(2,0)$}
\ncline{->}{e}{f}
\end{pspicture}
\hfill
\begin{pspicture}(-2.5,-0.5)(2.5,3)
\psset{radius=0.1}
\Cnode(0,2.4){a}
\uput[u](0,2.4){$(0,0,2)$}
\Cnode(0.7,1.2){b}
\uput[ur](0.7,1.2){$(0,1,1)$}
\ncline{->}{a}{b}
\Cnode(1.4,0){c}
\uput[r](1.4,0){$(0,2,0)$}
\ncline{->}{b}{c}
\Cnode(-0.7,1.2){d}
\uput[ul](-0.7,1.2){$(1,0,1)$}
\ncline{->}{c}{d}
\Cnode(0,0){e}
\uput[d](0,0){$(1,1,0)$}
\ncline{->}{d}{e}
\Cnode(-1.4,0){f}
\uput[l](-1.4,0){$(2,0,0)$}
\ncline{->}{e}{f}
\end{pspicture}
\hfill
\mbox{}
\end{center}
We may
write $(\sigma,k)\tl\infty$ for all $(\sigma,k)$ in $\vnn^m\times n$.
Suppose $(x_h\colon h{D_1}>> L_0\\
@V{D_0}VV @VV{D_0}V\\
L_1 @>>{D_1}> M
\end{CD}
\end{equation*}
Suppose also that $a$ is an element of $M$ that is separably algebraic over
$K$. Then each $D_i$ extends uniquely to $K(a)$, and $D_ia\in
L_{1-i}(a)$, so $D_{1-i}D_ia$ is also well-defined. Moreover, $[D_0,D_1]a=0$.
\end{lemma}
\begin{proof}
The claim follows from standard facts, at least if $L_0=K=L_1$; but
the proof is the same in the general case. Indeed, though the
derivations $D_0$ and $D_1$ are defined on $K$, their bracket
$[D_0,D_1]$ need not be so, since the compositions $D_0D_1$ and
$D_1D_0$ need not be so; but if they are, then $[D_0,D_1]$ is a
\emph{derivation} on $K$.
A derivation on $K$ extends uniquely to $\sep K$; if the derivation
is $0$ on $K$, then it is $0$ on $\sep K$
\cite[Fact~1.1~(2)]{MR2114160}.
In the present case, as $a\in \sep K$, so $D_ia\in L_{1-i}(a)$, and
therefore $D_ia\in\sep{L_{1-i}{}}$; hence $D_{1-i}D_ia$ is defined.
Thus $[D_0,D_1]$ is
defined on $K(a)$, where $a\in \sep K$; and if the bracket is $0$ on
$K$, then is $0$ at $a$.
\end{proof}
Another example illustrates the following theorem in positive
characteristic. Over a differential field
$(K,\partial_0,\partial_1)$, where $\Char K=p>0$,
the differential equation
\begin{equation*}
(\partial_0x)^p+x=\partial_1x
\end{equation*}
determines an extension
$K(a^{\xi}\colon\size{\xi}\leq 2)$ of $K$ that meets the differential
condition: the generators form a triangle thus:
\begin{equation*}
\begin{matrix}
a&b^p+a&b^p+a\\
b&b & \\
c& &
\end{matrix}
\end{equation*}
where $(a,b,c)$ is algebraically independent over $K$.
In particular, $a^{(1,0)}$ (which has the value $b$) is an inseparable leader,
but none of the generators of height $2$ (namely, $a^{(0,2)}$,
$a^{(1,1)}$ and $a^{(2,0)}$) is an inseparable
leader.
\begin{theorem}\label{thm:first}
Suppose $(K,\partial_0,\dots,\partial_{m-1})\models\mDF$, and $K$
has an extension $K(a_h^{\xi}\colon\size{\xi}\leq2r\land
h2r$.
Hence, if $\tau(i)>0$, so that $\tau-\ichar$ is defined, then
$\size{\tau-\ichar}\geq2r$, so
$a_{\ell}^{\tau-\ichar}$ is not an inseparable leader.
If $a_{\ell}^{\tau-\ichar}$ is not a
leader at all, for any $i$ in $m$, then we may let $a_{\ell}^{\tau}$ be a
new transcendental, and we may define each derivative
$D_ia_{\ell}^{\tau-\ichar}$ as this \cite[Fact~1.1~(1)]{MR2114160}.
In the other case, $a_{\ell}^{\tau-\ichar}$ is a
separable leader for some $i$. Then $D_ia_{\ell}^{\tau-\ichar}$ is determined
(Lemma~\ref{lem:above}). We want to let $a_{\ell}^{\tau}$ be this
derivative. However, possibly also $a_{\ell}^{\tau-\jchar}$ is a
separable leader, where $i\neq j$. In this case, we must check that
\begin{equation}\label{eqn:comm}
D_ja_{\ell}^{\tau-\jchar}=D_ia_{\ell}^{\tau-\ichar},
\end{equation}
that is, $[D_i,D_j]a_{\ell}^{\tau-\ichar-\jchar}=0$.
There are minimal separable leaders $a_{\ell}^{\pi}$ and $a_{\ell}^{\rho}$
below $a_{\ell}^{\tau-\ichar}$ and
$a_{\ell}^{\tau-\jchar}$ respectively.
Let $\nu$ be $\pi\vee\rho$,
the least upper bound of $\{\pi,\rho\}$ with respect to $\leq$.
Then $\nu\leq\tau$. But
$\size{\nu}\leq\size{\pi}+\size{\rho}\leq2r<\size{\tau}$; so $\nu<\tau$.
Hence $\nu\leq\tau-\kchar$ for some $k$ in $m$, which means
$a_{\ell}^{\nu}$ is below $a_{\ell}^{\tau-\kchar}$.
Consequently,
\begin{enumerate}
\item
$a_{\ell}^{\pi}$ is below both $a_{\ell}^{\tau-\ichar}$ and
$a_{\ell}^{\tau-\kchar}$;
\item
$a_{\ell}^{\rho}$ is below both $a_{\ell}^{\tau-\jchar}$ and
$a_{\ell}^{\tau-\kchar}$.
\end{enumerate}
If $k=j$, then $a_{\ell}^{\pi}$ is below
$a_{\ell}^{\tau-\ichar-\jchar}$, so this is a separable leader. As
$D_i$ and $D_j$ commute on
$K(a_h^{\xi}\colon (\xi,h)\tl(\tau-\ichar-\jchar,{\ell}))$ by the
differential condition, they must
commute also at $a_{\ell}^{\tau-\ichar-\jchar}$ (Lemma~\ref{lem:comm}),
so~\eqref{eqn:comm} is established. The argument is the same if
$k=i$. If $k$ is different from $i$ and $j$, then again the same
argument yields
$D_ja_{\ell}^{\tau-\jchar}=D_ka_{\ell}^{\tau-\kchar}$ and
$D_ka_{\ell}^{\tau-\kchar}=D_ia_{\ell}^{\tau-\ichar}$,
so~\eqref{eqn:comm} holds.
In no case did we introduce a new minimal separable leader or an
inseparable leader. This completes the induction and the
proof.
\end{proof}
The claim at the end of the last subsection (\ref{subsect:example}) is
now justified.
In terms of differential polynomials and ideals, the theorem can be
understood as follows. Given the hypothesis of the theorem, let $S$
be the set of differential polynomials
$f(\partial^{\xi}x_h\colon\size{\xi}<2r\land h2$. If
$\size{\tau}\leq2$ and $\size{\sigma+\tau}\leq\size{\mu}$, let
$a_{(\sigma,k)}^{\tau}$ denote $a_k^{\sigma+\tau}$. Then the
extension of $K$ can be written as
\begin{equation}\label{eqn:ext}
K(a_{(\xi,h)}^{\eta}\colon
\size{\eta}\leq2\land(\xi,h)\tl((0,\dots,0,\size{\mu}-1),0)),
\end{equation}
but this no longer need satisfy the conditions in
Theorem~\ref{thm:third}. For example, in case $m=2$ and $n=1$ and
$\mu=(3,0)$, the original extension might determine the following
triangle, with the single leader underlined:
\begin{equation}\label{eqn:a-k}
\begin{matrix}
a&b&d&g\\
c&e&h& \\
f&k& & \\
\underline a& & &
\end{matrix}
\end{equation}
Then the derived extension in~\eqref{eqn:ext} determines three
triangles thus, with minimal separable leaders underlined:
\begin{equation*}
\begin{matrix}
a&\underline b&d\\
\underline c&e& \\
f & &
\end{matrix}
\qquad\qquad
\begin{matrix}
b&d&g\\
e&h& \\
k& &
\end{matrix}
\qquad\qquad
\begin{matrix}
c&\underline e&h\\
f&k& \\
\underline a& &
\end{matrix}
\end{equation*}
We know that the two minimal separable leaders in the last triangle
will not cause a problem; but we don't know this directly from the
tree small triangles. In the present context, the
system~\eqref{eqn:step-1} is
\begin{align*}
\dee a&=\dee t^0\cdot c+\dee t^1\cdot b,&
\dee b&=\dee t^0\cdot e+\dee t^1\cdot d,&
\dee c&=\dee t^0\cdot f+\dee t^1\cdot e,\\
\dee d&=\dee t^0\cdot h+\dee t^1\cdot g,&
\dee e&=\dee t^0\cdot k+\dee t^1\cdot h,&
\dee f&=\dee t^0\cdot a+\dee t^1\cdot k,
\end{align*}
and then~\eqref{eqn:jkim} consists of $\partial_0g=\partial_1h$,
$\partial_0h=\partial_1k$, and
$\partial_0k=b$. As linear equations, these are soluble, but they
don't carry the information in~\eqref{eqn:a-k} that lets us know that
the corresponding differential system is soluble.
\subsection{Another sufficient condition}
If $(K,\partial_0,\dots,\partial_{m-1})\models\mDF$, and
$K(a_h^{\xi}\colon\size{\xi}\leq\size{\pi}\land h