Finding a bug in Dummit and Foote's Abstract Algebra

This one is not just in Dummit and Foote; it's just too easy to miss. I'd guess it appears in half the places that state this result. Fixed it in my own lecture notes a few months ago.

It warms my heart every time I see an interactive proof assistant being used to improve rather than simply slow down mathematical thinking.

After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.

While the proposed fix of requiring "either that A be inhabited or that B be uninhabited" works, it seems tacked on just to solve this particular edge-case.

I think a more elegant solution would be to soften the definition of a left inverse from a function `g: B -> A` to a function `g: f(A) -> A` where `f(A)` is the subset of elements in `B`, that actually get mapped to by `f` or in the words of the book's function definition, the set of "right" elements in `f`.

This solves the edge-case too, as `f(A) = f({}) = {}` and there exists (exactly one) function `g: {} -> {}`, which also trivially is a left inverse of `f`.

The real problem here was, that the statement `g: B -> A` needlessly required `g` to map back elements in B to A, that couldn't even be produced by `f` and should therefore be irrelevant for a left inverse.

What I would add here is that the property of left-cancellation is exactly equivalent to injectivity, i.e., f : A -> B is injective iff, for any g, h : C -> A, f o g = f o h implies g = h. If A = {} then f is injective and left-cancellative, both vacuously.

The subtlety is now that left-cancellativity is not equivalent to having a left inverse, for exactly the reason pointed out.

The value of this observation is that left-cancellativity is a useful generalization of injectivity that works in any category, where left-cancellative morphisms are called monomorphisms. If you already know about monomorphisms, it's easier to notice that there's something "off" about D&F's exercise!

I don’t think it’s fair to call {}-> injective just because no two inputs map to the same output. That’s vacuous.

I asked AI to formalize an old important paper in analysis. In the paper there is a sequence of epsilon_n > 0, epsilon_n -> 0. It came back, and said: "I formalized it, it is all good, but the assumption that epsilons > 0 is not used anywhere. Shall we remove it, you a get a stronger result this way?"

LOL

Help me out, I feel dumb.

The first criterion for a function is stated as:

> The first item in each pair comes from A.

The counter-evidence for the proposition says:

> Let A = {}, and B = {1}. Let f: A -> B = {}

How does this f satisfy the first criterion, if A is uninhabited? It feels like this function can't be invoked. Am I thinking too much in terms of types here?

I mean, yes, there are a lot of things that are often omitted in mathematical writing and it's up to the reader to infer them (that's "mathematical maturity"). When textbooks discuss intervals, such as [a,b] for example, should the author specify the interval is nondegenerate/nonempty each time? That is, should we repeatedly see "a<b" as part of the hypothesis? Degenerate cases are often not the primary interest of the particular area or theorem you're studying. We don't usually care about functions with empty or singleton domains. And, yes, you could say a lot of results are technically false due to those degenerate/trivial cases. But usually it just means the author didn't want to clutter their writing, or it's not significant to the rest of the theory.

The post proposes a counterexample of a function with a empty domain A. Some authors do actually specify that the domain should be nonempty in this theorem. This is a common result. Others authors don't. It's not a huge deal.