The center bounds the number of simple modules of a semisimple algebra

A semisimple ring R has finitely many isomorphism classes of simple modules, indexed by the isotypic components of the regular module (TauCeti.simpleSubmoduleClassesEquiv). When R is an algebra over a field k with finite-dimensional center, this file bounds that number by the dimension of the center:

Nat.card (isotypicComponents R R) ≤ Module.finrank k (Subalgebra.center k R).

The bound is the counting half of Artin-Wedderburn, obtained without choosing a presentation R ≃+* ∏ᵢ Matₙᵢ(Dᵢ): for such a product the center is ∏ᵢ Z(Dᵢ), of dimension at least the number of blocks, and the argument here says exactly that intrinsically. Where RingEquiv.card_blocks_eq compares two presentations, this bound mentions none.

The mechanism is that each isotypic component of the regular module contains a nonzero central element (TauCeti.exists_ne_zero_mem_center_of_mem_isotypicComponents). Writing 1 = ∑_c e_c along the decomposition of R into its isotypic components, the summand e_c is central because for z : R the two decompositions z = ∑_c z * e_c and z = ∑_c e_c * z have their c-th terms in the same summand: the first because c is a left ideal, the second because an isotypic component of the regular module is two-sided (TauCeti.isTwoSided_of_mem_isotypicComponents, Mathlib's isFullyInvariant_iff_isTwoSided read on isotypicComponents R R). It is nonzero because the same uniqueness gives x * e_c = x for x ∈ c. Elements chosen one from each summand of an independent family are linearly independent, so the components are at most as many as the dimension of the center.

Nothing here needs R itself to be finite-dimensional: only the center is assumed finite as a k-module, which is what a group algebra supplies through its class-sum basis. The central-element construction works over any commutative semiring of scalars.

Main results

• TauCeti.isTwoSided_of_mem_isotypicComponents: an isotypic component of the regular module is a two-sided ideal.
• TauCeti.exists_ne_zero_mem_center_of_mem_isotypicComponents: it contains a nonzero central element.
• TauCeti.card_isotypicComponents_le_finrank_center: the number of isotypic components of the regular module is at most the dimension of the center.

References

• T. Y. Lam, A First Course in Noncommutative Rings, GTM 131, §3.
• C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §25.

theorem TauCeti.isTwoSided_of_mem_isotypicComponents {R : Type u_1} [Ring R] {c : Ideal R} (hc : c ∈ isotypicComponents R R) : c.IsTwoSided

An isotypic component of the regular module is a two-sided ideal. Mathlib's Submodule.IsFullyInvariant.of_mem_isotypicComponents makes it invariant under every endomorphism of the regular module, and those endomorphisms are the right multiplications.

theorem TauCeti.exists_ne_zero_mem_center_of_mem_isotypicComponents (k : Type u_2) (R : Type u_3) [CommSemiring k] [Ring R] [Algebra k R] [IsSemisimpleRing R] {c : Submodule R R} (hc : c ∈ isotypicComponents R R) : ∃ e ∈ c, e ≠ 0 ∧ e ∈ Subalgebra.center k R

Every isotypic component of the regular module contains a nonzero central element. It is the corresponding summand of the decomposition of 1; only these two properties are recorded, being all that the dimension count below consumes.

theorem TauCeti.card_isotypicComponents_le_finrank_center (k : Type u_2) (R : Type u_3) [Field k] [Ring R] [Algebra k R] [IsSemisimpleRing R] [Module.Finite k ↥(Subalgebra.center k R)] : Nat.card ↑(isotypicComponents R R) ≤ Module.finrank k ↥(Subalgebra.center k R)

The center bounds the number of isomorphism classes of simple modules. Over a semisimple k-algebra whose center is finite-dimensional, the isotypic components of the regular module, which TauCeti.simpleSubmoduleClassesEquiv identifies with the isomorphism classes of simple modules, are at most as many as the dimension of the center.

For a group algebra the right-hand side is the number of conjugacy classes, by TauCeti.finrank_center_monoidAlgebra.