The category of R-modules has enough projectives.

instance ModuleCat.projective_of_categoryTheory_projective {R : Type u} [Ring R] (P : ModuleCat R) [Module.Projective R ↑P] : CategoryTheory.Projective P

instance ModuleCat.projective_of_module_projective {R : Type u} [Ring R] (P : ModuleCat R) [Small.{v, u} R] [CategoryTheory.Projective P] : Module.Projective R ↑P

theorem IsProjective.iff_projective {R : Type u} [Ring R] [Small.{v, u} R] (P : Type v) [AddCommGroup P] [Module R P] : Module.Projective R P ↔ CategoryTheory.Projective (ModuleCat.of R P)

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 w} (b : Basis ι R ↑M) : CategoryTheory.Projective M

Modules that have a basis are projective.

instance ModuleCat.enoughProjectives {R : Type u} [Ring R] [Small.{v, u} R] : CategoryTheory.EnoughProjectives (ModuleCat R)

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