Conditions on a ℂ-linear category

The ambient conditions a tensor category is asked to satisfy: finite-dimensional Hom-spaces and semisimplicity in the form that every object is a finite biproduct of simple objects. The third, scalar endomorphisms of the tensor unit (HasScalarUnit), is defined in RS/Definitions.lean.

def RS.HasFinDimHom (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] : Prop

Every Hom-space is finite dimensional over ℂ.

Equations

• RS.HasFinDimHom A = ∀ (X Y : A), FiniteDimensional ℂ (X ⟶ Y)

def RS.IsSemisimple (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteBiproducts A] : Prop

Every object is a finite biproduct of simple objects.

Equations

• RS.IsSemisimple A = ∀ (X : A), ∃ (n : ℕ) (S : Fin n → A), (∀ (i : Fin n), CategoryTheory.Simple (S i)) ∧ Nonempty (X ≅ ⨁ S)