Alloyを使って可換環(有限)を調べてみる

ashiato45.hatenablog.jpで、prime avoidance lemma

環Aとそのイデアル $\frak a$ と素イデアル $\frak p_1,\dots,\frak p_n$ について、
$\frak a \subset \bigcup_{i=1}^n \frak p_i$ となっているとする。
このとき、あるiに対して $\frak a \subset \frak p_i$ となる。

から素イデアル条件を外したときの反例を探していて、とりあえずn=2だと見つからないということを証明したのでした。
そこで、n=3のときの反例をAlloyで探そうとAlloyの勉強をしていたのですが、その前にid:qnighyさんが見つけてくれました(記事参照)。
とはいえ、やはりここでAlloyの使い方を覚えて反例探しを効率化したかったので、私は私でAlloyを使って見つけようと思っていたのでした。
ashiato45.hatenablog.jp
この記事で練習は済んだので、早速反例を探してみます。
コードはhttps://gist.github.com/ashiato45/bf148bfd114e45b0857baba6231e2a7cに貼ってあります。
あとちょっと補足しておくと、Alloyを使っている以上有限のものしか相手にできないので、もしも反例が無限の環にしかないのならお手上げです。

コードは群のときと大体同じです。今回は加法に対する単位元はzeroと名前をつけてあり、乗法に対する単位元はunと命名してあります。
oneにしなかったのは、Alloyのキーワードとぶつかっているからで、とりあえずフランス語の「1」にしておきました。
途中で可換環の定義が正しくできていることを確かめるために例を表示してみたのですが(50行目)、割と初心者殺しの観がある零環*1が見つかったのを見て、
「確かにAlloyで予めモデリングしておけばバグ発見に役立ちそうだなあ」と思いました。

そして、我々の例について位数8以下の環について例を探させたところ、次のものを得ました。
f:id:sle:20170219150720p:plain
元は8個で、Elements(番号)という形で出てくるので、ここではそれらを $a_0,\dots,a_7$ と書くことにします。
出力によると $1=a_3$ であり、 $0=a_7$ です。
そして、イデアルは
${\frak a} = \{a_4,a_5,a_6,a_7\}$ 、 ${\frak p}_1 = \{a_6, a_7\}$ 、 ${\frak p}_2 = \{a_5, a_7\}$ 、 ${\frak p}_3 = \{a_4, a_7\}$
でした。これを見ながら、これがどのような環かを考えてみます。

まず、8つの元の環なので、有限生成アーベル群の分類定理から、加法については ${\mathbb Z}/8{\mathbb Z}$ か ${\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}$ か $({\mathbb Z}/2{\mathbb Z})^3$ のいずれかであることが分かります。
イデアル ${\frak p}_1,{\frak p}_2,{\frak p}_3$ を見ると、2倍にすると0になる異なる元が3つあることになるので、とりあえず ${\mathbb Z}/8{\mathbb Z}$ ではなさそうです。
2倍したときの性質は気になるので、さらに $a_0,a_1,a_2,a_3$ の様子を加法の表(画像参照)で調べると、
$a_0+a_0 = a_1 + a_1 = a_2 + a_2 = a_3 + a_3 = a_4$ となることがわかります。2倍して非零な同じもの $a_4$ になる異なる元が4つあるので、 $({\mathbb Z}/2{\mathbb Z})^3$ でもなさそうです。よって、この環の和についての構造は ${\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}$ だということが分かります。
この環のなかで2倍された元でかつ非零な元というのは $(2,0)$ しか有り得ないので、 $a_4=(2,0)$ が分かります。
さらに、 $a_0+a_0 = a_1 + a_1 = a_2 + a_2 = a_3 + a_3 = a_4$ ということを考えてみると、
$a_0,a_1,a_2,a_3$ はそれぞれ $(1,0),(3,0),(1,1),(3,1)$ のどれかであることがわかります。 $a_5,a_6$ は2倍すると0になる元でかつ $a_4=(2,0)$ ではないので、 $(2,1),(0,1)$ のいずれかであることがわかります。

積については何も見ていないのですが、 $(1,1)$ が多分乗法についての単位元だろうという気がするのでそれで辻褄が合うかを見てみます。
つまり、この環は ${\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}$ に要素毎の加法と乗法を入れたもので、 $0=(0,0)$ であり、 $1=(1,1)$ であるものであり、
${\frak a}=\{(2,0),(2,1),(0,1),(0,0)\}$ 、 ${\frak p}_1=\{(0,0),(2,0)\}$ 、 ${\frak p}_2=\{(0,0),(2,1)\}$ 、 ${\frak p}_3=\{(0,0),(0,1)\}$ であるということになります。考えてみると、これで確かに辻褄があっていて、無事に反例が見つかり、その構造がわかりました。めでたしめでたし。

*1:元が1つで、その元が0でもあり1でもある環。この上では(かの有名な)0=1が成立する。