Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- 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
by shmoil - 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?
by psYchotic - I don’t think it’s fair to call {}-> injective just because no two inputs map to the same output. That’s vacuous.by hyperhello
- 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!
by jonlong - 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.
by troethe - 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.
by Paracompact - 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.by generationP