Invariance of the number of matrix blocks

Artin--Wedderburn presents a semisimple ring R as a finite product of positive-size matrix algebras over division rings. RingEquiv.card_blocks_eq compares any two such presentations: the number of blocks is an invariant of the ring.

Simplicity of the coefficient rings is all the argument uses. Positivity of the matrix sizes is essential: a zero-size matrix algebra is trivial, so any presentation could be padded with such blocks. These are the same NeZero hypotheses produced by IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing. Semisimplicity of R guarantees a Wedderburn presentation exists, but is not needed to compare presentations.

The underlying factor matching and cardinality invariance for arbitrary products of simple rings are RingEquiv.exists_equiv_factors and RingEquiv.card_eq_of_pi_of_isSimpleRing in TauCeti/RingTheory/SimpleRing/Pi.lean. The finer uniqueness of the matrix sizes and division rings is RingEquiv.wedderburn_blocks_unique in TauCeti/RingTheory/Semisimple/Wedderburn/Uniqueness.lean, which applies TauCeti.nonempty_ringEquiv_matrix_iff to the matched matrix blocks.

Main results

• RingEquiv.card_blocks_eq: two presentations as finite products of positive-size matrix algebras over simple rings have the same number of blocks.

References

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

theorem RingEquiv.card_blocks_eq {R : Type u_1} [Ring R] {m n : ℕ} {D : Fin m → Type u_2} {D' : Fin n → Type u_3} [(i : Fin m) → Ring (D i)] [∀ (i : Fin m), IsSimpleRing (D i)] [(i : Fin n) → Ring (D' i)] [∀ (i : Fin n), IsSimpleRing (D' i)] {d : Fin m → ℕ} {d' : Fin n → ℕ} [∀ (i : Fin m), NeZero (d i)] [∀ (i : Fin n), NeZero (d' i)] (f : R ≃+* ((i : Fin m) → Matrix (Fin (d i)) (Fin (d i)) (D i))) (g : R ≃+* ((i : Fin n) → Matrix (Fin (d' i)) (Fin (d' i)) (D' i))) : m = n

Invariance of the block count. Two presentations of the same ring as finite products of positive-size matrix algebras over simple rings have the same number of blocks.

This applies in particular to two Wedderburn presentations. The NeZero hypotheses are essential: a zero-size matrix algebra is trivial, so any presentation could be padded with empty blocks. Semisimplicity of R guarantees a Wedderburn presentation exists, but is not needed here.