Finding a bug in Dummit and Foote's Abstract Algebra

# Ben Kallus's cool website Source: [https://kallus.org/blog/dummit_and_foote.html](https://kallus.org/blog/dummit_and_foote.html) ## Finding a Bug in Dummit and Foote's Abstract Algebra During my second week at the Recurse Center, I've been trying to formalize Dummit and Foote's abstract algebra textbook \(appropriately titled "Abstract Algebra"\) in Rocq\. I had quite a hard time with the first proof exercise in the book because the stated proof goal is not true\. This was both frustrating and exciting to figure out :\) ### Definitions A**function**f from a set A to a set B \(written "f: A \-\> B"\) is a set of pairs such that - The first item in each pair comes from A\. - The second item in each pair comes from B\. - For each element of A, it is the first item in exactly one of the pairs\. In other words, for the programmers among you, a function is defined by the set of all its input\-output pairs, and must be deterministic\.A function is**injective**if no two distinct inputs map to the same output\. For example, f: int \-\> int by f\(x\) = x^2 is not injective because f\(1\) = f\(\-1\)\. A function f: A \-\> B has a**left inverse**if there exists a function g: B \-\> A such that forall a in A, g\(f\(a\)\) = a\. In other words, f's left inverse "undoes" f\. ### Proposition 1**\(1\)** The first proof exercise in the book is to show that a function is injective if and only if it has a left inverse\. This statement is false\. Let A = \{\}, and B = \{1\}\. Let f: A \-\> B = \{\}\. The function f is indeed a function because it satisfies the 3 criteria listed in the definition above\. The function f is injective because it is \(vacuously\) true that no two distinct inputs map to the same output\. However, f does not have a left inverse, because there are no functions from B to A\. I probably wouldn't have thought of this corner case if I was doing this exercise on paper\. Because I was using Rocq, I just kept running into walls trying to prove the proposition as stated\. All the ways I could think of proving the statement required either that A be inhabited or that B be uninhabited\. After way too long, I started to wonder if the proposition just wasn't even true, and here we are :\) While writing this post, I checked the book's errata, and this is already in there\. Oh well :\)