% This edition is being prepared after reception of the referee's report
% The latest round of editing started March 17, 2012
\documentclass[draft,reqno]{amsart}
%\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} % for asl
\address{Mathematics Department\\
Mimar Sinan Fine Arts University\\
Istanbul, Turkey}
\email{dpierce@msgsu.edu.tr}
\urladdr{http://mat.msgsu.edu.tr/~dpierce}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
% More packages %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\usepackage{amsthm} % I wanted \qedhere but the package caused problems
\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 [?]
\usepackage{verbatim}
%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Stylistic preferences %
%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\theenumi}{\roman{enumi}}
\renewcommand{\labelenumi}{(\theenumi)}
\usepackage{amssymb}
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}
\renewcommand{\phi}{\varphi}
\renewcommand{\emptyset}{\varnothing}
%\renewcommand{\qedsymbol}{\circ} % This didn't work
\renewcommand{\land}{\mathrel{\&}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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}}
\newcommand{\lto}{\Rightarrow}
%%%%%%%%%%%%%%%%%%
% 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{\mDPF}{\text{$m$-$\thy{DPF}$}} % diff. perf. 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
\usepackage{upgreek}
\newcommand{\vnn}{\upomega} % 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}
For every natural number $m$,
the existentially closed models of the theory of fields with $m$ commuting
derivations can be given a first-order geometric characterization in several ways.
In particular, the theory of these differential fields has a model-companion.
The axioms are that
certain differential varieties
determined by certain ordinary varieties are nonempty. There is no restriction on the characteristic of the underlying field.
\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 of fields with a given
finite number 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
theory of fields with
$m$ commuting derivations will be called here $\mDF$; its model-companion, $\mDCF$. A specified characteristic can be indicated by a subscript.
The model-companion of $\mDF_0$ (in
characteristic~$0$) has been axiomatized before, explicitly in terms
of differential polynomials: see \S \ref{sect:several}. 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}.
In \S \ref{sect:one}, I review the various known characterizations of
existentially closed fields with single derivations.
In fact, little of this work is of use in the passage to several derivations; but this near-irrelevance is itself interesting.
In \S \ref{sect:several}, I analyze the error of my earlier
attempt, in \cite{MR2000487}, to axiomatize $\mDCF_0$
in terms of
differential forms. Something of value from this earlier work does remain: when we do have $\mDCF_0$, or more generally $\mDCF$, then we can obtain from it a model-companion of the theory of fields with $m$ derivations whose linear span over the field is closed under the Lie bracket.
In \S \ref{sect:resolution}, I obtain $\mDCF$ itself.
\section{Model-theoretic background}\label{sect:mt}
I try in this section
to give original references, when
I have been able to consult them. An exposition can also be found for example in Hodges \cite{MR94e:03002} (particularly chapter 8).
% The present account will follow the typographical convention whereby a word in \defn{boldface}{} is being defined by the sentence in which it appears.
Let $\Gamma$ be a
set of (first-order) sentences in some signature; the structures that have this signature and are models of $\Gamma$ compose the
class denoted by
\myboxed{\Mod{\Gamma}}.
Every class $\bm K$ of structures of some signature has a \textbf{theory,} denoted by
\myboxed{\Th{\bm K}}; this is the set of sentences in the signature that are true in each of the structures in $\bm K$. Immediately $\bm K\included\Mod{\Th{\bm K}}$; in case of
equality, $\bm K$ is called \defn{elementary}. Similarly, $\Gamma\included\Th{\Mod{\Gamma}}$; in case of equality, that is, in case $\Gamma$ is actually the theory of $\Mod{\Gamma}$, then $\Gamma$ is called a \textbf{theory,} simply. So there is a Galois correspondence between elementary classes and theories.
Let $\str M$ be an arbitrary (first-order) structure; the theory of $\{\str M\}$ is denoted by \myboxed{\Th{\str M}}.
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$. The class of
structures in
which $\str M$ embeds need not be elementary: for example, $\str M$ could be an uncountable model of a countable theory.
However, 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}.
A model of $\Th{\str M_M}$ itself is just a structure in
which $\str M_M$
embeds \textbf{elementarily.} Thus the class of such structures is elementary.
The class of
substructures of models of a theory $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}{} a theory $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$ will be called \defn{equivalent}{} if they are soluble in precisely 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)\lto
\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 $D$, and let
\myboxed{\DPF}{} be
the theory of models of $\DF$ that, for each prime $\ell$, satisfy also
\begin{equation*}
\Forall x\Exists y(\ell=0\land
Dx=0\lto y^{\ell}=x),
\end{equation*}
where the first occurrence of $\ell$ stands for $1+\dots+1$ (with $\ell$ occurrences of $1$); and $y^{\ell}$ stands for $y\dotsm y$ (with $\ell$ occurrences of $y$).
Models of $\DPF$ are called \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, called
\myboxed{\DCF_p}, which is the model-completion of $\DPF_p$.
\end{theorem}
The existence of a model-companion or model-completion of a theory does not
necessarily tell us much about the existentially closed models of the
theory. Since it involves \emph{all} systems over a given theory,
Robinson's criterion yields the crudest possible axiomatization for a
model-completion. In the case of $\DCF_p$ (again where $p$ is prime or $0$), there are two ways of
refining the axiomatization---refining in the sense of finding seemingly weaker
conditions on models of $\DF_p$ that are still sufficient for being
existentially closed. It suffices to consider either systems in only one
variable or systems involving only first derivatives. In the
generalization to several derivations, the former
refinement seems to be of little use; the latter refinement is of use
indirectly, through its introduction of geometric ideas.
\subsection{Single variables}\label{subsect:one-var}
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 $\DPF_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, called \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$.
Given a system
over $(K,D)$, we can rewrite it so that $D$ is applied only to
variables or derivatives of variables; then we can replace each
derivative with a new variable, obtaining a system
\begin{equation}\label{eqn:1st}
\bigwedge_ff=0\land g\neq0\land D\tuple x=\tuple y,
\end{equation}
where $f,g\in K[\tuple x,\tuple y]$ and $D\tuple x=\tuple y$ stands for $\bigwedge_iDx^i=y^i$. We can also incorporate this condition into the rest of the system, writing
$\bigwedge_ff(\tuple x,D\tuple x)=0\land g(\tuple x,D\tuple x)\neq0$.
Suppose~\eqref{eqn:1st} has the solution $(\tuple a,\tuple b)$.
Then $K(\tuple a,\tuple b)/K$ is separable
\cite[Lem.~1.5, p.~1328]{MR2114160}. Let
$V$ and $W$ be the varieties over $K$ with generic points $\tuple a$
and $(\tuple a,\tuple b)$ respectively, let \myboxed{T_D(V)}{} be the
twisted tangent bundle of $V$, and let $U$ be the open subset of $W$
defined by the inequation $g\neq0$.
\begin{comment}
then the situation can be
depicted thus:
\begin{equation*}
\SelectTips{cm}{}
\newdir{ >}{{}*!/-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*}
\end{comment}
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}.
By the trick of replacing $g\neq0$ with $z\cdot g=1$, we may
assume that there is no inequation in~\eqref{eqn:1st}.
In an alternative geometric approach to $\DCF$, we can then
consider~\eqref{eqn:1st} as a special case of
\begin{equation}\label{eqn:1-my}
\bigwedge_ff=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}
\end{comment}
We may
write $(\sigma,k)\tl\infty$ for all $(\sigma,k)$ in $\vnn^m\times n$.
Suppose $(x_h\colon h0$.
Let $L$ be an extension of $K$ with generators that are indexed by an initial
segment of $(\vnn^m\times n,\tleq)$; that is,
\begin{equation}\label{eqn:L}
L=K(a_h^{\xi}\colon(\xi,h)\tl(\tau,\ell)),
\end{equation}
where $(\tau,\ell)\in\vnn^m\times n$, or possibly $(\tau,\ell)=\infty$,
in which case $L=K(a_h^{\xi}\colon(\xi,h)\in\vnn^m\times n)$.
It could happen that, in the generating tuple $(a_h^{\xi}\colon(\xi,h)\tl(\tau,\ell))$ of $L/K$, the same element of $L$ may appear twice, with different indices. In this case, when
writing $a_h^{\xi}$, we may mean not just a particular element of $L$, but that element together with the pair $(\xi,h)$ of indices.
For example, by~\eqref{eqn:sks}, if $(\sigma+\ichar,k)\tl(\tau,\ell)$, then $(\sigma,k)\tl(\tau,\ell)$; hence we may say that,
if $a_k^{\sigma+\ichar}$ is one of the generators
of $L/K$, then so is $a_k^{\sigma}$. Let us say that $L$, with the
tuple of generators given in~\eqref{eqn:L}, meets the \defn{differential condition}{} if there is
no obstacle to extending each derivation $\partial_i$ to a derivation
$D_i$ on $K(a_h^{\xi}\colon(\xi+\ichar,h)\tl(\tau,\ell))$ such that
\begin{equation}\label{eqn:Dia}
D_ia_k^{\sigma}=a_k^{\sigma+\ichar}
\end{equation}
whenever $(\sigma+\ichar,k)\tl(\tau,\ell)$.
(If the right-hand member of~\eqref{eqn:Dia} is not defined,
then the left need not be defined.)
To be precise,
if $f$ is a rational function over $K$
in variables $(x_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))$ for some $(\sigma,k)$ in $\vnn^m\times n$, and $D$ is a derivation of $K$, then $f$ has a derivative $Df$, which is the linear function over $K(x_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))$ given by
\begin{equation*}
Df= \sum_{(\xi,h)\tleq(\sigma,k)}
\frac{\partial f}{\partial
x_h^{\xi}}\cdot
y_h^{\xi}+
f^D.
\end{equation*}
Then the differential condition is that for all such $f$, if
$(\sigma+\ichar,k)\tl(\tau,\ell)$ for some $i$ in $m$, and if
\begin{equation}\label{eqn:fahx}
f(a_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))=0,
\end{equation}
then
\begin{math}
\partial_if(a_h^{\xi},a_h^{\xi+\ichar}\colon(\xi,h)\tleq(\sigma,k))=0
\end{math}, that is,
\begin{equation}\label{eqn:sumeta}
\sum_{(\eta,g)\tleq(\sigma,k)}
\frac{\partial f}{\partial
x_g^{\eta}}(a_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))\cdot
a_g^{\eta+\ichar}+
f^{\partial_i}(a_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))=0.
\end{equation}
(Note well the assumption that
$(\sigma+\ichar,k)\tl(\tau,\ell)$. In~\eqref{eqn:sumeta}, each
of the $a_g^{\eta+\ichar}$ must exist, even though the
coefficient $(\partial f/\partial
x_g^{\eta})(a_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))$ might be $0$.)
So the differential condition is \emph{necessary} for the
extensibility of the $\partial_i$ as desired (see for example
\cite[Fact~1.1~(0)]{MR2114160}); sufficiency is part of
Lemma~\ref{lem:above} below.
An extension $(M,D_0,\dots,D_{m-1})$ of
$(K,\partial_0,\dots,\partial_{m-1})$ is \defn{compatible}{} with the
extension $L$ of $K$ given in~\eqref{eqn:L} if $L\included M$,
and~\eqref{eqn:Dia} holds whenever
$(\sigma+\ichar,k)\tl(\tau,\ell)$.
Borrowing some terminology
used for differential polynomials \cite[\S IX.1, p.~163]{MR0201431},
let us say that a generator $a_k^{\sigma}$ of $L/K$ is a \defn{leader}{} if
it is algebraically dependent over $K$ on its predecessors, that is,
\begin{equation*}
a_k^{\sigma}\in\alg{K(a_h^{\xi}\colon(\xi,h)\tl(\sigma,k))}.
\end{equation*}
Then
$a_k^{\sigma}$ is a \defn{separable}{} leader if it is separably
algebraic over $K(a_h^{\xi}\colon(\xi,h)\tl(\sigma,k))$; otherwise, it
is an \defn{inseparable}{} leader. A separable
leader $a_k^{\sigma}$ is \defn{minimal}{} if
there is no separable leader strictly below it---no separable leader
$a_k^{\rho}$ such that $\rho<\sigma$.
\begin{comment}
For example, in the field $K(a^{(i,j)}\colon(i,j)\leq(3,3))$ depicted
in~\eqref{eqn:matrix} above, the generator
$a^{(3,3)}$ is a (non-minimal) separable leader, and
$a^{(3,1)}$ is a minimal separable leader. But here we wanted $a^{(3,3)}$
ultimately to be a derivative of $a^{(3,1)}$, namely
$\partial_1{}^2a^{(3,1)}$. Passing to a larger field
in~\eqref{eqn:matrix2}, we found the
condition $a^{(3,0)}=a^{(0,2)}$; then $a^{(3,0)}$ became a new separable
leader, strictly below the formerly minimal separable leader $a^{(3,1)}$.
\end{comment}
\begin{lemma}\label{lem:above}
Suppose $(K,\partial_0,\dots,\partial_{m-1})\models\mDF$ and $L$ meets the differential condition, where $L$ is
an extension
$K(a_h^{\xi}\colon(\xi,h)\tl(\tau,\ell))$ of $K$. Then the derivations
$\partial_i$ extend to derivations $D_i$ from
$K(a_h^{\xi}\colon(\xi+\ichar,h)\tl(\tau,\ell))$ into $L$
such that~\eqref{eqn:Dia} holds when $(\sigma+\ichar,k)\tl(\tau,\ell)$.
If $a_k^{\sigma}$ is a
separable leader, and $(\sigma+\ichar,k)\tl(\tau,\ell)$, then
\begin{equation}\label{eqn:aksi}
a_k^{\sigma+\ichar}\in K(a_h^{\xi}\colon (\xi,h)\tl(\sigma+\ichar,k))
\end{equation}
(that is, $a_k^{\sigma+\ichar}$ is a rational function over $K$ of its
predecessors);
in particular, $a_k^{\sigma+\ichar}$ is a separable leader. Therefore
generators of $L/K$ that are above separable leaders are themselves
separable leaders.
\end{lemma}
\begin{proof}
The claim follows from the basic properties of derivations, such as
are gathered in \cite[\S 1]{MR2114160}.
We extend the derivations to each generator in turn, according to the ordering $\tl$.
Suppose
$D_i$ has been defined as desired on $K(a_h^{\xi}\colon(\xi,h)\tl(k,\sigma))$ (so that~\eqref{eqn:Dia} holds
whenever it applies).
If $a_k^{\sigma}$ is not a leader, then we are free to define the derivatives $D_ia_k^{\sigma}$ as we like. Now suppose
$a_k^{\sigma}$ is a separable leader, and
$(\sigma+\ichar,k)\tl(\tau,\ell)$. Then $D_ia_k^{\sigma}$ is
obtained by differentiating the minimal polynomial of $a_k^{\sigma}$
over $K(B)$. That is, $D_ia_k^{\sigma}$ is obtained by
differentiating an equation like~\eqref{eqn:fahx}; by the differential
condition, $D_ia_k^{\sigma}$ must be $a_k^{\sigma+\ichar}$ as given
by~\eqref{eqn:sumeta}; this shows that $a_k^{\sigma+\ichar}$ is a
rational function over $K$ of its predecessors.
Finally, in a
positive characteristic~$p$,
$a_k^{\sigma}$ may be an inseparable leader. Then $(a_k^{\sigma})^{p^r}\in \sep{K(a_h^{\xi}\colon
(\xi,h)\tl(\sigma,k))}$ for some positive $r$. If
$(\sigma+\ichar,k)\tl(\tau,\ell)$, then we are free to define
$D_ia_k^{\sigma}$ as $a_k^{\sigma+\ichar}$, provided
$D_i((a_k^{\sigma})^{p^r})=0$. But again this condition is ensured by
the differential condition. Indeed, we may suppose~\eqref{eqn:fahx}
shows the separable dependence of $(a_k^{\sigma})^{p^r}$ over the
predecessors of $a_k^{\sigma}$.
That is, we can understand $f(a_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))$
as $g((a_k^{\sigma})^{p^r})$ for some separable polynomial $g$ over
$K(a_h^{\xi}\colon(\xi,h)\tl(\sigma,k))$.
Then $D_i((a_k^{\sigma})^{p^r})$ is
obtained from~\eqref{eqn:sumeta}, provided we replace the term
$(\partial f/\partial
x_k^{\sigma})(a_h^{\xi}\colon(\xi,h)\tleq(\sigma,k))\cdot
a_k^{\sigma+\ichar}$ with
$g'((a_k^{\sigma})^{p^r})\cdot
D_i((a_k^{\sigma})^{p^r})$. But in the present case, the former term
is $0$. Since,
after the replacement, the resulting
equation still holds, we must have $D_i((a_k^{\sigma})^{p^r})=0$.
\end{proof}
\begin{comment}
\subsection{An example}\label{subsect:example}
Suppose we want to know whether the system
\begin{align}\label{eqn:orig-system}
\partial^{(1,1)}x&=\partial^{(0,2)}x,
& \partial^{(1,2)}x&=\partial^{(2,0)}x
\end{align}
has a solution in an extension of a differential field
$(K,\partial_0,\partial_1)$. We may first consider an extension
$K(a^{\sigma}\colon\size{\sigma}\leq 3)$ of $K$ for which we seek a
compatible extension of $(K,\partial_0,\partial_1)$; we then require
\begin{align}\label{eqn:a11a02}
a^{(1,1)}&=a^{(0,2)},
& a^{(1,2)}&=a^{(2,0)}.
\end{align}
These conditions are shown in a triangle (as in
\S \ref{subsect:another}), where leaders are underlined:
\begin{equation}\label{eqn:aabb}
\begin{matrix}
*&*&a&*\\
*&\underline a&\underline b&\\
b&*& & \\
*& & &
\end{matrix}
\end{equation}
If we differentiate~\eqref{eqn:orig-system} according
to~\eqref{eqn:Dia} as much as possible, considering only those
$a^{\sigma}$ such that $\size{\sigma}\leq 3$, we arrive at a triangle
\begin{equation}\label{eqn:ababbb}
\begin{matrix}
*&*&a&\underline b\\
*&\underline a&b&\\
b&b& & \\
*& & &
\end{matrix}
\end{equation}
with minimal leaders underlined. The corresponding extension of $K$
meets the differential condition. However, this observation, by
itself, is not enough to ensure that~\eqref{eqn:orig-system} has a
solution. The problem is that the triangle~\eqref{eqn:ababbb} does
not provide enough room to compare the common derivative $a^{(1,3)}$
of the two minimal leaders.
So far, we have in effect noted that, by the computation
\begin{equation*}
\partial^{(0,1)}(\partial^{(1,1)}x-\partial^{(0,2)}x)
-(\partial^{(1,2)}x-\partial^{(2,0)}x)
=\partial^{(2,0)}x-\partial^{(0,3)}x,
\end{equation*}
we have an equation
\begin{equation*}
[\partial^{(1,1)}x-\partial^{(0,2)}x,
\partial^{(1,2)}x-\partial^{(2,0)}x]=
[\partial^{(1,1)}x-\partial^{(0,2)}x,
\partial^{(0,3)}x-\partial^{(2,0)}x]
\end{equation*}
of differential ideals. Equating the least common derivative of the
minimal leaders in~\eqref{eqn:ababbb} corresponds to the computations
\begin{gather*}
\partial^{(0,2)}(\partial^{(1,1)}x-\partial^{(0,2)}x)
-\partial^{(1,0)}(\partial^{(0,3)}x-\partial^{(2,0)}x)
=\partial^{(3,0)}x-\partial^{(0,4)}x,\\
-(\partial^{(3,0)}x-\partial^{(0,4)}x)
-\partial^{(0,1)}(\partial^{(0,3)}x-\partial^{(2,0)}x)
=\partial^{(2,1)}x-\partial^{(3,0)}x,
\end{gather*}
which give us an equation
\begin{equation}\label{eqn:ideals23}
[\partial^{(1,1)}x-\partial^{(0,2)}x,
\partial^{(1,2)}x-\partial^{(2,0)}x]=
[\partial^{(1,1)}x-\partial^{(0,2)}x,
\partial^{(0,3)}x-\partial^{(2,0)}x,
\partial^{(3,0)}x-\partial^{(2,1)}]
\end{equation}
of differential ideals. The conditions imposed by the generators of
the right member of~\eqref{eqn:ideals23} can be depicted as follows:
\begin{equation}\label{eqn:triangle2}
\begin{matrix}
*&*&a&\underline b\\
*&\underline a&*&\\
b&c&&\\
\underline c&&&
\end{matrix}
\end{equation}
By going outside~\eqref{eqn:ababbb}, we have found a new minimal
leader.
As we obtained~\eqref{eqn:ababbb} from~\eqref{eqn:aabb}, so
from~\eqref{eqn:triangle2} we obtain
\begin{equation*}
\begin{matrix}
*&*&a&\underline b\\
*&\underline a&b&\\
b&b&&\\
\underline b&&&
\end{matrix}
\end{equation*}
which generates an extension of $K$ meeting the differential
condition. Moreover, there is a larger extension of $K$, namely
$K(a^{\sigma}\colon\size{\sigma}\leq 6)$ or $L$, where the relations
among the generators are depicted thus:
\begin{equation}\label{eqn:triangle3}
\begin{array}{cccc|ccc}
*&*&a&\underline b&b&b&b\\
*&\underline a&b&b&b&b& \\
b&b&b&b&b& & \\
\underline b&b&b&b& & & \\\cline{1-4}
b&b&b&\multicolumn{4}{c}{} \\
b&b& &\multicolumn{4}{c}{} \\
b& & &\multicolumn{4}{c}{}
\end{array}
\end{equation}
The minimal leaders are the same as before, and $L$ meets the
differential condition. Finally, the least common derivative of any
two minimal leaders, as such, falls within the last triangle---indeed,
within the delineated square in the triangle. We shall see that this
is enough to ensure that the original system~\eqref{eqn:orig-system}
is soluble.
Equating, for example, $\partial^{(3,0)}a^{(0,3)}$ and
$\partial^{(0,3)}a^{(3,0)}$ corresponds to the computation
\begin{multline*}
% \partial^{(3,0)}(\partial^{(0,3)}x-\partial^{(2,0)}x)-
%\partial^{(0,3)}(\partial^{(3,0)}x-\partial^{(2,1)})
%=
\partial^{(3,0)}(\partial^{(0,3)}x-\partial^{(2,0)}x)-
\partial^{(0,3)}(\partial^{(3,0)}x-\partial^{(2,1)}x)\\
=\partial^{(3,3)}x-\partial^{(5,0)}x-
\partial^{(3,3)}x+\partial^{(2,4)}x
=\partial^{(2,4)}x-\partial^{(5,0)}x,
\end{multline*}
where we must work with derivatives as great as
$\partial^{(3,3)}x$; but alternatively, we have
\begin{multline*}
\partial^{(2,1)}(\partial^{(0,3)}x-\partial^{(2,0)}x)-
\partial^{(2,0)}(\partial^{(3,0)}x-\partial^{(2,1)}x)\\
=\partial^{(2,4)}x-\partial^{(4,1)}x-
\partial^{(5,0)}x+\partial^{(4,1)}x
=\partial^{(2,4)}-\partial^{(5,0)}x,
\end{multline*}
where no derivative is as great as $\partial^{(3,3)}x$.
Similar computations are possible for the other pairs of leaders.
In the terminology introduced by Azriel Rosenfeld \cite[\S I.2,
p.~397]{MR0107642} in characteristic $0$, the set of generators of
the right member of~\eqref{eqn:ideals23} is
\emph{coherent.}
\end{comment}
\subsection{A solubility condition}
If $(K,\partial_0,\dots,\partial_{m-1})\models\mDF$, then this model
has an extension whose underlying field is the separable closure of
$K$ (as by \cite[Lem.~3.4, p.~930]{MR2000487} and \cite[Lem.~2.4,
p.~1334]{MR2114160}). We shall need this in a more general form:
\begin{lemma}\label{lem:comm}
Suppose a field $M$ has two subfields $L_0$ and $L_1$, which in turn
have a common subfield $K$. For each $i$ in $2$, suppose there is a
derivation $D_i$ mapping $K$ into $L_i$ and $L_{1-i}$ into $M$.
Then the bracket $[D_0,D_1]$ is a well-defined
derivation on $K$. Suppose it is the $0$-derivation.
\begin{comment}
, that is, the
following diagram commutes.
\begin{equation*}
\begin{CD}
K @>{D_1}>> L_0\\
@V{D_0}VV @VV{D_0}V\\
L_1 @>>{D_1}> M
\end{CD}
\end{equation*}
\end{comment}
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}
Obvious from \cite[Fact~1.1~(2)]{MR2114160}.
\begin{comment}
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{comment}
\end{proof}
In a positive characteristic, the possibility of inseparably algebraic
extensions presents a challenge, which however is handled by the following.
\begin{comment}
The following example illustrates how the challenge
can be overcome. 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.
\end{comment}
\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.
\end{comment}
\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