Decomposition into indecomposables in FGModuleCat

Every finitely generated Artinian module X is a direct summand of a finite sum of finitely generated indecomposable modules W j (FGModuleCat.exists_indecomposable_sum_comp_eq_id). This is read off from the existence half of the Krull-Schmidt theorem, TauCeti.exists_indecomposable_iso_biproduct, inside FGModuleCat A. The summand is recorded by morphisms a j : X ⟶ W j and b j : W j ⟶ X with ∑ j, a j ≫ b j = 𝟙 X, which needs no biproducts in FGModuleCat A. By Fitting's lemma, a finitely generated indecomposable module of finite length has a local endomorphism ring (FGModuleCat.isLocalRing_end_of_indecomposable).

theorem FGModuleCat.exists_indecomposable_sum_comp_eq_id {A : Type v} [Ring A] (X : FGModuleCat A) [IsArtinian A ↑X.obj] : ∃ (n : ℕ) (W : Fin n → FGModuleCat A) (a : (j : Fin n) → X ⟶ W j) (b : (j : Fin n) → W j ⟶ X), (∀ (j : Fin n), CategoryTheory.Indecomposable (W j).obj) ∧ ∑ j : Fin n, CategoryTheory.CategoryStruct.comp (a j) (b j) = CategoryTheory.CategoryStruct.id X

Every finitely generated Artinian module X is a direct summand of a finite sum of finitely generated indecomposable modules W j, in the form of morphisms a j : X ⟶ W j and b j : W j ⟶ X with ∑ j, a j ≫ b j = 𝟙 X.

theorem FGModuleCat.isLocalRing_end_of_indecomposable {A : Type v} [Ring A] {X : FGModuleCat A} [IsNoetherian A ↑X.obj] [IsArtinian A ↑X.obj] (hX : CategoryTheory.Indecomposable X.obj) : IsLocalRing (CategoryTheory.End X)

Fitting's lemma in FGModuleCat A: a finitely generated indecomposable module of finite length (Noetherian and Artinian) has a local endomorphism ring.