# 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

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

- out : ∃ (s : P →ₗ[R] P →₀ R), Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s

Instances

source
theorem Module.projective_def {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] :
Projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s
source
theorem Module.projective_def' {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] :
Projective R P ↔ ∃ (s : P →ₗ[R] P →₀ R), Finsupp.linearCombination R id ∘ₗ s = LinearMap.id
source
theorem Module.projective_lifting_property {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] [h : Projective R P] (f : M →ₗ[R] N) (g : P →ₗ[R] N) (hf : Function.Surjective ⇑f) :
∃ (h : P →ₗ[R] M), f ∘ₗ h = g

A projective R-module has the property that maps from it lift along surjections.

source
theorem LinearMap.exists_rightInverse_of_surjective {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {M : Type u_3} [AddCommMonoid M] [Module R M] [Module.Projective R P] (f : M →ₗ[R] P) (hf_surj : range f = ⊤) :
∃ (g : P →ₗ[R] M), f ∘ₗ g = id
source
theorem Function.Surjective.surjective_linearMapComp_left {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {M : Type u_3} [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module.Projective R P] {f : M →ₗ[R] P} (hf_surj : Surjective ⇑f) :
Surjective fun (g : N →ₗ[R] M) => f ∘ₗ g
source
theorem Module.Projective.of_lifting_property'' {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P] (huniv : ∀ (f : (P →₀ R) →ₗ[R] P), Function.Surjective ⇑f → ∃ (h : P →ₗ[R] P →₀ R), f ∘ₗ h = LinearMap.id) :
Projective R P

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.

source
instance Module.instProjectiveProd {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {Q : Type u_5} [AddCommMonoid Q] [Module R Q] [Projective R P] [Projective R Q] :
Projective R (P × Q)
source
instance Module.instProjectiveDFinsupp {R : Type u_1} [Semiring R] {ι : Type u_6} (A : ι → Type u_7) [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [h : ∀ (i : ι), Projective R (A i)] :
Projective R (Π₀ (i : ι), A i)
source
theorem Module.Projective.of_basis {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {ι : Type u_8} (b : Basis ι R P) :
Projective R P

Free modules are projective.

source
@[instance 100]
instance Module.Projective.of_free {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] [Free R P] :
Projective R P
source
theorem Module.Projective.of_split {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {M : Type u_3} [AddCommMonoid M] [Module R M] [Projective R M] (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s ∘ₗ i = LinearMap.id) :
Projective R P

A direct summand of a projective module is projective.

source
theorem Module.Projective.of_equiv {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {M : Type u_3} [AddCommMonoid M] [Module R M] [Projective R M] (e : M ≃ₗ[R] P) :
Projective R P
source
theorem Module.Projective.iff_split_of_projective {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] {M : Type u_3} [AddCommMonoid M] [Module R M] [Projective R M] (s : M →ₗ[R] P) (hs : Function.Surjective ⇑s) :
Projective R P ↔ ∃ (i : P →ₗ[R] M), s ∘ₗ i = LinearMap.id

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

source
theorem Module.Projective.of_ringEquiv {R : Type u_8} {S : Type u_9} [Semiring R] [Semiring S] {M : Type u_10} {N : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] (e₁ : R ≃+* S) (e₂ : M ≃ₛₗ[↑e₁] N) [Projective R M] :
Projective S N
source
theorem Module.Projective.iff_split' {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P] [Small.{w, u} R] [Small.{w, v} P] :
Projective R P ↔ ∃ (M : Type w) (x : AddCommMonoid M) (x_1 : Module R M) (_ : Free R M) (i : P →ₗ[R] M) (s : M →ₗ[R] P), s ∘ₗ i = LinearMap.id

A variant of `Projective.iff_split` allowing for a more flexible selection of the universe for the free module `M`.

source
theorem Module.Projective.iff_split {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P] :
Projective R P ↔ ∃ (M : Type (max u v)) (x : AddCommMonoid M) (x_1 : Module R M) (_ : Free 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.

source
instance Module.Projective.tensorProduct {R : Type u} [Semiring R] {R₀ : Type u_2} {M : Type u_1} {N : Type u_3} [CommSemiring R₀] [Algebra R₀ R] [AddCommMonoid M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [AddCommMonoid N] [Module R₀ N] [hM : Projective R M] [hN : Projective R₀ N] :
Projective R (TensorProduct R₀ M N)
source
theorem Module.Projective.of_lifting_property' {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P] [Small.{v, u} R] (h : ∀ {M N : Type v} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Module R M] [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g) :
Projective R P

A module which satisfies the universal property is projective.

source
theorem Module.Projective.of_lifting_property {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Small.{v, u} R] (h : ∀ {M N : Type v} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ (h : P →ₗ[R] M), f ∘ₗ h = g) :
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 `AddCommGroup` instance.