Documentation

TauCeti.CategoryTheory.Preadditive.KrullSchmidt.Decomposition

Decomposition into objects with local endomorphism rings #

Let C be a linear category over a commutative Artinian ring R in which idempotents split, for instance a Hom-finite idempotent-complete linear category over a field. Then every object X whose endomorphisms are finitely generated over R is a direct summand of a finite sum of objects W j with local endomorphism rings (TauCeti.exists_isLocalRing_end_sum_comp_eq_id), in the form of morphisms a j : X ⟶ W j and b j : W j ⟶ X with ∑ j, a j ≫ b j = 𝟙 X. This is the existence half of the Krull-Schmidt theorem for such a category; stating it with morphisms needs no biproducts.

The proof splits an idempotent e of X through an object Y. If 0 and 1 are the only idempotents of End Y, then End Y is local by Fitting's lemma (TauCeti.isLocalRing_end_of_idempotent_eq_zero_or_id). Otherwise a nontrivial idempotent of Y writes e as the sum of two idempotents of X below e. Each of them has a strictly smaller submodule of left multiples in the Artinian R-module X ⟶ X (TauCeti.range_leftComp_lt_range_leftComp), so the splitting stops.

References #

source
theorem TauCeti.exists_isLocalRing_end_sum_comp_eq_id (R : Type u_1) [CommRing R] [IsArtinianRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.IsIdempotentComplete C] (X : C) [Module.Finite R (X ⟶ X)] :
∃ (n : ℕ) (W : Fin n → C) (a : (j : Fin n) → X ⟶ W j) (b : (j : Fin n) → W j ⟶ X), (∀ (j : Fin n), IsLocalRing (CategoryTheory.End (W j))) ∧ ∑ j : Fin n, CategoryTheory.CategoryStruct.comp (a j) (b j) = CategoryTheory.CategoryStruct.id X

Every object is a direct summand of a finite sum of objects with local endomorphism rings, in an idempotent-complete linear category over a commutative Artinian ring R, when the endomorphisms of the object are finitely generated over R. The summand is recorded by morphisms a j : X ⟶ W j and b j : W j ⟶ X with ∑ j, a j ≫ b j = 𝟙 X.