From f60fcd9f1b61b5da8c8e49fd06691c6cc30beecc Mon Sep 17 00:00:00 2001
From: syur2 <sif4delta0@mail.ustc.edu.cn>
Date: Sat, 19 Oct 2024 10:26:22 +0800
Subject: [PATCH] Update NoZeroSMulDivisors.lean

---
 ModuleLocalProperties/NoZeroSMulDivisors.lean | 25 ++++++++++++++-----
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/ModuleLocalProperties/NoZeroSMulDivisors.lean b/ModuleLocalProperties/NoZeroSMulDivisors.lean
index 9232dcd..3621de2 100644
--- a/ModuleLocalProperties/NoZeroSMulDivisors.lean
+++ b/ModuleLocalProperties/NoZeroSMulDivisors.lean
@@ -11,12 +11,6 @@ import ModuleLocalProperties.MissingLemmas.LocalizedModule
 
 open Submodule LocalizedModule IsLocalizedModule LinearMap nonZeroDivisors
 
-#check IsLocalization.map_comap
-#check Module.annihilator
-#check NoZeroSMulDivisors
-#check IsLocalization.map_nonZeroDivisors_le
-#check IsDomain
-
 section missinglemma
 
 lemma IsLocalization.mem_map_nonZeroDivisors {R : Type*} [CommSemiring R] (S : Submonoid R)
@@ -111,3 +105,22 @@ lemma localized_torsion [IsDomain R] :
     exact localized_torsion_nontrival_ge _ _ trivial
 
 end localized_torsion_commutivity
+
+section NoZeroSMulDivisors_local_property
+
+variable {R : Type*} [CommRing R] [IsDomain R] (M : Type*) [AddCommGroup M] [Module R M]
+
+lemma noZeroSMulDivisors_of_localization (h : ∀ (J : Ideal R) (hJ : J.IsMaximal),
+    NoZeroSMulDivisors (Localization J.primeCompl) (LocalizedModule J.primeCompl M)) :
+    NoZeroSMulDivisors R M :=
+  noZeroSMulDivisors_iff_torsion_eq_bot.mpr <| submodule_eq_bot_of_localization _ <| fun J hJ ↦
+  localized_torsion J.primeCompl M ▸ noZeroSMulDivisors_iff_torsion_eq_bot.mp <| h J hJ
+
+lemma noZeroSMulDivisors_of_localization_iff :
+    NoZeroSMulDivisors R M ↔ ∀ (J : Ideal R) (hJ : J.IsMaximal),
+    NoZeroSMulDivisors (Localization J.primeCompl) (LocalizedModule J.primeCompl M) :=
+  ⟨fun h J _ ↦ (noZeroSMulDivisors_iff_torsion_eq_bot.mp h) ▸ localized_torsion J.primeCompl M ▸
+    noZeroSMulDivisors_iff_torsion_eq_bot.mpr <| localized_bot _ ,
+  fun h ↦ noZeroSMulDivisors_of_localization M h⟩
+
+end NoZeroSMulDivisors_local_property