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

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

## Main theorems #

• Module.projective_lifting_property : a map from a projective module can be lifted along a surjection.

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

• Module.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 Module.Projective (R : Type u_1) [] (P : Type u_2) [] [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.

Instances
theorem Module.Projective.out {R : Type u_1} [] {P : Type u_2} [] [Module R P] [self : ] :
∃ (s : P →ₗ[R] P →₀ R), Function.LeftInverse (Finsupp.total P P R id) s
theorem Module.projective_def {R : Type u_1} [] {P : Type u_2} [] [Module R P] :
∃ (s : P →ₗ[R] P →₀ R), Function.LeftInverse (Finsupp.total P P R id) s
theorem Module.projective_def' {R : Type u_1} [] {P : Type u_2} [] [Module R P] :
∃ (s : P →ₗ[R] P →₀ R), Finsupp.total P P R id ∘ₗ s = LinearMap.id
theorem Module.projective_lifting_property {R : Type u_1} [] {P : Type u_2} [] [Module R P] {M : Type u_3} [] [Module R M] {N : Type u_4} [] [Module R N] [h : ] (f : M →ₗ[R] N) (g : P →ₗ[R] N) (hf : ) :
∃ (h : P →ₗ[R] M), f ∘ₗ 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} [] {P : Type v} [] [Module R P] (huniv : ∀ (f : (P →₀ R) →ₗ[R] P), ∃ (h : P →ₗ[R] P →₀ R), f ∘ₗ h = LinearMap.id) :

A module which satisfies the universal property is projective: If all surjections of R-modules (P →₀ R) →ₗ[R] P have R-linear left inverse maps, then P is projective.

instance Module.instProjectiveProd {R : Type u_1} [] {P : Type u_2} [] [Module R P] {Q : Type u_5} [] [Module R Q] [] [] :
Equations
• =
instance Module.instProjectiveDFinsupp {R : Type u_1} [] {ι : Type u_6} (A : ιType u_7) [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [h : ∀ (i : ι), Module.Projective R (A i)] :
Module.Projective R (Π₀ (i : ι), A i)
Equations
• =
theorem Module.Projective.of_basis {R : Type u} [Ring R] {P : Type v} [] [Module R P] {ι : Type u_1} (b : Basis ι R P) :

Free modules are projective.

@[instance 100]
instance Module.Projective.of_free {R : Type u} [Ring R] {P : Type v} [] [Module R P] [] :
Equations
• =
theorem Module.Projective.of_split {R : Type u} [Ring R] {P : Type v} [] [Module R P] {M : Type u_1} [] [Module R M] [] (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s ∘ₗ i = LinearMap.id) :
theorem Module.Projective.of_equiv {R : Type u} [Ring R] {P : Type v} [] [Module R P] {M : Type u_1} [] [Module R M] [] (e : M ≃ₗ[R] P) :
theorem Module.Projective.iff_split {R : Type u} [Ring R] {P : Type v} [] [Module R P] :
∃ (M : Type (max u v)) (x : ) (x_1 : Module R M) (_ : ) (i : P →ₗ[R] M) (s : M →ₗ[R] P), s ∘ₗ i = LinearMap.id

A module is projective iff it is the direct summand of a free module.

theorem Module.Projective.iff_split_of_projective {R : Type u} [Ring R] {P : Type v} [] [Module R P] {M : Type u_1} [] [Module R M] [] (s : M →ₗ[R] P) (hs : ) :
∃ (i : P →ₗ[R] M), s ∘ₗ i = LinearMap.id

A quotient of a projective module is projective iff it is a direct summand.

instance Module.Projective.tensorProduct {R : Type u} [Ring R] {R₀ : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R₀] [Algebra R₀ R] [] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [] [Module R₀ N] [hM : ] [hN : ] :
Equations
• =
theorem Module.Projective.of_lifting_property' {R : Type u} [] {P : Type (max u v)} [] [Module R P] (huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : ] [inst_1 : ] [inst_2 : Module R M] [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), ∃ (h : P →ₗ[R] M), f ∘ₗ 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)} [] [Module R P] (huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : ] [inst_1 : ] [inst_2 : Module R M] [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), ∃ (h : P →ₗ[R] M), f ∘ₗ h = g) :

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