Modules over a simple Artinian ring are classified by their dimension

Over a simple Artinian ring R all simple modules are isomorphic: Mathlib records this as IsSimpleRing.isIsotypic, which says that any two simple submodules of any R-module are isomorphic. A semisimple module is a direct sum of simple ones, so a finitely generated R-module is Sⁿ for a fixed simple module S and a single natural number n, and n is the only invariant there is.

This file turns that into the working statement: if R is moreover an algebra over a field K and M, N are R-modules which are finite-dimensional over K, then

M ≃ₗ[R] N ↔ finrank K M = finrank K N.

The dimension count is the bookkeeping that converts "the same number of simple summands" into a condition that can be checked, and it is what makes the classification usable: two R-module structures put on the same finite-dimensional K-vector space are automatically isomorphic. That is exactly the input the Skolem-Noether theorem needs, in TauCeti/Algebra/CentralSimple/SkolemNoether.lean.

Main results

• TauCeti.IsIsotypicOfType.of_isSimpleRing: over a simple Artinian ring, every module is isotypic of the type of any fixed simple module. This upgrades Mathlib's IsSimpleRing.isIsotypic, which compares simple submodules of a single module, to a comparison against a fixed simple module, which is what lets two different modules be compared with each other.
• TauCeti.IsSimpleRing.nonempty_linearEquiv_of_finrank_eq: two finite-dimensional modules over a finite-dimensional simple K-algebra with the same K-dimension are isomorphic.
• TauCeti.IsSimpleRing.nonempty_linearEquiv_iff_finrank_eq: the two-way form, the classification itself.

Implementation notes

The simple module the classification compares M and N against is a minimal left ideal S : Submodule R R, produced as an atom of the lattice of submodules of the regular module rather than assumed. Taking it inside R rather than inside M is what makes it available to M and N at once, and it inherits the K-module structure from R, so its dimension is finite and nonzero and can be cancelled.

The two classification statements ask R to be finite-dimensional over K and do not also ask it to be Artinian: IsArtinianRing.of_finite derives that from finite-dimensionality, so callers never have to supply it. Only TauCeti.IsIsotypicOfType.of_isSimpleRing, which has no field in sight, takes IsArtinianRing R as a hypothesis.

Simplicity of R is not weakened to semisimplicity: over a semisimple ring with more than one block the dimension is not a complete invariant, since a module can distribute the same total dimension over the blocks in different ways.

References

This supplies the classification of modules over a simple Artinian ring used by the Layer 5 target skolemNoether of the semisimple algebras roadmap. See T. Y. Lam, A First Course in Noncommutative Rings, GTM 131, Chapter 1, and R. S. Pierce, Associative Algebras, GTM 88, Chapter 3.

theorem TauCeti.IsIsotypicOfType.of_isSimpleRing (R : Type u_1) [Ring R] [IsSimpleRing R] [IsArtinianRing R] (S : Type u_2) [AddCommGroup S] [Module R S] [IsSimpleModule R S] (M : Type u_3) [AddCommGroup M] [Module R M] : IsIsotypicOfType R M S

Over a simple Artinian ring R, every R-module is isotypic of the type of any fixed simple module S: every simple submodule of every R-module is isomorphic to S.

Mathlib's IsSimpleRing.isIsotypic compares two simple submodules of one and the same module. The content added here is that the comparison can be made against a simple module fixed once and for all, so that simple submodules of different modules become comparable: because R is semisimple, a simple submodule of M and S itself are both isomorphic to ideals of R, and those two ideals are isomorphic because R is isotypic over itself.

theorem TauCeti.IsSimpleRing.nonempty_linearEquiv_of_finrank_eq {R : Type u_1} [Ring R] [IsSimpleRing R] (K : Type u_2) [Field K] [Algebra K R] [FiniteDimensional K R] {M : Type u_3} [AddCommGroup M] [Module K M] [Module R M] [IsScalarTower K R M] [FiniteDimensional K M] {N : Type u_4} [AddCommGroup N] [Module K N] [Module R N] [IsScalarTower K R N] [FiniteDimensional K N] (h : Module.finrank K M = Module.finrank K N) : Nonempty (M ≃ₗ[R] N)

Modules over a simple Artinian algebra are classified by their dimension. If R is a finite-dimensional simple K-algebra and M, N are R-modules which are finite-dimensional over K, then equal K-dimension forces an R-linear isomorphism.

Both modules are direct sums of copies of one and the same simple module S (TauCeti.IsIsotypicOfType.of_isSimpleRing), say Sⁿ and Sᵐ; comparing dimensions gives n * finrank K S = m * finrank K S, and finrank K S ≠ 0, so n = m.

theorem TauCeti.IsSimpleRing.nonempty_linearEquiv_iff_finrank_eq {R : Type u_1} [Ring R] [IsSimpleRing R] (K : Type u_2) [Field K] [Algebra K R] [FiniteDimensional K R] {M : Type u_3} [AddCommGroup M] [Module K M] [Module R M] [IsScalarTower K R M] [FiniteDimensional K M] {N : Type u_4} [AddCommGroup N] [Module K N] [Module R N] [IsScalarTower K R N] [FiniteDimensional K N] : Nonempty (M ≃ₗ[R] N) ↔ Module.finrank K M = Module.finrank K N

The classification of finite-dimensional modules over a simple Artinian algebra: the K-dimension is a complete invariant. The forward implication holds over any ring; the content is the converse, TauCeti.IsSimpleRing.nonempty_linearEquiv_of_finrank_eq.