From cdc03dcd9a528b39be6f950688017734356fdb41 Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevi.ch>
Date: Sun, 24 May 2026 07:31:41 +0200
Subject: [PATCH 1/6] feat(Module/Projective): direct sum of projective modules
 is projective

---
 Mathlib/Algebra/Module/Projective.lean | 35 ++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean
index 00e6a6bda6d6a2..b200c438afa538 100644
--- a/Mathlib/Algebra/Module/Projective.lean
+++ b/Mathlib/Algebra/Module/Projective.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Module.Shrink
 public import Mathlib.LinearAlgebra.TensorProduct.Basis
 public import Mathlib.Logic.UnivLE
+public import Mathlib.LinearAlgebra.DirectSum.Basis
 
 /-!
 
@@ -59,6 +60,7 @@ projective module
 universe w v u
 
 open LinearMap hiding id
+open DirectSum hiding id id_apply
 open Finsupp
 
 /- The actual implementation we choose: `P` is projective if the natural surjection
@@ -287,4 +289,37 @@ theorem Projective.of_lifting_property {R : Type u} [Ring R] {P : Type v} [AddCo
 
 end OfLiftingProperty
 
+section DirectSum
+
+variable {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)]
+    [(i : ι) → Module R (M i)]
+
+theorem directSum_iff : Module.Projective R (⨁ i, M i) ↔ ∀ (i : ι), Module.Projective R (M i) := by
+  classical
+  constructor
+  · intro H i
+    refine Projective.iff_split'.{max u v w} |>.mpr ?_
+    obtain ⟨T, I₁, I₂, I₃, f, g, hfg⟩ := Projective.iff_split.mp H
+    refine ⟨T, I₁, I₂, I₃, f.comp (DirectSum.lof ..), (DirectSum.component ..).comp g, ?_⟩
+    rw [LinearMap.ext_iff] at hfg
+    ext
+    simp at hfg
+    simp [hfg]
+  · intro H
+    refine Projective.iff_split.mpr ?_
+    have := fun i ↦ Projective.iff_split'.{max u v w}.mp (H i)
+    choose T I₁ I₂ I₃ f g hfg using this
+    refine ⟨⨁ i, T i, inferInstance, inferInstance, inferInstance, ?_⟩
+    use DirectSum.toModule _ _ _ fun i ↦ (DirectSum.lof ..).comp (f i)
+    use DirectSum.toModule _ _ _ fun i ↦ (DirectSum.lof ..).comp (g i)
+    ext x
+    have := LinearMap.ext_iff.mp (hfg x)
+    simp at this
+    simp [this]
+
+instance Projective.directSum [∀ (i : ι), Module.Projective R (M i)] :
+    Module.Projective R (⨁ i, M i) := directSum_iff.mpr ‹_›
+
+end DirectSum
+
 end Module

From c8f9cd065cc87d3eed621e20c75efb474bd3f73b Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevi.ch>
Date: Sun, 24 May 2026 09:15:04 +0200
Subject: [PATCH 2/6] Monica feedback

---
 Mathlib/Algebra/DirectSum/Module.lean  |  8 ++++++++
 Mathlib/Algebra/Module/Projective.lean | 26 ++++++++++----------------
 2 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Algebra/DirectSum/Module.lean b/Mathlib/Algebra/DirectSum/Module.lean
index e10dff85371f95..c00ca03b0bd727 100644
--- a/Mathlib/Algebra/DirectSum/Module.lean
+++ b/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*}
diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean
index b200c438afa538..56a3baffa13ef8 100644
--- a/Mathlib/Algebra/Module/Projective.lean
+++ b/Mathlib/Algebra/Module/Projective.lean
@@ -294,31 +294,25 @@ section DirectSum
 variable {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)]
     [(i : ι) → Module R (M i)]
 
-theorem directSum_iff : Module.Projective R (⨁ i, M i) ↔ ∀ (i : ι), Module.Projective R (M i) := by
+theorem Projective.directSum_iff : Projective R (⨁ i, M i) ↔ ∀ (i : ι), Projective R (M i) := by
   classical
-  constructor
-  · intro H i
-    refine Projective.iff_split'.{max u v w} |>.mpr ?_
-    obtain ⟨T, I₁, I₂, I₃, f, g, hfg⟩ := Projective.iff_split.mp H
+  refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
+  · refine iff_split'.{max u v w} |>.mpr ?_
+    obtain ⟨T, I₁, I₂, I₃, f, g, hfg⟩ := iff_split.mp H
     refine ⟨T, I₁, I₂, I₃, f.comp (DirectSum.lof ..), (DirectSum.component ..).comp g, ?_⟩
-    rw [LinearMap.ext_iff] at hfg
-    ext
-    simp at hfg
-    simp [hfg]
-  · intro H
-    refine Projective.iff_split.mpr ?_
-    have := fun i ↦ Projective.iff_split'.{max u v w}.mp (H i)
+    simp [← comp_assoc _ f, comp_assoc _ g, hfg]
+  · refine iff_split.mpr ?_
+    have := fun i ↦ iff_split'.{max u v w}.mp (H i)
     choose T I₁ I₂ I₃ f g hfg using this
     refine ⟨⨁ i, T i, inferInstance, inferInstance, inferInstance, ?_⟩
     use DirectSum.toModule _ _ _ fun i ↦ (DirectSum.lof ..).comp (f i)
     use DirectSum.toModule _ _ _ fun i ↦ (DirectSum.lof ..).comp (g i)
     ext x
-    have := LinearMap.ext_iff.mp (hfg x)
-    simp at this
+    have := by simpa using LinearMap.ext_iff.mp (hfg x)
     simp [this]
 
-instance Projective.directSum [∀ (i : ι), Module.Projective R (M i)] :
-    Module.Projective R (⨁ i, M i) := directSum_iff.mpr ‹_›
+instance Projective.directSum [∀ (i : ι), Projective R (M i)] : Projective R (⨁ i, M i) :=
+  directSum_iff.mpr ‹_›
 
 end DirectSum
 

From 3ef4b9f2f08315a57dd108f57ad3929496d525f6 Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevi.ch>
Date: Sun, 24 May 2026 09:19:46 +0200
Subject: [PATCH 3/6] import order

---
 Mathlib/Algebra/Module/Projective.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean
index 56a3baffa13ef8..83b1fa5026786e 100644
--- a/Mathlib/Algebra/Module/Projective.lean
+++ b/Mathlib/Algebra/Module/Projective.lean
@@ -6,9 +6,9 @@ Authors: Kevin Buzzard, Antoine Labelle
 module
 
 public import Mathlib.Algebra.Module.Shrink
+public import Mathlib.LinearAlgebra.DirectSum.Basis
 public import Mathlib.LinearAlgebra.TensorProduct.Basis
 public import Mathlib.Logic.UnivLE
-public import Mathlib.LinearAlgebra.DirectSum.Basis
 
 /-!
 

From a0d141d0c8283f1a17a7a70824a9d6917b5f7fdd Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevi.ch>
Date: Sun, 24 May 2026 09:21:22 +0200
Subject: [PATCH 4/6] variable lines

---
 Mathlib/Algebra/Module/Projective.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean
index 83b1fa5026786e..f9fb9414ac18de 100644
--- a/Mathlib/Algebra/Module/Projective.lean
+++ b/Mathlib/Algebra/Module/Projective.lean
@@ -291,8 +291,8 @@ end OfLiftingProperty
 
 section DirectSum
 
-variable {R : Type u} [Semiring R] {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)]
-    [(i : ι) → Module R (M i)]
+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

From fd52a81f9ea8a61d3b592e2d9576c70fd208f9a2 Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevi.ch>
Date: Sun, 24 May 2026 12:00:39 +0200
Subject: [PATCH 5/6] Robin's feedback

---
 Mathlib/Algebra/Module/Projective.lean | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean
index f9fb9414ac18de..44d4db1d658dfe 100644
--- a/Mathlib/Algebra/Module/Projective.lean
+++ b/Mathlib/Algebra/Module/Projective.lean
@@ -60,7 +60,7 @@ projective module
 universe w v u
 
 open LinearMap hiding id
-open DirectSum hiding id id_apply
+open DirectSum hiding id_apply
 open Finsupp
 
 /- The actual implementation we choose: `P` is projective if the natural surjection
@@ -297,19 +297,9 @@ variable {ι : Type v} {M : ι → Type w} [(i : ι) → AddCommMonoid (M i)] [(
 theorem Projective.directSum_iff : Projective R (⨁ i, M i) ↔ ∀ (i : ι), Projective R (M i) := by
   classical
   refine ⟨fun H i ↦ ?_, fun H ↦ ?_⟩
-  · refine iff_split'.{max u v w} |>.mpr ?_
-    obtain ⟨T, I₁, I₂, I₃, f, g, hfg⟩ := iff_split.mp H
-    refine ⟨T, I₁, I₂, I₃, f.comp (DirectSum.lof ..), (DirectSum.component ..).comp g, ?_⟩
-    simp [← comp_assoc _ f, comp_assoc _ g, hfg]
-  · refine iff_split.mpr ?_
-    have := fun i ↦ iff_split'.{max u v w}.mp (H i)
-    choose T I₁ I₂ I₃ f g hfg using this
-    refine ⟨⨁ i, T i, inferInstance, inferInstance, inferInstance, ?_⟩
-    use DirectSum.toModule _ _ _ fun i ↦ (DirectSum.lof ..).comp (f i)
-    use DirectSum.toModule _ _ _ fun i ↦ (DirectSum.lof ..).comp (g i)
-    ext x
-    have := by simpa using LinearMap.ext_iff.mp (hfg x)
-    simp [this]
+  · 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 ‹_›

From ae4265723423f5784777ae8f8435b04aa7314e0c Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevi.ch>
Date: Sun, 24 May 2026 13:52:13 +0200
Subject: [PATCH 6/6] delete unnecessary import

---
 Mathlib/Algebra/Module/Projective.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Algebra/Module/Projective.lean b/Mathlib/Algebra/Module/Projective.lean
index 44d4db1d658dfe..c04d5236d6454d 100644
--- a/Mathlib/Algebra/Module/Projective.lean
+++ b/Mathlib/Algebra/Module/Projective.lean
@@ -6,7 +6,6 @@ Authors: Kevin Buzzard, Antoine Labelle
 module
 
 public import Mathlib.Algebra.Module.Shrink
-public import Mathlib.LinearAlgebra.DirectSum.Basis
 public import Mathlib.LinearAlgebra.TensorProduct.Basis
 public import Mathlib.Logic.UnivLE