Isomorphisms between products of simple rings

A ring isomorphism between arbitrary products of simple rings induces an equivalence of their index sets and isomorphisms between the matched factors. The original isomorphism acts coordinatewise through these factor isomorphisms, including on elements with infinite support.

A coordinate central idempotent δᵢ is primitive among central idempotents: the only central idempotents e satisfying e * δᵢ = e are 0 and δᵢ. A ring isomorphism therefore carries δᵢ to exactly one coordinate central idempotent. Applying the inverse isomorphism gives a bijection of the indices. Multiplying an arbitrary product element by δᵢ then identifies its image at the matched coordinate and gives the factor isomorphism. The central-idempotent dichotomy used here is TauCeti.centralIdempotents_eq_pair.

No finiteness or semisimplicity hypothesis is needed. In particular, this applies to genuinely infinite products. The matrix-block specialization for Wedderburn presentations is RingEquiv.card_blocks_eq in TauCeti/RingTheory/Semisimple/BlockCount.lean.

Main results

• RingEquiv.exists_equiv_factors: an isomorphism between products of simple rings acts coordinatewise through an equivalence of their index sets and matched factor isomorphisms.
• RingEquiv.card_eq_of_pi_of_isSimpleRing: two presentations of a ring as products of simple rings have equal Nat.card of their index sets.

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.exists_equiv_factors {ι : Type u} {κ : Type v} {A : ι → Type w} {B : κ → Type x} [(i : ι) → Ring (A i)] [∀ (i : ι), IsSimpleRing (A i)] [(j : κ) → Ring (B j)] [∀ (j : κ), IsSimpleRing (B j)] (f : ((i : ι) → A i) ≃+* ((j : κ) → B j)) : ∃ (σ : ι ≃ κ), ∀ (i : ι), ∃ (e : A i ≃+* B (σ i)), ∀ (a : (i : ι) → A i), f a (σ i) = e (a i)

A ring isomorphism between products of simple rings permutes their factors.

The returned factor isomorphisms describe the original isomorphism coordinatewise: the value at σ i of the image of any product element depends only on its value at i. The images of the coordinate central idempotents determine σ, even when some factors are isomorphic. No finiteness or decidable-equality assumption on either index set is needed.

theorem RingEquiv.card_eq_of_pi_of_isSimpleRing {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} {A : ι → Type u_4} {B : κ → Type u_5} [(i : ι) → Ring (A i)] [∀ (i : ι), IsSimpleRing (A i)] [(j : κ) → Ring (B j)] [∀ (j : κ), IsSimpleRing (B j)] (f : R ≃+* ((i : ι) → A i)) (g : R ≃+* ((j : κ) → B j)) : Nat.card ι = Nat.card κ

Two presentations of a ring as products of simple rings have equal Nat.card of their index sets. In particular, two finite products have the same number of factors.

The index sets are in fact equivalent, by RingEquiv.exists_equiv_factors.