LeftInverse and RightInverse

Stream: mathlib4

[Violeta Hernández]

Why have both? LeftInverse f g is exactly the same as RightInverse g f.

docs#Function.LeftInverse docs#Function.RightInverse

[Miyahara Kō]

These defs are made in 2016, before Mathlib was curved out as math library from Lean.
https://github.com/leanprover-community/lean/commit/93692d01af6ee90051a47f9912953b2ee73a50b8

[Jovan Gerbscheid]

Do we need any of them? We could write f ∘ g = id?

[Miyahara Kō]

Personally, I think it is useful to have at least one of them. These propositions are mainly convenient for proving surjectivity or injectivity, and they can be used via dot notation, which is quite helpful.

[Yaël Dillies]

But in my experience you in fact never have a LeftInverse assumption lying around, meaning that actually docs#Function.RightInverse.surjective should be renamed to Function.Surjective.of_rightInverse so as to leverage anonymous dot notation on Function.Surjective. At this point, one could indeed get rid of Function.RightInverse

[Miyahara Kō]

Indeed, when actually carrying out proofs, assumptions or conclusions of the form ∀ x, f (g x) = x appear much more often. However, this is just my personal view, but from the perspective of theorem searchability, I think it is better to introduce definitions for important properties, even if they can be written in a very simple form.

A representative example is Function.IsFixedPt. Although this is a very simple definition that could be written directly as f x = x, explicitly rewriting it as Function.IsFixedPt and placing it as an assumption of a theorem makes it much easier to find relevant results via Loogle when results from dynamical systems are needed.

That said, even I think that Function.LeftInverse and Function.RightInverse should be unified, and I honestly wonder why Function.HasLeftInverse and Function.HasRightInverse are still in Mathlib at this point :sweat_smile:

[Violeta Hernández]

I'm not sure how I feel about IsFixedPt either. If not for perhaps discoverability, this feels like a wrapper that's too simple for its own good. But that can be another thread.

[Yaël Dillies]

At least in IsFixedPt there is a variable that appears twice in the body: IsFixedPt f x := f x = x vs LeftInverse f g := f ∘ g = id.

[Violeta Hernández]

I think we could try out the Surjective.of_rightInverse/Injective.of_leftInverse design you mention. I suspect this would get rid of 95% of uses of these predicates, and then we can figure out the other 5%.

[Eric Wieser]

I think at least one of them is worth keeping, since it saves you having to decide whether to quantify your inverse property or state it as an equality of functions.

[Aaron Liu]

we could merge them

[Aaron Liu]

which one has the better argument order

[Eric Wieser]

I think the argument for having both is that LeftInverse g as a predicate implies Injective and similarly for RightInverse g and Surjective; that is, each has a "main" argument

[Eric Wieser]

I'm not sure this is necessarily a good design, but I do think it is intentional

[Violeta Hernández]

I can never remember which one is which.

[Eric Wieser]

Renaming to f.IsRightInvOf g would help

[Eric Wieser]

Dot notation didn't work on functions way back when these were defined