Injection iff Left Inverse/Proof 1

Theorem

A mapping $f: S \to T, S \ne \O$ is an injection if and only if:

$\exists g: T \to S: g \circ f = I_S$

where $g$ is a mapping.

That is, if and only if $f$ has a left inverse.

Proof

Let:

$\exists g: T \to S: g \circ f = I_S$

From Identity Mapping is Injection, $I_S$ is injective, so $g \circ f$ is injective.

So from Injection if Composite is Injection, $f$ is an injection.

Note that the existence of such a $g$ requires that $S \ne \varnothing$.

$\Box$

Now, assume $f$ is an injection.

We now define a mapping $g: T \to S$ as follows.

As $S \ne \O$, we choose $x_0 \in S$.

By definition of injection:

$f^{-1} {\restriction_{\Img f} } \to S$ is a mapping

so it is possible to define:

$\map g y = \begin{cases} x_0: & y \in T \setminus \Img f \\ \map {f^{-1} } y: & y \in \Img f \end{cases}$

So, for all $x \in S$:

$\map {g \circ f} x = \map g {\map f x}$

is the unique element of $S$ which $f$ maps to $\map f x$.

This unique element is $x$.

Thus $g \circ f = I_S$.

$\blacksquare$

Law of the Excluded Middle

This theorem depends on the Law of the Excluded Middle, by way of Where?.

This is one of the axioms of logic that was determined by Aristotle, and forms part of the backbone of classical (Aristotelian) logic.

However, the intuitionist school rejects the Law of the Excluded Middle as a valid logical axiom. This in turn invalidates this theorem from an intuitionistic perspective.

Remarks

Notice that it does not matter what the elements of $T \setminus \Img f$ are — using the construction given, the equation $g \circ f = I_S$ holds whatever value (or values) we choose for $g \sqbrk {T \setminus \Img f}$. The left-over elements of $T$ we can map how we wish and they will not affect the final destination of any $x \in S$ under the mapping $g \circ f$.