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.
@[protected, instance]
The category of modules has enough projectives, since every module is a quotient of a free module.