Finite semisimple categories

An abelian category is finite semisimple when every object is isomorphic to a finite biproduct of simple objects. This file introduces that property and proves that it is invariant under equivalence of categories. In a finite semisimple category every object is injective, so every monomorphism splits: a monomorphism out of a simple object splits by Schur's lemma, and a finite biproduct of injective objects is injective.

The decomposition condition is independent of a choice of coefficient field. Linearity and finite-dimensionality of morphism spaces are separate hypotheses when they are needed.

Main results

• TauCeti.IsFiniteSemisimpleCategory: every object is a finite biproduct of simple objects.
• TauCeti.IsFiniteSemisimpleCategory.of_equivalence: transport finite semisimplicity across an equivalence.
• TauCeti.IsFiniteSemisimpleCategory.exists_biproduct_simples_of_isZero, TauCeti.IsFiniteSemisimpleCategory.exists_biproduct_simples_of_simple and TauCeti.IsFiniteSemisimpleCategory.exists_biproduct_simples_biprod: zero objects and simple objects are finite biproducts of simple objects, and such decompositions combine along ⊞.
• TauCeti.isSplitMono_of_nonzero_from_simple and TauCeti.isSplitEpi_of_nonzero_to_simple: a nonzero morphism out of (resp. into) a simple object is a split monomorphism (resp. split epimorphism).
• TauCeti.exists_nonzero_from_simple_iff_exists_nonzero_to_simple: a simple object maps nontrivially to an object exactly when the object maps nontrivially to it.
• TauCeti.biproduct_ι_comp_inv_ne_zero: the inclusion of a simple summand is nonzero.
• TauCeti.exists_simple_hom_ne_zero: a nonzero object receives a nonzero morphism from a simple object.
• TauCeti.IsFiniteSemisimpleCategory.injective: every object of a finite semisimple category is injective.
• TauCeti.IsFiniteSemisimpleCategory.splitMonoCategory: every monomorphism of a finite semisimple category splits.
• CategoryTheory.Functor.hom_ext_of_simple: a morphism out of the image of an object under an additive functor is determined by its composites with the images of morphisms from simple objects.
• TauCeti.natTrans_ext_of_simple: a natural transformation out of an additive functor is determined by its components at the simple objects.

class TauCeti.IsFiniteSemisimpleCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : Prop

An abelian category is finite semisimple if every object is isomorphic to a finite biproduct of simple objects.

• exists_biproduct_simples (X : C) : ∃ (ι : Type) (x : Fintype ι) (f : ι → C) (_ : ∀ (i : ι), CategoryTheory.Simple (f i)) (x : CategoryTheory.Limits.HasBiproduct f), Nonempty (X ≅ ⨁ f)

  Every object is isomorphic to a finite biproduct of simple objects.

theorem TauCeti.IsFiniteSemisimpleCategory.of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (e : C ≌ D) [IsFiniteSemisimpleCategory C] : IsFiniteSemisimpleCategory D

Finite semisimplicity is preserved by an equivalence of abelian categories.

theorem TauCeti.IsFiniteSemisimpleCategory.iff_of_equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (e : C ≌ D) : IsFiniteSemisimpleCategory C ↔ IsFiniteSemisimpleCategory D

Equivalent abelian categories are finite semisimple simultaneously.

theorem TauCeti.IsFiniteSemisimpleCategory.exists_biproduct_simples_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (hX : CategoryTheory.Limits.IsZero X) : ∃ (ι : Type) (x : Fintype ι) (f : ι → C) (_ : ∀ (i : ι), CategoryTheory.Simple (f i)) (x : CategoryTheory.Limits.HasBiproduct f), Nonempty (X ≅ ⨁ f)

A zero object is the biproduct of the empty family of simple objects.

theorem TauCeti.IsFiniteSemisimpleCategory.exists_biproduct_simples_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) [CategoryTheory.Simple X] : ∃ (ι : Type) (x : Fintype ι) (f : ι → C) (_ : ∀ (i : ι), CategoryTheory.Simple (f i)) (x : CategoryTheory.Limits.HasBiproduct f), Nonempty (X ≅ ⨁ f)

A simple object is the biproduct of the family consisting of itself.

theorem TauCeti.IsFiniteSemisimpleCategory.exists_biproduct_simples_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (hX : ∃ (ι : Type) (x : Fintype ι) (f : ι → C) (_ : ∀ (i : ι), CategoryTheory.Simple (f i)) (x : CategoryTheory.Limits.HasBiproduct f), Nonempty (X ≅ ⨁ f)) (hY : ∃ (ι : Type) (x : Fintype ι) (f : ι → C) (_ : ∀ (i : ι), CategoryTheory.Simple (f i)) (x : CategoryTheory.Limits.HasBiproduct f), Nonempty (Y ≅ ⨁ f)) : ∃ (ι : Type) (x : Fintype ι) (f : ι → C) (_ : ∀ (i : ι), CategoryTheory.Simple (f i)) (x : CategoryTheory.Limits.HasBiproduct f), Nonempty (X ⊞ Y ≅ ⨁ f)

Decompositions of X and Y into finite biproducts of simple objects combine to one of X ⊞ Y.

theorem TauCeti.isSplitMono_of_nonzero_from_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {S Z : C} [CategoryTheory.Simple S] {f : S ⟶ Z} (hf : f ≠ 0) : CategoryTheory.IsSplitMono f

In a finite semisimple category, a nonzero morphism out of a simple object is a split monomorphism.

theorem TauCeti.isSplitEpi_of_nonzero_to_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {S Y : C} [CategoryTheory.Simple S] {g : Y ⟶ S} (hg : g ≠ 0) : CategoryTheory.IsSplitEpi g

In a finite semisimple category, a nonzero morphism into a simple object is a split epimorphism.

theorem TauCeti.exists_nonzero_from_simple_iff_exists_nonzero_to_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {S Y : C} [CategoryTheory.Simple S] : (∃ (f : S ⟶ Y), f ≠ 0) ↔ ∃ (g : Y ⟶ S), g ≠ 0

In a finite semisimple category, a simple object maps nontrivially to an object exactly when the object maps nontrivially to it.

theorem TauCeti.biproduct_ι_comp_inv_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {a : ι → C} [CategoryTheory.Limits.HasBiproduct a] {Y : C} (e : Y ≅ ⨁ a) (i : ι) [CategoryTheory.Simple (a i)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι a i) e.inv ≠ 0

The inclusion of a simple summand into an object decomposed as a biproduct is nonzero.

theorem TauCeti.exists_simple_hom_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {Y : C} (hY : ¬CategoryTheory.Limits.IsZero Y) : ∃ (S : C) (_ : CategoryTheory.Simple S) (f : S ⟶ Y), f ≠ 0

In a finite semisimple category, a nonzero object receives a nonzero morphism from a simple object: the inclusion of a summand of a decomposition into simple objects.

instance TauCeti.IsFiniteSemisimpleCategory.injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] (X : C) : CategoryTheory.Injective X

Every object of a finite semisimple category is injective.

instance TauCeti.IsFiniteSemisimpleCategory.splitMonoCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] : CategoryTheory.SplitMonoCategory C

Every monomorphism of a finite semisimple category splits.

theorem CategoryTheory.Functor.hom_ext_of_simple {C : Type u} [Category.{v, u} C] [Abelian C] [TauCeti.IsFiniteSemisimpleCategory C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.Additive] {X : C} {Z : D} {f g : F.obj X ⟶ Z} (h : ∀ (S : C) [Simple S] (s : S ⟶ X), CategoryStruct.comp (F.map s) f = CategoryStruct.comp (F.map s) g) : f = g

In a finite semisimple category, the images under an additive functor of the morphisms from simple objects into X are jointly epimorphic: two morphisms out of F.obj X agreeing after precomposition with every F.map s, for s : S ⟶ X with S simple, are equal.

theorem TauCeti.natTrans_ext_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] {F G : CategoryTheory.Functor C D} [F.Additive] {α β : F ⟶ G} (h : ∀ (X : C) [CategoryTheory.Simple X], α.app X = β.app X) : α = β

In a finite semisimple category, a natural transformation out of an additive functor is determined by its components at the simple objects.