# “Abstract nonsense” proof of the splitting lemma

As remarked in the "talk" part of the wikipedia article, the proof is done with elements of a set and functions. I guess it's possible to carry it out purely with "objects" and "arrows"

Who volonteers to do that?

Edit: If possible without that Freyd embedding thm mentionned in the talk.

-
Why don't you take a crack at it? –  Ian Coley Apr 10 '14 at 19:48
The obvious part is that a biproduct implies that the short exact sequence splits on the right and on the left. For the converse, the fact that the short exact sequence splits on either side with give a diagram that looks pretty much like either a product or a coproduct, here is where I am –  user39158 Apr 10 '14 at 19:54
This is proposition 1.8.7 in Borceux's Handbook of Categorical Algebra, Vol II - Categories and Structures. –  Exterior Jan 7 at 19:53

Notations: The short exact sequence splits on the left

$$0 \longrightarrow A \underset{\underset{\phi}{\longleftarrow}}{\overset{f}{\longrightarrow}} B \overset{g}{\longrightarrow} C \longrightarrow 0 \quad, \quad \phi\circ f =\mathrm{id}_A$$

Want to show that $B \cong A\oplus C$

$\underline{1)}$ $\ P:= f\circ \phi$ is an idempotent ($P\circ P=P$)

In an abelian category, any arrow has a kernel and a cokernel (hence also image and coimage) so $P$ splits into $B \overset{j_P}{\longrightarrow} \mathrm{Im}(P) \overset{i_P}{\longrightarrow} B$ ( recall def. of image, epi mono factorization in an abelian category)

With this two observations (in partic. $j_P$ epi, $i_P$ mono), one can show that $j_P$ is actually a left inverse of $i_P$ and that $j_P\circ f$ is actually an isomorphism $A \cong \mathrm{Im}(P)$

$\underline{2)}$ An abelian category has hom set that are abelian groups, e.g. $(\mathrm{Hom}(B,B),+)$ is an abelian group, hence it makes sense to define $Q := \mathrm{id}_B -P$

As previously $Q$ factorizes as $Q=i_Q \circ j_Q$ and one checks that $$j_P\circ i_Q = 0 \quad ,\quad j_Q \circ i_P = 0$$

$\underline{3)}$ The two maps $\ i_P: \mathrm{Im}(P)\rightarrow B\ ,\ i_Q: \mathrm{Im}(Q)\rightarrow B$ define by the universal property of the coproduct a map $\Phi: \mathrm{Im}(P)\coprod \mathrm{Im}(Q) \rightarrow B$ (this could also be written $i_P+i_Q$, + symbolically if we were not in an abelian category )

and the two maps $j_P : B \rightarrow \mathrm{Im}(P)\ ,\ j_Q : B \rightarrow \mathrm{Im}(Q)$ a map $\Psi: B\rightarrow \mathrm{Im}(P)\prod \mathrm{Im}(Q)$

Using $j_{P/Q}\circ i_{P/Q} = \mathrm{id}_{\mathrm{Im}(P/Q)}$ and the equalities in $\underline{2)}$ (and also with the def. biproduct) one checks the isomorphism $B\cong \mathrm{Im}(P)\oplus \mathrm{Im}(Q)$, or $$\Phi\circ \Psi =P+Q = \mathrm{id}_B\quad \text{and} \quad \Psi\circ \Phi =\mathrm{id}_{\mathrm{Im}(P)\oplus\mathrm{Im}(Q)}$$

-