mathlib documentation

algebra.category.Module.projective

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.

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.

@[instance]

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