mathlib documentation

algebra.category.Module.projective

The category of R-modules has enough projectives. #

source
theorem is_projective.iff_projective {R : Type u} [ring R] {P : Type (max u v)} [add_comm_group P] [module R P] :
module.projective R P ↔ category_theory.projective (Module.of R P)

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

source
theorem Module.projective_of_free {R : Type u} [ring R] {M : Module R} {ι : Type u_1} (b : basis ι R ↥M) :
category_theory.projective M

Modules that have a basis are projective.

source
@[protected, instance]
def Module.Module_enough_projectives {R : Type u} [ring R] :
category_theory.enough_projectives (Module R)

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