QE で可換 - ATPとCASのこと

　今回も線形代数の話題です．

　2 次の正方行列 $A,\quad X$ が $AX=XA$ を満たすならばスカラー $s,t$ が存在して
$X=s A+t $\array{1\quad 0\\ 0\quad 1}$$
となるための $A$ の条件を考えます．

　まず行列を

A:={{a,b},{c,d}};X:={{x,y},{z,w}};E2:={{1,0},{0,1}};O2:={{0,0},{0,0}};

のように準備し，それらについての等式を LogicalExpand 関数で展開して，上記を論理式で表し，QE します．

Reduce[
　ForAll[{x, y, z, w},
　　LogicalExpand[A.X - X.A == O2 ],
　　Exists[{s, t}, LogicalExpand[X == s*A + t*E2] ]
　]
]

すると Mathematica は

b != 0 || c != 0 || a (a - d) != 0 || (a - d) d != 0

と答えますが，見難いので

Reduce[ Not[%] ]

のように否定をとると

(c == 0 && b == 0 && a == d) || (d == 0 && c == 0 && b == 0 && a == 0)

となり，仕上げは QEPCAD B で

rlqepcad *1;

のように QE すれば

a - d = 0 and b = 0 and c = 0

と出力されます．よって，条件は「 $A$ がスカラー行列でないこと」と判ります．

*1:c = 0 and b = 0 and a = d) or (d = 0 and c = 0 and b = 0 and a = 0