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.

A finitely generated semisimple module is a finite direct sum of simple modules

Statement

Every finitely generated semisimple module is a finite direct sum of simple modules. See Semisimple modules as direct sums of simple modules.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

A left $R$ -module is semisimple when it is an internal direct sum of simple submodules, allowing the empty direct sum. Hence the zero module is semisimple. (Semisimple modules as direct sums of simple modules).

[L2]

Let $M$ be a left $R$ -module and $S \subseteq M$ . The submodule generated by $S$ is $⟨ S ⟩_{R} : = ⋂ {N \leq M : S \subseteq N} .$ The family is nonempty because $M \leq M$ , and its intersection is a submodule by lem-submodule-criterion-sums-and-intersections. Thus $⟨ S ⟩_{R}$ is the smallest submodule of $M$ containing $S$ , just as def-generated-subgroup defines a generated subgroup. (Generated submodule, cyclic and finitely generated modules, module basis and free module).

Proof

technique · direct

1.1

In a direct-sum decomposition, each generator has finite support; the union of those finite supports contains every generator and hence the whole module.

L1L2givenalgebra

2.1

The finite subfamily located in step 1.1 already consists of simple summands of the original internal direct sum, so no summand is zero and no index repeats; its internal sum is therefore a finite direct sum of simple modules, and by step 1.1 it is all of $M$ . For a module generated by the empty set, $M = ⟨ \emptyset ⟩_{R} = 0$ , which is the empty direct sum and semisimple by [L1]. This proves the stated claim.

step 1.1L1L2givenalgebra∎

Depends on

Used by

Semisimple rings are left and right Noetherian and Artinian Corollary
Wedderburn–Artin theorem for semisimple rings Theorem

Dependency tree · next 3 levels

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

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