Scalar endomorphisms imply indecomposability

A nonzero object in a linear category whose endomorphisms are all scalar is indecomposable. This is the categorical Schur argument used when transporting the concrete factor grading across the poset-space equivalence.

theorem MagnitudeConjecture.CategoryTheory.indecomposable_of_endomorphism_eq_smul_id {k : Type s} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) (hX : ¬CategoryTheory.Limits.IsZero X) (hscalar : ∀ (f : X ⟶ X), ∃ (c : k), c • CategoryTheory.CategoryStruct.id X = f) : CategoryTheory.Indecomposable X

A nonzero object with only scalar endomorphisms cannot split as a biproduct of two nonzero objects.