Dummit & Foote『Abstract Algebra』にバグを発見
Finding a bug in Dummit and Foote's Abstract Algebra
Recurse Centerでの2週目、Ben Kallus氏はRocqでDummit & Footeの『Abstract Algebra』の形式化に挑戦。最初の証明演習で、命題が偽であることに気づく。Aが空集合でBが非空の場合、関数は単射だが左逆写像を持たない。紙上では気づきにくいコーナーケースを、証明支援系が明らかにした。書籍の正誤表に既に記載されていた。
Rocqを使っていたからこそ、このコーナーケースを思いついたでしょう。紙でこの演習をしていたら、おそらく気づかなかったはずです。
HNでの議論
36- generationP
これはDummitとFooteに限った話ではなく、単に見落としやすいだけだ。この結果を述べている場所の半分には載っているのではないかと思う。数ヶ月前に自分の講義ノートでは修正した。
- Paracompact
対話型証明アシスタントが数学的思考を単に遅くするのではなく、改善するために使われているのを見るたびに心が温まる。長年これらを使ってきたが、新しい概念を試行錯誤するためのスクラッチペーパーを完全に置き換えることができる、高速なプロトタイピング用途に十分な焦点が当てられていないと感じている。
- troethe
提案された修正、すなわち「Aが空でないか、Bが空であること」を要求するのは機能するが、この特定のエッジケースを解決するためだけに付け足されたように見える。よりエレガントな解決策は、左逆写像の定義を関数 `g: B -> A` から関数 `g: f(A) -> A` へと緩和することだと思う。ここで `f(A)` は `B` の部分集合で、実際に `f` によって写像される要素、つまり本の関数定義の言葉で言えば `f` の「右」要素の集合である。これもエッジケースを解決する。なぜなら `f(A) = f({}) = {}` であり、関数 `g: {} -> {}` が（ちょうど一つ）存在し、それが自明に `f` の左逆写像となるからだ。ここでの本当の問題は、`g: B -> A` というステートメントが、`f` によって生成され得ない `B` の要素を `A` に写像し戻すことを `g` に不要に要求しており、したがって左逆写像にとって無関係であるべきだということだった。
- jonlong
ここで付け加えたいのは、左簡約性の性質が単射性と正確に同値であるということだ。すなわち、`f : A -> B` が単射であるのは、任意の `g, h : C -> A` に対して、`f o g = f o h` ならば `g = h` が成り立つとき、かつそのときに限る。もし `A = {}` ならば、`f` は単射かつ左簡約的であり、両方とも空虚に真である。微妙な点は、左簡約性が左逆写像を持つことと同値ではないということだ。これはまさに指摘された理由による。この観察の価値は、左簡約性が単射性の有用な一般化であり、任意の圏で機能するということだ。そこでは左簡約的な射はモノ射と呼ばれる。もしモノ射について既に知っていれば、D&Fの演習問題に何か「おかしい」点があることに気づきやすいだろう！
- hyperhello
{}-> を単射と呼ぶのは、2つの入力が同じ出力に写像されないからといって公平ではないと思う。それは空虚だ。