doc-next-gen

Mathlib.Algebra.Module.Projective

Module docstring

{"# 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

"}

Module.Projective structure
(R : Type*) [Semiring R] (P : Type*) [AddCommMonoid P] [Module R P]
Full source 
/-- 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. -/
class Module.Projective (R : Type*) [Semiring R] (P : Type*) [AddCommMonoid P] [Module R P] :
    Prop where
  out : ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (Finsupp.linearCombination R id) s
Projective Module
Informal description
An $R$-module $P$ is called *projective* if it is a direct summand of a free $R$-module. Equivalently, $P$ is projective if every module homomorphism from $P$ to any quotient module $B$ can be lifted to a module homomorphism from $P$ to $A$, where $A \to B$ is a surjective module homomorphism.
Module.projective_def theorem
: Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (linearCombination R id) s
Full source 
theorem projective_def :
    ProjectiveProjective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Function.LeftInverse (linearCombination R id) s :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩
Characterization of Projective Modules via Linear Splitting
Informal description
An $R$-module $P$ is projective if and only if there exists a linear map $s \colon P \to P \to_{\text{f}} R$ such that $s$ is a left inverse of the linear combination map $\text{linearCombination}_R \text{id}$. Here, $P \to_{\text{f}} R$ denotes the module of finitely supported functions from $P$ to $R$, and $\text{linearCombination}_R \text{id}$ is the map that sends a finitely supported function to its linear combination in $P$.
Module.projective_def' theorem
: Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.linearCombination R id ∘ₗ s = .id
Full source 
theorem projective_def' :
    ProjectiveProjective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.linearCombination R id ∘ₗ s = .id := by
  simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]
Characterization of Projective Modules via Linear Splitting
Informal description
An $R$-module $P$ is projective if and only if there exists a linear map $s \colon P \to P \to_{\text{f}} R$ such that the composition of $s$ with the linear combination map $\text{linearCombination}_R \text{id}$ is the identity map on $P$. Here, $P \to_{\text{f}} R$ denotes the module of finitely supported functions from $P$ to $R$.
Module.projective_lifting_property theorem
[h : Projective R P] (f : M →ₗ[R] N) (g : P →ₗ[R] N) (hf : Function.Surjective f) : ∃ h : P →ₗ[R] M, f ∘ₗ h = g
Full source 
/-- A projective R-module has the property that maps from it lift along surjections. -/
theorem projective_lifting_property [h : Projective R P] (f : M →ₗ[R] N) (g : P →ₗ[R] N)
    (hf : Function.Surjective f) : ∃ h : P →ₗ[R] M, f ∘ₗ h = g := by
  /-
    Here's the first step of the proof.
    Recall that `X →₀ R` is Lean's way of talking about the free `R`-module
    on a type `X`. The universal property `Finsupp.linearCombination` says that to a map
    `X → N` from a type to an `R`-module, we get an associated R-module map
    `(X →₀ R) →ₗ N`. Apply this to a (noncomputable) map `P → M` coming from the map
    `P →ₗ N` and a random splitting of the surjection `M →ₗ N`, and we get
    a map `φ : (P →₀ R) →ₗ M`.
    -/
  let φ : (P →₀ R) →ₗ[R] M := Finsupp.linearCombination _ fun p => Function.surjInv hf (g p)
  -- By projectivity we have a map `P →ₗ (P →₀ R)`;
  obtain ⟨s, hs⟩ := h.out
  -- Compose to get `P →ₗ M`. This works.
  use φ.comp s
  ext p
  conv_rhs => rw [← hs p]
  simp [φ, Finsupp.linearCombination_apply, Function.surjInv_eq hf, map_finsuppSum]
Lifting Property of Projective Modules
Informal description
Let $R$ be a semiring and $P$ be a projective $R$-module. For any surjective $R$-linear map $f \colon M \to N$ and any $R$-linear map $g \colon P \to N$, there exists an $R$-linear map $h \colon P \to M$ such that $f \circ h = g$.
LinearMap.exists_rightInverse_of_surjective theorem
[Projective R P] (f : M →ₗ[R] P) (hf_surj : range f = ⊤) : ∃ g : P →ₗ[R] M, f ∘ₗ g = LinearMap.id
Full source 
theorem _root_.LinearMap.exists_rightInverse_of_surjective [Projective R P]
    (f : M →ₗ[R] P) (hf_surj : range f = ⊤) : ∃ g : P →ₗ[R] M, f ∘ₗ g = LinearMap.id :=
  projective_lifting_property f (.id : P →ₗ[R] P) (LinearMap.range_eq_top.1 hf_surj)
Existence of Right Inverse for Surjective Linear Maps from Projective Modules
Informal description
Let $R$ be a semiring and $P$ be a projective $R$-module. For any surjective $R$-linear map $f \colon M \to P$ (i.e., with $\text{range}(f) = \top$), there exists an $R$-linear map $g \colon P \to M$ such that $f \circ g$ is the identity map on $P$.
Function.Surjective.surjective_linearMapComp_left theorem
[Projective R P] {f : M →ₗ[R] P} (hf_surj : Surjective f) : Surjective (fun g : N →ₗ[R] M ↦ f.comp g)
Full source 
theorem _root_.Function.Surjective.surjective_linearMapComp_left [Projective R P]
    {f : M →ₗ[R] P} (hf_surj : Surjective f) : Surjective (fun g : N →ₗ[R] M ↦ f.comp g) :=
  surjective_comp_left_of_exists_rightInverse <|
    f.exists_rightInverse_of_surjective <| range_eq_top_of_surjective f hf_surj
Surjectivity of Linear Map Composition for Projective Modules
Informal description
Let $R$ be a semiring and $P$ be a projective $R$-module. For any surjective $R$-linear map $f \colon M \to P$, the composition map $g \mapsto f \circ g$ is surjective on the space of $R$-linear maps from any $R$-module $N$ to $M$.
Module.Projective.of_lifting_property'' theorem
{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.comp h = .id) : Projective R P
Full source 
/-- 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. -/
theorem 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.comp h = .id) :
    Projective R P :=
  projective_def'.2 <| huniv (Finsupp.linearCombination R (id : P → P))
    (linearCombination_surjective _ Function.surjective_id)
Projective Module Characterization via Lifting Property for Finitely Supported Functions
Informal description
Let $R$ be a semiring and $P$ be an $R$-module. If for every surjective linear map $f \colon (P \to_{\text{f}} R) \to P$ there exists a linear map $h \colon P \to (P \to_{\text{f}} R)$ such that $f \circ h = \text{id}_P$, then $P$ is a projective $R$-module. Here, $P \to_{\text{f}} R$ denotes the module of finitely supported functions from $P$ to $R$.
Module.instProjectiveProd instance
[Projective R P] [Projective R Q] : Projective R (P × Q)
Full source 
instance [Projective R P] [Projective R Q] : Projective R (P × Q) := by
  refine .of_lifting_property'' fun f hf ↦ ?_
  rcases projective_lifting_property f (.inl _ _ _) hf with ⟨g₁, hg₁⟩
  rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩
  refine ⟨coprod g₁ g₂, ?_⟩
  rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
Projectivity of Direct Product of Projective Modules
Informal description
For any semiring $R$ and projective $R$-modules $P$ and $Q$, the direct product $P \times Q$ is also a projective $R$-module.
Module.instProjectiveDFinsupp instance
[h : ∀ i : ι, Projective R (A i)] : Projective R (Π₀ i, A i)
Full source 
instance [h : ∀ i : ι, Projective R (A i)] : Projective R (Π₀ i, A i) :=
  .of_lifting_property'' fun f hf ↦ by
    classical
      choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
      replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
      refine ⟨DFinsupp.coprodMap g, ?_⟩
      ext i x j
      simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
Projectivity of Dependent Functions with Finite Support
Informal description
For any semiring $R$ and a family of $R$-modules $A_i$ indexed by $i \in \iota$, if each $A_i$ is a projective $R$-module, then the dependent function space $\Pi_{i \in \iota} A_i$ with finite support is also a projective $R$-module.
Module.Projective.of_basis theorem
{ι : Type*} (b : Basis ι R P) : Projective R P
Full source 
/-- Free modules are projective. -/
theorem Projective.of_basis {ι : Type*} (b : Basis ι R P) : Projective R P := by
  -- need P →ₗ (P →₀ R) for definition of projective.
  -- get it from `ι → (P →₀ R)` coming from `b`.
  use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
  intro m
  simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single,
    map_finsuppSum]
  exact b.linearCombination_repr m
Modules with basis are projective
Informal description
Let $R$ be a semiring and $P$ be an $R$-module. If $P$ has a basis indexed by a type $\iota$, then $P$ is a projective $R$-module.
Module.Projective.of_split theorem
[Module.Projective R M] (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s.comp i = LinearMap.id) : Module.Projective R P
Full source 
/-- A direct summand of a projective module is projective. -/
theorem Projective.of_split [Module.Projective R M]
    (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s.comp i = LinearMap.id) : Module.Projective R P := by
  obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.linearCombination R id) s
    (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)
  refine ⟨g.comp i, fun x ↦ ?_⟩
  rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
    ← LinearMap.comp_apply, H, LinearMap.id_apply]
Direct Summand of a Projective Module is Projective
Informal description
Let $R$ be a semiring, and let $M$ and $P$ be $R$-modules. Suppose $M$ is projective, and there exist $R$-linear maps $i \colon P \to M$ and $s \colon M \to P$ such that $s \circ i = \text{id}_P$. Then $P$ is also projective.
Module.Projective.of_equiv theorem
[Module.Projective R M] (e : M ≃ₗ[R] P) : Module.Projective R P
Full source 
theorem Projective.of_equiv [Module.Projective R M]
    (e : M ≃ₗ[R] P) : Module.Projective R P :=
  Projective.of_split e.symm e.toLinearMap (by ext; simp)
Linear Equivalence Preserves Projectivity of Modules
Informal description
Let $R$ be a semiring, and let $M$ and $P$ be $R$-modules. If $M$ is projective and there exists a linear equivalence $e \colon M \simeq_R P$ between $M$ and $P$, then $P$ is also projective.
Module.Projective.iff_split_of_projective theorem
[Module.Projective R M] (s : M →ₗ[R] P) (hs : Function.Surjective s) : Module.Projective R P ↔ ∃ i, s ∘ₗ i = LinearMap.id
Full source 
/-- A quotient of a projective module is projective iff it is a direct summand. -/
theorem Projective.iff_split_of_projective [Module.Projective R M] (s : M →ₗ[R] P)
    (hs : Function.Surjective s) :
    Module.ProjectiveModule.Projective R P ↔ ∃ i, s ∘ₗ i = LinearMap.id :=
  ⟨fun _ ↦ projective_lifting_property _ _ hs, fun ⟨i, H⟩ ↦ Projective.of_split i s H⟩
Projectivity of Quotient Module via Splitting Condition
Informal description
Let $R$ be a semiring, and let $M$ and $P$ be $R$-modules with $M$ projective. Given a surjective $R$-linear map $s \colon M \to P$, the module $P$ is projective if and only if there exists an $R$-linear map $i \colon P \to M$ such that $s \circ i = \text{id}_P$.
Module.Projective.of_ringEquiv theorem
{R S} [Semiring R] [Semiring S] {M N} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N] (e₁ : R ≃+* S) (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] N) [Projective R M] : Projective S N
Full source 
theorem Projective.of_ringEquiv {R S} [Semiring R] [Semiring S] {M N}
    [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N]
    (e₁ : R ≃+* S) (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] N)
    [Projective R M] : Projective S N := by
  obtain ⟨f, hf⟩ := ‹Projective R M›
  let g : N →ₗ[S] N →₀ S :=
  { toFun := fun x ↦ (equivCongrLeft e₂ (f (e₂.symm x))).mapRange e₁ e₁.map_zero
    map_add' := fun x y ↦ by ext; simp
    map_smul' := fun r v ↦ by ext i; simp [e₂.symm.map_smulₛₗ] }
  refine ⟨⟨g, fun x ↦ ?_⟩⟩
  replace hf := congr(e₂ $(hf (e₂.symm x)))
  simpa [linearCombination_apply, sum_mapRange_index, g, map_finsuppSum, e₂.map_smulₛₗ] using hf
Projectivity is preserved under ring isomorphism and semilinear equivalence
Informal description
Let $R$ and $S$ be semirings, and let $M$ and $N$ be modules over $R$ and $S$ respectively. Given a ring isomorphism $e₁: R \simeq S$ and a semilinear equivalence $e₂: M \simeq N$ with respect to $e₁$, if $M$ is projective as an $R$-module, then $N$ is projective as an $S$-module.
Module.Projective.iff_split theorem
: Module.Projective R P ↔ ∃ (M : Type max u v) (_ : AddCommMonoid M) (_ : Module R M) (_ : Module.Free R M) (i : P →ₗ[R] M) (s : M →ₗ[R] P), s.comp i = LinearMap.id
Full source 
/-- A module is projective iff it is the direct summand of a free module. -/
theorem Projective.iff_split : Module.ProjectiveModule.Projective R P ↔
    ∃ (M : Type max u v) (_ : AddCommMonoid M) (_ : Module R M) (_ : Module.Free R M)
      (i : P →ₗ[R] M) (s : M →ₗ[R] P), s.comp i = LinearMap.id :=
  ⟨fun ⟨i, hi⟩ ↦ ⟨P →₀ R, _, _, inferInstance, i, Finsupp.linearCombination R id, LinearMap.ext hi⟩,
    fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
Projective Module Characterization via Free Module Splitting
Informal description
An $R$-module $P$ is projective if and only if there exists a free $R$-module $M$ and linear maps $i \colon P \to M$ and $s \colon M \to P$ such that $s \circ i = \text{id}_P$.
Module.Projective.tensorProduct instance
[hM : Module.Projective R M] [hN : Module.Projective R₀ N] : Module.Projective R (M ⊗[R₀] N)
Full source 
instance Projective.tensorProduct [hM : Module.Projective R M] [hN : Module.Projective R₀ N] :
    Module.Projective R (M ⊗[R₀] N) := by
  obtain ⟨sM, hsM⟩ := hM
  obtain ⟨sN, hsN⟩ := hN
  have : Module.Projective R (M ⊗[R₀] (N →₀ R₀)) := by
    fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
    · exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · exact (AlgebraTensorModule.map
        (Finsupp.linearCombination R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · ext; simp [hsM _]
  fapply Projective.of_split (R := R) (M := (M ⊗[R₀] (N →₀ R₀)))
  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) sN)
  · exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (linearCombination R₀ id))
  · ext; simp [hsN _]
Tensor Product of Projective Modules is Projective
Informal description
Let $R$ and $R_0$ be semirings, and let $M$ and $N$ be projective modules over $R$ and $R_0$ respectively. Then the tensor product $M \otimes_{R_0} N$ is a projective module over $R$.
Module.Projective.of_lifting_property' theorem
{R : Type u} [Semiring R] {P : Type max u v} [AddCommMonoid P] [Module R P] -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`, (huniv : ∀ {M : Type max v u} {N : Type max u v} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) : -- then `P` is projective.Projective R P
Full source 
/-- A module which satisfies the universal property is projective. Note that the universe variables
in `huniv` are somewhat restricted. -/
theorem Projective.of_lifting_property' {R : Type u} [Semiring R] {P : Type max u v}
    [AddCommMonoid P] [Module R P]
    -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
    (huniv : ∀ {M : Type max v u} {N : Type max u v} [AddCommMonoid M] [AddCommMonoid N]
      [Module R M] [Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N),
        Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) :
    -- then `P` is projective.
    Projective R P :=
  .of_lifting_property'' (huniv · _)
Projective Module Characterization via Universal Lifting Property
Informal description
Let $R$ be a semiring and $P$ be an $R$-module. Suppose that for all $R$-modules $M$ and $N$, every surjective linear map $f \colon M \to N$, and every linear map $g \colon P \to N$, there exists a linear map $h \colon P \to M$ such that $f \circ h = g$. Then $P$ is a projective $R$-module.
Module.Projective.of_lifting_property theorem
{R : Type u} [Ring R] {P : Type max u v} [AddCommGroup P] [Module R P] -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`, (huniv : ∀ {M : Type max v u} {N : Type max u v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) : -- then `P` is projective.Projective R P
Full source 
/-- A variant of `of_lifting_property'` when we're working over a `[Ring R]`,
which only requires quantifying over modules with an `AddCommGroup` instance. -/
theorem Projective.of_lifting_property {R : Type u} [Ring R] {P : Type max u v} [AddCommGroup P]
    [Module R P]
    -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
    (huniv : ∀ {M : Type max v u} {N : Type max u v} [AddCommGroup M] [AddCommGroup N]
      [Module R M] [Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N),
        Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) :
    -- then `P` is projective.
    Projective R P :=
  .of_lifting_property'' (huniv · _)
Projective Module Characterization via Universal Lifting Property
Informal description
Let $R$ be a ring and $P$ be an $R$-module. Suppose that for all $R$-modules $M$ and $N$ with additive commutative group structures, and for every surjective linear map $f \colon M \to N$ and every linear map $g \colon P \to N$, there exists a linear map $h \colon P \to M$ such that $f \circ h = g$. Then $P$ is a projective $R$-module.