一位开发者在使用Rocq形式化验证工具研习Dummit and Foote的《抽象代数》教材时，发现书中第一道证明习题存在错误1。该题声称函数的单射性等价于存在左逆元，但这一命题在特定情况下并不成立1。
作者通过反例揭示了这一缺陷：当定义域A为空集，值域B为非空集合（如{1}）时，函数f: A → B虽然是单射（空集映射满足单射条件），但不存在从B到A的函数，因此不存在左逆元1。这说明单射性与左逆元存在性的等价性在边界情况下不成立1。
作者在Recurse Center第二周期间遇到了这一问题1。该错误已被收入教材勘误表中1。
A mathematician discovered a logical error in the first proof exercise of Dummit and Foote's widely-used abstract algebra textbook while formalizing the material using the Rocq proof assistant 1. The problem claims that a function is injective if and only if it possesses a left inverse, but this proposition fails to hold in certain boundary cases 1.
The counterexample involves mapping an empty set to a non-empty set: when A is the empty set and B contains the element 1, the function f from A to B is indeed injective—since no two distinct elements in the empty domain can map to the same element 1. However, no function can exist from B back to A, making it impossible for f to have a left inverse 1. This demonstrates that the biconditional statement in the problem is incorrect. The error has since been added to the textbook's official errata list 1, and the finder encountered the issue during the second week at Recurse Center 1.
评论
还没有评论，欢迎留下第一条。