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.