Lately been falling asleep doing the #SplittingLemma in my head.
It is fun to be #CountingSheep by a simple diagram chase!
To recap, given the short exact sequence
0 → 𝐴 → 𝐵 → 𝐶 → 0 it splits if 𝐴 → 𝐵 is invertible at 𝐴 or 𝐵 → 𝐶 is invertible at 𝐶. In either equivalent case, 𝐵 ≅ 𝐴⊕𝐶.
The fun part is now to prove all of these equivalences in your head so you can fall asleep. For simplicity, let's assume an abelian category. Or just plain modules (kind of implied by the direct sum, I think, you get a partial splitting lemma in nonabelian groups).
Let's do 𝐴 → 𝐵 is invertible implies 𝐵 ≅ 𝐴⊕𝐶 !
Giving these morphisms names, let 𝑖: 𝐴 → 𝐵 and 𝑗: 𝐵 → 𝐶 and let's call the inverse 𝑝: 𝐵 → 𝐴. Need to check that 𝑏 ↦ (𝑝(𝑏), ,𝑗(𝑏)) is both mono and epi.
Let's begin with (𝑝(𝑏), ,𝑗(𝑏)) = (0,0) implies 𝑏=0. Since 𝑏 ∈ ker 𝑗, by exactness at 𝐵 we have that 𝑏 = 𝑖(𝑎) for some 𝑎. But then 0 = 𝑝(𝑏) = 𝑝(𝑖(𝑎)) = 𝑎 because 𝑝 is an inverse. Since 𝑖 is mono, 0 = 𝑖(0) = 𝑖(𝑎) = 𝑏.
Now we need to construct 𝑏 such that (𝑝(𝑏), 𝑗(𝑏))=(𝑎, 𝑐) for arbitrary 𝑎 and 𝑐. Since 𝑗 is epi, there exists 𝑏' such that 𝑗(𝑏') = 𝑐. But 𝑝(𝑏') might be any old thing! Let's patch up 𝑏' and consider 𝑏 := 𝑏' + 𝑖(𝑎−𝑝(𝑏')). By exactness at 𝐵, we also have that 𝑗(𝑏) = 𝑗(𝑏') = 𝑐. As a similar check, 𝑝(𝑏) = 𝑝(𝑏'+𝑖(𝑎−𝑝(𝑏'))) = 𝑝(𝑏')+𝑝(𝑖(𝑎−𝑝(𝑏')) but since 𝑝 is an inverse this is 𝑝(𝑏')+𝑎−𝑝(𝑏') = 𝑎, proving that 𝑏 has been constructed as desired.