mathlib documentation


Projective modules #

This file contains a definition of a projective module, the proof that our definition is equivalent to a lifting property, and the proof that all free modules are projective.

Main definitions #

Let R be a ring (or a semiring) and let M be an R-module.

Main theorems #

Implementation notes #

The actual definition of projective we use is that the natural R-module map from the free R-module on the type M down to M splits. This is more convenient than certain other definitions which involve quantifying over universes, and also universe-polymorphic (the ring and module can be in different universes).

Everything works for semirings and modules except that apparently we don't have free modules over semirings, so here we stick to rings.

References #


All of these should be relatively straightforward.

Tags #

projective module

def is_projective (R : Type u) [semiring R] (P : Type v) [add_comm_monoid P] [module R P] :

An R-module is projective if it is a direct summand of a free module, or equivalently if maps from the module lift along surjections. There are several other equivalent definitions.

theorem is_projective.lifting_property {R : Type u} [semiring R] {P : Type v} [add_comm_monoid P] [module R P] {M : Type u_1} [add_comm_group M] [module R M] {N : Type u_2} [add_comm_group N] [module R N] (h : is_projective R P) (f : M →ₗ[R] N) (g : P →ₗ[R] N) (hf : function.surjective f) :
∃ (h : P →ₗ[R] M), f.comp h = g

A projective R-module has the property that maps from it lift along surjections.

theorem is_projective.of_lifting_property {R : Type u} [semiring R] {P : Type v} [add_comm_monoid P] [module R P] (huniv : ∀ {M : Type (max v u)} {N : Type v} [_inst_11 : add_comm_monoid M] [_inst_12 : add_comm_monoid N] [_inst_13 : module R M] [_inst_14 : module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), function.surjective f(∃ (h : P →ₗ[R] M), f.comp h = g)) :

A module which satisfies the universal property is projective. Note that the universe variables in huniv are somewhat restricted.

theorem is_projective.of_free {R : Type u} [ring R] {P : Type v} [add_comm_group P] [module R P] {ι : Type u_1} (b : basis ι R P) :

Free modules are projective.