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.
Left and right semisimplicity of a ring agree
Statement
A unital ring is semisimple as a left regular module if and only if it is semisimple as a right regular module. See Wedderburn–Artin theorem for semisimple rings.
Facts & Assumptions
Given: The hypotheses and objects in the Statement.
A unital ring is semisimple when its left regular module is semisimple; the zero ring is semisimple because its regular module is zero. (A semisimple ring as a ring whose left regular module is semisimple).
Let be a nonzero unital ring. Then is semisimple if and only if for positive integers and division rings . (Wedderburn–Artin theorem for semisimple rings).
For a unital ring , the opposite ring has the same underlying abelian group, identity, and addition as , with multiplication . Associativity and both distributive laws follow from those of with the order reversed, and the same element is a two-sided identity. Thus the displayed operations really form a unital ring, including when is the zero ring. (The opposite ring ).
For a division ring and , the ring is semisimple and its left regular module is a finite direct sum of simple column ideals. (Matrix rings over division rings are semisimple).
Proof
First suppose that is semisimple on the left. If is the zero ring, its right regular module is also the zero module and is semisimple. Otherwise [L2] gives .
By [L4], it suffices to identify the opposite factors as matrix rings over division rings. Each is a division ring, and entrywise transpose defines a ring isomorphism because with the products interpreted in the indicated rings. Hence . By [L4], each factor's left regular module is semisimple, and the regular module of the finite product is their finite direct sum. Thus is left semisimple, equivalently is right semisimple.
Conversely, if is right semisimple, then is left semisimple. Applying steps 1.1–2.1 to makes it right semisimple, which is exactly left semisimplicity of . This also retains the zero-ring case.
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
- William Crawley-Boevey, Noncommutative Algebra, Chapter 1 Sections 1.1-1.9 (standard reference, not scraped)