We now define *elimination ideals*, a notion
critical to this section.

**Definition 11.1***
Let I be an ideal of
and *1*
j
n. The j-th elimination ideal
is the ideal of
defined by
*

The NCProcess command generates output which is
displayed as a list of *V*-categories
(see
§)
and the *V*-categories
are defined in such a way that if one of the polynomials
in a category is in the elimination ideal, then the entire
category is a subset of the elimination ideal.

It is helpful to be able to find a generating set
(or even a Gröbner Basis)
not only for *I* but also for the *j*-th elimination ideals.
If one has a Gröbner Basis with respect to certain
types of monomial orders, then, if one considers
the subset of the Gröbner Basis which lies in the
*j*-th elimination ideal, then this set is itself a Gröbner Basis
and generates the *j*-th elimination ideal. This is
the content of Theorem 11.3.

To layout the correspondence of the rest of this
section to Chapter 3 of **[CLS]**,
note that the definition of an
elimination ideal (§1 Definition 1)
an elimination order (§1 Exercise 5),
an Elimination Theorem (§1 Theorem 2)
and an Extension Theorem (§1 Theorem 3)
are given in **[CLS]**. We now give the corresponding
definitions, a corresponding Elimination theorem
and discuss issues involving extensions
in the noncommuative case.

**Definition 11.2 [CLS]***
Let j and n be natural numbers such that *1*
j
n. A monomial order is of j-th elimination type provided that any
monic monomial involving
or
is greater than any monic monomial of
.
*

In this section, we follow the ordering convention
used in **[CLS]**.
With the definition of elimination order given above,
if .
For instance, if 1 < *j* < *n*, then
. In the discussions in the rest of the
paper, we have always taken .

If one considers a multigraded lex order (§ and §) under which

then this multigraded lex order is of *j*th
elimination type. Note that a pure lex order
is of
*j*-th elimination type for any *j* such that .

The following theorem is the main result of this section
and shows that a Gröbner Basis for an ideal *I* with
respect to an *j*-th elimination order yields a
Gröbner Basis with respect to the *j*-th elimination ideal.

**Theorem 11.3***
Let R =
let
be a term order on the monic monomials of R, let I be an ideal of R
and let G be a Gröbner Basis of I with respect to
.
If
*1*
j
n and
is of j-th elimination type, then
G
is a Gröbner Basis for
I
*

If a pure lex order is used, if one runs NCProcess
*until the GBA being used by NCProcess
generates a Gröbner Basis*
and all of the shrinking (see
§)
parts of the NCProcess commands are turned off,
then the categories which this outputs
can be used to determine generating
sets for the elimination ideals.
More precisely,
the union of the categories which are subsets of
the *j*-th elimination ideal is
a generating set for the *j*-th elimination ideal.

The comments of the last paragraph
hold when a multigraded lex order is used rather
than a pure lex order *and* one only considers
*j*-th elimination ideal only if the order is described
by placing a `` '' between and .

We begin by proving the following lemma.

**Lemma 11.4***
If f is a nonzero polynomial in
,
if
is a monomial order, if
is of the j-th elimination type and if the leading monomial of f
with respect to
is in
,
then
f.
*

Proof. \
Let *lm*(*f*) denote the leading monomial of *f* with
respect to the order .

Suppose and
are monic
monomials in such that
and
.
Suppose there exists an
such that
.
Definition
11.2
and the assumption that
imply that .
But since *lm*(*f*) is the
leading monomial of *f*.
But then
which is a contradiction.
Therefore,
for . Therefore, . This completes the
proof of Lemma 11.4.

We now move to the proof of Theorem 11.3.

**Proof of Theorem 11.3.**

Throughout this proof, for any nonzero polynomial *p*,
*lm*(*p*) will denote the leading monomial of *p*
with respect to the order .

Let be
nonzero. Since and *G* is a Gröbner
Basis, *f* has a finite *d*-representation with
respect to *G* (**[FMora]**). That is,
there exist scalars there exists ,
and there exist monic monomials
such that

and

We wish to show that for .
Since , its
leading term
*lm*(*f*) is in .
Therefore,
(gbdefn:two) implies that
, , .
An application of Lemma 11.4
yields . For
,

Now, (11.8)
implies that
, , .
Since is of *j*-th elimination type,
an application
of Lemma 11.4 yields
for
. Thus,
*f* has a *d*-representation in
with respect to .
Since every element of
has a finite d-representation with respect to
, an application
of Proposition 2.2 of
**[FMora]** proves that
is a Gröbner Basis. The completes the proof
of Theorem 11.3.

Note that
we have not analyzed what
is called
extendibility of solutions in
commutative theory (**[CLS]**).
The main theorem involving extendibility of solutions
can be viewed as giving sufficient conditions,
in the commutative case, as to when backsolving
is possible.
We now give a brief description of these ideas.

Elimination ideals (and, therefore, Gröbner Basis with respect
to term orders of elimination type) can be used to simplify
the problem of finding common zeros of sets of polynomial equations.
In other words, these elimination ideals can facilitate the
process of backsolving.
One process of finding a common zero of the set of
polynomials in an ideal *I* involves
first finding a common zero of the polynomials in
a -th elimination ideal for close to *n*.
This common zero will only assign values to the variables
. One then
tries to extend this common zero to a common zero
of the -elimination ideal for . Extending
the common zero consists of trying to assign values
to the variables . The procedure
repeats until one cannot extend a common zero (in which case
one has to backtrack and pick a different common zero in
the previous steps if there are any other choices) or
until one finds a common zero of the entire ideal.

For the case of common zeros of commutative polynomials
whose coefficients are complex numbers,
Chapter 3 §1 of **[CLS]** gives a theorem
which guarantees the
extendibility of common zeros from one elimination ideal
to the next under certain conditions. The authors
do not know
of any theorem of this type in the noncommutative case.
The main reason we have not looked into it
ourselves is that in the examples
we have run (many besides those presented here),
it was obvious that backsolving was possible
for any choice of solution at each stage.
Possibly more complicated theorems in systems
or operator theory will require such a theory.
This remains to be seen.

Wed Jul 3 10:27:42 PDT 1996