From 6956dbbdbc630d4fa05de86ad0a18b25493996e3 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 2 Jul 2024 16:52:59 +0200
Subject: [PATCH 1/6] adic completion as tensor product

---
 Mathlib.lean                                  |   3 +
 Mathlib/LinearAlgebra/TensorProduct/Pi.lean   |  86 ++++++++++
 .../AdicCompletion/AsTensorProduct.lean       | 151 ++++++++++++++++++
 3 files changed, 240 insertions(+)
 create mode 100644 Mathlib/LinearAlgebra/TensorProduct/Pi.lean
 create mode 100644 Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 1b593c8fd6ecbb..a78148742a4c12 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2899,6 +2899,7 @@ import Mathlib.LinearAlgebra.TensorProduct.Graded.External
 import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
 import Mathlib.LinearAlgebra.TensorProduct.Opposite
+import Mathlib.LinearAlgebra.TensorProduct.Pi
 import Mathlib.LinearAlgebra.TensorProduct.Prod
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.LinearAlgebra.TensorProduct.Submodule
@@ -3543,8 +3544,10 @@ import Mathlib.RepresentationTheory.Invariants
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RepresentationTheory.Rep
 import Mathlib.RingTheory.AdicCompletion.Algebra
+import Mathlib.RingTheory.AdicCompletion.AsTensorProduct
 import Mathlib.RingTheory.AdicCompletion.Basic
 import Mathlib.RingTheory.AdicCompletion.Exactness
+import Mathlib.RingTheory.AdicCompletion.Flat
 import Mathlib.RingTheory.AdicCompletion.Functoriality
 import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.Adjoin.FG
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Pi.lean b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
new file mode 100644
index 00000000000000..f83dbe3709e69b
--- /dev/null
+++ b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 Judith Ludwig, Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Judith Ludwig, Christian Merten
+-/
+import Mathlib.LinearAlgebra.TensorProduct.Tower
+import Mathlib.LinearAlgebra.Pi
+
+/-!
+
+# Tensor product and products
+
+In this file we examine the behaviour of the tensor product with arbitrary and finite products.
+
+Let `S` be an `R`-algebra, `N` an `S`-module and `ι` an index type. We then have a natural map
+
+`TensorProduct.piScalarRightHom`: `N ⊗[R] (ι → R) →ₗ[S] (ι → N)`
+
+In general, this is not an isomorphism, but if `ι` is finite, then it is
+and it is packaged as `TensorProduct.piScalarRight`.
+
+-/
+
+variable (R : Type*) [CommRing R]
+variable (S : Type*) [CommRing S] [Algebra R S]
+variable (N : Type*) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N]
+variable (ι : Type*)
+
+open LinearMap TensorProduct
+
+private def TensorProduct.piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) where
+  toFun n := LinearMap.compLeft (toSpanSingleton R N n) ι
+  map_add' x y := by
+    ext i j
+    simp
+  map_smul' s x := by
+    ext i j
+    dsimp only [coe_comp, coe_single, Function.comp_apply, compLeft_apply, toSpanSingleton_apply,
+      RingHom.id_apply, smul_apply, Pi.smul_apply]
+    rw [← IsScalarTower.smul_assoc, _root_.Algebra.smul_def, mul_comm, mul_smul]
+    simp
+
+/-- For any `R`-module `N` and index type `ι`, there is a natural
+linear map `N ⊗[R] (ι → R) →ₗ (ι → N)`. This map is an isomorphism if `ι` is finite. -/
+noncomputable def TensorProduct.piScalarRightHom : N ⊗[R] (ι → R) →ₗ[S] (ι → N) :=
+  AlgebraTensorModule.lift <| piScalarRightHomBil R S N ι
+
+@[simp]
+lemma TensorProduct.piScalarRightHom_tmul (x : N) (f : ι → R) :
+    piScalarRightHom R S N ι (x ⊗ₜ f) = (fun j ↦ f j • x) := by
+  ext j
+  simp [piScalarRightHom, piScalarRightHomBil]
+
+variable [Fintype ι] [DecidableEq ι]
+
+private noncomputable
+def TensorProduct.piScalarRightInv : (ι → N) →ₗ[S] N ⊗[R] (ι → R) :=
+  LinearMap.lsum S (fun _ ↦ N) S <| fun i ↦ {
+    toFun := fun n ↦ n ⊗ₜ Pi.single i 1
+    map_add' := fun x y ↦ by simp [add_tmul]
+    map_smul' := fun s x ↦ rfl
+  }
+
+@[simp]
+private lemma TensorProduct.piScalarRightInv_single (x : N) (i : ι) :
+    piScalarRightInv R S N ι (Pi.single i x) = x ⊗ₜ Pi.single i 1 := by
+  simp [piScalarRightInv, Pi.single_apply, TensorProduct.ite_tmul]
+
+@[simp]
+lemma Pi.single_apply_smul (x : N) (i j : ι) :
+    (Pi.single i 1 : ι → R) j • x = (Pi.single i x : ι → N) j := by
+  simp [Pi.single_apply]
+
+/-- For any `R`-module `N` and finite index type `ι`, `N ⊗[R] (ι → R)` is canonically
+isomorphic to `ι → N`. -/
+noncomputable def TensorProduct.piScalarRight : N ⊗[R] (ι → R) ≃ₗ[S] (ι → N) :=
+  LinearEquiv.ofLinear
+    (piScalarRightHom R S N (ι := ι))
+    (piScalarRightInv R S N (ι := ι))
+    (by ext i x j; simp [Pi.single_apply])
+    (by ext x i; simp)
+
+@[simp]
+lemma TensorProduct.piScalarRight_tmul (x : N) (f : ι → R) :
+    piScalarRight R S N ι (x ⊗ₜ f) = (fun j ↦ f j • x) := by
+  simp [piScalarRight]
diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
new file mode 100644
index 00000000000000..062fd418592b0a
--- /dev/null
+++ b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2024 Judith Ludwig, Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Judith Ludwig, Christian Merten
+-/
+import Mathlib.LinearAlgebra.TensorProduct.Pi
+import Mathlib.RingTheory.AdicCompletion.Exactness
+import Mathlib.RingTheory.TensorProduct.Basic
+
+/-!
+
+# Adic completion as tensor product
+
+In this file we examine properties of the natural map
+
+`AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M`.
+
+We show
+
+- it is an isomorphism if `M = R^n`.
+- it is surjective, if `M` is a finite `R`-module.
+- it is an isomorphism if `M` is a finite `R`-module and `R` is Noetherian.
+
+## TODO
+
+- Show that `ofTensorProduct` is an isomorphism for any finite free `R`-module over an arbitrary
+  ring. This is mostly composing with the isomorphism to `R^n` and checking that a diagram commutes.
+
+-/
+
+variable {R : Type*} [CommRing R] (I : Ideal R)
+variable (M : Type*) [AddCommGroup M] [Module R M]
+variable {N : Type*} [AddCommGroup N] [Module R N]
+
+open TensorProduct
+
+namespace AdicCompletion
+
+private
+def ofTensorProductBil : AdicCompletion I R →ₗ[AdicCompletion I R] M →ₗ[R] AdicCompletion I M where
+  toFun r := LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M) r ∘ₗ of I M
+  map_add' x y := by
+    apply LinearMap.ext
+    simp
+  map_smul' r x := by
+    apply LinearMap.ext
+    intro y
+    simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
+      LinearMap.lsmul_apply, RingHom.id_apply, LinearMap.smul_apply]
+    rw [smul_eq_mul, mul_smul]
+
+@[simp]
+private lemma ofTensorProductBil_apply_apply (r : AdicCompletion I R) (x : M) :
+    ((AdicCompletion.ofTensorProductBil I M) r) x = r • (of I M) x :=
+  rfl
+
+/-- The natural `AdicCompletion I R`-linear map from `AdicCompletion I R ⊗[R] M` to
+the adic completion of `M`. -/
+noncomputable
+def ofTensorProduct : AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M :=
+  TensorProduct.AlgebraTensorModule.lift (ofTensorProductBil I M)
+
+@[simp]
+lemma ofTensorProduct_tmul (r : AdicCompletion I R) (x : M) :
+    ofTensorProduct I M (r ⊗ₜ x) = r • of I M x := by
+  simp [ofTensorProduct]
+
+variable {M} in
+/-- `ofTensorProduct` is functorial in `M`. -/
+lemma ofTensorProduct_naturality (f : M →ₗ[R] N) :
+    map I f ∘ₗ ofTensorProduct I M =
+      ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f := by
+  ext
+  simp
+
+section PiFintype
+
+/-
+In this section we show that `ofTensorProduct` is an isomorphism if `M = R^n`.
+-/
+
+attribute [-simp] _root_.smul_eq_mul Algebra.id.smul_eq_mul
+
+variable (ι : Type*) [Fintype ι] [DecidableEq ι]
+
+private lemma piEquivOfFintype_comp_ofTensorProduct_eq :
+    piEquivOfFintype I (fun _ : ι ↦ R) ∘ₗ ofTensorProduct I (ι → R) =
+      (TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).toLinearMap := by
+  ext i j k
+  suffices h : (if j = i then 1 else 0) = (if j = i then 1 else 0 : AdicCompletion I R).val k by
+    simpa [Pi.single_apply]
+  split <;> simp
+
+private lemma ofTensorProduct_eq :
+    ofTensorProduct I (ι → R) = (piEquivOfFintype I (fun _ : ι ↦ R)).symm.toLinearMap
+      ∘ₗ (TensorProduct.piScalarRight R (AdicCompletion I R) _ ι).toLinearMap := by
+  rw [← piEquivOfFintype_comp_ofTensorProduct_eq, ← LinearMap.comp_assoc]
+  simp
+
+/- If `M = R^ι` and `ι` is finite, we may construct an inverse to `ofTensorProduct I (ι → R)`. -/
+private noncomputable def ofTensorProductInvOfPiFintype :
+    AdicCompletion I (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R) :=
+  letI f := piEquivOfFintype I (fun _ : ι ↦ R)
+  letI g := (TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm
+  f.trans g
+
+private lemma ofTensorProductInvOfPiFintype_comp_ofTensorProduct :
+    ofTensorProductInvOfPiFintype I ι ∘ₗ ofTensorProduct I (ι → R) = LinearMap.id := by
+  simp only [ofTensorProductInvOfPiFintype]
+  rw [LinearEquiv.coe_trans, LinearMap.comp_assoc, piEquivOfFintype_comp_ofTensorProduct_eq]
+  simp
+
+private lemma ofTensorProduct_comp_ofTensorProductInvOfPiFintype :
+    ofTensorProduct I (ι → R) ∘ₗ ofTensorProductInvOfPiFintype I ι = LinearMap.id := by
+  dsimp only [ofTensorProductInvOfPiFintype]
+  rw [LinearEquiv.coe_trans, ofTensorProduct_eq, LinearMap.comp_assoc]
+  nth_rw 2 [← LinearMap.comp_assoc]
+  simp
+
+/-- `ofTensorProduct` as an equiv in the case of `M = R^ι` where `ι` is finite. -/
+noncomputable def ofTensorProductEquivOfPiFintype :
+    AdicCompletion I R ⊗[R] (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I (ι → R) :=
+  LinearEquiv.ofLinear
+    (ofTensorProduct I (ι → R))
+    (ofTensorProductInvOfPiFintype I ι)
+    (ofTensorProduct_comp_ofTensorProductInvOfPiFintype I ι)
+    (ofTensorProductInvOfPiFintype_comp_ofTensorProduct I ι)
+
+/-- If `M = R^ι`, `ofTensorProduct` is bijective. -/
+lemma ofTensorProduct_bijective_of_pi_of_fintype :
+    Function.Bijective (ofTensorProduct I (ι → R)) :=
+  EquivLike.bijective (ofTensorProductEquivOfPiFintype I ι)
+
+end PiFintype
+
+/-- If `M` is a finite `R`-module, then the canonical map
+`AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective. -/
+lemma ofTensorProduct_surjective_of_fg [Module.Finite R M] :
+    Function.Surjective (ofTensorProduct I M) := by
+  obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M
+  let f := ofTensorProduct I M ∘ₗ p.baseChange (AdicCompletion I R)
+  let g := map I p ∘ₗ ofTensorProduct I (Fin n → R)
+  have hfg : f = g := by
+    ext
+    simp [f, g]
+  have hf : Function.Surjective f := by
+    simp only [hfg, LinearMap.coe_comp, g]
+    apply Function.Surjective.comp
+    · exact AdicCompletion.map_surjective I hp
+    · exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective
+  exact Function.Surjective.of_comp hf

From e371dcc06b69330bae973db7ee776cde87656560 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 2 Jul 2024 16:56:51 +0200
Subject: [PATCH 2/6] fix mathlib

---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index a78148742a4c12..68b98a1ec56531 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3547,7 +3547,6 @@ import Mathlib.RingTheory.AdicCompletion.Algebra
 import Mathlib.RingTheory.AdicCompletion.AsTensorProduct
 import Mathlib.RingTheory.AdicCompletion.Basic
 import Mathlib.RingTheory.AdicCompletion.Exactness
-import Mathlib.RingTheory.AdicCompletion.Flat
 import Mathlib.RingTheory.AdicCompletion.Functoriality
 import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.Adjoin.FG

From 25025e533b569951cee6126d1527a6e036a77381 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 2 Jul 2024 16:58:16 +0200
Subject: [PATCH 3/6] fix docstring

---
 Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
index 062fd418592b0a..e8e402fe339863 100644
--- a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
+++ b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@@ -19,7 +19,6 @@ We show
 
 - it is an isomorphism if `M = R^n`.
 - it is surjective, if `M` is a finite `R`-module.
-- it is an isomorphism if `M` is a finite `R`-module and `R` is Noetherian.
 
 ## TODO
 

From 73b834a005a87b9931498ec18150e43a70043055 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Tue, 2 Jul 2024 20:43:16 +0200
Subject: [PATCH 4/6] adic completion is flat

---
 .../Limits/Shapes/Terminal.lean               |  14 ++
 .../AdicCompletion/AsTensorProduct.lean       | 230 +++++++++++++++++-
 2 files changed, 239 insertions(+), 5 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
index 15f5e057ea6a85..ef03db1257a724 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
@@ -803,6 +803,20 @@ instance isIso_ι_initial [HasInitial J] (F : J ⥤ C) [∀ (i j : J) (f : i ⟶
   isIso_ι_of_isInitial initialIsInitial F
 #align category_theory.limits.is_iso_ι_initial CategoryTheory.Limits.isIso_ι_initial
 
+/-- Any morphism between terminal objects is an isomorphism. -/
+lemma isIso_of_isTerminal {X Y : C} (hX : IsTerminal X) (hY : IsTerminal Y) (f : X ⟶ Y) :
+    IsIso f := by
+  refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩
+  simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]
+  apply IsTerminal.hom_ext hY
+
+/-- Any morphism between initial objects is an isomorphism. -/
+lemma isIso_of_isInitial {X Y : C} (hX : IsInitial X) (hY : IsInitial Y) (f : X ⟶ Y) :
+    IsIso f := by
+  refine ⟨⟨IsInitial.to hY X, ?_⟩⟩
+  simp only [IsInitial.to_comp, IsInitial.to_self, and_true]
+  apply IsInitial.hom_ext hX
+
 end
 
 end CategoryTheory.Limits
diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
index e8e402fe339863..dd2830f74bb45a 100644
--- a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
+++ b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@@ -3,9 +3,12 @@ Copyright (c) 2024 Judith Ludwig, Christian Merten. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Judith Ludwig, Christian Merten
 -/
+import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
+import Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
 import Mathlib.LinearAlgebra.TensorProduct.Pi
+import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.RingTheory.AdicCompletion.Exactness
-import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.RingTheory.Flat.Algebra
 
 /-!
 
@@ -15,10 +18,16 @@ In this file we examine properties of the natural map
 
 `AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M`.
 
-We show
+We show (in the `AdicCompletion` namespace):
 
-- it is an isomorphism if `M = R^n`.
-- it is surjective, if `M` is a finite `R`-module.
+- `ofTensorProduct_bijective_of_pi_of_fintype`: it is an isomorphism if `M = R^n`.
+- `ofTensorProduct_surjective_of_finite`: it is surjective, if `M` is a finite `R`-module.
+- `ofTensorProduct_bijective_of_finite_of_isNoetherian`: it is an isomorphism if `R` is Noetherian
+  and `M` is a finite `R`-module.
+
+As a corollary we obtain
+
+- `flat_of_isNoetherian`: the adic completion of a Noetherian ring `R` is `R`-flat.
 
 ## TODO
 
@@ -27,6 +36,8 @@ We show
 
 -/
 
+universe u v
+
 variable {R : Type*} [CommRing R] (I : Ideal R)
 variable (M : Type*) [AddCommGroup M] [Module R M]
 variable {N : Type*} [AddCommGroup N] [Module R N]
@@ -134,7 +145,7 @@ end PiFintype
 
 /-- If `M` is a finite `R`-module, then the canonical map
 `AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective. -/
-lemma ofTensorProduct_surjective_of_fg [Module.Finite R M] :
+lemma ofTensorProduct_surjective_of_finite [Module.Finite R M] :
     Function.Surjective (ofTensorProduct I M) := by
   obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M
   let f := ofTensorProduct I M ∘ₗ p.baseChange (AdicCompletion I R)
@@ -148,3 +159,212 @@ lemma ofTensorProduct_surjective_of_fg [Module.Finite R M] :
     · exact AdicCompletion.map_surjective I hp
     · exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective
   exact Function.Surjective.of_comp hf
+
+section Noetherian
+
+variable {R : Type u} [CommRing R] (I : Ideal R)
+variable (M : Type u) [AddCommGroup M] [Module R M]
+variable [IsNoetherianRing R]
+
+/-!
+
+### Noetherian case
+
+Suppose `R` is Noetherian. Then we show that the canonical map
+`AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M` is an isomorphism for every
+finite `R`-module `M`.
+
+The strategy is the following: Choose a surjection `f : (ι → R) →ₗ[R] M` and consider the following
+commutative diagram:
+
+ AdicCompletion I R ⊗[R] ker f -→ AdicCompletion I R ⊗[R] (ι → R) -→ AdicCompletion I R ⊗[R] M -→ 0
+               |                             |                                 |                  |
+               ↓                             ↓                                 ↓                  ↓
+    AdicCompletion I (ker f) ------→ AdicCompletion I (ι → R) -------→ AdicCompletion I M ------→ 0
+
+The vertical maps are given by `ofTensorProduct`. By the previous section we know that the second
+vertical map is an isomorphism. Since `R` is Noetherian, `ker f` is finitely-generated, so again
+by the previous section the first vertical map is surjective.
+
+Moreover, both rows are exact by right-exactness of the tensor product and exactness of adic
+completions over Noetherian rings. Hence we conclude by the 5-lemma.
+
+-/
+
+open CategoryTheory
+
+section
+
+variable {ι : Type} [Fintype ι] [DecidableEq ι] (f : (ι → R) →ₗ[R] M) (hf : Function.Surjective f)
+
+/- The first horizontal arrow in the top row. -/
+private noncomputable
+def lTensorKerIncl : AdicCompletion I R ⊗[R] LinearMap.ker f →ₗ[AdicCompletion I R]
+    AdicCompletion I R ⊗[R] (ι → R) :=
+  AlgebraTensorModule.map LinearMap.id (LinearMap.ker f).subtype
+
+/- The second horizontal arrow in the top row. -/
+private noncomputable def lTensorf :
+    AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] M :=
+  AlgebraTensorModule.map LinearMap.id f
+
+private lemma if_exact : Function.Exact (LinearMap.ker f).subtype f := by
+  intro x
+  constructor
+  · intro hx
+    exact ⟨⟨x, hx⟩, rfl⟩
+  · rintro ⟨x, rfl⟩
+    exact x.property
+
+private lemma tens_exact : Function.Exact (lTensorKerIncl I M f) (lTensorf I M f) :=
+  lTensor_exact (AdicCompletion I R) (if_exact M f) hf
+
+private lemma tens_surj : Function.Surjective (lTensorf I M f) :=
+  LinearMap.lTensor_surjective (AdicCompletion I R) hf
+
+private lemma adic_exact : Function.Exact (map I (LinearMap.ker f).subtype) (map I f) :=
+  map_exact (Submodule.injective_subtype _) (if_exact M f) hf
+
+private lemma adic_surj : Function.Surjective (map I f) :=
+  map_surjective I hf
+
+/- Instance to speed up instance inference. -/
+private noncomputable instance : AddCommGroup (AdicCompletion I R ⊗[R] (LinearMap.ker f)) :=
+  inferInstance
+
+private noncomputable def firstRow : ComposableArrows (ModuleCat (AdicCompletion I R)) 4 :=
+  ComposableArrows.mk₄
+    (ModuleCat.ofHom <| lTensorKerIncl I M f)
+    (ModuleCat.ofHom <| lTensorf I M f)
+    (ModuleCat.ofHom (0 : AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+
+private def secondRow : ComposableArrows (ModuleCat (AdicCompletion I R)) 4 :=
+  ComposableArrows.mk₄
+    (ModuleCat.ofHom (map I <| (LinearMap.ker f).subtype))
+    (ModuleCat.ofHom (map I f))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+
+private lemma firstRow_exact : (firstRow I M f).Exact where
+  zero k _ := match k with
+    | 0 => (tens_exact I M f hf).linearMap_comp_eq_zero
+    | 1 => LinearMap.zero_comp _
+    | 2 => LinearMap.zero_comp 0
+  exact k _ := by
+    rw [ShortComplex.moduleCat_exact_iff]
+    match k with
+    | 0 => intro x hx; exact (tens_exact I M f hf x).mp hx
+    | 1 => intro x _; exact (tens_surj I M f hf) x
+    | 2 => intro _ _; exact ⟨0, rfl⟩
+
+private lemma secondRow_exact : (secondRow I M f).Exact where
+  zero k _ := match k with
+    | 0 => (adic_exact I M f hf).linearMap_comp_eq_zero
+    | 1 => LinearMap.zero_comp (map I f)
+    | 2 => LinearMap.zero_comp 0
+  exact k _ := by
+    rw [ShortComplex.moduleCat_exact_iff]
+    match k with
+    | 0 => intro x hx; exact (adic_exact I M f hf x).mp hx
+    | 1 => intro x _; exact (adic_surj I M f hf) x
+    | 2 => intro _ _; exact ⟨0, rfl⟩
+
+/- The compatible vertical maps between the first and the second row. -/
+private noncomputable def firstRowToSecondRow : firstRow I M f ⟶ secondRow I M f :=
+  ComposableArrows.homMk₄
+    (ModuleCat.ofHom (ofTensorProduct I (LinearMap.ker f)))
+    (ModuleCat.ofHom (ofTensorProduct I (ι → R)))
+    (ModuleCat.ofHom (ofTensorProduct I M))
+    (ModuleCat.ofHom 0)
+    (ModuleCat.ofHom 0)
+    (ofTensorProduct_naturality I <| (LinearMap.ker f).subtype).symm
+    (ofTensorProduct_naturality I f).symm
+    rfl
+    rfl
+
+private lemma ofTensorProduct_iso : IsIso (ModuleCat.ofHom (ofTensorProduct I M)) := by
+  refine Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
+    (firstRow_exact I M f hf) (secondRow_exact I M f hf) (firstRowToSecondRow I M f) ?_ ?_ ?_ ?_
+  · apply ConcreteCategory.epi_of_surjective
+    exact ofTensorProduct_surjective_of_finite I (LinearMap.ker f)
+  · apply (ConcreteCategory.isIso_iff_bijective _).mpr
+    exact ofTensorProduct_bijective_of_pi_of_fintype I ι
+  · show IsIso (ModuleCat.ofHom 0)
+    apply Limits.isIso_of_isTerminal
+      <;> exact Limits.IsZero.isTerminal (ModuleCat.isZero_of_subsingleton _)
+  · apply ConcreteCategory.mono_of_injective
+    intro x y _
+    rfl
+
+private
+lemma ofTensorProduct_bijective_of_map_from_fin : Function.Bijective (ofTensorProduct I M) := by
+  have : IsIso (ModuleCat.ofHom (ofTensorProduct I M)) :=
+    ofTensorProduct_iso I M f hf
+  exact ConcreteCategory.bijective_of_isIso (ModuleCat.ofHom (ofTensorProduct I M))
+
+end
+
+/-- If `R` is a Noetherian ring and `M` is a finite `R`-module, then the natural map
+given by `AdicCompletion.ofTensorProduct` is an isomorphism. -/
+theorem ofTensorProduct_bijective_of_finite_of_isNoetherian [Module.Finite R M] :
+    Function.Bijective (ofTensorProduct I M) := by
+  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
+  exact ofTensorProduct_bijective_of_map_from_fin I M f hf
+
+/-- `ofTensorProduct` packaged as linear equiv if `M` is a finite `R`-module and `R` is
+Noetherian. -/
+noncomputable def ofTensorProductEquivOfFiniteNoetherian [Module.Finite R M] :
+    AdicCompletion I R ⊗[R] M ≃ₗ[AdicCompletion I R] AdicCompletion I M :=
+  LinearEquiv.ofBijective (ofTensorProduct I M)
+    (ofTensorProduct_bijective_of_finite_of_isNoetherian I M)
+
+@[simp]
+lemma ofTensorProductEquivOfFiniteNoetherian_apply [Module.Finite R M]
+    (x : AdicCompletion I R ⊗[R] M) :
+    ofTensorProductEquivOfFiniteNoetherian I M x = ofTensorProduct I M x :=
+  rfl
+
+@[simp]
+lemma ofTensorProductEquivOfFiniteNoetherian_symm_of [Module.Finite R M] (x : M) :
+    (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ x := by
+  have h : (of I M) x = ofTensorProductEquivOfFiniteNoetherian I M (1 ⊗ₜ x) := by
+    simp
+  rw [h, LinearEquiv.symm_apply_apply]
+
+section
+
+variable {M : Type u} [AddCommGroup M] [Module R M]
+variable {N : Type u} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N)
+variable [Module.Finite R M] [Module.Finite R N]
+
+lemma tensor_map_id_left_eq_map :
+    (AlgebraTensorModule.map LinearMap.id f) =
+      (ofTensorProductEquivOfFiniteNoetherian I N).symm.toLinearMap ∘ₗ
+      map I f ∘ₗ
+      (ofTensorProductEquivOfFiniteNoetherian I M).toLinearMap := by
+  erw [ofTensorProduct_naturality I f]
+  ext x
+  simp
+
+lemma tensor_map_id_left_injective_of_injective (hf : Function.Injective f) :
+    Function.Injective (AlgebraTensorModule.map LinearMap.id f :
+        AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) := by
+  rw [tensor_map_id_left_eq_map I f]
+  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
+    EquivLike.injective_comp]
+  exact map_injective I hf
+
+end
+
+/-- Adic completion of a Noetherian ring `R` is flat over `R`. -/
+instance flat_of_isNoetherian [IsNoetherianRing R] : Algebra.Flat R (AdicCompletion I R) where
+  out := by
+    apply (Module.Flat.iff_lTensor_injective' R (AdicCompletion I R)).mpr
+    intro J
+    apply tensor_map_id_left_injective_of_injective I (Submodule.subtype J)
+    exact Submodule.injective_subtype J
+
+end Noetherian
+
+end AdicCompletion

From 1ed93bdbb50acabba418b1dfab49526fac850835 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Wed, 3 Jul 2024 14:36:57 +0200
Subject: [PATCH 5/6] review suggestions

---
 Mathlib/Algebra/SMulWithZero.lean             |  4 ++
 Mathlib/LinearAlgebra/TensorProduct/Pi.lean   | 44 +++++++++++--------
 Mathlib/LinearAlgebra/TensorProduct/Prod.lean |  5 +++
 .../AdicCompletion/AsTensorProduct.lean       |  4 +-
 4 files changed, 35 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Algebra/SMulWithZero.lean b/Mathlib/Algebra/SMulWithZero.lean
index 4b1cfdca6a8a26..cb920ac6246436 100644
--- a/Mathlib/Algebra/SMulWithZero.lean
+++ b/Mathlib/Algebra/SMulWithZero.lean
@@ -176,6 +176,10 @@ lemma ite_zero_smul (a : R) (b : M) : (if p then a else 0 : R) • b = if p then
 
 lemma boole_smul (a : M) : (if p then 1 else 0 : R) • a = if p then a else 0 := by simp
 
+lemma Pi.single_apply_smul {ι : Type*} [DecidableEq ι] (x : M) (i j : ι) :
+    (Pi.single i 1 : ι → R) j • x = (Pi.single i x : ι → M) j := by
+  rw [single_apply, ite_smul, one_smul, zero_smul, single_apply]
+
 /-- Pullback a `MulActionWithZero` structure along an injective zero-preserving homomorphism.
 See note [reducible non-instances]. -/
 protected abbrev Function.Injective.mulActionWithZero (f : ZeroHom M' M) (hf : Function.Injective f)
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Pi.lean b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
index f83dbe3709e69b..539c4ad30c807a 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@@ -19,16 +19,22 @@ Let `S` be an `R`-algebra, `N` an `S`-module and `ι` an index type. We then hav
 In general, this is not an isomorphism, but if `ι` is finite, then it is
 and it is packaged as `TensorProduct.piScalarRight`.
 
+## Notes
+
+See `Mathlib.LinearAlgebra.TensorProduct.Prod` for binary products.
+
 -/
 
-variable (R : Type*) [CommRing R]
-variable (S : Type*) [CommRing S] [Algebra R S]
+variable (R : Type*) [CommSemiring R]
+variable (S : Type*) [CommSemiring S] [Algebra R S]
 variable (N : Type*) [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N]
 variable (ι : Type*)
 
-open LinearMap TensorProduct
+open LinearMap
 
-private def TensorProduct.piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) where
+namespace TensorProduct
+
+private def piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) where
   toFun n := LinearMap.compLeft (toSpanSingleton R N n) ι
   map_add' x y := by
     ext i j
@@ -42,11 +48,11 @@ private def TensorProduct.piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R]
 
 /-- For any `R`-module `N` and index type `ι`, there is a natural
 linear map `N ⊗[R] (ι → R) →ₗ (ι → N)`. This map is an isomorphism if `ι` is finite. -/
-noncomputable def TensorProduct.piScalarRightHom : N ⊗[R] (ι → R) →ₗ[S] (ι → N) :=
+noncomputable def piScalarRightHom : N ⊗[R] (ι → R) →ₗ[S] (ι → N) :=
   AlgebraTensorModule.lift <| piScalarRightHomBil R S N ι
 
 @[simp]
-lemma TensorProduct.piScalarRightHom_tmul (x : N) (f : ι → R) :
+lemma piScalarRightHom_tmul (x : N) (f : ι → R) :
     piScalarRightHom R S N ι (x ⊗ₜ f) = (fun j ↦ f j • x) := by
   ext j
   simp [piScalarRightHom, piScalarRightHomBil]
@@ -54,7 +60,7 @@ lemma TensorProduct.piScalarRightHom_tmul (x : N) (f : ι → R) :
 variable [Fintype ι] [DecidableEq ι]
 
 private noncomputable
-def TensorProduct.piScalarRightInv : (ι → N) →ₗ[S] N ⊗[R] (ι → R) :=
+def piScalarRightInv : (ι → N) →ₗ[S] N ⊗[R] (ι → R) :=
   LinearMap.lsum S (fun _ ↦ N) S <| fun i ↦ {
     toFun := fun n ↦ n ⊗ₜ Pi.single i 1
     map_add' := fun x y ↦ by simp [add_tmul]
@@ -62,25 +68,25 @@ def TensorProduct.piScalarRightInv : (ι → N) →ₗ[S] N ⊗[R] (ι → R) :=
   }
 
 @[simp]
-private lemma TensorProduct.piScalarRightInv_single (x : N) (i : ι) :
+private lemma piScalarRightInv_single (x : N) (i : ι) :
     piScalarRightInv R S N ι (Pi.single i x) = x ⊗ₜ Pi.single i 1 := by
   simp [piScalarRightInv, Pi.single_apply, TensorProduct.ite_tmul]
 
-@[simp]
-lemma Pi.single_apply_smul (x : N) (i j : ι) :
-    (Pi.single i 1 : ι → R) j • x = (Pi.single i x : ι → N) j := by
-  simp [Pi.single_apply]
-
 /-- For any `R`-module `N` and finite index type `ι`, `N ⊗[R] (ι → R)` is canonically
 isomorphic to `ι → N`. -/
-noncomputable def TensorProduct.piScalarRight : N ⊗[R] (ι → R) ≃ₗ[S] (ι → N) :=
+noncomputable def piScalarRight : N ⊗[R] (ι → R) ≃ₗ[S] (ι → N) :=
   LinearEquiv.ofLinear
-    (piScalarRightHom R S N (ι := ι))
-    (piScalarRightInv R S N (ι := ι))
+    (piScalarRightHom R S N ι)
+    (piScalarRightInv R S N ι)
     (by ext i x j; simp [Pi.single_apply])
-    (by ext x i; simp)
+    (by ext x i; simp [Pi.single_apply_smul])
+
+@[simp]
+lemma piScalarRight_apply (x : N ⊗[R] (ι → R)) :
+    piScalarRight R S N ι x = piScalarRightHom R S N ι x := by
+  rfl
 
 @[simp]
-lemma TensorProduct.piScalarRight_tmul (x : N) (f : ι → R) :
-    piScalarRight R S N ι (x ⊗ₜ f) = (fun j ↦ f j • x) := by
+lemma piScalarRight_symm_single (x : N) (i : ι) :
+    (piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ Pi.single i 1 := by
   simp [piScalarRight]
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
index 458f1d4c8d1cea..70179a735dc318 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
@@ -15,6 +15,11 @@ This file shows that taking `TensorProduct`s commutes with taking `Prod`s in bot
 
 * `TensorProduct.prodLeft`
 * `TensorProduct.prodRight`
+
+## Notes
+
+See `Mathlib.LinearAlgebra.TensorProduct.Pi` for arbitrary products.
+
 -/
 
 universe uR uM₁ uM₂ uM₃
diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
index dd2830f74bb45a..2cf9f54e97bf91 100644
--- a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
+++ b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@@ -89,8 +89,6 @@ section PiFintype
 In this section we show that `ofTensorProduct` is an isomorphism if `M = R^n`.
 -/
 
-attribute [-simp] _root_.smul_eq_mul Algebra.id.smul_eq_mul
-
 variable (ι : Type*) [Fintype ι] [DecidableEq ι]
 
 private lemma piEquivOfFintype_comp_ofTensorProduct_eq :
@@ -98,7 +96,7 @@ private lemma piEquivOfFintype_comp_ofTensorProduct_eq :
       (TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).toLinearMap := by
   ext i j k
   suffices h : (if j = i then 1 else 0) = (if j = i then 1 else 0 : AdicCompletion I R).val k by
-    simpa [Pi.single_apply]
+    simpa [Pi.single_apply, -smul_eq_mul, -Algebra.id.smul_eq_mul]
   split <;> simp
 
 private lemma ofTensorProduct_eq :

From dd8f45e97e5bce9c94cbb3656b7b72ed4bbc2b05 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Thu, 18 Jul 2024 18:34:07 +0200
Subject: [PATCH 6/6] review suggestions

---
 .../AdicCompletion/AsTensorProduct.lean        | 18 ++++++------------
 1 file changed, 6 insertions(+), 12 deletions(-)

diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
index f19fbb9e6eeb3e..fac622842d38e2 100644
--- a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
+++ b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@@ -206,13 +206,8 @@ private def lTensorf :
     AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] M :=
   AlgebraTensorModule.map LinearMap.id f
 
-private lemma if_exact : Function.Exact (LinearMap.ker f).subtype f := by
-  intro x
-  constructor
-  · intro hx
-    exact ⟨⟨x, hx⟩, rfl⟩
-  · rintro ⟨x, rfl⟩
-    exact x.property
+private lemma if_exact : Function.Exact (LinearMap.ker f).subtype f := fun x ↦
+  ⟨fun hx ↦ ⟨⟨x, hx⟩, rfl⟩, by rintro ⟨x, rfl⟩; exact x.property⟩
 
 private lemma tens_exact : Function.Exact (lTensorKerIncl I M f) (lTensorf I M f) :=
   lTensor_exact (AdicCompletion I R) (if_exact M f) hf
@@ -345,6 +340,8 @@ lemma tensor_map_id_left_eq_map :
   ext x
   simp
 
+variable {f}
+
 lemma tensor_map_id_left_injective_of_injective (hf : Function.Injective f) :
     Function.Injective (AlgebraTensorModule.map LinearMap.id f :
         AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) := by
@@ -357,11 +354,8 @@ end
 
 /-- Adic completion of a Noetherian ring `R` is flat over `R`. -/
 instance flat_of_isNoetherian [IsNoetherianRing R] : Algebra.Flat R (AdicCompletion I R) where
-  out := by
-    apply (Module.Flat.iff_lTensor_injective' R (AdicCompletion I R)).mpr
-    intro J
-    apply tensor_map_id_left_injective_of_injective I (Submodule.subtype J)
-    exact Submodule.injective_subtype J
+  out := (Module.Flat.iff_lTensor_injective' R (AdicCompletion I R)).mpr <| fun J ↦
+    tensor_map_id_left_injective_of_injective I (Submodule.injective_subtype J)
 
 end Noetherian