ashiato45.hatenablog.jpで、prime avoidance lemma
から素イデアル条件を外したときの反例を探していて、とりあえず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以下の環について例を探させたところ、次のものを得ました。
元は8個で、Elements(番号)という形で出てくるので、ここではそれらをと書くことにします。
出力によるとであり、です。
そして、イデアルは
、、、
でした。これを見ながら、これがどのような環かを考えてみます。
まず、8つの元の環なので、有限生成アーベル群の分類定理から、加法についてはかかのいずれかであることが分かります。
イデアルを見ると、2倍にすると0になる異なる元が3つあることになるので、とりあえずではなさそうです。
2倍したときの性質は気になるので、さらにの様子を加法の表(画像参照)で調べると、
となることがわかります。2倍して非零な同じものになる異なる元が4つあるので、でもなさそうです。よって、この環の和についての構造はだということが分かります。
この環のなかで2倍された元でかつ非零な元というのはしか有り得ないので、が分かります。
さらに、ということを考えてみると、
はそれぞれのどれかであることがわかります。は2倍すると0になる元でかつではないので、のいずれかであることがわかります。
積については何も見ていないのですが、が多分乗法についての単位元だろうという気がするのでそれで辻褄が合うかを見てみます。
つまり、この環はに要素毎の加法と乗法を入れたもので、であり、であるものであり、
、、、であるということになります。考えてみると、これで確かに辻褄があっていて、無事に反例が見つかり、その構造がわかりました。めでたしめでたし。
*1:元が1つで、その元が0でもあり1でもある環。この上では(かの有名な)0=1が成立する。