在Dummit和Foote的Abstract Algebra中发现一个错误

# Ben Kallus的酷网站 来源：https://kallus.org/blog/dummit_and_foote.html ## 在Dummit与Foote的《抽象代数》中发现一个错误 在Recurse Center的第二周，我尝试用Rocq形式化Dummit与Foote的《抽象代数》教材。书中第一个证明练习让我遇到了很大困难，因为所陈述的证明目标并不成立。发现这一点既令人沮丧又令人兴奋 :) ### 定义 从集合A到集合B的**函数**f（记作"f: A -> B"）是一组有序对，满足： - 每对中的第一个元素来自A - 每对中的第二个元素来自B - 对于A中的每个元素，它恰好是其中一对的第一个元素 换句话说，对程序员而言，函数由其所有输入-输出对的集合定义，且必须是确定性的。**单射函数**是指没有两个不同的输入映射到相同输出的函数。例如，f: int -> int 定义为 f(x) = x² 不是单射函数，因为 f(1) = f(-1)。 函数 f: A -> B 存在**左逆**当且仅当存在函数 g: B -> A，使得对所有 a ∈ A 有 g(f(a)) = a。换句话说，f 的左逆函数能"撤销"f 的作用。 ### 命题1 (1) 书中第一个证明练习是要求证明：函数是单射的当且仅当它存在左逆。 该命题是错误的。设 A = {}（空集），B = {1}。定义函数 f: A -> B = {}。函数 f 确实满足上述定义中的三个条件，因此是一个函数。该函数是单射的，因为（空虚地）不存在两个不同的输入映射到相同输出。然而，f 没有左逆，因为不存在从 B 到 A 的函数。 如果我在纸上做这个练习，可能不会想到这个边界情况。由于使用的是Rocq，在证明该命题时总是碰壁。我想到的所有证明方法都要求 A 非空或 B 非空。经过很长时间后，我开始怀疑这个命题本身可能不成立，于是就有了这篇文章 :) 撰写本文时，我查阅了该书的勘误表，发现这个错误已被记录。不过，好吧 :)