商環の同値関係a/s≡b/tをat=bsで定義してはいけない理由(あとまたAlloy)

またAtiyah-MacDonaldの可換環論入門を読んでいて、こんなことが書いてあった。

そのつくり方は、a,s∈A, s≠0なるすべての順序対(a, s)をとり、これらの組に対して次のように同値関係を定義することからなる。 (a,s)\equiv (b,t) \iff at-bs=0.この定義はAが整域であるときだけうまく昨日する。なぜなら、この関係が推移的であることの証明は消去律が成り立つこと、すなわちAは0と異なる零因子をもたないことを意味しているからである。

確かに商環の定義を at-bs=0としていけないとは習ったのだが、なんでそうしてはいけないのか、どんな例で推移律が失敗するのかを考えたことはなかった。とりあえず電車のなかで Z/4Zを積閉集合{1, 3}で商環にしたときのことを考えてみたのだがうまく行かなかったのでAlloyで調べてみた。

コードはgistに上げてある:
https://gist.github.com/ashiato45/0d0d0272dc6b2dc0ab22db2673a35d6b

  • isMultClosedでiが積閉集合であることの判定をする。
  • pEquiv [a, s, b, t]でa/sとb/tが上の意味で「等しい」かどうかを判定する。この関係をa/s \sim b/tと書くことにする。

これでmain3で、
「mcを積閉集合とし、a,b,cを環の元とし、s,t,uをmcの元とし、 a/s\sim b/t b/t\sim c/uがみたされているとする。このとき、 a/s\sim c/uが成り立つ。」と主張し、「check main3」でその反例を探しにいく。すると、次のような例がみつかった。
f:id:sle:20170531232016p:plain
これは、環 Z/2Zを考え、積閉集合として環全体をとり、 a/s=0/1, b/t=0/0, c/u=1/0を考えることに相当する。確かに at-bs=bu-ct=0だが、 au-cs=1となっていて、 0/1\sim 0/0, 0/0\sim 1/0だが 0/1\not\sim 1/0となっている。

そういうわけで一応反例は見つかったのだが、分母に0が来るのはなんとなく反則感があるので「積閉集合に0が入らない」という制約を追加して調べてみる。これがmain4である。実行すると、次のような例がみつかった。和と積は次のように入っている。
f:id:sle:20170531232919p:plain

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}

これは環 Z/2Z\times Z/2Zで、積閉集合として \{(0, 1), (1, 1)\}を考えている。
すると、 (1, 0)/(0, 1)\sim (0, 0)/(0, 1), (0, 0)/(0, 1)\sim (1, 0)/(1, 1)となっているが、
 (1, 0)/(0, 1)\not\sim (1, 0)/(1, 1) (1, 0)\cdot (1, 1) - (0, 1)\cdot (1, 1) = (1, 1) \neq (0, 0)よりわかる。

整域じゃない環について商環を真剣に考えたことがなかったので良い例が手に入って面白かった。あと、またAlloyが使えたので満足。