Recognizing indecomposable objects from their endomorphisms

Mathlib defines CategoryTheory.Indecomposable X as the conjunction "X is not a zero object, and in every decomposition X ≅ Y ⊞ Z one of Y, Z is zero", and proves exactly one criterion for it: a simple object is indecomposable (CategoryTheory.indecomposable_of_simple). That criterion is too strong for the objects that carry the theory of a finite-dimensional algebra: an indecomposable projective module is almost never simple. The criterion that does apply is the one this file supplies — an object all of whose idempotent endomorphisms are trivial is indecomposable — together with the two forms in which it is used in practice. An object whose endomorphisms are recorded faithfully in a local ring, by a map preserving zero, the identity and squares, is indecomposable; this is the criterion behind the Krull–Schmidt theorem, and the one the quiver Jordan blocks need, their endomorphism algebra k[X]/(Xⁿ⁺¹) being local but not a field. And over a division ring, an object whose endomorphism space is one-dimensional (a brick) is indecomposable.

The converse holds as soon as idempotents split, that is, over an idempotent-complete category (CategoryTheory.IsIdempotentComplete, which every abelian category is): splitting e and 𝟙 - e produces two retracts of X whose idempotents add up to the identity, and any such pair realizes X as their biproduct. So over such a category an object is indecomposable exactly when it is nonzero and carries no idempotent endomorphism other than 0 and the identity, which is the form in which indecomposability is used: it turns a decomposition of a vertex space into a decomposition of the whole object.

Main results

• TauCeti.indecomposable_of_idempotent_eq_zero_or_id: a nonzero object whose only idempotent endomorphisms are 0 and the identity is indecomposable.
• TauCeti.indecomposable_of_injective_of_isLocalRing: an object whose endomorphisms are recorded faithfully in a local ring, by a map preserving zero, the identity and squares, is indecomposable.
• TauCeti.indecomposable_of_finrank_end_eq_one: in a k-linear category over a division ring, a brick is indecomposable.
• TauCeti.isoBiprodOfRetracts: two retracts of X whose idempotents sum to the identity exhibit X as their biproduct.
• TauCeti.idempotent_eq_zero_or_id_of_indecomposable: the converse of the first criterion, over an idempotent-complete category, packaged with it as TauCeti.indecomposable_iff_idempotent_eq_zero_or_id.
• TauCeti.isIso_of_isIso_comp: an invertible composite f ≫ g through an object with only trivial idempotent endomorphisms has f invertible.
• CategoryTheory.Functor.indecomposable_obj_of_map_bijective: a functor preserving zero morphisms and bijective on the endomorphisms of an indecomposable object carries it to an indecomposable object; in particular a fully faithful one does.

Implementation notes

The idempotent hypothesis is phrased with composition, e ≫ e = e, rather than through the ring CategoryTheory.End X, whose multiplication is composition in the opposite order; for an idempotent the two agree, but the hypothesis is easier to discharge as stated.

indecomposable_of_injective_of_isLocalRing records the endomorphisms in an unbundled map φ, asked to be injective, to send 0 to 0 and 𝟙 X to 1, and to carry squares to squares, φ (e ≫ e) = φ e * φ e. On a square the two orders of multiplication agree, so no use site has to choose between ≫ and the multiplication of End X; bundling φ as a ring homomorphism would settle the order and demand additivity besides. The ring is not asked to be commutative because the endomorphism ring of an indecomposable object, the intended source of φ, is not.

Two neighbours state the same idea in narrower settings. TauCeti.indecomposable_iff_isLocalRing_end asks CategoryTheory.End itself to be local but is confined to ModuleCat A and to modules of finite length; TauCeti.isIndecomposableModule_of_isLocalRing_end is the statement for bare modules. A quiver representation is a functor Paths Q ⥤ ModuleCat k, not an object of ModuleCat A, and recording its endomorphisms in a ring already known to be local is what makes the criterion cheap to apply.

The criteria that only produce or consume idempotents and zero objects are stated over CategoryTheory.Limits.HasZeroMorphisms, the setting of CategoryTheory.Indecomposable itself; only the converse direction, which forms 𝟙 X - e, and the biproduct decomposition from retracts need a preadditive category. The brick criterion is stated over a division ring.

isoBiprodOfRetracts asks only for the two retractions and the identity r₁ ≫ i₁ + r₂ ≫ i₂ = 𝟙 X; the orthogonality relations i₁ ≫ r₂ = 0 and i₂ ≫ r₁ = 0 follow. Stating it this way keeps it usable from any source of complementary idempotents, not only from CategoryTheory.IsIdempotentComplete.idempotents_split.

theorem TauCeti.indecomposable_of_idempotent_eq_zero_or_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : C} (hX : ¬CategoryTheory.Limits.IsZero X) (h : ∀ (e : X ⟶ X), CategoryTheory.CategoryStruct.comp e e = e → e = 0 ∨ e = CategoryTheory.CategoryStruct.id X) : CategoryTheory.Indecomposable X

An object with no nontrivial idempotent endomorphism is indecomposable.

theorem TauCeti.indecomposable_of_injective_of_isLocalRing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : C} (hX : ¬CategoryTheory.Limits.IsZero X) {R : Type u_1} [Ring R] [IsLocalRing R] (φ : (X ⟶ X) → R) (hφ : Function.Injective φ) (hzero : φ 0 = 0) (hid : φ (CategoryTheory.CategoryStruct.id X) = 1) (hsq : ∀ (e : X ⟶ X), φ (CategoryTheory.CategoryStruct.comp e e) = φ e * φ e) : CategoryTheory.Indecomposable X

An object whose endomorphisms are recorded faithfully in a local ring is indecomposable. The record φ is asked to be injective and to preserve zero, the identity and squares. This is the criterion behind the Krull–Schmidt theorem: an object whose endomorphism ring is local is indecomposable.

theorem TauCeti.isIso_of_isIso_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (hX : CategoryTheory.CategoryStruct.id X ≠ 0) (hY : ∀ (e : Y ⟶ Y), CategoryTheory.CategoryStruct.comp e e = e → e = 0 ∨ e = CategoryTheory.CategoryStruct.id Y) (f : X ⟶ Y) (g : Y ⟶ X) (h : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f g)) : CategoryTheory.IsIso f

A composite that is invertible has an invertible first factor, when the object it passes through has only the trivial idempotent endomorphisms and the identity of the source is nonzero. Both hypotheses hold when the source is nonzero and the middle object is indecomposable in a category where idempotents split (TauCeti.idempotent_eq_zero_or_id_of_indecomposable).

noncomputable def TauCeti.isoBiprodOfRetracts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y Z : C} (i₁ : Y ⟶ X) (r₁ : X ⟶ Y) (i₂ : Z ⟶ X) (r₂ : X ⟶ Z) (h₁ : CategoryTheory.CategoryStruct.comp i₁ r₁ = CategoryTheory.CategoryStruct.id Y) (h₂ : CategoryTheory.CategoryStruct.comp i₂ r₂ = CategoryTheory.CategoryStruct.id Z) (h : CategoryTheory.CategoryStruct.comp r₁ i₁ + CategoryTheory.CategoryStruct.comp r₂ i₂ = CategoryTheory.CategoryStruct.id X) : X ≅ Y ⊞ Z

Two retracts whose idempotents sum to the identity split an object as a biproduct. Its comparison map and inverse are read off by TauCeti.isoBiprodOfRetracts_hom and TauCeti.isoBiprodOfRetracts_inv.

Equations

• TauCeti.isoBiprodOfRetracts i₁ r₁ i₂ r₂ h₁ h₂ h = { hom := CategoryTheory.Limits.biprod.lift r₁ r₂, inv := CategoryTheory.Limits.biprod.desc i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TauCeti.isoBiprodOfRetracts_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y Z : C} {i₁ : Y ⟶ X} {r₁ : X ⟶ Y} {i₂ : Z ⟶ X} {r₂ : X ⟶ Z} {h₁ : CategoryTheory.CategoryStruct.comp i₁ r₁ = CategoryTheory.CategoryStruct.id Y} {h₂ : CategoryTheory.CategoryStruct.comp i₂ r₂ = CategoryTheory.CategoryStruct.id Z} {h : CategoryTheory.CategoryStruct.comp r₁ i₁ + CategoryTheory.CategoryStruct.comp r₂ i₂ = CategoryTheory.CategoryStruct.id X} : (isoBiprodOfRetracts i₁ r₁ i₂ r₂ h₁ h₂ h).hom = CategoryTheory.Limits.biprod.lift r₁ r₂

The comparison map of TauCeti.isoBiprodOfRetracts is the pair of the two retractions.

@[simp]

theorem TauCeti.isoBiprodOfRetracts_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X Y Z : C} {i₁ : Y ⟶ X} {r₁ : X ⟶ Y} {i₂ : Z ⟶ X} {r₂ : X ⟶ Z} {h₁ : CategoryTheory.CategoryStruct.comp i₁ r₁ = CategoryTheory.CategoryStruct.id Y} {h₂ : CategoryTheory.CategoryStruct.comp i₂ r₂ = CategoryTheory.CategoryStruct.id Z} {h : CategoryTheory.CategoryStruct.comp r₁ i₁ + CategoryTheory.CategoryStruct.comp r₂ i₂ = CategoryTheory.CategoryStruct.id X} : (isoBiprodOfRetracts i₁ r₁ i₂ r₂ h₁ h₂ h).inv = CategoryTheory.Limits.biprod.desc i₁ i₂

The inverse of TauCeti.isoBiprodOfRetracts is the pair of the two sections.

theorem TauCeti.idempotent_eq_zero_or_id_of_indecomposable {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X : C} (hX : CategoryTheory.Indecomposable X) {e : X ⟶ X} (he : CategoryTheory.CategoryStruct.comp e e = e) : e = 0 ∨ e = CategoryTheory.CategoryStruct.id X

An indecomposable object has no nontrivial idempotent endomorphism, as soon as idempotents split. This is the converse of TauCeti.indecomposable_of_idempotent_eq_zero_or_id.

theorem TauCeti.indecomposable_iff_idempotent_eq_zero_or_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X : C} : CategoryTheory.Indecomposable X ↔ ¬CategoryTheory.Limits.IsZero X ∧ ∀ (e : X ⟶ X), CategoryTheory.CategoryStruct.comp e e = e → e = 0 ∨ e = CategoryTheory.CategoryStruct.id X

Indecomposability is the triviality of the idempotent endomorphisms, over a category in which idempotents split.

theorem TauCeti.not_isZero_of_finrank_end_eq_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [Nontrivial k] [CategoryTheory.Linear k C] {X : C} (h : Module.finrank k (X ⟶ X) = 1) : ¬CategoryTheory.Limits.IsZero X

An object whose endomorphism space is one-dimensional is not a zero object.

theorem TauCeti.id_ne_zero_of_finrank_end_eq_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [Semiring k] [Nontrivial k] [CategoryTheory.Linear k C] {X : C} (h : Module.finrank k (X ⟶ X) = 1) : CategoryTheory.CategoryStruct.id X ≠ 0

An object whose endomorphism space is one-dimensional has a nonzero identity.

theorem TauCeti.indecomposable_of_finrank_end_eq_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {k : Type u_1} [DivisionRing k] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X : C} (h : Module.finrank k (X ⟶ X) = 1) : CategoryTheory.Indecomposable X

A brick is indecomposable: an object whose endomorphism space over a division ring is one-dimensional is indecomposable.

theorem CategoryTheory.Functor.indecomposable_obj_of_map_bijective {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms D] [Limits.HasBinaryBiproducts C] [IsIdempotentComplete C] [Limits.HasBinaryBiproducts D] (F : Functor C D) {X : C} (hX : Indecomposable X) (hF : Function.Bijective F.map) : Indecomposable (F.obj X)

A functor bijective on the endomorphisms of an indecomposable object carries it to an indecomposable object, when idempotents split in the source. A fully faithful functor qualifies, by CategoryTheory.Functor.FullyFaithful.map_bijective.