A proof of the splitting lemma for Stacks

The goal of this patch is to establish the well-known splitting lemma,
currently [Lemma 010G](https://stacks.math.columbia.edu/tag/010G) (`lemma-ses-split`)
with proof omitted in [Section 00ZX](https://stacks.math.columbia.edu/tag/00ZX) (`section-abelian-categories`).

However, the theorem can be stated in a manner which is equivalent for Abelian categories
and true in all preadditive categories; cf `lemma-split-morphism-splitting` below.

Our approach to proving the theorem is to first show (in the full generality of the preadditive setting)
the well-known splitting result for idempotents
(cf. [Lemma 09SH](https://stacks.math.columbia.edu/tag/09SH), `lemma-karoubian`).
This involves the creation of 5 labels:
- 1 preliminary remark in `section-additive-categories` concerning idempotents
- 2 lemmate in `section-additive-categories` concerning idempotents
- 2 lemmate in `section-additive-categories` concerning section/retraction pairs.
As an incidental bonus we are able to complete and simplify the proof of the aforementioned
[Lemma 09SH](https://stacks.math.columbia.edu/tag/09SH) (`lemma-karoubian`).

There is room to consider merging created lemmata; cf. the below lists:

**Labels created:**
- `lemma-idempotent-symmetry`: The complement of an idempotent is idempotent, and the two annihilate one another.
- `lemma-idempotent-kernel-cokernel`: An idempotent has a kernel iff it has a cokernel, and likewise for its complement.
- `lemma-idempotent-splitting`: Idempotents beget direct product decompositions of their (co)domains.
- `lemma-split-morphism-kernel-cokernel`: The section/retraction of a split pair of morphisms is a kernel/cokernel respectively.
- `lemma-split-morphism-splitting`: The section/retraction of a split pair of morphisms beget a splitting of the codomain/domain respectively.

**Labels modified:**
- `lemma-karoubian`: Proof is completed ("omit" eliminated) and simplified with the claim an immediate corollary of the above and [Lemma 09QG](https://stacks.math.columbia.edu/tag/09QG) (`lemma-additive-cat-biproduct-kernel`)
- `lemma-ses-split`: Proof is added; the claim is trivialized via the created lemmata.

Author: thesnakefromthelemma

homology.tex

@@ -294,6 +294,157 @@ \section{Preadditive and additive categories}
 Similarly, (4) follows from (1).
 \end{proof}
 
+\noindent
+Recall that an endomorphism $f$ is said to be
+idempotent if and only if $f \circ f = f$.
+
+\begin{remark}
+\label{remark-idempotent-symmetry}
+Let $\mathcal{A}$ be a preadditive category,
+$x$ be an object of $\mathcal{A}$,
+and $f : x \to x$ be idempotent.
+Writing $g = \text{id} _ x - f$,
+one has $f \circ g = 0$, $g \circ f = 0$, and $g \circ g = g$.
+\end{remark}
+
+\begin{lemma}
+\label{lemma-idempotent-kernel-cokernel}
+Let $\mathcal{A}$ be a preadditive category,
+$x$ be an object of $\mathcal{A}$,
+and $f : x \to x$ be idempotent.
+Write $g = \text{id} _ x - f$
+and recall by Remark \ref{remark-idempotent-symmetry}
+that $f \circ g = g \circ f = 0$.
+\begin{enumerate}
+\item If $f$ has kernel $i : \Ker (f) \to x$
+and $p$ is the unique morphism such that $g = i \circ p$,
+then $p \circ i = \text{id} _ {\Ker (f)}$
+and $p$ is the cokernel of $f$.
+\item If $f$ has cokernel $p : x \to \Coker (f)$
+and $i$ is the unique morphism such that $g = i \circ p$,
+then $p \circ i = \text{id} _ {\Coker (f)}$
+and $i$ is the kernel of $f$.
+\item If $g$ has kernel $j : \Ker (g) \to x$
+and $q$ is the unique morphism such that $f = j \circ q$,
+then $q \circ j = \text{id} _ {\Ker (g)}$
+and $q$ is the cokernel of $g$.
+\item If $g$ has cokernel $q : x \to \Coker (g)$
+and $j$ is the unique morphism such that $f = j \circ q$,
+then $q \circ j = \text{id} _ {\Coker (g)}$
+and $j$ is the kernel of $g$.
+\end{enumerate}
+\end{lemma}
+
+\begin{proof}
+As for (1), compute first that $i = (f + g) \circ i = g \circ i$.
+By the construction of $p$, this implies that
+$i \circ p \circ i = g \circ i = i \circ \text{id} _ {\Ker (f)}$.
+By Lemma \ref{lemma-kernel-mono} we conclude that
+$p \circ i = \text{id} _ {\Ker (f)}$.
+
+\medskip\noindent
+It remains to show that $p : x \to \Ker (f)$
+satisfies the universal property of the cokernel of $f$,
+i.e., that given a morphism $a : x \to y$ satisfying $a \circ f = 0$
+there exists a unique morphism $b : \Ker (f) \to y$
+such that $a = b \circ p$.
+Existence follows by first computing that $a = a \circ (f + g) = a \circ g$
+and concluding by the construction of $p$
+that $a = a \circ g = a \circ i \circ p$
+(so that we can take $b = a \circ i$).
+Uniqueness follows from that $b = b \circ p \circ i = a \circ i$
+(so that $a$ determines $b$).
+
+\medskip\noindent
+By duality,
+symmetry (i.e., that $g$ is itself idempotent;
+cf. Remark \ref{remark-idempotent-symmetry}),
+and duality and symmetry respectively, (2), (3), and (4) follow as did (1).
+\end{proof}
+
+\begin{lemma}
+\label{lemma-idempotent-splitting}
+Let $\mathcal{A}$ be a preadditive category,
+$x$ be an object of $\mathcal{A}$,
+and $f : x \to x$ be idempotent.
+Write $g = \text{id} _ x - f$.
+If each of $f$ and $g$ have at least one of a kernel or cokernel
+and in turn morphisms $i , j , p , q$ are constructed
+as in the statement of Lemma \ref{lemma-idempotent-kernel-cokernel},
+then all four (co)kernels exist and
+\begin{align*}
+x
+& \simeq \Ker (f) \oplus \Ker (g) \\
+& \simeq \Coker (f) \oplus \Ker (g) \\
+& \simeq \Ker (f) \oplus \Coker (g) \\
+& \simeq \Coker (f) \oplus \Coker (g)
+\end{align*}
+with the structure of each direct product given by $i , j , p , q$.
+\end{lemma}
+
+\begin{proof}
+By Lemma \ref{lemma-idempotent-kernel-cokernel}
+$p \circ i = \text{id} _ {\Ker (f)} = \text{id} _ {\Coker (f)}$
+and $q \circ j = \text{id} _ {\Ker (g)} = \text{id} _ {\Coker (g)}$.
+By construction, $i \circ p + j \circ q = f + g = \text{id} _ x$.
+By Remark \ref{remark-direct-sum} the claim follows.
+\end{proof}
+
+\begin{lemma}
+\label{lemma-split-morphism-kernel-cokernel}
+Let $\mathcal{A}$ be a preadditive category,
+$x$ and $y$ be objects of $\mathcal{A}$,
+and $j : y \to x$ and $q : x \to y$ be morphisms
+satisfying $q \circ j = \text{id} _ y$.
+Then
+\begin{enumerate}
+\item $\text{id} _ x - j \circ q$ has kernel $j$.
+\item $\text{id} _ x - j \circ q$ has cokernel $q$.
+\end{enumerate}
+\end{lemma}
+
+\begin{proof}
+As for (1), compute first that $(\text{id} _ x - j \circ q) \circ j = 0$.
+We must show that $j$ satisfies the universal property
+of the kernel of $\text{id} _ {x} - j \circ q$,
+i.e., that given a morphism $a : z \to x$
+satisfying $(\text{id} _ x - j \circ q) \circ a = 0$
+there exists a unique morphism $b : z \to y$
+such that $a = j \circ b$.
+Existence follows by computing that $a = j \circ q \circ a$
+(so that we can take $b = q \circ a$).
+Uniqueness follows from that $b = q \circ j \circ b = q \circ a$
+(so that $a$ determines $b$).
+
+\medskip\noindent
+By duality, (2) follows as did (1).
+\end{proof}
+
+\begin{lemma}
+\label{lemma-split-morphism-splitting}
+Let $\mathcal{A}$ be a preadditive category,
+$x$ and $y$ be objects of $\mathcal{A}$,
+and $j : y \to x$ and $q : x \to y$ be morphisms
+satisfying $q \circ j = \text{id} _ y$.
+If $j \circ q$ has at least one of a kernel or cokernel,
+then both (co)kernels exist and
+\begin{align*}
+x
+& \simeq \Ker (j \circ q) \oplus y \\
+& \simeq \Coker (j \circ q) \oplus y
+\end{align*}
+with the structure of either direct product including $j , q$,
+and the canonical (co)kernel morphism,
+and the remaining map uniquely determined.
+\end{lemma}
+
+\begin{proof}
+Write $f = j \circ q$,
+compute that $f \circ f = f$,
+and apply Lemma \ref{lemma-idempotent-splitting}
+and Lemma \ref{lemma-split-morphism-kernel-cokernel}.
+\end{proof}
+
 \begin{lemma}
 \label{lemma-coim-im-map}
 Let $f : x \to y$ be a morphism in a preadditive category
@@ -386,16 +537,9 @@ \section{Karoubian categories}
 \end{lemma}
 
 \begin{proof}
-Assume (1) and let $p : z \to z$ be as in (3).
-Let $x = \Ker(p)$ and $y = \Ker(1 - p)$. There are maps
-$x \to z$ and $y \to z$. Since $(1 - p)p = 0$ we see that $p : z \to z$
-factors through $y$, hence we obtain a morphism $z \to y$. Similarly
-we obtain a morphism $z \to x$. We omit the verification that these
-four morphisms induce an isomorphism $x = y \oplus z$ as in
-Remark \ref{remark-direct-sum}.
-Thus (1) $\Rightarrow$ (3). The implication (2) $\Rightarrow$ (3)
-is dual. Finally, condition (3) implies (1) and (2) by
-Lemma \ref{lemma-additive-cat-biproduct-kernel}.
+Immediate via Lemma \label{lemma-idempotent-kernel-cokernel}
+and Lemma \label{lemma-idempotent-splitting},
+and Lemma \label{lemma-additive-cat-biproduct-kernel}.
 \end{proof}
 
 \begin{lemma}
@@ -659,7 +803,7 @@ \section{Abelian categories}
 \end{lemma}
 
 \begin{proof}
-Omitted.
+Immediate corollary of Lemma \ref{lemma-split-morphism-splitting}.
 \end{proof}
 
 \begin{lemma}