Multiplicities in finite simple decompositions

The simple multiplicities of an object in a finite semisimple abelian category form a finitely supported function on SimpleClasses C. They count summands up to isomorphism, independently of the chosen decomposition. No coefficient field, splitness, or finiteness of the endomorphism division rings is required. Equal multiplicities characterize isomorphic objects, and the multiplicities are additive on binary biproducts and vanish exactly on zero objects. A simple object has nonzero multiplicity precisely when it maps nontrivially into the given object.

Uniqueness uses Mathlib's HomOrthogonal.equiv_of_iso: Schur's lemma makes the chosen simple representatives hom orthogonal and their endomorphism rings division rings.

theorem TauCeti.exists_equiv_of_iso_biproduct_simples {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι κ : Type} [Finite ι] [Finite κ] (f : ι → C) (g : κ → C) [∀ (i : ι), CategoryTheory.Simple (f i)] [∀ (j : κ), CategoryTheory.Simple (g j)] (e : ⨁ f ≅ ⨁ g) : ∃ (a : ι ≃ κ), ∀ (i : ι), Nonempty (f i ≅ g (a i))

Two finite decompositions into simple objects have the same summands, up to a bijection of indices and isomorphisms of the corresponding objects.

theorem TauCeti.sum_simpleClasses_eq_of_iso_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι κ : Type} [Fintype ι] [Fintype κ] (f : ι → C) (g : κ → C) [∀ (i : ι), CategoryTheory.Simple (f i)] [∀ (j : κ), CategoryTheory.Simple (g j)] (e : ⨁ f ≅ ⨁ g) : ∑ i : ι, Finsupp.single (SimpleClasses.classOf (f i)) 1 = ∑ j : κ, Finsupp.single (SimpleClasses.classOf (g j)) 1

Counting the simple classes in a decomposition is invariant under isomorphism of its biproduct.

noncomputable def TauCeti.simpleMultiplicities {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] (X : C) : SimpleClasses C →₀ ℕ

The finitely supported function counting the copies of each simple isomorphism class in an object. These are decomposition multiplicities, not dimensions over a coefficient field.

theorem TauCeti.simpleMultiplicities_eq_of_iso_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {ι : Type} [Fintype ι] (f : ι → C) [hf : ∀ (i : ι), CategoryTheory.Simple (f i)] {X : C} (e : X ≅ ⨁ f) : simpleMultiplicities X = ∑ i : ι, Finsupp.single (SimpleClasses.classOf (f i)) 1

Any finite decomposition into simple objects computes the simple multiplicities.

theorem TauCeti.simpleMultiplicities_eq_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {X Y : C} (e : X ≅ Y) : simpleMultiplicities X = simpleMultiplicities Y

Isomorphic objects have the same simple multiplicities.

@[simp]

theorem TauCeti.simpleMultiplicities_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] (X : C) [CategoryTheory.Simple X] : simpleMultiplicities X = Finsupp.single (SimpleClasses.classOf X) 1

A simple object has one copy of its own class and no copies of any other class.

@[simp]

theorem TauCeti.simpleMultiplicities_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] : simpleMultiplicities 0 = 0

The zero object has no simple summands.

theorem TauCeti.simpleMultiplicities_apply_eq_card {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {ι : Type} [Finite ι] (f : ι → C) [∀ (i : ι), CategoryTheory.Simple (f i)] {X : C} (e : X ≅ ⨁ f) (S : SimpleClasses C) : (simpleMultiplicities X) S = Nat.card { i : ι // SimpleClasses.classOf (f i) = S }

The multiplicity of a class is the number of summands of that class in any simple decomposition. In particular, the formula is valid over nonsplit endomorphism division rings.

theorem TauCeti.simpleMultiplicities_apply_classOf_eq_sum {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] {ι : Type} [Fintype ι] (f : ι → C) [∀ (i : ι), CategoryTheory.Simple (f i)] {X : C} (e : X ≅ ⨁ f) (S : C) [CategoryTheory.Simple S] : (simpleMultiplicities X) (SimpleClasses.classOf S) = ∑ i : ι, if Nonempty (S ≅ f i) then 1 else 0

The multiplicity of a simple object is the sum of the indicators that it is isomorphic to each summand in any simple decomposition.

theorem TauCeti.nonempty_iso_iff_simpleMultiplicities_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] (X Y : C) : Nonempty (X ≅ Y) ↔ simpleMultiplicities X = simpleMultiplicities Y

Simple multiplicities classify objects of a finite semisimple category up to isomorphism.

@[simp]

theorem TauCeti.simpleMultiplicities_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] (X Y : C) : simpleMultiplicities (X ⊞ Y) = simpleMultiplicities X + simpleMultiplicities Y

Simple multiplicities are additive on binary biproducts.

@[simp]

theorem TauCeti.simpleMultiplicities_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] (X : C) : simpleMultiplicities X = 0 ↔ CategoryTheory.Limits.IsZero X

An object has no simple summands exactly when it is a zero object.

theorem TauCeti.simpleMultiplicities_apply_classOf_ne_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [IsFiniteSemisimpleCategory C] (X S : C) [CategoryTheory.Simple S] : (simpleMultiplicities X) (SimpleClasses.classOf S) ≠ 0 ↔ ∃ (f : S ⟶ X), f ≠ 0

A simple object occurs with nonzero multiplicity precisely when it maps nontrivially into an object. The multiplicity counts copies over the endomorphism division ring, not over a chosen coefficient field.