# Prove that a function $f : X \mapsto X$ is injective if and only if it has a left inverse.

Prove that a function $f : X \mapsto X$ is injective if and only if it has a left inverse.

Can someone help me with this? What I've done is form predicates of the form $LI(f) \Rightarrow INJ(f)$ to begin step-by-step.

I understand the left hand side will be quantified to $\exists f,g: X \mapsto X: g \circ f = id_X$. Am I in the right direction here? Or am I missing something more that should be quantified? I know the following:

1. the identity function, $id_X: X \mapsto X$, is defined by $\forall x \in X, id_X(x)=x$.
2. A function $g \in \mathcal{F}$ is called a left inverse of a function $f \in \mathcal{F}$ if $g \circ f =id_X$.
• The full quantification would be: $\forall f:X\to X, ((\forall x, y\in X, f(x) = f(y) \rightarrow x = y) \leftrightarrow (\exists g:X\to X, g \circ f = \mathrm{id}_X))$. – Daniel Schepler Jun 6 '17 at 22:33
• @DanielSchepler What if we're doing it the other way around? Can we switch the statements then, obviously keeping/using $f$ and $g$ as required? – Yahya Farooq Jun 6 '17 at 22:37
• It's unclear what you're asking. What do you mean by "doing it the other way around"? – Daniel Schepler Jun 6 '17 at 22:40
• I mean, can it be expressed as $\forall X \mapsto X: g \circ f = id_X \Leftrightarrow \exists g: X \mapsto X,(\forall x,y \in X, f(x)=f(y) \Rightarrow x=y)$? – Yahya Farooq Jun 6 '17 at 22:43
• That formula doesn't really make sense because the first occurrence of $g$ isn't bound by any quantifier. – Daniel Schepler Jun 6 '17 at 22:47

First create a helper relation $g' = \{ ( f(x), x ) : x \in X \}$ . This relation is a (partial) function due to the injective property ensuring that for every element in the domain there is at most one image.
Then you can construct $g(x) = \begin{cases} g'(x) & \text{when } g'(x) \text{ is defined} \\ x & \text{otherwise} \end{cases}$
Which is a left inverse. You can show the converse by making use of the fact that for all functions $x = y \rightarrow g(x) = g(y)$