またAtiyah-MacDonaldの可換環論入門を読んでいて、こんなことが書いてあった。
そのつくり方は、a,s∈A, s≠0なるすべての順序対(a, s)をとり、これらの組に対して次のように同値関係を定義することからなる。この定義はAが整域であるときだけうまく昨日する。なぜなら、この関係が推移的であることの証明は消去律が成り立つこと、すなわちAは0と異なる零因子をもたないことを意味しているからである。
確かに商環の定義をとしていけないとは習ったのだが、なんでそうしてはいけないのか、どんな例で推移律が失敗するのかを考えたことはなかった。とりあえず電車のなかでを積閉集合{1, 3}で商環にしたときのことを考えてみたのだがうまく行かなかったのでAlloyで調べてみた。
コードはgistに上げてある:
https://gist.github.com/ashiato45/0d0d0272dc6b2dc0ab22db2673a35d6b
- isMultClosedでiが積閉集合であることの判定をする。
- pEquiv [a, s, b, t]でa/sとb/tが上の意味で「等しい」かどうかを判定する。この関係をと書くことにする。
これでmain3で、
「mcを積閉集合とし、a,b,cを環の元とし、s,t,uをmcの元とし、とがみたされているとする。このとき、が成り立つ。」と主張し、「check main3」でその反例を探しにいく。すると、次のような例がみつかった。
これは、環を考え、積閉集合として環全体をとり、を考えることに相当する。確かにだが、となっていて、だがとなっている。
そういうわけで一応反例は見つかったのだが、分母に0が来るのはなんとなく反則感があるので「積閉集合に0が入らない」という制約を追加して調べてみる。これがmain4である。実行すると、次のような例がみつかった。和と積は次のように入っている。
this/Ring<:add={Ring$0->Element$0->Element$0->Element$2,
Ring$0->Element$0->Element$1->Element$3,
Ring$0->Element$0->Element$2->Element$0,
Ring$0->Element$0->Element$3->Element$1,
Ring$0->Element$1->Element$0->Element$3,
Ring$0->Element$1->Element$1->Element$2,
Ring$0->Element$1->Element$2->Element$1,
Ring$0->Element$1->Element$3->Element$0,
Ring$0->Element$2->Element$0->Element$0,
Ring$0->Element$2->Element$1->Element$1,
Ring$0->Element$2->Element$2->Element$2,
Ring$0->Element$2->Element$3->Element$3,
Ring$0->Element$3->Element$0->Element$1,
Ring$0->Element$3->Element$1->Element$0,
Ring$0->Element$3->Element$2->Element$3,
Ring$0->Element$3->Element$3->Element$2}
this/Ring<:mult={Ring$0->Element$0->Element$0->Element$0,
Ring$0->Element$0->Element$1->Element$1,
Ring$0->Element$0->Element$2->Element$2,
Ring$0->Element$0->Element$3->Element$3,
Ring$0->Element$1->Element$0->Element$1,
Ring$0->Element$1->Element$1->Element$1,
Ring$0->Element$1->Element$2->Element$2,
Ring$0->Element$1->Element$3->Element$2,
Ring$0->Element$2->Element$0->Element$2,
Ring$0->Element$2->Element$1->Element$2,
Ring$0->Element$2->Element$2->Element$2,
Ring$0->Element$2->Element$3->Element$2,
Ring$0->Element$3->Element$0->Element$3,
Ring$0->Element$3->Element$1->Element$2,
Ring$0->Element$3->Element$2->Element$2,
Ring$0->Element$3->Element$3->Element$3}
これは環で、積閉集合としてを考えている。
すると、となっているが、
がよりわかる。
整域じゃない環について商環を真剣に考えたことがなかったので良い例が手に入って面白かった。あと、またAlloyが使えたので満足。