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

source

@[class]

structure module.projective (R : Type u_1) [semiring R] (P : Type u_2) [add_comm_monoid P] [module R P] :

Prop

out : ∃ (s : P →ₗ[R] P →₀ R), function.left_inverse ⇑(finsupp.total P P R id) ⇑s

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

source

theorem module.projective_def {R : Type u_1} [semiring R] {P : Type u_2} [add_comm_monoid P] [module R P] :

module.projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), function.left_inverse ⇑(finsupp.total P P R id) ⇑s

source

theorem module.projective_def' {R : Type u_1} [semiring R] {P : Type u_2} [add_comm_monoid P] [module R P] :

module.projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), (finsupp.total P P R id).comp s = linear_map.id

source

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.

source

@[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] :

module.projective R (P × Q)

source

@[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)

source

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

module.projective R P

Free modules are projective.

source

@[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] :

module.projective R P

source

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

module.projective R P

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

source

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

module.projective R P

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.