feat(algebra/module/projective): projective modules are closed under …

…direct sums (#16743)

I'm unsure what the universe should be for the index type `ι` in algebra/module/projective (`{ι : Type*}` doesn't work). 

- [x] depends on: #16735 



Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>

src/algebra/module/projective.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kevin Buzzard
+Authors: Kevin Buzzard, Antoine Labelle
 -/
 
 import algebra.module.basic
@@ -130,6 +130,41 @@ begin
   { rw [←snd_apply _, apply_total R], exact hsQ x, },
 end
 
+variables {ι : Type*} (A : ι → Type*) [Π (i : ι), add_comm_monoid (A i)]
+  [Π (i : ι), module R (A i)]
+
+instance [h : Π (i : ι), projective R (A i)] : projective R (Π₀ i, A i) :=
+begin
+  classical,
+  rw module.projective_def',
+  simp_rw projective_def at h, choose s hs using h,
+
+  letI : Π (i : ι), add_comm_monoid (A i →₀ R) := λ i, by apply_instance,
+  letI : Π (i : ι), module R (A i →₀ R) := λ i, by apply_instance,
+  letI : add_comm_monoid (Π₀ (i : ι), A i →₀ R) := @dfinsupp.add_comm_monoid ι (λ i, A i →₀ R) _,
+  letI : module R (Π₀ (i : ι), A i →₀ R) := @dfinsupp.module ι R (λ i, A i →₀ R) _ _ _,
+
+  let f := λ i, lmap_domain R R (dfinsupp.single i : A i → Π₀ i, A i),
+  use dfinsupp.coprod_map f ∘ₗ dfinsupp.map_range.linear_map s,
+
+  ext i x j,
+  simp only [dfinsupp.coprod_map, direct_sum.lof, total_map_domain R _ dfinsupp.single_injective,
+    coe_comp, coe_lsum, id_coe, linear_equiv.coe_to_linear_map, finsupp_lequiv_dfinsupp_symm_apply,
+    function.comp_app, dfinsupp.lsingle_apply, dfinsupp.map_range.linear_map_apply,
+    dfinsupp.map_range_single, lmap_domain_apply, dfinsupp.to_finsupp_single,
+    finsupp.sum_single_index, id.def, function.comp.left_id, dfinsupp.single_apply],
+  rw [←dfinsupp.lapply_apply j, apply_total R],
+
+  obtain rfl | hij := eq_or_ne i j,
+
+  { convert (hs i) x,
+    { ext, simp },
+    { simp } },
+  { convert finsupp.total_zero_apply _ ((s i) x),
+    { ext, simp [hij] },
+    { simp [hij] } }
+end
+
 end semiring
 
 section ring

src/linear_algebra/dfinsupp.lean

@@ -206,6 +206,25 @@ lemma map_range.linear_equiv_symm (e : Π i, β₁ i ≃ₗ[R] β₂ i) :
 
 end map_range
 
+section coprod_map
+
+variables [decidable_eq ι] [Π (x : N), decidable (x ≠ 0)]
+
+/-- Given a family of linear maps `f i : M i  →ₗ[R] N`, we can form a linear map
+`(Π₀ i, M i) →ₗ[R] N` which sends `x : Π₀ i, M i` to the sum over `i` of `f i` applied to `x i`.
+This is the map coming from the universal property of `Π₀ i, M i` as the coproduct of the `M i`.
+See also `linear_map.coprod` for the binary product version. -/
+noncomputable def coprod_map (f : Π (i : ι), M i  →ₗ[R] N) : (Π₀ i, M i) →ₗ[R] N :=
+finsupp.lsum ℕ (λ i : ι, linear_map.id) ∘ₗ
+(@finsupp_lequiv_dfinsupp ι R N _ _ _ _ _).symm.to_linear_map ∘ₗ
+(dfinsupp.map_range.linear_map f)
+
+lemma coprod_map_apply (f : Π (i : ι), M i  →ₗ[R] N) (x : Π₀ i, M i) :
+  coprod_map f x =
+  finsupp.sum (map_range (λ i, f i) (λ i, linear_map.map_zero _) x).to_finsupp (λ i, id) := rfl
+
+end coprod_map
+
 section basis
 
 /-- The direct sum of free modules is free.