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

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

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

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.

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

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

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.

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)

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)

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.

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

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.

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

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.

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

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.

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.

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)

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.

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.