mathlib documentation

algebra.module.projective

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).

We require that the module sits in at least as high a universe as the ring: without this, free modules don't even exist, and it's unclear if projective modules are even a useful notion.

References #

https://en.wikipedia.org/wiki/Projective_module

TODO #

All of these should be relatively straightforward.

Tags #

projective module

@[class]
structure module.projective (R : Type u) [semiring R] (P : Type (max u v)) [add_comm_monoid P] [module R P] :
Prop

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.

Instances of this typeclass
theorem module.projective_def {R : Type u} [semiring R] {P : Type (max u v)} [add_comm_monoid P] [module R P] :
theorem module.projective_lifting_property {R : Type u} [semiring R] {P : Type (max u v)} [add_comm_monoid P] [module R P] {M : Type (max u v)} [add_comm_group M] [module R M] {N : Type u_1} [add_comm_group N] [module R N] [h : module.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 module.projective_of_lifting_property' {R : Type u} [semiring R] {P : Type (max u v)} [add_comm_monoid P] [module R P] (huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [_inst_8 : add_comm_monoid M] [_inst_9 : add_comm_monoid N] [_inst_10 : module R M] [_inst_11 : 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 module.projective_of_lifting_property {R : Type u} [ring R] {P : Type (max u v)} [add_comm_group P] [module R P] (huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [_inst_4 : add_comm_group M] [_inst_5 : add_comm_group N] [_inst_6 : module R M] [_inst_7 : module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), function.surjective f(∃ (h : P →ₗ[R] M), f.comp h = g)) :

A variant of of_lifting_property' when we're working over a [ring R], which only requires quantifying over modules with an add_comm_group instance.

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

Free modules are projective.

@[protected, instance]
def module.projective_of_free {R : Type u} [ring R] {P : Type (max u v)} [add_comm_group P] [module R P] [module.free R P] :