5 ms·

Finding a bug in Dummit and Foote's Abstract Algebra

83 points by evakhoury 13d ago

Paracompact 10d 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.
- dnautics 9d ago
  WIP, but that is the target ethos in the prover I'm building: https://github.com/ityonemo/bpa https://github.com/ityonemo/bpa Its painfully verbose and explicit but its designed to let you cut down to the structure of the proof with a query language
- IngoBlechschmid 9d ago
  I agree! Martín Escardó never tires to say that he uses the Agda proof assistant in exactly this sense, as a kind of interactive blackboard for taking notes and structuring his thoughts. The vast TypeTopology repository is the result of years of following this philosophy: https://github.com/martinescardo/TypeTopology https://github.com/martinescardo/TypeTopology
generationP 9d ago
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.
- ndriscoll 9d ago
  I ran into this same thing formalizing some of my old notes in Lean a few days ago. The tricky thing I suppose is that 0. Injectivity and A non-empty or B empty implies left invertibility, 1. Left invertibility implies injectivity. 2. Surjectivity iff right invertibility, and 3. Surjectivity rules out this corner case, so bijectivity iff invertibility. So this one vacuous case just throws a wrench in what is "supposed" to be true.
shmoil 9d ago
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
- mitxela 9d ago
  Was the proof correct?
  - voxl 9d ago
    No you see people that use AI generally don't bother to consider this unimportant detail. Or they ask the AI to "double check" its work.
    - 9864325789976 9d ago
      You forgot to include empirical evidence of your claim, since I'd like to double check it.
    - shmoil 8d ago
      Nah, I tried to post a long reply yesterday, but YC was glitching, so I just gave up.
hyperhello 9d ago
I don’t think it’s fair to call {}-> injective just because no two inputs map to the same output. That’s vacuous.
- BeetleB 9d ago
  Generally mathematicians treat vacuous statements as true. I believe it doesn't make any difference to any meaningful result. It merely makes it easier to write theorems without specifying exceptions.
- tim-kt 9d ago
  It's true precisely because it's vacuous. If you quantify over the empty set, anything is true. In other words, the statement "for every x in {} it holds that <anything>" is always true.
  - layer8 9d ago
    What can be confusing is that the statement "for every x in {}, it doesn’t hold that <anything>" is always true as well.
    - tim-kt 9d ago
      I mean, yes. But "it doesn't hold that <anything>" is equivalent to "it holds that <not anything>" and since not anything is also anything... Ah, I see.
- gpm 9d ago
  Edit: Removed incorrect claim that |B| > |A| sufficed for the counter example. It's also the definitions the book supplies though (and the standard ones). Mathematics works over definitions. Everyone is free to do math over whatever definitions they want - but what is or isn't true follows from them. Lots of definitions and theorems exclude things like empty-set cases because they're weird, but that has to be explicit (otherwise someone will apply a theorem to the empty set and it will lead them to incorrect conclusions).
psYchotic 9d ago
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?
- changoplatanero 9d ago
  When there are no pairs, its certainly true that the first element of each pair comes from A. Just like if there are no living dinosaurs its true that all living dinosaurs speak English.
  - psYchotic 9d ago
    That helps. Thank you! I was trying to come up with something to explain why I couldn't see it myself: every element of an empty set of integers is both even and odd. This feels counterintuitive to me, until I flip it around into a question: what is the set of all integers that are both even and odd?
    - mitxela 9d ago
      Neat trick
    - jibal 9d ago
      Well done. Finding a way to look at things so that results that seemed unintuitive seem intuitive can be powerful and satisfying.
zero-sharp 9d ago
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.
troethe 9d ago
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.
- ndriscoll 9d ago
  That's basically saying you'll just take all functions to be surjective though, and it's stronger than you really need; the non-surjective case works fine for non-empty A. You could of course interpret some of these basic theorems as saying "well I'd might as well take my function to be surjective since the 'meat' is that case." Much like you could just take all functions to be injective by modding out the kernel since that's the real "meat." And indeed one might interpret the first isomorphism theorem as saying exactly those two things: the isomorphism A/ker f = im f is "the real substance of the map f."
  - troethe 9d ago
    No, f can still map to `B` and does not need to be surjective. We just loosened the definition of `g` a little in a way that doesn't matter.
    - ndriscoll 9d ago
      But f's codomain is B, and g isn't a function on B, so you can't compose them in the first place. And saying "well yeah but you could compose f's restriction" is exactly making f surjective. The basic result here is every function factors as a surjection (collapsing to the quotient) followed by an isomorphism (with the image) followed by an injection (enlarging the codomain). The surjection and injection are "trivial" and the isomorphism is the part that "does something" (permuting your thing somehow).
jonlong 9d ago
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!
deleted 9d ago
[deleted]

83 points by evakhoury 13d 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.

dnautics 9d ago
WIP, but that is the target ethos in the prover I'm building: https://github.com/ityonemo/bpa https://github.com/ityonemo/bpa Its painfully verbose and explicit but its designed to let you cut down to the structure of the proof with a query language
IngoBlechschmid 9d ago
I agree! Martín Escardó never tires to say that he uses the Agda proof assistant in exactly this sense, as a kind of interactive blackboard for taking notes and structuring his thoughts. The vast TypeTopology repository is the result of years of following this philosophy: https://github.com/martinescardo/TypeTopology https://github.com/martinescardo/TypeTopology

generationP 9d ago

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.

ndriscoll 9d ago
I ran into this same thing formalizing some of my old notes in Lean a few days ago. The tricky thing I suppose is that 0. Injectivity and A non-empty or B empty implies left invertibility, 1. Left invertibility implies injectivity. 2. Surjectivity iff right invertibility, and 3. Surjectivity rules out this corner case, so bijectivity iff invertibility. So this one vacuous case just throws a wrench in what is "supposed" to be true.

shmoil 9d ago

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

mitxela 9d ago
Was the proof correct?
- voxl 9d ago
  No you see people that use AI generally don't bother to consider this unimportant detail. Or they ask the AI to "double check" its work.
  - 9864325789976 9d ago
    You forgot to include empirical evidence of your claim, since I'd like to double check it.
  - shmoil 8d ago
    Nah, I tried to post a long reply yesterday, but YC was glitching, so I just gave up.

hyperhello 9d ago

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

BeetleB 9d ago
Generally mathematicians treat vacuous statements as true. I believe it doesn't make any difference to any meaningful result. It merely makes it easier to write theorems without specifying exceptions.
tim-kt 9d ago
It's true precisely because it's vacuous. If you quantify over the empty set, anything is true. In other words, the statement "for every x in {} it holds that <anything>" is always true.
- layer8 9d ago
  What can be confusing is that the statement "for every x in {}, it doesn’t hold that <anything>" is always true as well.
  - tim-kt 9d ago
    I mean, yes. But "it doesn't hold that <anything>" is equivalent to "it holds that <not anything>" and since not anything is also anything... Ah, I see.
gpm 9d ago
Edit: Removed incorrect claim that |B| > |A| sufficed for the counter example. It's also the definitions the book supplies though (and the standard ones). Mathematics works over definitions. Everyone is free to do math over whatever definitions they want - but what is or isn't true follows from them. Lots of definitions and theorems exclude things like empty-set cases because they're weird, but that has to be explicit (otherwise someone will apply a theorem to the empty set and it will lead them to incorrect conclusions).

psYchotic 9d ago

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?

changoplatanero 9d ago
When there are no pairs, its certainly true that the first element of each pair comes from A. Just like if there are no living dinosaurs its true that all living dinosaurs speak English.
- psYchotic 9d ago
  That helps. Thank you! I was trying to come up with something to explain why I couldn't see it myself: every element of an empty set of integers is both even and odd. This feels counterintuitive to me, until I flip it around into a question: what is the set of all integers that are both even and odd?
  - mitxela 9d ago
    Neat trick
  - jibal 9d ago
    Well done. Finding a way to look at things so that results that seemed unintuitive seem intuitive can be powerful and satisfying.

zero-sharp 9d ago

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.

troethe 9d ago

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.

ndriscoll 9d ago
That's basically saying you'll just take all functions to be surjective though, and it's stronger than you really need; the non-surjective case works fine for non-empty A. You could of course interpret some of these basic theorems as saying "well I'd might as well take my function to be surjective since the 'meat' is that case." Much like you could just take all functions to be injective by modding out the kernel since that's the real "meat." And indeed one might interpret the first isomorphism theorem as saying exactly those two things: the isomorphism A/ker f = im f is "the real substance of the map f."
- troethe 9d ago
  No, f can still map to `B` and does not need to be surjective. We just loosened the definition of `g` a little in a way that doesn't matter.
  - ndriscoll 9d ago
    But f's codomain is B, and g isn't a function on B, so you can't compose them in the first place. And saying "well yeah but you could compose f's restriction" is exactly making f surjective. The basic result here is every function factors as a surjection (collapsing to the quotient) followed by an isomorphism (with the image) followed by an injection (enlarging the codomain). The surjection and injection are "trivial" and the isomorphism is the part that "does something" (permuting your thing somehow).

jonlong 9d ago

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!

deleted 9d ago

[deleted]