ES version is available. Content is displayed in original English for accuracy.
Advertisement
Advertisement
⚡ Community Insights
Discussion Sentiment
62% Positive
Analyzed from 1113 words in the discussion.
Trending Topics
#function#empty#left#true#inverse#case#definitions#anything#set#functions
Discussion (26 Comments)Read Original on HackerNews
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.
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
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.
The problem here is that "forall a in A, g(f(a)) = a" ought to hold vacuously since a has no elements, but the definitions don't allow you to write down a g at all so you can't use the vacuousness in the first place.
I think the better fix is to change definitions to allow g = { (1, {}) } to be regarded as a left-inverse to g. So we would say that left-inverses need to be partial functions, rather than full functions. The definition still requires they be defined on the im f , but no choices have to be made on the complement of the image. I'm sure this breaks some other definitions but it seems intuitively correct to me.
This is kinda nice also because it means that for e.g. the function (a,b) -> (1, 2) given by f(a) = 1, f(b) = 1, you don't need its left inverse to specify that g(2) = a or b, but instead you can have g(2) = {} which doesn't require making any non-canonical choices.
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."
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).
I believe it doesn't make any difference to any meaningful result. It merely makes it easier to write theorems without specifying exceptions.
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).
The point is you either send an element of the codomain to its (unique by injectivity) preimage if it's in the image, or to an arbitrary element of A if it's not, and that's a left inverse. But then if B has an element, A needs one for you to pick your arbitrary target.
In a sense, your claim that the problem is a smaller domain than codomain does contribute though; if f is also surjective, then this case can't happen, so bijective iff invertible (the empty function is vacuously bijective and its own inverse).
In other words, the statement "for every x in {} it holds that <anything>" is always true.
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.
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 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?
LOL