theorem CategoryTheory.idem_trivial_of_indecomposable {C : Type u} [Category.{v, u} C] [Abelian C] {P : C} (hP : Indecomposable P) (e : P ⟶ P) (he : CategoryStruct.comp e e = e) : e = 0 ∨ e = CategoryStruct.id P

An indecomposable object in an abelian (idempotent-complete) category has only the trivial idempotent endomorphisms, namely 0 and the identity. The proof splits the idempotent e and its complement 1 - e via the idempotent-completion to exhibit P as a binary biproduct, then applies indecomposability.

instance CategoryTheory.hasLocalEndOfIndecomposable_of_finiteDimensionalEnd (k : Type w) [Field k] {C : Type u} [Category.{v, u} C] [Abelian C] [Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] : FiniteAbelianCategory.HasLocalEndOfIndecomposable k C

In a k-linear abelian category with finite-dimensional Hom spaces, every indecomposable object has a local endomorphism ring. This packages the categorical Fitting lemma: combine idem_trivial_of_indecomposable with the algebraic statement isLocalRing_of_finiteDimensional_of_no_nontrivial_idempotents.