Alphabeta MathHow 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.
Semisimple rings are left and right Noetherian and Artinian
Statement
Every semisimple ring is left and right Noetherian and left and right Artinian. See A semisimple ring as a ring whose left regular module is semisimple.
Facts & Assumptions
Given: The hypotheses and objects in the Statement.
A unital ring is semisimple when its left regular module is semisimple. This is a left-module definition and uses no Jacobson radical. For the zero ring, the regular module is zero and hence semisimple; the Wedderburn-Artin theorem below is stated for nonzero rings. (A semisimple ring as a ring whose left regular module is semisimple).
Every finitely generated semisimple module is a finite direct sum of simple modules. (A finitely generated semisimple module is a finite direct sum of simple modules).
A module with a composition series is both Noetherian and Artinian. The zero module has the empty composition series. (A module has a composition series if and only if it is Noetherian and Artinian, the converse using dependent choice).
A unital ring is semisimple as a left regular module if and only if it is semisimple as a right regular module. (Left and right semisimplicity of a ring agree).
Proof
The left regular module is cyclic and semisimple, hence a finite direct sum of simples and therefore has finite length.
The finite simple-factor chain in step 1.1 is a composition series, so [L3] gives left Noetherian and Artinian.
By [L4], the right regular module is also semisimple; repeating steps 1.1–2.1 for right modules gives right Noetherian and Artinian. The zero ring is covered by its zero regular modules.
Depends on
- A semisimple ring as a ring whose left regular module is semisimple
- A finitely generated semisimple module is a finite direct sum of simple modules
- A module has a composition series if and only if it is Noetherian and Artinian, the converse using dependent choice
- Left and right semisimplicity of a ring agree
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: 32 results over 10 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
- Arvind Nair, Algebra I, Lecture 5 (standard reference, not scraped)