在Dummit and Foote抽象代数中发现一个Bug
Finding a bug in Dummit and Foote's Abstract Algebra
我在Recurse Center的第二周，尝试用Rocq形式化Dummit and Foote的《Abstract Algebra》教材。第一个证明练习就让我卡住了——命题本身是错的。这让我既沮丧又兴奋。书中声称“函数是单射当且仅当它有左逆”，但在空集A到非空集B的情况下，函数是单射的，却不存在从B到A的函数，因此没有左逆。用Rocq推导时，我不断碰壁，最终意识到命题不成立。后来查勘误表，发现这个问题早已被指出。这次经历让我体会到形式化验证如何帮助发现传统笔算中容易忽略的边界情况。
我可能不会想到这个边界情况，如果我是用纸笔做这个练习的话。
HN 评论区
36- generationP
这个错误不只存在于 Dummit and 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` 不必要地要求 `g` 将 `B` 中那些根本无法由 `f` 产生的元素映射回 `A`，而这些元素对于左逆来说本应无关紧要。
- jonlong
我想补充的是，左消去律的性质恰好等价于单射性，即 `f : A -> B` 是单射当且仅当对于任意 `g, h : C -> A`，`f o g = f o h` 蕴含 `g = h`。如果 `A = {}`，则 `f` 既是单射也是左消去的，两者皆为空真。
微妙之处在于，左消去律并不等价于存在左逆，原因正是上文所指出的。
这一观察的价值在于，左消去律是单射性的一个有用推广，它在任何范畴中都成立，其中左消去态射被称为单态射（monomorphisms）。如果你已经了解单态射，就更容易注意到 D&F 这道习题中有些“不对劲”的地方！
- hyperhello
我不认为仅仅因为没有任何两个输入映射到同一个输出，就把 {}-> 称为单射是公平的。那是空真。