## Hitting the undo button

A natural question to ask about a process is whether it can be undone. We can ask the same about a function.

**Definition**. A *left inverse* to a function $f: A \to B$ is a function $g : B \to A$ such that $g \circ f = \operatorname{id}_A$. Here $\operatorname{id}_A$ is the identity function on $A$ so this can rewritten as $g(f(a)) = a$ for all $a$.

To define a left inverse in Lean, we confront an new problem: we really need to pieces of mathematical data: for the function $g : B \to A$ and then the proof that $g \circ f = \operatorname{id}$. We can bundle those two things together into a single `structure`

.

Given a `(g : LeftInverse f)`

, we can access the function `β → α`

as `g.to_fun`

and the proof that `g.to_fun ∘ f = id`

using `g.invl`

. To construct a `LeftInverse`

, we need to supply both pieces of data

It also helpful to define single proposition which is true if $f$ has a left inverse.

Here `Nonempty α`

is proposition that states there is actually some term of type `α`

.

**Definition**. A *right inverse* to $f$ is a function $h : B \to A$ such that $f \circ h = \operatorname{id}_B$. Of course, if $h$ is a right inverse for $f$, then $f$ is also a left inverse for $h$.

**Definition**. An *inverse* to $f$ is a function that is simultaneously a left and right inverse to $f$.

Possession of inverses and injectivity/surjective are tied closely together.

**Theorem**. If $f$ has a left inverse, then $f$ is injective.

## **Proof**. (Expand to view)

Assume we have $a_1,a_2$ with $f(a_1) = f(a_2)$ and let $g$ be a left-inverse of $f$. Then, we can apply $g$ to both sides of the equality $f(a_1) = f(a_2)$ to get $$ a_1 = g(f(a_1)) = g(f(a_2)) = a_2 $$ and see that $f$ is injective. ■

Here is a proof in Lean.

Similarly, if we have right inverse, then we are surjective. As a corollary, we get the following statement.

**Corollary**. If $f$ has both a right and left inverse, then $f$ is a bijection.

In fact if $f$ has both a left and right inverse, then they have to be equal.

## More nonconstructive tools

We saw about that if $f$ has a left inverse, then it is injective. The converse is also true allowing for new nonconstructive tools.

**Theorem**. Suppose $f: A \to B$ is injective and $A$ is nonempty. Then $f$ has a left inverse.

## **Proof**. (Expand to view)

We first make our candidate left inverse function $g: B \to A$. Pick some $b$ from $B$. The idea is to split the definition of $g(b)$ into two cases depending on whether there exists some $a$ with $f(a) = b$ or not. To do so, we know that $A$ is nonempty so we can pick some junk value $a_0$ for use. Then, we "define" $g$ as $$ g(b) = \begin{cases} a &\text{where $a$ is \textit{some} value satisfying $f(a) = b$} \\ a_0 &\text{if there is no such solution to $f(a) = b$} \end{cases} $$ Nothing so far depended on the assumption that $f$ is injective. But we haven't checked that $g$ is, in fact, a left inverse. From the definition, we know that $g(f(a)) = a'$ where $a'$ is some value satisfying $f(a') = f(a)$. Since $f$ is injective, we can conclude that $a = a'$ and that we indeed have a left inverse. ■

So why the quotes around “define” there. It seems reasonable to assume we can pick a value from a nonempty set for each value $b$ where there is one. But this is not a consequence in set theory and requires additional axiom: the Axiom of Choice.

Let’s see what this looks like in Lean where we see the use of choice.