Local finite-dimensional endomorphism rings of indecomposable objects

In an idempotent-complete preadditive category, an idempotent endomorphism splits the object as the biproduct of its image and complementary image. Categorical indecomposability therefore makes every idempotent zero or one. When the endomorphism algebra is finite-dimensional, the regular-module Fitting criterion makes that algebra local.

theorem MagnitudeConjecture.CategoryTheory.indecomposable_idempotent_eq_zero_or_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] (X : C) (hX : CategoryTheory.Indecomposable X) (p : X ⟶ X) (hp : CategoryTheory.CategoryStruct.comp p p = p) : p = 0 ∨ p = CategoryTheory.CategoryStruct.id X

An indecomposable object in an idempotent-complete preadditive category has no nontrivial idempotent endomorphisms.

theorem MagnitudeConjecture.CategoryTheory.end_isLocalRing_of_finiteDimensional_indecomposable {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] (X : C) [FiniteDimensional k (CategoryTheory.End X)] (hX : CategoryTheory.Indecomposable X) : IsLocalRing (CategoryTheory.End X)

If the endomorphism algebra of an indecomposable object is finite-dimensional, then it is local.