For the record, the axiom of choice is not required to prove the splitting lemma. I can see why you might think it might; I once came to the same conclusion myself. To split the sequence on the right, you could start by finding a section of the surjection, invoking AC. Then you can project out the part of your section which doesn't lie in the kernel, which ensures the map is a homomorphism. I asked about for clarification on math.SE, with a negative answer: no choice necessary. Basically, instead of starting by splitting the surjection, you recall that a retraction of the injection was part of your given data, and use it to construct the splitting of the surjection, without making any arbitrary choices. http://math.stackexchange.com/questions/151438/does-the-splitting-lemma-hold-without-the-axiom-of-choice/