Does the splitting lemma hold without the axiom of choice? In part of the proof of the splitting lemma (a left-split short exact sequence of abelian groups is right-split) it seems necessary to invoke the axiom of choice. That is, if $0\to A\overset{f}{\to} B\overset{g}{\to} C\to 0$ is exact and there is a retraction $B\overset{r}{\to}A$, then we can find a section $C\overset{s}{\to}B$ by choosing any right inverse of $g$ and removing the part in the kernel of $f$, which gives a well-defined morphism independent of the choice.
Is this invocation of the axiom of choice essential? I thought I had an example that showed it was: $0\to\mathbb{Q}\to\mathbb{R}\to\mathbb{R}/\mathbb{Q}\to0$ splits on the right if you can choose a basis for $\mathbb{R}$ as a vector space over $\mathbb{Q}$. But actually now I think it doesn't split on the left without a basis either.
The map $C\to B$ is supposed to be a canonical injection map. Can something be "canonical" if it requires choice?
 A: There's no choice involved in the following argument showing that $f$ has a left inverse (if and) only if $g$ has a right inverse:
Consider the morphism $h = 1_B-fr\colon B \to B$. Then $hf = f -frf = 0$, so $h$ factors as $h = sg$ for a unique morphism $s\colon C \to B$ (note that $s(b+A) = h(b)$ is well-defined as a map $s: B/A \to B$). Now $gsg = gh =g-gfr = g = 1_C g$, so $gs = 1_C$ because $g$ is onto, so $s$ is a section of $g$.

We also have $frsg = frh = fr-frfr = 0$, so $frs = 0$ because $g$ is onto, so $rs = 0$ because $f$ is injective and by construction of $s$ we have $fr + sg = fr + h = 1_B$. In particular, we have an isomorphism 
$$
\begin{bmatrix} f & s \end{bmatrix}\colon A \oplus C \longleftrightarrow {B :} \begin{bmatrix} r \\ g \end{bmatrix}.
$$
Note that $s$ is uniquely determined by $r$ and similarly one shows that if $s$ is a right inverse of $g$ then there is a uniquely determined right inverse $r$ of $g$ such that $fr = 1-sg$.

Concerning the existence of a retraction of the inclusion $\mathbb{Q} \to \mathbb{R}$: assuming such a retraction exists, the previous part gives us a section $s\colon\mathbb{R/Q} \to \mathbb{R}$ of $g\colon \mathbb{R} \to \mathbb{R/Q}$. Modifiying this section by setting $t(x) = s(x) - \lfloor s(x) \rfloor$, we get a Vitali set $t(\mathbb{R}/\mathbb{Q}) \subset [0,1]$, whose existence we cannot prove from ZF alone, so we cannot prove from ZF that there is a left inverse of the inclusion $\mathbb{Q} \to \mathbb{R}$.

A simple example of something “canonical” that requires choice in order to be non-trivial would be a product of an arbitrary collection of sets. 
My naïve way of thinking of the axiom of choice is that it is first and foremost an axiom ensuring the existence of things. In my experience it is quite often the case that things can be defined and shown to be unique (hence “canonical”) if they exist (or non-uniqueness is controlled in some tractable way), but their existence requires additional assumptions.
