Effective aspects of semiperfect rings

This paper studies effective aspects of semiperfect rings from the standpoint of reverse mathematics. Based on first-order Jacobson radicals of rings, we define a ring R with the Jacobson radical Jac(R) to be semiperfect if the quotient ring R/Jac(R) is semisimple, and idempotents of the quotient ring can be lifted to R. Using elementary matrix operations in linear algebra, we show that RCA0 proves a characterization of semiperfect rings in terms of idempotents of rings. Semiperfect rings are generalizations of semisimple rings and local rings, and semiperfect rings R with R/Jac(R) simple are isomorphic to matrix rings over local rings. Based on the effective characterization of semiperfect rings via idempotents, we prove the structure theorem of semiperfect rings R with R/Jac(R) simple in RCA0. Left perfect rings or right perfect rings are always semiperfect. Finally, we provide a proof for the structure theorem of one-sided perfect rings R with R/Jac(R) simple in WKL0.