Wedderburn blocks enumerate the simple modules

Artin--Wedderburn presents a semisimple ring R as a finite product of matrix algebras over division rings,

R ≃+* ∏ᵢ Matₙᵢ(Dᵢ),

and RingEquiv.card_blocks_eq shows that the number of factors does not depend on the presentation. That count is anonymous: it is read off the central idempotents and says nothing about what a block is. This file identifies the index: the blocks of any such presentation correspond to the isomorphism classes of simple R-modules, so a presentation with n blocks exhibits exactly n simple modules up to isomorphism, and every simple module is one of them.

The bridge between the two descriptions is the endomorphism ring of the regular module. Mathlib's IsSemisimpleModule.endRingEquiv splits End_R R along the isotypic components of R,

Rᵐᵒᵖ ≃+* End_R R ≃+* ∏_{c} End_R c,

and each factor is a simple ring, because an isotypic component is a finite power of one simple module and so has a matrix endomorphism ring (TauCeti.isSimpleRing_moduleEnd_of_isIsotypic). A presentation R ≃+* ∏ᵢ Aᵢ by simple rings gives a second such product decomposition of Rᵐᵒᵖ, so RingEquiv.exists_equiv_factors matches the two index types. Composing with TauCeti.simpleSubmoduleClassesEquiv, which identifies the isotypic components of R with the isomorphism classes of simple left ideals, and with TauCeti.simpleModuleClass, which realizes an abstract simple module by a left ideal, turns the block count into a count of simple modules.

Main results

• RingEquiv.card_isotypicComponents_eq_of_pi: a presentation of R as a product of simple rings indexed by any type has as many factors as R has isotypic components.
• RingEquiv.card_simpleSubmoduleClasses_eq_of_pi: such a presentation has as many factors as there are isomorphism classes of simple R-modules.
• RingEquiv.nonempty_equiv_simpleSubmoduleClasses_of_pi: the factors of a presentation indexed by any type are in bijection with the isomorphism classes of simple R-modules.
• RingEquiv.exists_simpleSubmodule_of_pi: the blocks enumerate the simple modules. A presentation of R by simple rings indexed by ι yields a family of simple left ideals indexed by ι, pairwise non-isomorphic, with every simple left ideal isomorphic to one of them.
• RingEquiv.exists_simpleSubmodule_of_pi_matrix: the same statement for a Wedderburn presentation R ≃+* ∏ᵢ Matₙᵢ(Dᵢ) indexed by Fin n.
• TauCeti.exists_nonempty_linearEquiv_of_forall_submodule: such a family exhausts not only the simple left ideals but every simple R-module, because over a semisimple ring a simple module is realized by a left ideal.

Implementation notes

The presentation equivalence, family and cardinality results accept arbitrary index types without an explicit finiteness hypothesis. Semisimplicity of R nevertheless forces the index of an actual presentation by nontrivial simple rings to be finite. The general factor theorem in TauCeti/RingTheory/SimpleRing/Pi.lean also applies to genuinely infinite products.

The results are stated for a presentation R ≃+* ∏ᵢ Aᵢ by arbitrary simple rings rather than by matrix algebras: simplicity of the factors is all the argument uses, and Artin--Wedderburn is what supplies such a presentation, not part of the statement. The positivity hypotheses NeZero (d i) of the matrix form enter only to make Matₙᵢ(Dᵢ) simple, exactly as in RingEquiv.card_blocks_eq; a block of size 0 is the trivial ring, and any presentation could be padded with such blocks.

The isomorphism classes are handled through TauCeti.SimpleSubmoduleClasses R R, the classes of simple left ideals, which unlike the classes of abstract simple modules form a type. The exhaustion clause of RingEquiv.exists_simpleSubmodule_of_pi is likewise stated for left ideals, and TauCeti.exists_nonempty_linearEquiv_of_forall_submodule upgrades it to arbitrary simple modules in any universe; keeping the two apart is what lets the main statement stay universe-monomorphic in the modules it quantifies over.

References

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

theorem RingEquiv.nonempty_equiv_simpleSubmoduleClasses_of_pi {R : Type u} [Ring R] [IsSemisimpleRing R] {ι : Type u_1} {A : ι → Type v} [(i : ι) → Ring (A i)] [∀ (i : ι), IsSimpleRing (A i)] (e : R ≃+* ((i : ι) → A i)) : Nonempty (ι ≃ TauCeti.SimpleSubmoduleClasses R R)

The factors of a presentation of a semisimple ring by simple rings indexed by any type are in bijection with the isomorphism classes of simple modules.

Match the given decomposition of Rᵐᵒᵖ with its decomposition along the isotypic components of the regular module, then identify those components with the isomorphism classes of simple modules.

theorem RingEquiv.card_isotypicComponents_eq_of_pi {R : Type u} [Ring R] [IsSemisimpleRing R] {ι : Type u_1} {A : ι → Type v} [(i : ι) → Ring (A i)] [∀ (i : ι), IsSimpleRing (A i)] (e : R ≃+* ((i : ι) → A i)) : Nat.card ↑(isotypicComponents R R) = Nat.card ι

A presentation of a semisimple ring as a product of simple rings indexed by any type has one factor for each isotypic component of the regular module.

This is the cardinality consequence of matching the given decomposition of Rᵐᵒᵖ with the splitting of End_R R ≃+* Rᵐᵒᵖ along its isotypic components.

theorem RingEquiv.card_simpleSubmoduleClasses_eq_of_pi {R : Type u} [Ring R] [IsSemisimpleRing R] {ι : Type u_1} {A : ι → Type v} [(i : ι) → Ring (A i)] [∀ (i : ι), IsSimpleRing (A i)] (e : R ≃+* ((i : ι) → A i)) : Nat.card (TauCeti.SimpleSubmoduleClasses R R) = Nat.card ι

A presentation of a semisimple ring as a product of simple rings indexed by any type has one factor for each isomorphism class of simple modules.

theorem RingEquiv.exists_simpleSubmodule_of_pi {R : Type u} [Ring R] [IsSemisimpleRing R] {ι : Type u_1} {A : ι → Type v} [(i : ι) → Ring (A i)] [∀ (i : ι), IsSimpleRing (A i)] (e : R ≃+* ((i : ι) → A i)) : ∃ (S : ι → Submodule R R), (∀ (i : ι), IsSimpleModule R ↥(S i)) ∧ (∀ (i j : ι), Nonempty (↥(S i) ≃ₗ[R] ↥(S j)) → i = j) ∧ ∀ (I : Submodule R R), IsSimpleModule R ↥I → ∃ (i : ι), Nonempty (↥I ≃ₗ[R] ↥(S i))

The blocks enumerate the simple modules. A presentation of a semisimple ring R as a product of simple rings indexed by ι produces a family of simple left ideals indexed by ι which are pairwise non-isomorphic and exhaust the simple left ideals up to isomorphism.

Since every simple R-module is isomorphic to a simple left ideal, the family is a complete irredundant list of the simple R-modules; that consequence is TauCeti.exists_nonempty_linearEquiv_of_forall_submodule.

theorem RingEquiv.exists_simpleSubmodule_of_pi_matrix {R : Type u} [Ring R] [IsSemisimpleRing R] {n : ℕ} {D : Fin n → Type v} [(i : Fin n) → DivisionRing (D i)] {d : Fin n → ℕ} [∀ (i : Fin n), NeZero (d i)] (e : R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))) : ∃ (S : Fin n → Submodule R R), (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i j : Fin n), Nonempty (↥(S i) ≃ₗ[R] ↥(S j)) → i = j) ∧ ∀ (I : Submodule R R), IsSimpleModule R ↥I → ∃ (i : Fin n), Nonempty (↥I ≃ₗ[R] ↥(S i))

Blocks enumerate the simple modules, for a Wedderburn presentation R ≃+* ∏ᵢ Matₙᵢ(Dᵢ): the n blocks yield n pairwise non-isomorphic simple left ideals which exhaust the simple left ideals up to isomorphism.

The positivity hypotheses NeZero (d i) are what make the matrix blocks simple rings; they are the same hypotheses that IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing produces and that RingEquiv.card_blocks_eq needs.

The general statement it specializes is RingEquiv.exists_simpleSubmodule_of_pi.

theorem TauCeti.exists_nonempty_linearEquiv_of_forall_submodule {R : Type u} [Ring R] [IsSemisimpleRing R] {κ : Type u_1} {S : κ → Submodule R R} (hS : ∀ (I : Submodule R R), IsSimpleModule R ↥I → ∃ (k : κ), Nonempty (↥I ≃ₗ[R] ↥(S k))) (M : Type u_2) [AddCommGroup M] [Module R M] [IsSimpleModule R M] : ∃ (k : κ), Nonempty (M ≃ₗ[R] ↥(S k))

A family of simple left ideals exhausting the simple left ideals exhausts every simple module. Over a semisimple ring every simple module is isomorphic to a left ideal, so no information is lost by listing only the left ideals; this is what turns the family produced by RingEquiv.exists_simpleSubmodule_of_pi into a list of all the simple R-modules, in any universe.