Hom dimensions in a split finite semisimple category

Over an algebraically closed field, Schur's lemma identifies the multiplicity of a simple object in a finite semisimple category with the dimension of the corresponding Hom space. Both orientations are recorded: morphisms from the simple object and morphisms to it have the same dimension, equal to its decomposition multiplicity.

The algebraic-closedness and finite-dimensionality assumptions are essential. Over a nonsplit field, the endomorphism division algebra of a simple object can have dimension greater than one, so the dimension of its Hom space need not equal its decomposition multiplicity.

@[simp]

theorem TauCeti.finrank_hom_simple_eq_simpleMultiplicities (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (S X : C) [CategoryTheory.Simple S] : Module.finrank k (S ⟶ X) = (simpleMultiplicities X) (SimpleClasses.classOf S)

The dimension of the morphisms from a simple object to an object is the multiplicity of that simple object in the target.

@[simp]

theorem TauCeti.finrank_homTo_simple_eq_simpleMultiplicities (k : Type w) [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [IsFiniteSemisimpleCategory C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (X S : C) [CategoryTheory.Simple S] : Module.finrank k (X ⟶ S) = (simpleMultiplicities X) (SimpleClasses.classOf S)

The dimension of the morphisms from an object to a simple object is the multiplicity of that simple object in the source.