Lifting full idempotents modulo the Jacobson radical

A full idempotent is one generating the entire ring as a two-sided ideal. In a semiperfect ring, every full idempotent of the radical quotient lifts to a full idempotent of the ring. Idempotent lifting is supplied by semiperfectness, and any lift retains fullness because the Jacobson radical cannot contribute to generation of the unit ideal.

This permits a full idempotent selected in a semisimple radical quotient to define a Morita equivalence with its lifted corner ring. In particular it applies to finite-dimensional algebras, which are semiperfect. No choice of matrix decomposition or base field is needed.

Main results

• TauCeti.IsSemiperfectRing.exists_isIdempotentElem_full_eq: a full idempotent of the radical quotient of a semiperfect ring lifts to a full idempotent of the ring.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras I, Sections I.4 and I.6.

theorem TauCeti.IsSemiperfectRing.exists_isIdempotentElem_full_eq {R : Type u_1} [Ring R] [IsSemiperfectRing R] (e : R ⧸ Ring.jacobson R) (he : IsIdempotentElem e) (hfull : TwoSidedIdeal.span {e} = ⊤) : ∃ (f : R), IsIdempotentElem f ∧ (Ideal.Quotient.mk (Ring.jacobson R)) f = e ∧ TwoSidedIdeal.span {f} = ⊤

A full idempotent of the radical quotient of a semiperfect ring lifts to a full idempotent of the ring, with the specified quotient image.