From 7cd339444de298761c9698ed16e9e633888df701 Mon Sep 17 00:00:00 2001
From: syur2 <sif4delta0@mail.ustc.edu.cn>
Date: Tue, 15 Oct 2024 12:29:41 +0800
Subject: [PATCH] fix

---
 .../MissingLemmas/LocalizedModule.lean        |  7 ++++-
 .../MissingLemmas/TensorProduct.lean          | 27 ++++++++++---------
 2 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean b/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean
index 58d265b..11eba84 100644
--- a/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean
+++ b/ModuleLocalProperties/MissingLemmas/LocalizedModule.lean
@@ -289,6 +289,8 @@ lemma LocalizedMapLift_mk (f : M →ₗ[R] N) (m : M) (s t : S) :
 
 end LocalizedMapLift
 
+--to make a algebraequiv between Localzation S and LocalzedModule S R
+
 section Localization_is_LocalizedModule
 
 namespace Localization
@@ -384,6 +386,9 @@ lemma Map_inj : Function.Injective (Map S) := by
 noncomputable def Equiv : Localization S ≃ₐ[R] LocalizedModule S R :=
   AlgEquiv.ofBijective (Map S) ⟨Map_inj _,Map_surj _⟩
 
-lemma Equiv_mk (r : R) (s : S) : Map S (Localization.mk r s) = mk r s := rfl
+lemma Equiv_mk (r : R) (s : S) : Equiv S (Localization.mk r s) = mk r s := rfl
+
+lemma Equiv_symm_mk (r : R) (s : S) : (Equiv S).symm (mk r s) = Localization.mk r s :=
+  (AlgEquiv.symm_apply_eq (Equiv S)).mpr rfl
 
 end Localization
diff --git a/ModuleLocalProperties/MissingLemmas/TensorProduct.lean b/ModuleLocalProperties/MissingLemmas/TensorProduct.lean
index 7182bd1..cab429b 100644
--- a/ModuleLocalProperties/MissingLemmas/TensorProduct.lean
+++ b/ModuleLocalProperties/MissingLemmas/TensorProduct.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Song Yi
 -/
 import Mathlib.Algebra.Module.LocalizedModule
-import Mathlib.RingTheory.Flat.Basic
-import Mathlib.RingTheory.IsTensorProduct
+
 import ModuleLocalProperties.MissingLemmas.LocalizedModule
 
 open  TensorProduct LocalizedModule
@@ -33,8 +32,8 @@ section LocalizedModule_TensorProduct_Exchange
 
 namespace LocalizedModule
 
-variable {R : Type*} [CommSemiring R] (S : Submonoid R) (M N : Type*) [AddCommMonoid M] [Module R M] [AddCommMonoid N]
-  [Module R N]
+variable {R : Type*} [CommSemiring R] (S : Submonoid R) (M N : Type*) [AddCommMonoid M] [Module R M]
+    [AddCommMonoid N] [Module R N]
 
 noncomputable def TensorProductBilinearMap : (LocalizedModule S M) →ₗ[Localization S]
     (LocalizedModule S N) →ₗ[Localization S] LocalizedModule S (M ⊗[R] N) :=
@@ -84,7 +83,7 @@ lemma InvTensorProductMap_apply' (m : M) (n : N) (s t : S) :
     InvTensorProductMap S M N (mk (m ⊗ₜ n) (s * t)) = ((mk m s) ⊗ₜ (mk n t)) := by
   rw [InvTensorProductMap_apply]
   symm
-  rw [← mk_right_smul_mk_den_one, ← mk_right_smul_mk_den_one (s := t), TensorProduct.smul_tmul_smul,
+  rw [← mk_right_smul_mk_left, ← mk_right_smul_mk_left (s := t), TensorProduct.smul_tmul_smul,
     Localization.mk_mul, one_mul]
 
 lemma TensorProductMap_rightInv :
@@ -93,18 +92,22 @@ lemma TensorProductMap_rightInv :
   induction' x with y s
   dsimp
   induction' y with m n m n hm hn
-  · simp only [zero_mk, map_zero]
+  · rw [zero_mk, map_zero, map_zero]
   · rw [InvTensorProductMap_apply, map_smul, TensorProductMap_mk,
-      one_mul, mk_right_smul_mk_den_one]
+      one_mul, mk_right_smul_mk_left]
   · rw [mk_add_mk_right, map_add, map_add, hm, hn]
 
 lemma TensorProductMap_leftInv :
     InvTensorProductMap S M N ∘ₗ (TensorProductMap S M N) = LinearMap.id := by
-  ext x y
-  dsimp
-  induction' x with m s
-  induction' y with n t
-  rw [TensorProductMap_mk, InvTensorProductMap_apply']
+  ext u
+  induction' u with x y a b ha hb
+  · rw [map_zero, map_zero]
+  · dsimp
+    induction' x with m s
+    induction' y with n t
+    rw [TensorProductMap_mk, InvTensorProductMap_apply']
+  · rw [LinearMap.id_coe, id_eq, map_add] at *
+    rw[ha, hb]
 
 noncomputable def TensorProductEquiv : (LocalizedModule S M) ⊗[Localization S] (LocalizedModule S N)
     ≃ₗ[Localization S] LocalizedModule S (M ⊗[R] N) :=