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

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

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.

L1L2givenalgebra

2.1

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.

step 1.1givenalgebra

3.1

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.

step 2.1givenalgebra∎

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: 20 results over 8 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)