Projectivity of principal ideals of idempotents #
For an idempotent e in a semiring R, right multiplication by e retracts the regular
module onto its principal left ideal Re. Thus Re is projective. This is the projectivity
input for constructing projective covers from primitive idempotents.
References #
- T. Y. Lam, A First Course in Noncommutative Rings, 2nd ed., §21.
theorem
IsIdempotentElem.projective_span_singleton
{R : Type u_1}
[Semiring R]
{e : R}
(he : IsIdempotentElem e)
:
Module.Projective R ↥(Ideal.span {e})
The principal left ideal of an idempotent is projective: right multiplication by the idempotent retracts the regular module onto that ideal.