Structure of semisimple rings in reverse and computable mathematics

This paper studies the structure of semisimple rings using techniques of reverse mathematics, where a ring is left semisimple if the left regular module is a finite direct sum of simple submodules. The structure theorem of left semisimple rings, also called Wedderburn-Artin Theorem, is a famous theorem in noncommutative algebra, says that a ring is left semisimple if and only if it is isomorphic to a finite direct product of matrix rings over division rings. We provide a proof for the theorem in RCA(0), showing the structure theorem for computable semisimple rings. The decomposition of semisimple rings as finite direct products of matrix rings over division rings is unique. Based on an effective proof of the Jordan-Holder Theorem for modules with composition series, we also provide an effective proof for the uniqueness of the matrix decomposition of semisimple rings in RCA(0).

Automated summary

This paper uses techniques of reverse mathematics to study the structure of semisimple rings. A ring is left semisimple if its left regular module is a finite direct sum of simple submodules. The famous Wedderburn-Artin Theorem states that a ring is left semisimple if and only if it is isomorphic to a finite direct product of matrix rings over division rings. We provide a proof for this theorem in RCA(0), showing the structure of computable semisimple rings.