The endomorphism algebra of a module over a simple Artinian algebra

Let K be a field, let R be a finite-dimensional simple K-algebra and let M be an R-module which is finite-dimensional over K. All simple R-modules are isomorphic, to a fixed minimal left ideal S, and M is a direct sum of k copies of S (TauCeti.IsIsotypicOfType.of_isSimpleRing), so

End_R M ≃ₐ[K] Mat_k(End_R S),

a matrix algebra over the division algebra End_R S supplied by Schur's lemma. Two consequences are recorded here: End_R M is again a simple ring when M ≠ 0, and its dimension satisfies

finrank K (End_R M) * finrank K R = (finrank K M)².

Only the dimension identity needs the field: simplicity of End_R M is stated with no K in sight, for a nonzero module M finite over a simple Artinian ring R.

The dimension identity is what makes End_R M computable without naming S, k or the division algebra: writing finrank K S = s, finrank K M = k * s and finrank K R = m * s, the matrix presentation gives finrank K (End_R M) = k² * d and finrank K (End_R R) = m² * d for d = finrank K (End_R S). Since End_R R is R itself, the second identity reads m * s = m² * d and pins s = m * d; substituting turns the first into the displayed formula, in which S, k, m and d have all disappeared.

Applied to R = B ⊗[K] Aᵐᵒᵖ acting on a simple algebra A containing a central simple subalgebra B, whose endomorphism algebra is the centralizer of B, this is the engine of the centralizer theorem in TauCeti/Algebra/CentralSimple/Centralizer.lean.

Main results

• TauCeti.IsSimpleRing.finrank_end_mul_finrank_eq_sq: the dimension identity finrank K (End_R M) * finrank K R = (finrank K M)².
• TauCeti.IsSimpleRing.moduleEnd: End_R M is a simple ring, for M a nonzero module finite over a simple Artinian ring R.

Implementation notes

The simple module S that both M and the regular module R are compared against is taken to be a minimal left ideal of R, exactly as in TauCeti/RingTheory/Semisimple/SimpleArtinian.lean: taking it inside R is what lets the same S serve both, which is what makes the two matrix presentations comparable and lets d = finrank K (End_R S) cancel.

Simplicity of R is not weakened to semisimplicity. Over a semisimple ring with several blocks End_R M is a product of matrix algebras, hence simple only when M is isotypic, and the dimension identity fails: for R = K × K and M = K × 0, End_R M is K, so the left-hand side is 1 * 2 = 2 while (finrank K M)² = 1.

References

This supplies the module-theoretic engine of the Layer 5 centralizer theorem of the semisimple algebras roadmap. See R. S. Pierce, Associative Algebras, GTM 88, Chapter 12, and T. Y. Lam, A First Course in Noncommutative Rings, GTM 131, Chapter 1.

theorem TauCeti.IsSimpleRing.moduleEnd {R : Type u_1} [Ring R] [IsSimpleRing R] [IsArtinianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : IsSimpleRing (Module.End R M)

The endomorphism ring of a nonzero finite module over a simple Artinian ring is simple. It is the matrix ring Mat_k(End_R S) over the division ring of Schur's lemma, with k ≠ 0 because M ≠ 0.

No base field is involved: M is a power Sᵏ of a minimal left ideal S of R because R is simple Artinian and M is finite over R. That is the only use made of simplicity of R, so this is the specialization of TauCeti.isSimpleRing_moduleEnd_of_isIsotypic along IsSimpleRing.isIsotypic.

theorem TauCeti.IsSimpleRing.finrank_end_mul_finrank_eq_sq (K : Type u_1) [Field K] {R : Type u_2} [Ring R] [IsSimpleRing R] [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] : Module.finrank K (Module.End R M) * Module.finrank K R = Module.finrank K M ^ 2

The dimension of the endomorphism algebra of a module over a simple Artinian algebra. For a finite-dimensional simple K-algebra R and an R-module M finite-dimensional over K,

finrank K (End_R M) * finrank K R = (finrank K M)².

Both sides are k² * m² * d² in the notation of the module docstring: M is Sᵏ and R is Sᵐ for a minimal left ideal S with finrank K S = m * d, where d = finrank K (End_R S).

The identity determines finrank K (End_R M) outright, since finrank K R ≠ 0; it is stated as a product rather than a quotient to stay inside ℕ.