feat(Module/Projective): direct sum of projective modules is projective (leanprover-community#39764)

Author: vlad902

Mathlib/Algebra/DirectSum/Module.lean

@@ -213,6 +213,14 @@ theorem component.of [DecidableEq ι] (i j : ι) (b : M j) :
     component R ι M i ((lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0 :=
   DFinsupp.single_apply
 
+lemma component_comp_lof [DecidableEq ι] (i j : ι) :
+    component R ι M i ∘ₗ lof R ι M j = if h : j = i then h ▸ .id else 0 := by
+  aesop (add simp component.of)
+
+@[simp]
+lemma component_comp_lof_same [DecidableEq ι] (i : ι) : component R ι M i ∘ₗ lof R ι M i = .id := by
+  simp [component_comp_lof]
+
 section map
 
 variable {R} {N : ι → Type*}

Mathlib/Algebra/Module/Projective.lean

@@ -59,6 +59,7 @@ projective module
 universe w v u
 
 open LinearMap hiding id
+open DirectSum hiding id_apply
 open Finsupp
 
 /- The actual implementation we choose: `P` is projective if the natural surjection
@@ -287,4 +288,21 @@ theorem Projective.of_lifting_property {R : Type u} [Ring R] {P : Type v} [AddCo
 
 end OfLiftingProperty
 
+section DirectSum
+
+variable {R : Type u} [Semiring R]
+variable {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)]
+
+theorem Projective.directSum_iff : Projective R (⨁ i, M i) ↔ ∀ (i : ι), Projective R (M i) := by
+  classical
+  refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
+  · exact .of_split (DirectSum.lof ..) (DirectSum.component ..) (by simp)
+  · let e : (⨁ i, M i) ≃ₗ[R] Π₀ i, M i := .refl ..
+    exact Projective.of_equiv' e.symm
+
+instance Projective.directSum [∀ (i : ι), Projective R (M i)] : Projective R (⨁ i, M i) :=
+  directSum_iff.mpr ‹_›
+
+end DirectSum
+
 end Module