Dummit and Footeの抽象代数学におけるバグの発見

Ben Kallus

Dummit and Footeの抽象代数学におけるバグの発見

Recurse Centerでの2週目に、私はDummit and Footeの抽象代数学の教科書（「Abstract Algebra」という適切なタイトルのもの）をRocqで形式化しようとしていました。本の最初の証明演習でかなり苦労しました。なぜなら、提示された証明の目標が真ではなかったからです。それを解明するのは、フラストレーションが溜まるのと同時に、エキサイティングなことでした :)

定義

集合Aから集合Bへの関数 f（"f: A -> B"と表記）は、以下の条件を満たすペアの集合です。

• 各ペアの最初の要素はAから来る。
• 各ペアの2番目の要素はBから来る。
• Aの各要素について、それはペアの最初の要素としてちょうど1回現れる。

言い換えれば、プログラマーの皆さんにとって、関数はすべての入力-出力ペアの集合によって定義され、決定論的でなければなりません。

関数が単射であるとは、2つの異なる入力が同じ出力にマッピングされない場合です。例えば、f(x) = x^2 という f: int -> int は単射ではありません。なぜなら f(1) = f(-1) だからです。

関数 f: A -> B が左逆元を持つとは、すべての a in A に対して g(f(a)) = a となるような関数 g: B -> A が存在する場合です。言い換えれば、fの左逆元はfを「元に戻す」操作です。

命題1 (1)

この本での最初の証明演習は、関数が単射であることと、左逆元を持つことが同値であることを示すことです。

この命題は偽です。A = {}、B = {1} とします。関数 f: A -> B = {} とします。この関数fは、上記の定義にリストされた3つの基準を満たすため、確かに関数です。この関数fは単射です。なぜなら、「2つの異なる入力が同じ出力にマッピングされない」ということが（空虚に）真であるからです。しかし、fは左逆元を持ちません。なぜなら、BからAへの関数が存在しないからです。

もし私がこの演習を紙の上で行っていたら、このコーナーケースに気づかなかったでしょう。Rocqを使用していたため、命題がそのままでは真ではないことに気づくまで、壁にぶつかり続けました。命題を証明するために考えられるすべての方法では、Aが非空であるか、またはBが空であるかのいずれかが必要でした。あまりにも長い時間が経過した後、命題自体が真ではないのではないかと思い始めました。そして、今に至ります :)

この投稿を書いている間に、本の正誤表を確認したところ、これはすでに記載されていました。まあ、仕方ないです :)