Completing proof of splitting lemma

[thesnakefromthelemma]

The goal of this patch is to establish the splitting lemma, currently Lemma 010G (lemma-ses-split) in Section 00ZX (section-abelian-categories) with proof omitted.

Our approach is to first show (in the full generality of the preadditive setting) the underlying splitting results for idempotents and (in turn) section/retraction pairs; (cf. Lemma 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

There is room to consider merging/eliding created lemmata.

As an incidental bonus we are able to complete and simplify the proof of Lemma 09SH (lemma-karoubian); this should position us nicely to subsequently add material on idempotent completions as mentioned in Comment 8065 if still desired.

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 (lemma-additive-cat-biproduct-kernel)
• lemma-ses-split: Proof is added ("omit" eliminated); the claim is trivialized via the created lemmata.

[pbelmans]

If LLMs were used in creating this pull request, can you describe how?

[thesnakefromthelemma]

@pbelmans They were not, I am happy to discuss any concerns?

[pbelmans]

No concerns, it's just that the pull request message has some LLM characteristics, in which case it's important to know whether the TeX also was edited using LLMs.

[thesnakefromthelemma]

Gotcha. To be sure I didn't use LLMs for either, but I did write up the pr message (modulo some minor edits yesterday; cf. the difference between it and the commit message) last November, when I was in between jobs, so I had a lot of free time on my hands to dot the 'i's and cross the 't's.