mathlib3 documentation


The category of R-modules has enough projectives. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.