Uniqueness of Wedderburn blocks

Artin--Wedderburn presents a semisimple ring as a finite product of matrix rings over division rings. RingEquiv.wedderburn_blocks_unique proves that two such presentations have the same matrix sizes and division rings after one permutation of the blocks. More generally, it compares products over arbitrary index sets, with each matrix block indexed by any finite nonempty type; the products themselves need not be semisimple.

The generic factor matching in RingEquiv.exists_equiv_factors permutes the factors of the two products. The single-block classification TauCeti.nonempty_ringEquiv_matrix_iff then identifies the matrix size and coefficient division ring of each matched pair.

Main results

• RingEquiv.wedderburn_blocks_unique: two products of matrix rings over division rings with finite nonempty row indices have matching degrees and coefficients after a permutation of blocks.

References

See T. Y. Lam, A First Course in Noncommutative Rings, GTM 131, section 3, or C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, section 26.

theorem RingEquiv.wedderburn_blocks_unique {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} {D : ι → Type u_4} {E : κ → Type u_5} [(i : ι) → DivisionRing (D i)] [(j : κ) → DivisionRing (E j)] {m : ι → Type u_6} {n : κ → Type u_7} [(i : ι) → Fintype (m i)] [(j : κ) → Fintype (n j)] [∀ (i : ι), Nonempty (m i)] [∀ (j : κ), Nonempty (n j)] (f : R ≃+* ((i : ι) → Matrix (m i) (m i) (D i))) (g : R ≃+* ((j : κ) → Matrix (n j) (n j) (E j))) : ∃ (σ : ι ≃ κ), ∀ (i : ι), Fintype.card (m i) = Fintype.card (n (σ i)) ∧ Nonempty (D i ≃+* E (σ i))

Uniqueness of every block in a product of matrix rings over division rings. Two such presentations differ only by a permutation of the blocks: corresponding matrix sizes agree and their coefficient division rings are isomorphic. The block index sets are arbitrary; each matrix index type is finite and nonempty.

The nonemptiness hypotheses are essential. A zero-size matrix ring is trivial and can be inserted with arbitrary coefficients without changing the product.