Left multiples of idempotent endomorphisms

In an R-linear category, the left multiples {e ≫ g} of an endomorphism e : X ⟶ X form the R-submodule LinearMap.range (Linear.leftComp R X e) of X ⟶ X. For an idempotent f and an endomorphism e with e ≫ f = f and f ≫ e = f, for instance an idempotent f below an idempotent e, the submodule of f lies in the one of e, and strictly unless f = e (TauCeti.range_leftComp_lt_range_leftComp). When X ⟶ X is an Artinian R-module, this bounds how often an idempotent can be split into smaller ones, as in the existence half of the Krull-Schmidt theorem.

theorem TauCeti.range_leftComp_lt_range_leftComp (R : Type u_1) [Semiring R] {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X : C} {e f : X ⟶ X} (hf : CategoryTheory.CategoryStruct.comp f f = f) (hef : CategoryTheory.CategoryStruct.comp e f = f) (hfe : CategoryTheory.CategoryStruct.comp f e = f) (hne : f ≠ e) : (CategoryTheory.Linear.leftComp R X f).range < (CategoryTheory.Linear.leftComp R X e).range

Left multiples of a smaller idempotent form a smaller submodule. If f is an idempotent endomorphism of X and e an endomorphism of X with e ≫ f = f, f ≫ e = f and f ≠ e, then the left multiples of f form a proper submodule of the left multiples of e.