Semiperfect rings

A ring is semiperfect when its radical quotient R ⧸ Ring.jacobson R is a semisimple ring and idempotents lift modulo the radical. This is the hypothesis under which projective covers of finitely generated modules exist, and it is the property of a finite-dimensional algebra that TauCeti/Algebra/Module/ProjectiveCover/Existence.lean uses in its sharper, nilpotent form.

Mathlib packages the neighbouring notion, IsSemiprimaryRing: the radical is nilpotent and the radical quotient is semisimple. Nilpotence of the radical makes its elements nil, so idempotents lift along R ↠ R ⧸ Ring.jacobson R by Mathlib's exists_isIdempotentElem_eq_of_ker_isNilpotent; a semiprimary ring is therefore semiperfect (TauCeti.IsSemiperfectRing.of_isSemiprimaryRing), and a ring that is finite-dimensional over a division ring acting compatibly with its multiplication — such as a finite-dimensional algebra over a field — being an Artinian ring, is semiprimary and hence semiperfect (TauCeti.isSemiperfectRing_of_finiteDimensional).

Bass' characterization — R is semiperfect exactly when every finitely generated R-module has a projective cover — is not proved here. The existence half of it over a semiprimary ring, in the stronger form that covers every module, is TauCeti.exists_isProjectiveCover.

Main definitions

• TauCeti.IsSemiperfectRing: the radical quotient is semisimple and idempotents lift modulo the radical.

Main results

• TauCeti.IsSemiperfectRing.of_isSemiprimaryRing: a semiprimary ring is semiperfect.
• TauCeti.isSemiperfectRing_of_finiteDimensional: a ring finite-dimensional over a division ring, such as a finite-dimensional algebra over a field, is semiperfect.

References

See T. Y. Lam, A First Course in Noncommutative Rings, §23-24.

class TauCeti.IsSemiperfectRing (R : Type u) [Ring R] : Prop

A ring is semiperfect if its quotient by the Jacobson radical is a semisimple ring and every idempotent of that quotient is the class of an idempotent of the ring.

• isSemisimpleRing : IsSemisimpleRing (R ⧸ Ring.jacobson R)

  The radical quotient of a semiperfect ring is a semisimple ring.

• exists_isIdempotentElem_eq (e : R ⧸ Ring.jacobson R) (he : IsIdempotentElem e) : ∃ (f : R), IsIdempotentElem f ∧ (Ideal.Quotient.mk (Ring.jacobson R)) f = e

  Idempotents lift modulo the Jacobson radical.

instance TauCeti.IsSemiperfectRing.of_isSemiprimaryRing (R : Type u) [Ring R] [IsSemiprimaryRing R] : IsSemiperfectRing R

A semiprimary ring is semiperfect.

theorem TauCeti.isSemiperfectRing_of_finiteDimensional (k : Type v) [DivisionRing k] (A : Type u) [Ring A] [Module k A] [IsScalarTower k A A] [FiniteDimensional k A] : IsSemiperfectRing A

A ring finite-dimensional over a division ring is semiperfect, for a division ring k acting on A compatibly with its multiplication; for instance, a finite-dimensional algebra over a field is semiperfect.