Link Search Menu Expand Document

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.

structure LeftInverse (f : α  β) where 
  to_fun : β  α  
  invl : to_fun  f = id 

def TheFun (g : LeftInverse f) : β  α := g.to_fun 
example : g.to_fun  f = id := g.invl

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

def IdInv : LeftInverse (@id α) := id,by rfl 

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

def HasLeftInv (f : α  β) : Prop := Nonempty (LeftInverse f) 

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.

theorem has_left_inv_injective (f : α  β) (h : HasLeftInv f) : Injective f := by 
  -- Introduce a pair of arguments and the assumption that 
  -- f evaluates to the same on them 
  intro (a:α) (a:α) (l: f a = f a)
  -- Break up the existence of a left-inverse into a function and a proof it is a
  -- left inverse
  have g,l := h 
  -- A calculation block allows us to more efficiently perform equality manipulations
    a = id a        := by rfl -- these reduce to an equality 
    _  = (g  f) a   := Eq.symm (congrFun l a) -- we apply equal functions 
    _  = (g  f) a   := congrArg g l -- we apply a function to equal arguments
    _  = id a        := congrFun l a -- we apply equal functions to same value again
    _  = a           := by rfl -- done

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.

theorem left_inv_right_inv_eq { f : α  β } (g : LeftInverse f) (h : RightInverse f) : 
  g.to_fun = h.to_fun := by
    apply funext 
    intro (b: β) 
        g.to_fun b = g.to_fun (f (h.to_fun b))  := 
          congrArg g.to_fun (Eq.symm (congrFun h.invr b)) 
        _    = h.to_fun b                       := 
          congrFun g.invl (h.to_fun b)  

theorem inv_unique (f : α  β) (g : Inverse f) (h : Inverse f) : 
  g.to_fun = h.to_fun := by 
      g.to_fun = (InvtoLeftInv g).to_fun    := by rfl  
      _        = (InvtoRightInv h).to_fun   := 
        left_inv_right_inv_eq (InvtoLeftInv g) (InvtoRightInv h)   
      _        = h.to_fun                   := by rfl 

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.

-- this definition constructs the g in the proof above. It is marked noncomputable 
-- because Lean cannot make a computer program out of it 
noncomputable def Section (f : α  β) (l : Nonempty α) : β  α := by 
  intro (b:β)
  have a : α := Classical.choice l 
  -- propDecicable tells Lean is ok that that we may not actually be able check 
  -- using a computer program the condition in the following if, then statement 
  have : Decidable ( a, f a = b) := Classical.propDecidable ( a, f a = b) 
  exact if h :  a, f a = b then Classical.choose h else a 

theorem inj_has_left_inv (f : α  β) (l : Nonempty α) (h : Injective f) : HasLeftInv f := by 
  -- let is like have except it allows for better computation
  let g : β  α := Section f l 
  -- suffices changes the goal to u and shows we can close if we have u using ⟨g,u⟩
  suffices u : g  f = id from g,u
  apply funext 
  intro (a:α) 
  -- exists is a helper technique for establishing existential statements 
  have (v :  x, f x = f a) := by exists a 
  -- dif_pos is a helper result that says the result of the if, then is what we expect 
  -- when the if condition is true
  have (w : g (f a) = Classical.choose v) := dif_pos v   
    g (f a) = Classical.choose v  := w 
    _       = a                   := h (Classical.choose_spec v)