Finding a bug in Dummit and Foote's Abstract Algebra
1–10 of 39 posts
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#2It 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.
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#3It 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.
WIP, but that is the target ethos in the prover I'm building:
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
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#4This 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.
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#5I 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
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#6I don’t think it’s fair to call {}-> injective just because no two inputs map to the same output. That’s vacuous.
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#7Help 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?
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#8I don’t think it’s fair to call {}-> injective just because no two inputs map to the same output. That’s vacuous.
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.
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#9Help 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?
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.
Re: Finding a bug in Dummit and Foote's Abstract Algebra
#10I don’t think it’s fair to call {}-> injective just because no two inputs map to the same output. That’s vacuous.
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 " is always true.