TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Uniqueness of the Wedderburn–Artin factors

Statement

The division rings and matrix sizes in a Wedderburn-Artin decomposition of a nonzero semisimple ring are unique up to permutation and division-ring isomorphism. See Wedderburn–Artin theorem for semisimple rings.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

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).

[L2]

For $r \geq 1$ , $n_{i} \geq 1$ , and division rings $D_{i}$ , every simple left module over $\prod_{i} M_{n_{i}} (D_{i})$ is supported on exactly one factor and is isomorphic to that factor's column module $D_{i}^{n_{i}}$ ; these give all isomorphism classes. (Simple modules over a product of matrix rings over division rings).

[L3]

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

[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]

Any two composition series of a module have the same length, and their simple factors agree up to permutation and isomorphism. (Jordan–Hölder theorem for modules).

Proof

technique · direct

1.1

In a decomposition $R ≅ \prod_{i} M_{n_{i}} (D_{i})$ , the simple left module supported on factor $i$ is its column module $S_{i} = D_{i}^{n_{i}}$ . Distinct coordinate idempotents show that the $S_{i}$ are pairwise nonisomorphic as $R$ -modules, and [L3] decomposes the regular module with exactly $n_{i}$ copies of $S_{i}$ .

L1L2L3L4L5givenalgebra

2.1

Let $f : S_{i} \to S_{i}$ commute with the matrix action and put $v = f (e_{1})$ . For $k \neq 1$ , the matrix unit $e_{k k}$ annihilates $e_{1}$ , so it annihilates $v$ ; hence $v = e_{1} d$ for a unique $d \in D_{i}$ . Since $e_{j} = e_{j 1} e_{1}$ , one has $f (e_{j}) = e_{j 1} f (e_{1}) = e_{j} d$ , and additivity then gives $f (x) = x d$ for every column $x$ . Thus the endomorphisms are precisely right scalar multiplications, composition reverses the scalar order, and ${End}_{R} (S_{i}) ≅ D_{i}^{o p}$ . Therefore $D_{i} ≅ {End}_{R} (S_{i})^{o p}$ is determined by the simple-module type with the orientation fixed.

L3L4step 1.1givenalgebra

3.1

Jordan–Hölder [L5] makes the simple-module types and their multiplicities in $_{R} R$ invariant. Hence the pairs $(n_{i}, D_{i})$ are determined up to reordering and division-ring isomorphism. This proves the stated claim.

L5step 1.1step 2.1given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 45 results over 18 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

MIT 18.706, Lecture 2: Semisimple Modules, Socles, Artinian Rings, Wedderburn's Theorem (standard reference, not scraped)