Documentation

Mathlib.Algebra.Module.Projective

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.

Main theorems #

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 #

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

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} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] [self : Module.Projective R P] :
    ∃ (s : P →ₗ[R] P →₀ R), Function.LeftInverse (Finsupp.total P P R id) s
    theorem Module.projective_def {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] :
    Module.Projective R P ∃ (s : P →ₗ[R] P →₀ R), Function.LeftInverse (Finsupp.total P P R id) s
    theorem Module.projective_def' {R : Type u_1} [Semiring R] {P : Type u_2} [AddCommMonoid P] [Module R P] :
    Module.Projective 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} [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 : Module.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 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) :

    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] [Module.Projective R P] [Module.Projective R Q] :
    Equations
    • =
    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 : ι), 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} [AddCommGroup P] [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} [AddCommGroup P] [Module R P] [Module.Free R P] :
    Equations
    • =
    theorem Module.Projective.of_split {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] {M : Type u_1} [AddCommGroup M] [Module R M] [Module.Projective 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} [AddCommGroup P] [Module R P] {M : Type u_1} [AddCommGroup M] [Module R M] [Module.Projective R M] (e : M ≃ₗ[R] P) :
    theorem Module.Projective.iff_split {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] :
    Module.Projective R P ∃ (M : Type (max u v)) (x : AddCommGroup M) (x_1 : Module R M) (_ : Module.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.

    theorem Module.Projective.iff_split_of_projective {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] {M : Type u_1} [AddCommGroup M] [Module R M] [Module.Projective R M] (s : M →ₗ[R] P) (hs : Function.Surjective s) :
    Module.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.

    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] [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [AddCommGroup N] [Module R₀ N] [hM : Module.Projective R M] [hN : Module.Projective R₀ N] :
    Equations
    • =
    theorem Module.Projective.of_lifting_property' {R : Type u} [Semiring R] {P : Type (max u v)} [AddCommMonoid P] [Module R P] (huniv : ∀ {M : Type (max v u)} {N : Type (max u 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) :

    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)} [AddCommGroup P] [Module R P] (huniv : ∀ {M : Type (max v u)} {N : Type (max u 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) :

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