ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

A product of two fields is semisimple with two simple-module types

Example

For fields $F$ and $K$ , the ring $F \times K$ is semisimple. Its simple left modules are, up to isomorphism, $F$ supported on the first factor and $K$ supported on the second. See Wedderburn–Artin theorem for semisimple rings.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

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

Verification

technique · direct

1.1L1L2givenalgebra

The central idempotents $e_{F} = (1, 0)$ and $e_{K} = (0, 1)$ satisfy $e_{F} + e_{K} = 1$ and $e_{F} e_{K} = 0$ . Thus the regular module splits as the direct sum of the simple left ideals $F \times 0$ and $0 \times K$ , proving semisimplicity.

2.1step 1.1givenalgebra

For every left module $M$ , one has $M = e_{F} M \oplus e_{K} M$ . If $M$ is simple, exactly one summand is nonzero; it is then a simple vector space over the corresponding field and hence isomorphic to $F$ on the first factor or $K$ on the second.

3.1step 2.1givenalgebra∎

Even when $F ≅ K$ as fields, the two modules are not isomorphic as $F \times K$ -modules because $e_{F}$ acts as the identity on one and as zero on the other. This proves the stated claim.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

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