mathlib3 documentation

algebra.module.projective

Projective modules #

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

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_1) [semiring R] (P : Type u_2) [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_lifting_property {R : Type u_1} [semiring R] {P : Type u_2} [add_comm_monoid P] [module R P] {M : Type u_3} [add_comm_monoid M] [module R M] {N : Type u_4} [add_comm_monoid 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.

@[protected, instance]
def module.prod.projective {R : Type u_1} [semiring R] {P : Type u_2} [add_comm_monoid P] [module R P] {Q : Type u_5} [add_comm_monoid Q] [module R Q] [hP : module.projective R P] [hQ : module.projective R Q] :
@[protected, instance]
def module.dfinsupp.projective {R : Type u_1} [semiring R] {ι : Type u_6} (A : ι Type u_7) [Π (i : ι), add_comm_monoid (A i)] [Π (i : ι), module R (A i)] [h : (i : ι), module.projective R (A i)] :
module.projective R (Π₀ (i : ι), A i)
theorem module.projective_of_basis {R : Type u_1} [ring R] {P : Type u_2} [add_comm_group P] [module R P] {ι : Type u_3} (b : basis ι R P) :

Free modules are projective.

@[protected, instance]
def module.projective_of_free {R : Type u_1} [ring R] {P : Type u_2} [add_comm_group P] [module R P] [module.free R P] :
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_4 : add_comm_monoid M] [_inst_5 : add_comm_monoid 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 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.