CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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.

Left and right semisimplicity of a ring agree

Statement

A unital ring is semisimple as a left regular module if and only if it is semisimple as a right regular module. See Wedderburn–Artin theorem for semisimple rings.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

A unital ring $R$ is semisimple when its left regular module $_{R} R$ is semisimple; the zero ring is semisimple because its regular module is zero. (A semisimple ring as a ring whose left regular module is semisimple).

[L2]

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}$ . (Wedderburn–Artin theorem for semisimple rings).

[L3]

For a unital ring $R$ , the opposite ring $R^{o p}$ has the same underlying abelian group, identity, and addition as $R$ , with multiplication $a ⋆ b : = b a$ . Associativity and both distributive laws follow from those of $R$ with the order reversed, and the same element $1$ is a two-sided identity. Thus the displayed operations really form a unital ring, including when $R$ is the zero ring. (The opposite ring $R^{o p}$ ).

[L4]

For a division ring $D$ and $n \geq 1$ , the ring $M_{n} (D)$ is semisimple and its left regular module is a finite direct sum of simple column ideals. (Matrix rings over division rings are semisimple).

Proof

technique · direct

1.1L1L2given

First suppose that $R$ is semisimple on the left. If $R$ is the zero ring, its right regular module is also the zero module and is semisimple. Otherwise [L2] gives $R ≅ \prod_{i} M_{n_{i}} (D_{i})$ .

2.1L3L4step 1.1givenalgebra

By [L4], it suffices to identify the opposite factors as matrix rings over division rings. Each $D_{i}^{o p}$ is a division ring, and entrywise transpose defines a ring isomorphism $M_{n_{i}} (D_{i})^{o p} ⟶ M_{n_{i}} (D_{i}^{o p}), A ⟼ A^{T},$ because $(A B)^{T} = B^{T} A^{T}$ with the products interpreted in the indicated rings. Hence $R^{o p} ≅ \prod_{i} M_{n_{i}} (D_{i}^{o p})$ . By [L4], each factor's left regular module is semisimple, and the regular module of the finite product is their finite direct sum. Thus $R^{o p}$ is left semisimple, equivalently $R$ is right semisimple.

3.1L3step 1.1step 2.1givenalgebra∎

Conversely, if $R$ is right semisimple, then $R^{o p}$ is left semisimple. Applying steps 1.1–2.1 to $R^{o p}$ makes it right semisimple, which is exactly left semisimplicity of $R$ . This also retains the zero-ring case.

Depends on

Used by

Semisimple rings are left and right Noetherian and Artinian Corollary

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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