Solution via a Prestrategy

We now apply a strategy to see how one might discover this theorem. The formalities of what a strategy is are not important here. This chapter is designed to illustrate NCProcess and allied commands. For a description of the formalities of a strategy see [HS] or for a sketch see Chapter 19.

Before running NCProcess1, we must declare $A$, $B$ and $C$ to be knowns and the remaining variables to be unknowns. The ``**" below denotes matrix multiplication.

In[1]:=Get["NCGB.m"];
In[2]:=SetNonCommuative[A,B,C0,m1,m2,n1,n2];
In[3]:=SetKnowns[A,B,C];
In[4]:=SetUnknowns[m1,m2,n1,n2,a,b,c,e,f,g];

We now set the variable FAC equal to the list of polynomials in §17.2.

In[5]:=FAC = {A**m1 - m1**a - m2**f**c,
              A**m2 - m2**e,
              B - m1**b - m2**f,
              -c + C0**m1,
              -g + C0**m2,
              n1**m1 - 1,
              n1**m2,
              n2**m1,
              n2**m2 - 1,
              m1**n1 + m2**n2 - 1};

The commands above and below will be explained in Chapter 18.

The command which produces the output in the file Spreadsheet1.dvi is the following.

In[6]:= result = NCProcess1[FAC,2,"Spreadsheet1"];

Here NCProcess1 is being applied to the set of relations FAC for 2 iterations. The NCProcess1 command has two outputs, one will be stored in result and the other will be stored in the file Spreadsheet1.dvi. The Spreadsheet1.dvi file appears below and is likely to be more interesting and useful than the value of result. The file created by NCProcess is a list of equations whose solution set is the same as the solution set for FAC. (We added the $<===$ appearing below after the spreadsheet was created.) The $\rightarrow$ below can be read as an equal sign.

THE ORDER IS NOW THE FOLLOWING:
$A<B<C\ll m_{1}\ll m_{2}\ll n_{1}\ll n_{2}\ll a\ll b\ll c\ll e\ll f\ll g\\$
YOUR SESSION HAS DIGESTED
THE FOLLOWING RELATIONS

THE FOLLOWING VARIABLES HAVE BEEN SOLVED FOR:

$\{a,b,c,e,f,g\}$

The corresponding rules are the following:

$a\rightarrow n_{1} A m_{1}$

$b\rightarrow n_{1} B$

$c\rightarrow C m_{1}$

$e\rightarrow n_{2} A m_{2}$

$f\rightarrow n_{2} B$

$g\rightarrow C m_{2}$

USER CREATIONS APPEAR BELOW


SOME RELATIONS WHICH APPEAR BELOW
MAY BE UNDIGESTED

THE FOLLOWING VARIABLES HAVE NOT BEEN SOLVED FOR:
$\{m_{1},m_{2},n_{1},n_{2}\}$

2.0 The expressions with unknown variables $\{n_{1},m_{1}\}$
and knowns $\{A,B,C\}$

$n_{1} m_{1}\rightarrow 1$

$(1-m_{1} n_{1}) A m_{1} + -1(1-m_{1} n_{1}) BC m_{1} = 0 \hspace{1.7in} <===$

2.0 The expressions with unknown variables $\{n_{1},m_{2}\}$
and knowns $\{A\}$

$n_{1} m_{2}\rightarrow 0$

$n_{1} A m_{2}\rightarrow 0$

2.0 The expressions with unknown variables $\{n_{2},m_{1}\}$
and knowns $\{A,B,C\}$

$n_{2} m_{1}\rightarrow 0$

$n_{2} B C m_{1}\rightarrow n_{2} A m_{1}$

2.0 The expressions with unknown variables $\{n_{2},m_{2}\}$
and knowns $\{\}$

$n_{2} m_{2}\rightarrow 1$

4.0 The expressions with unknown variables $\{n_{2},n_{1},m_{2},m_{1}\}$
and knowns $\{\}$

$m_{2} n_{2}\rightarrow 1-1m_{1} n_{1}\hspace{3in} <===$

The above ``spreadsheet" indicates that the unknowns $a$, $b$, $c$, $e$, $f$ and $g$ are solved for and states their values. The following are facts about the output: (1) there are no equations in 1 unknown, (2) there are 4 categories of equations in 2 unknowns and (3) there is one category of equations in 4 unknowns. A user must observe that the first equation ¹which we marked with $<===$ becomes an equation in the unknown quantity $m_1 n_1$ when multiplied on the right by $n_1$. This motivates the creation of a new variable $P$ defined by setting

$$P_1 = m_1 n_1 .$$ (3)

The user may notice at this point that the second equation marked with $<===$ is an equation in only one unknown quantity $m_2 n_2$ once the above assignment has been made and $P_1$ is considered known². These observations lead us to ``select" (see footnote corresponding to O2 in §18.2) the equations $m_1 n_1-P_1$ and $m_2 n_2 - 1 + m_1 n_1$. Since we selected an equation in $m_1 n_1$ and an equation in $m_2 n_2$, it is reasonable to select the the equations $n_1 m_1 - 1$, and $n_2 m_2 - 1$ because they have exactly the same unknowns. While useless at this point we illustrate the command GetCategory with the following examples

In[10]:= GetCategory[{n1,m1},NCPAns ]
Out[10]= { n1**m1 - 1 }

In[11]:= GetCategory[{n1,m1,n2,m2},NCPAns ]
Out[11]= {m2**n2 + m1**n1 - 1 }

Run NCProcess1 again ³with (17.3) added and $P_1$ declared known as well as $A$, $B$ and $C$ declared known. See Chapter 18.4 for the precise call. The output is:

THE ORDER IS NOW THE FOLLOWING:
$A<B<C<P_{1}\ll m_{1}\ll m_{2}\ll n_{1}\ll n_{2}\ll a\ll b\ll c\ll e\ll f\ll g\\$
YOUR SESSION HAS DIGESTED
THE FOLLOWING RELATIONS

THE FOLLOWING VARIABLES HAVE BEEN SOLVED FOR:

$\{a,b,c,e,f,g\}$

The corresponding rules are the following:

$a\rightarrow n_{1} A m_{1}$

$b\rightarrow n_{1} B$

$c\rightarrow C m_{1}$

$e\rightarrow n_{2} A m_{2}$

$f\rightarrow n_{2} B$

$g\rightarrow C m_{2}$

The expressions with unknown variables $\{\}$
and knowns $\{A,B,C,P_{1}\}$

$P_{1} P_{1}\rightarrow P_{1}$

$-1P_{1} A (1+ -1P_{1}) = 0$

$A P_{1}+ -1P_{1} A+ -1(1+ -1P_{1}) BC P_{1} =0$

USER CREATIONS APPEAR BELOW

$m_{1} n_{1}\rightarrow P_{1}$

$n_{1} m_{1}\rightarrow 1$

$n_{2} m_{2}\rightarrow 1$

$m_{2} n_{2}\rightarrow 1+ -1m_{1} n_{1}$

SOME RELATIONS WHICH APPEAR BELOW
MAY BE UNDIGESTED

THE FOLLOWING VARIABLES HAVE NOT BEEN SOLVED FOR:
$\{m_{1},m_{2},n_{1},n_{2}\}$

2.0 The expressions with unknown variables $\{n_{1},m_{1}\}$
and knowns $\{P_{1}\}$

$\Uparrow\ m_{1} n_{1}\rightarrow P_{1}$

$\Uparrow\ n_{1} m_{1}\rightarrow 1$

2.0 The expressions with unknown variables $\{n_{2},m_{2}\}$
and knowns $\{\}$

$\Uparrow\ n_{2} m_{2}\rightarrow 1$

4.0 The expressions with unknown variables $\{n_{2},n_{1},m_{2},m_{1}\}$
and knowns $\{\}$

$\Uparrow\ m_{2} n_{2}\rightarrow 1+ -1m_{1} n_{1}$

Note that the equations in the above display which are in the undigested section (i.e., below the lowest set of bold lines) are repeats of those which are in the digested section (i.e., above the lowest set of bold lines). The symbol $\Uparrow$ indicates that the polynomial equation also appears as a user select on the spreadsheet. We relist these particular equations simply as a convenience for categorizing them. We will see how this helps us in §17.4. Since all equations are digested, we have finished using NCProcess1 (see S4). As we shall see, this output spreadsheet leads directly to the theorem about factoring systems.