Krull-Schmidt categories

A preadditive category with finite biproducts is Krull-Schmidt when every object is isomorphic to a finite biproduct of objects with local endomorphism rings.

Main definitions

• TauCeti.IsKrullSchmidt: Krull-Schmidt categories.

Main results

• TauCeti.isIdempotentComplete_of_isKrullSchmidt: a Krull-Schmidt category is idempotent complete.
• TauCeti.IsKrullSchmidt.indecomposable_iff_isLocalRing_end: in a Krull-Schmidt category, an object is indecomposable exactly when its endomorphism ring is local.
• CategoryTheory.Equivalence.isKrullSchmidt: the Krull-Schmidt property is invariant under equivalence of categories.

Implementation notes

Idempotent completeness is proved by peeling off one summand at a time. Let e be an idempotent of X = P ⊞ X' with End P local. The component c of e on P is invertible, or 1 - c is. In the first case ι_P ≫ e exhibits P as a summand of the image of e, split off by an idempotent q below e; in the second, ι_P ≫ (1 - e) exhibits P inside the image of 1 - e. Either way the idempotent that remains, e - q or e, kills a copy of P whose projection to P is invertible. Replacing P by that copy gives a new decomposition X = P ⊞ X' in which the remaining idempotent is carried by X', where it splits by induction on the number of summands.

TauCeti.exists_isLocalRing_end_sum_comp_eq_id, in TauCeti.CategoryTheory.Preadditive.KrullSchmidt.Decomposition, provides decompositions into objects with local endomorphism rings in Hom-finite idempotent-complete linear categories over a commutative Artinian ring.

References

• Henning Krause, Krull-Schmidt categories and projective covers, Expo. Math. 33 (2015), 535–549, Section 4.

class TauCeti.IsKrullSchmidt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : Prop

A Krull-Schmidt category: every object is isomorphic to a finite biproduct of objects with local endomorphism rings.

• exists_iso_biproduct (X : C) : ∃ (n : ℕ) (P : Fin n → C), (∀ (i : Fin n), IsLocalRing (CategoryTheory.End (P i))) ∧ Nonempty (X ≅ ⨁ P)

  Every object is isomorphic to a finite biproduct of objects with local endomorphism rings.

instance TauCeti.isIdempotentComplete_of_isKrullSchmidt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [IsKrullSchmidt C] : CategoryTheory.IsIdempotentComplete C

A Krull-Schmidt category is idempotent complete.

theorem TauCeti.IsKrullSchmidt.indecomposable_iff_isLocalRing_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [IsKrullSchmidt C] (X : C) : CategoryTheory.Indecomposable X ↔ IsLocalRing (CategoryTheory.End X)

In a Krull-Schmidt category, an object is indecomposable exactly when its endomorphism ring is local. The converse direction holds in any preadditive category with binary biproducts (TauCeti.indecomposable_of_isLocalRing_end).

theorem CategoryTheory.Equivalence.isKrullSchmidt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] [Limits.HasFiniteBiproducts C] [Limits.HasFiniteBiproducts D] [TauCeti.IsKrullSchmidt C] (e : C ≌ D) : TauCeti.IsKrullSchmidt D

The Krull-Schmidt property is invariant under equivalence of categories.