Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Finding a bug in Dummit and Foote's Abstract Algebra

kallus.org

Post reply on HN
Print view View original

31–39 of 39 posts

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#31

Post by ajkjk »

troethe wrote: post #28
ajkjk wrote: post #27

Earlier quoted context omitted.

I think a slightly better fix is to change definitions to allow g = { (1, {}) } to be regarded as a left-inverse to g, that is, to allow left-inverses to be partial functions, rather than full functions. The definition still requires they be defined on the image of f, but no choices have to be made on the complement of the image. Probably this breaks some other definitions but it seems intuitively correct to me. It k…

> your fix kinda breaks a lot of the structure of algebra in other ways What are you referring to here in particular? I think the property of `g` to be a well defined function is a lot more important than for its domain to be `B`, when `f(A)` is enough to make the composition well defined.

sorry I edited my comment because I wasn't quite sure what I meant by that either. I am too sleepy.

But, I disagree. partial functions B->A are just a superset of functions B->A, so requiring g to be partial is just relaxing a requirement. Whereas requiring g: im(A)->A adds an additional restriction, potentially breaking any place that concept of a left inverse is used. Invariably someone will just define a new thing equivalent to what is normally called the left inverse because they still need the concept for some reason.

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#32

Post by jonlong »

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!

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#33

Post by troethe »

ndriscoll wrote: post #30
troethe wrote: post #23

Earlier quoted context omitted.

Of course I can compose `f: A -> B` and `g: f(A) -> A`. The composition maps a `x` from `A` to `g(f(x))` which is well defined. Therefore the composition is a function. `g` and `f` aren't functions in a programming language and `A` and `B` are not types. There is nothing like a type checker forbidding you from composing `f: A -> B` and `g: f(A) -> A`.

I suppose, but then your definition of composition requires checking compatibility of codomain/domain instead of it being automatic (and your definition of composition does not fit the shape to form a category), which seems way worse than stipulating f non-empty for some theorem that isn't even true for other categories either. And for e.g. for vector spaces or modules over semisimple rings they're actually the same…

I think we can sit here and speculate which properties of left inverses are actually important for quite a while.

But we will only ever get a real answer to this question, when the original poster finishes formalizing the whole book and can tell us which weakenings break further proofs in the books and which won't.

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#34

Post by voxl »

mitxela wrote: post #26
shmoil wrote: post #5

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

Was the proof correct?

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.

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#35

Post by jibal »

psYchotic wrote: post #15
changoplatanero wrote: post #9

Earlier quoted context omitted.

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.

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?

Well done. Finding a way to look at things so that results that seemed unintuitive seem intuitive can be powerful and satisfying.

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#37

Post by 9864325789976 »

voxl wrote: post #34
mitxela wrote: post #26

Earlier quoted context omitted.

Was the proof correct?

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.

You forgot to include empirical evidence of your claim, since I'd like to double check it.

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#38

Post by IngoBlechschmid »

Paracompact wrote: post #2

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.

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

Re: Finding a bug in Dummit and Foote's Abstract Algebra

#39

Post by shmoil »

voxl wrote: post #34
mitxela wrote: post #26

Earlier quoted context omitted.

Was the proof correct?

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.

Nah, I tried to post a long reply yesterday, but YC was glitching, so I just gave up.
Post reply on HN