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.

Simple modules over a product of matrix rings over division rings

Statement

Let $r \geq 1$ , let every $n_{i} \geq 1$ , let every $D_{i}$ be a division ring, and put $R = \prod_{i = 1}^{r} M_{n_{i}} (D_{i})$ . Then every simple left $R$ -module is supported on exactly one factor and is isomorphic to that factor's column module $D_{i}^{n_{i}}$ . These column modules give all simple left $R$ -module isomorphism classes, with one class for each factor. See Wedderburn–Artin theorem for semisimple rings.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

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

[L2]

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

Proof

technique · direct

1.1

Write $c_{i} \in R$ for the central idempotent that is $1$ in factor $i$ and $0$ elsewhere. For a simple left $R$ -module $S$ , every $c_{i} S$ is a submodule and $S = \sum_{i} c_{i} S$ . Hence some $c_{i} S$ is nonzero and therefore equals $S$ ; then $c_{j} S = c_{j} c_{i} S = 0$ for $j \neq i$ . Thus $S$ is supported on exactly one factor $A_{i} = M_{n_{i}} (D_{i})$ .

givenalgebra

2.1

Choose $0 \neq s \in S$ . The map $A_{i} \to S$ , $a \mapsto a s$ , is surjective because its image is a nonzero submodule. By [L2], $A_{i}$ is a direct sum of simple column ideals $C_{j} ≅ D_{i}^{n_{i}}$ . At least one restriction $C_{j} \to S$ is nonzero, so [L1] makes it an isomorphism. Hence $S ≅ D_{i}^{n_{i}}$ .

L1L2step 1.1givenalgebra

3.1

Conversely each column module is simple by [L2]. Modules supported on different factors cannot be isomorphic, because the corresponding $c_{i}$ acts as the identity on one and as zero on the other. For a fixed factor all column ideals are isomorphic to $D_{i}^{n_{i}}$ by [L2]. This proves the classification, including the one-factor case $r = 1$ .

L2step 1.1step 2.1givenalgebra∎

Depends on

Used by

Dependency tree · next 3 levels

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