# mathlib3documentation

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.

• is_projective R M : the proposition saying that M is a projective R-module.

## Main theorems #

• is_projective.lifting_property : a map from a projective module can be lifted along a surjection.

• is_projective.of_lifting_property : If for all R-module surjections A →ₗ B, all maps M →ₗ B lift to M →ₗ A, then M is projective.

• is_projective.of_free : Free modules are projective

## 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 #

• Direct sum of two projective modules is projective.
• Arbitrary sum of projective modules is projective.

All of these should be relatively straightforward.

## Tags #

projective module

@[class]
structure module.projective (R : Type u_1) [semiring R] (P : Type u_2) [ 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_1} [semiring R] {P : Type u_2} [ P] :
(s : P →ₗ[R] P →₀ R), s
theorem module.projective_def' {R : Type u_1} [semiring R] {P : Type u_2} [ P] :
(s : P →ₗ[R] P →₀ R), P R id).comp s = linear_map.id
theorem module.projective_lifting_property {R : Type u_1} [semiring R] {P : Type u_2} [ P] {M : Type u_3} [ M] {N : Type u_4} [ N] [h : 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} [ P] {Q : Type u_5} [ Q] [hP : P] [hQ : Q] :
(P × 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 : ι), (A i)] [h : (i : ι), (A i)] :
(Π₀ (i : ι), A i)
theorem module.projective_of_basis {R : Type u_1} [ring R] {P : Type u_2} [ P] {ι : Type u_3} (b : R P) :

Free modules are projective.

@[protected, instance]
def module.projective_of_free {R : Type u_1} [ring R] {P : Type u_2} [ P] [ P] :
theorem module.projective_of_lifting_property' {R : Type u} [semiring R] {P : Type (max u v)} [ P] (huniv : {M : Type (max v u)} {N : Type (max u v)} [_inst_4 : [_inst_5 : [_inst_6 : M] [_inst_7 : N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), ( (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)} [ P] (huniv : {M : Type (max v u)} {N : Type (max u v)} [_inst_4 : [_inst_5 : [_inst_6 : M] [_inst_7 : N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), ( (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.