update nozerosmuldivisors

ModuleLocalProperties/FinitePresentation.lean

@@ -73,3 +73,29 @@ lemma isNoetherianRing_of_localization_finitespan {R : Type*} [CommRing R](s : F
     IsNoetherianRing R :=
   (isNoetherianRing_iff_ideal_fg _).mpr <| fun _ => Ideal.fg_of_localizationSpan _ spn <|
   fun r => (isNoetherianRing_iff_ideal_fg _).mp (h r) <| _
+
+section
+
+variable {R M S_M : Type*} (S_R : Type*) [CommRing R] [CommRing S_R] [Algebra R S_R]
+    [AddCommGroup M] [Module R M] [AddCommGroup S_M] [Module R S_M] [Module S_R S_M]
+    [IsScalarTower R S_R S_M]
+    (S : Submonoid R) [IsLocalization S S_R]
+    (f : M →ₗ[R] S_M) [IsLocalizedModule S f]
+    {p q : Submodule R M}
+
+
+namespace Submodule
+
+lemma localized'_of_finite (h : p.FG) : (localized' S_R S f p).FG := by
+  rw [fg_def] at h ⊢
+  rcases h with ⟨s, hfin, hspan⟩
+  use f '' s
+  constructor
+  · exact Set.Finite.image f hfin
+  · rw [← hspan, localized'_span]
+
+lemma localized_of_finite (h : p.FG) : (localized S p).FG := localized'_of_finite _ _ _ h
+
+end Submodule
+
+end

ModuleLocalProperties/MissingLemmas/Localization.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yi Song
 -/
 import Mathlib.Algebra.Module.Submodule.Localization
-
+import Mathlib.RingTheory.Localization.Ideal
 open nonZeroDivisors
 
 namespace IsLocalization
@@ -41,17 +41,52 @@ end IsLocalization.nontrivial
 section IsDomain
 
 variable {R : Type*} (S_R : Type*) [CommRing R] [CommRing S_R] [Algebra R S_R]
-    (S : Submonoid R) [IsLocalization S S_R] [IsDomain R]
+    (S : Submonoid R) [IsLocalization S S_R]
 include S
 
-lemma isDomain_of_isDomain_nontrivial (h : 0 ∉ S) : IsDomain S_R :=
+lemma isDomain_of_isDomain_nontrivial [IsDomain R] (h : 0 ∉ S) : IsDomain S_R :=
   isDomain_of_le_nonZeroDivisors R <| le_nonZeroDivisors_of_noZeroDivisors h
 
-lemma isDomain_of_noZeroDivisors : NoZeroDivisors S_R := by
+lemma isDomain_of_noZeroDivisors [IsDomain R] : NoZeroDivisors S_R := by
   by_cases trivial : 0 ∈ S
   · haveI : Subsingleton S_R := subsingleton trivial
     apply Subsingleton.to_noZeroDivisors
   · haveI := isDomain_of_isDomain_nontrivial S_R S trivial
     apply IsDomain.to_noZeroDivisors
 
+lemma noZeroDivisors_of_noZeroDivisors [NoZeroDivisors R] : NoZeroDivisors S_R := by
+  by_cases nontrivial : Nontrivial R
+  · haveI := (isDomain_iff_noZeroDivisors_and_nontrivial R).mpr ⟨inferInstance , nontrivial⟩
+    exact isDomain_of_noZeroDivisors _ S
+  · haveI := not_nontrivial_iff_subsingleton.mp nontrivial
+    haveI : Subsingleton S_R := subsingleton <| (subsingleton_iff_zero_eq_one.mpr this) ▸ one_mem S
+    apply Subsingleton.to_noZeroDivisors
+
 end IsDomain
+
+section
+
+variable {R : Type*} (S_R : Type*) [CommSemiring R] [CommSemiring S_R] [Algebra R S_R]
+    (S : Submonoid R) [IsLocalization S S_R] (p q : Ideal R)
+include S
+
+lemma ideal_map_inf : Ideal.map (algebraMap R S_R) (p ⊓ q) =
+    Ideal.map (algebraMap R S_R) p ⊓ Ideal.map (algebraMap R S_R) q := by
+  apply eq_of_le_of_le <| Ideal.map_inf_le (algebraMap R S_R)
+  rintro x ⟨hp, hq⟩
+  rcases mk'_surjective S x with ⟨r, s, hmk⟩
+  rw [SetLike.mem_coe] at hp hq
+  rw [← hmk, mk'_mem_map_algebraMap_iff S] at hp hq ⊢
+  rcases hp with ⟨u, hu, hpmk⟩
+  rcases hq with ⟨v, hv, hqmk⟩
+  use u * v
+  constructor
+  · exact Submonoid.mul_mem S hu hv
+  · apply Ideal.mem_inf.mpr
+    constructor
+    · rw [mul_comm u, mul_assoc]
+      exact p.mul_mem_left _ hpmk
+    · rw [mul_assoc]
+      apply q.mul_mem_left _ hqmk
+
+end

ModuleLocalProperties/MissingLemmas/Submodule.lean

@@ -17,8 +17,8 @@ end zero_mem_nonZeroDivisors
 
 section mk_lemma
 
-variable {R M S_M : Type*} (S_R : Type*) [CommRing R] [CommRing S_R] [Algebra R S_R]
-    [AddCommGroup M] [Module R M] [AddCommGroup S_M] [Module R S_M] [Module S_R S_M]
+variable {R M S_M : Type*} (S_R : Type*) [CommSemiring R] [CommSemiring S_R] [Algebra R S_R]
+    [AddCommMonoid M] [Module R M] [AddCommMonoid S_M] [Module R S_M] [Module S_R S_M]
     [IsScalarTower R S_R S_M]
     (S : Submonoid R) [IsLocalization S S_R]
     (f : M →ₗ[R] S_M) [IsLocalizedModule S f]
@@ -30,7 +30,7 @@ lemma mk'_right_smul_mk' (m : M) (s t : S) :
     IsLocalization.mk' S_R 1 s • mk' f m t = mk' f m (s * t) := by
   rw[mk'_smul_mk', one_smul]
 
-lemma mk'_right_smul_mk_left' (m : M) (s : S) :
+lemma mk'_right_smul_mk'_left (m : M) (s : S) :
     IsLocalization.mk' S_R 1 s • f m = mk' f m s := by
   rw[← mul_one s, ← mk'_right_smul_mk' S_R, mk'_one, mul_one]
 
@@ -46,15 +46,15 @@ variable {R M S_M : Type*} (S_R : Type*) [CommRing R] [CommRing S_R] [Algebra R
     (S : Submonoid R) [IsLocalization S S_R]
     (f : M →ₗ[R] S_M) [IsLocalizedModule S f]
     (S_p : Submodule S_R S_M)
-#check Submodule.restrictScalars
+
 lemma localized'_comap_eq : localized' S_R S f (comap f (restrictScalars R S_p)) = S_p := by
   ext x
   constructor
   all_goals intro h
   · rw [mem_localized'] at h
     rcases h with ⟨m, hm, s, hmk⟩
     rw [mem_comap, restrictScalars_mem] at hm
-    rw [← hmk, ← mk'_right_smul_mk_left' S_R]
+    rw [← hmk, ← mk'_right_smul_mk'_left S_R]
     exact smul_mem _ _ hm
   · rw [mem_localized']
     rcases mk'_surjective S f x with ⟨⟨m, s⟩, hmk⟩
@@ -154,7 +154,7 @@ lemma localized'_span (s : Set M) : localized' S_R S f (span R s) = span S_R (f
     rw [← hmk]
     clear hmk
     induction' hm using span_induction with a ains a b _ _ hamk hbmk r a _ hamk
-    · rw [← mk'_right_smul_mk_left' S_R]
+    · rw [← mk'_right_smul_mk'_left S_R]
       exact smul_mem _ _ <| mem_span.mpr fun p hsub ↦ hsub <| Set.mem_image_of_mem f ains
     · simp only [mk'_zero, zero_mem]
     · rw [mk'_add]