The category of R-modules has enough projectives.

theorem IsProjective.iff_projective {R : Type u} [Ring R] {P : Type (max u 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 u'} (b : Basis ι R ↑M) : CategoryTheory.Projective M

Modules that have a basis are projective.

instance ModuleCat.moduleCat_enoughProjectives {R : Type u} [Ring R] : CategoryTheory.EnoughProjectives (ModuleCat R)

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

Equations

• (_ : CategoryTheory.EnoughProjectives (ModuleCat R)) = (_ : CategoryTheory.EnoughProjectives (ModuleCat R))