The category of R-modules has enough projectives. #

The categorical notion of projective object agrees with the explicit module-theoretic notion.

theorem ModuleCat.projective_of_free {R : Type u} [Ring R] {M : ModuleCat R} {ι : Type u'} (b : Basis ι R M) :

Modules that have a basis are projective.

The category of modules has enough projectives, since every module is a quotient of a free module.