TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Wedderburn–Artin theorem for semisimple rings

Statement

Let $R$ be a nonzero unital ring. Then $R$ is semisimple if and only if $R ≅ \prod_{i = 1}^{r} M_{n_{i}} (D_{i})$ for positive integers $r, n_{i}$ and division rings $D_{i}$ . See ${End}_{R} (_{R} R) ≅ R^{o p}$ .

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

For every unital ring $R$ , evaluation at $1$ identifies endomorphisms of the left regular module with right multiplications and gives a ring isomorphism ${End}_{R} (_{R} R) ≅ R^{o p} .$ . ( ${End}_{R} (_{R} R) ≅ R^{o p}$ ).

[L2]

For left $R$ -modules $M_{1}, \dots, M_{n}$ , endomorphisms of $⨁_{j} M_{j}$ correspond to matrices $(f_{i j})$ with $f_{i j} \in {Hom}_{R} (M_{j}, M_{i})$ , and composition is matrix multiplication using composition in the entries. (Endomorphisms of a finite direct sum are matrices of Hom-groups).

[L3]

Every finitely generated semisimple module is a finite direct sum of simple modules. (A finitely generated semisimple module is a finite direct sum of simple modules).

[L4]

A nonzero homomorphism between simple modules is an isomorphism. Consequently the endomorphism ring of a simple module is a division ring. (Schur's lemma for simple modules).

[L5]

For a division ring $D$ and $n \geq 1$ , matrices with product $(A B)_{i j} = \sum_{k} a_{i k} b_{k j}$ form a semisimple ring whose left regular module is the direct sum of its simple column ideals. (Matrix rings over division rings are semisimple).

[L6]

The opposite ring $R^{o p}$ has the same addition and identity as $R$ and multiplication $a ⋆ b : = b a$ . (The opposite ring $R^{o p}$ ).

[L7]

A unital ring $R$ is semisimple when its left regular module $_{R} R$ is semisimple. This is a left-module definition and uses no Jacobson radical. For the zero ring, the regular module is zero and hence semisimple; the Wedderburn-Artin theorem below is stated for nonzero rings. (A semisimple ring as a ring whose left regular module is semisimple).

Proof

technique · direct

1.1

If $R$ is semisimple, its cyclic left regular module is a finite direct sum of simple modules. Grouping isomorphic summands gives $_{R} R ≅ ⨁_{i = 1}^{r} S_{i}^{n_{i}}$ with pairwise nonisomorphic $S_{i}$ and positive $r, n_{i}$ .

L1L2L3L4L5L6L7givenalgebra

2.1

Schur's lemma gives ${Hom}_{R} (S_{j}, S_{i}) = 0$ for $i \neq j$ and makes $E_{i} = {End}_{R} (S_{i})$ a division ring. Hence the endomorphism-matrix theorem gives ${End}_{R} (_{R} R) ≅ \prod_{i} M_{n_{i}} (E_{i})$ .

step 1.1givenalgebra

3.1

Since ${End}_{R} (_{R} R) ≅ R^{o p}$ , taking opposites gives $R ≅ \prod_{i} M_{n_{i}} (E_{i})^{o p}$ . The opposite $E_{i}^{o p}$ is again a division ring, and entrywise transpose is a ring isomorphism $M_{n_{i}} (E_{i})^{o p} ⟶ M_{n_{i}} (E_{i}^{o p}), A ⟼ A^{T},$ because reversing both the matrix product and the entry product gives $(B A)^{T} = A^{T} B^{T}$ in the target. Thus $R ≅ \prod_{i} M_{n_{i}} (D_{i})$ with $D_{i} = E_{i}^{o p}$ .

L5L6step 2.1givenalgebra

4.1

Conversely, each $M_{n_{i}} (D_{i})$ is semisimple by its column-ideal decomposition, and a finite product is semisimple because its regular module is the finite direct sum of the factors' regular modules.

step 3.1givenalgebra

5.1

The Statement assumes that $R$ is nonzero, so the decomposition has at least one factor; no empty-product convention is asserted. This proves the stated claim.

step 4.1givenalgebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

William Crawley-Boevey, Noncommutative Algebra, Chapter 1 Sections 1.1-1.9 (standard reference, not scraped)