Stream: Beginner Questions

Topic: Inverse of bijective function


view this post on Zulip Nicolò Cavalleri (Jun 23 2021 at 23:32):

Suppose I have a lemma proving that a given function is bijective. How do I define the inverse function? In my real life problem I actually have a function f which satisfies bij_betw f UNIV (S :: 'b set) and I need to build a function 'b => 'a such that it is the inverse if f on S. Can I do this?

view this post on Zulip Jakub Kądziołka (Jun 23 2021 at 23:34):

see the_inv_into

view this post on Zulip Nicolò Cavalleri (Jun 24 2021 at 12:13):

Thank you! I am puzzled though: how does that definition work? If f is not surjective the inverse is not unique, and f is never assumed surjective, so how does THE work? My guess is that it uses some very powerful axiom of choice...

view this post on Zulip Jakub Kądziołka (Jun 24 2021 at 12:50):

THE is a variation on Hilbert's epsilon operator, which is present in Isabelle as SOME. SOME indeed corresponds to the axiom of choice, and is defined as follows: if EX x. P x, then SOME returns some x that has the property, otherwise an arbitrary x from your type. THE additionally requires that there is exactly one x st. P x, which, means the happy case doesn't require AC, as it corresponds to a function {x} \mapsto x, which should be constructible in ZF? Though, the case where ALL x. P x = False corresponds to undefined :: 'a, and I'm not sure whether that's AC or not...

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:02):

THE is the unique choice operator, and its existence is actually "weaker" than that of the existence of the SOME operator (non-unique choice). But I'll leave the precise explanation of what that means to people who actually know something about logic (in contrast to me).

view this post on Zulip Nicolò Cavalleri (Jun 24 2021 at 19:03):

Bu my point is precisely that if the function is not surjective the inverse is not unique! In fact I was very surprised to see a THE there

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:06):

In that case you just get some unspecified value that you can prove nothing about (cf. undefined).

view this post on Zulip Nicolò Cavalleri (Jun 24 2021 at 19:06):

You mean in the case the function is not surjetive?

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:07):

HOL cannot prevent you from writing down "nonsense". There are a number of terms that are "nonsensical" in some sense, e.g. 1 / 0. Some of them have some halfway sensible dummy values like 1 / 0 = 0, others are just unspecified (e.g. ln (-1 :: real) or THE x. False).

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:10):

Nicolò Cavalleri said:

You mean in the case the function is not surjetive?

The way the_inv_into is defined, the_inv_into A f y is the unique value x such that x ∈ A and f(x) = y if such a unique value exists; otherwise you get "nonsense".

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:11):

If the function is not injective and surjective, there will be some values y where the_inv_into A f y will be "nonsense" (i.e. unspecified). It might still work for other values of y though if the choice is unique.

view this post on Zulip Nicolò Cavalleri (Jun 24 2021 at 19:11):

But then what if I have an injective function of which I want a right inverse? Isn't there a theory of inverse functions that makes use of SOME? In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:11):

For instance, if f(x)=x2f(x) = x^2, then the_inv_into UNIV f 0 = 0. For anything other than 0, it's unspecified.

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:12):

Nicolò Cavalleri said:

But then what if I have an injective function of which I want a right inverse? Isn't there a theory of inverse functions that makes use of SOME? In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

Yes, there is inv_into. Frankly I've never used the_inv_into; I didn't even know it existed.

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:12):

I don't think there is any reason to ever use the_inv_into over inv_into.

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:13):

inv_into also works if the value is not unique, it's enough for the preimage to be nonempty.

view this post on Zulip Nicolò Cavalleri (Jun 24 2021 at 19:13):

Oh great then I was looking for inv_into I guess!

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:13):

Nicolò Cavalleri said:

In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

Do you have any examples?

view this post on Zulip Nicolò Cavalleri (Jun 24 2021 at 19:13):

Manuel Eberl said:

I don't think there is any reason to ever use the_inv_into over inv_into.

Yep I don't see it either!

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:13):

I guess surjectivity is generally an unnecessarily strong assumption.

view this post on Zulip Manuel Eberl (Jun 24 2021 at 19:14):

It's enough for the specific values you're plugging into the the_inv_into to be in the image of A under f, i.e. in f`A.


Last updated: Sep 25 2021 at 09:17 UTC