mathlib documentation

algebra.category.Module.projective

The category of R-modules has enough projectives. #

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.

@[protected, instance]

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