def UnitProjectiveSemisimple.HasFiniteLength {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : Prop

An object has finite length if the subobject lattice is both noetherian and artinian (well-founded under < and >).

class UnitProjectiveSemisimple.LocallyFiniteCategory (k : Type u_1) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] : Prop

A locally finite k-linear abelian category: every hom-space is finite-dimensional over k, and every object has finite length.

• homFinite (X Y : C) : Module.Finite k (X ⟶ Y)
• hasFiniteLength (X : C) : HasFiniteLength X

class UnitProjectiveSemisimple.MultiringCategory (k : Type u_1) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] extends UnitProjectiveSemisimple.LocallyFiniteCategory k C : Prop

Multiring category: a locally finite k-linear abelian monoidal category in which left and right whiskerings preserve both monomorphisms and epimorphisms.

• homFinite (X Y : C) : Module.Finite k (X ⟶ Y)
• hasFiniteLength (X : C) : HasFiniteLength X
• whiskerRight_mono {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] (Z : C) : CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
• whiskerLeft_mono (Z : C) {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
• whiskerRight_epi {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (Z : C) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
• whiskerLeft_epi (Z : C) {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)

class UnitProjectiveSemisimple.IsSemisimpleCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop

A category is semisimple if every object decomposes as a finite biproduct of simple objects.

• semisimple (X : C) : ∃ (n : ℕ) (Y : Fin n → C) (_ : ∀ (i : Fin n), CategoryTheory.Simple (Y i)) (x : CategoryTheory.Limits.HasBiproduct Y), Nonempty (X ≅ ⨁ Y)

theorem UnitProjectiveSemisimple.Proposition_1_13_6 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P X : C} [hP : CategoryTheory.Projective P] [hX : CategoryTheory.HasRightDual X] (whiskerRight_epi : ∀ {A B : C} (f : A ⟶ B) [CategoryTheory.Epi f] (Z : C), CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)) : CategoryTheory.Projective (CategoryTheory.MonoidalCategoryStruct.tensorObj P X)

Proposition 1.13.6: In a monoidal category where right whiskering preserves epimorphisms, the tensor product P ⊗ X of a projective object P with an object admitting a right dual is projective.

theorem UnitProjectiveSemisimple.allProjective_implies_semisimple (k : Type u_1) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] [MultiringCategory k C] (h : ∀ (X : C), CategoryTheory.Projective X) : IsSemisimpleCategory C

In a multiring category, if every object is projective then the category is semisimple.

theorem UnitProjectiveSemisimple.semisimple_implies_projective (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [IsSemisimpleCategory C] (X : C) : CategoryTheory.Projective X

In a semisimple category, every object is projective.