The category of R-modules has enough projectives. #
theorem
is_projective.iff_projective
{R : Type u}
[ring R]
{P : Type (max u v)}
[add_comm_group P]
[module R P] :
The categorical notion of projective object agrees with the explicit module-theoretic notion.
theorem
Module.projective_of_free
{R : Type u}
[ring R]
{M : Module R}
{ι : Type u_1}
(b : basis ι R ↥M) :
Modules that have a basis are projective.
@[instance]
The category of modules has enough projectives, since every module is a quotient of a free module.