move map' from LocalizedModule to Defs , and update Isom

ModuleLocalProperties/Defs.lean

@@ -37,6 +37,26 @@ noncomputable def LocalizedModule.map {R : Type*} [CommSemiring R] (S : Submonoi
     (M →ₗ[R] M') →ₗ[R] (LocalizedModule S M) →ₗ[R] (LocalizedModule S M') :=
   IsLocalizedModule.map S (mkLinearMap S M) (mkLinearMap S M')
 
+section LocalizedModule.map'
+
+variable {R : Type*} [CommSemiring R] (S : Submonoid R) {M N : Type*}
+    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+
+noncomputable def map' : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N where
+  toFun := fun f => LinearMap.extendScalarsOfIsLocalization S _ <| LocalizedModule.map S f
+  map_add' := by
+    intro f g
+    ext x
+    dsimp
+    rw [map_add, LinearMap.add_apply]
+  map_smul' := by
+    intro r f
+    ext x
+    dsimp
+    rw [map_smul, LinearMap.smul_apply]
+
+end LocalizedModule.map'
+
 section Properties
 
 section IsLocalizedModule

ModuleLocalProperties/Flat.lean

@@ -7,18 +7,13 @@ import Mathlib.RingTheory.Flat.Basic
 import Mathlib.Algebra.Module.Submodule.Localization
 import Mathlib.RingTheory.Localization.BaseChange
 
-import ModuleLocalProperties.MissingLemmas.LocalizedModule
 import ModuleLocalProperties.MissingLemmas.Submodule
 import ModuleLocalProperties.MissingLemmas.FlatIff
-import ModuleLocalProperties.MissingLemmas.TensorProduct
 import ModuleLocalProperties.Basic
+import ModuleLocalProperties.Isom
 
 open Submodule IsLocalizedModule LocalizedModule Ideal IsLocalization LinearMap
 
-lemma inj_of_local {R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Injective (map' J.primeCompl f)) : Function.Injective f := by
-  simp only [← ker_eq_bot] at h ⊢
-  exact submodule_eq_bot_of_localization _ fun J hJ ↦ (localized'_ker_eq_ker_localizedMap _ _ _ _ f).trans (h J hJ)
-
 section Tensor
 open TensorProduct IsBaseChange LinearEquiv
 
@@ -59,7 +54,7 @@ theorem Flat_of_localization (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Module.F
     (LocalizedModule.AtPrime J M)) : Module.Flat R M := by
   apply (Module.Flat.iff_rTensor_preserves_injective_linearMap' R M).mpr
   intro N N' _ _ _ _ f finj
-  apply inj_of_local
+  apply injective_of_localization
   intro J hJ
   have inj : Function.Injective (map' J.primeCompl f) := by
     unfold map' LocalizedModule.map
@@ -91,7 +86,7 @@ theorem Flat_of_localization' (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Module.
     (LocalizedModule.AtPrime J M)) : Module.Flat R M := by
   apply (Module.Flat.iff_rTensor_preserves_injective_linearMap' R M).mpr
   intro N N' _ _ _ _ f finj
-  apply inj_of_local
+  apply injective_of_localization
   intro J hJ
   have inj : Function.Injective (map' J.primeCompl f) := by
     unfold map' LocalizedModule.map

ModuleLocalProperties/Isom.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2024 Yi Song. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yi Song, SiHan Su
+-/
+import Mathlib.Algebra.Module.Submodule.Localization
+
+import ModuleLocalProperties.Basic
+
+open Submodule IsLocalizedModule LocalizedModule Ideal LinearMap
+
+variable {R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+    (f : M →ₗ[R] N)
+
+lemma injective_of_localization
+    (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Injective (map' J.primeCompl f)) :
+    Function.Injective f := by
+  simp only [← ker_eq_bot] at h ⊢
+  exact submodule_eq_bot_of_localization _
+    fun J hJ ↦ (localized'_ker_eq_ker_localizedMap _ _ _ _ f).trans (h J hJ)
+
+lemma surjective_of_localization
+    (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Function.Surjective (map' J.primeCompl f)) :
+    Function.Surjective f := by
+  simp only [← range_eq_top] at h ⊢
+  exact submodule_eq_top_of_localization _
+    fun J hJ ↦ (localized'_range_eq_range_localizedMap _ _ _ f).trans (h J hJ)
+
+lemma bijective_of_localization
+    (h : ∀ (J : Ideal R) (_ : J.IsMaximal), Function.Bijective (map' J.primeCompl f)) :
+    Function.Bijective f :=
+  ⟨injective_of_localization _ fun J hJ => (h J hJ).1,
+  surjective_of_localization _ fun J hJ => (h J hJ).2⟩
+
+noncomputable def linearEquivOfLocalization (h : ∀ (J : Ideal R) (_ : J.IsMaximal),
+    Function.Bijective (map' J.primeCompl f)) : M ≃ₗ[R] N :=
+  LinearEquiv.ofBijective f <| bijective_of_localization _ h

ModuleLocalProperties/MissingLemmas/LocalizedModule.lean

@@ -184,26 +184,6 @@ end lift.LiftOnLocalizationModule'
 
 end liftOnLocalizationModule
 
-section LocalizedModule.map'
-
-variable {R : Type*} [CommSemiring R] (S : Submonoid R) {M N : Type*}
-    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
-
-noncomputable def map' : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N where
-  toFun := fun f => LinearMap.extendScalarsOfIsLocalization S _ <| map S f
-  map_add' := by
-    intro f g
-    ext x
-    dsimp
-    rw [map_add, LinearMap.add_apply]
-  map_smul' := by
-    intro r f
-    ext x
-    dsimp
-    rw [map_smul, LinearMap.smul_apply]
-
-end LocalizedModule.map'
-
 section LocalizedModule.mapfromlift
 -- This is LocalizedModule.map and LocalizedModule.map' with out using IsLocalizedModule.map
 

ModuleLocalProperties/MissingLemmas/Units.lean

@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2024 Yi Song. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yi Song
+-/
+
 import Mathlib.Algebra.Group.Units
 
 open IsUnit

ModuleLocalProperties/SpanIsom.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Yi Song. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yi Song, Yongle Hu
 -/
+
 import ModuleLocalProperties.Basic
 
 open Submodule IsLocalizedModule LocalizedModule Ideal
@@ -12,31 +13,27 @@ variable {R M M' : Type*} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGro
 include spn
 
 lemma injective_of_localization_finitespan (h : ∀ r : s, Function.Injective
-    ((map (Submonoid.powers r.1) f).extendScalarsOfIsLocalization (Submonoid.powers r.1)
-    (Localization (Submonoid.powers r.1)))) :
+    (map' (Submonoid.powers r.1) f)) :
     Function.Injective f := by
   simp only [← LinearMap.ker_eq_bot] at h ⊢
   apply submodule_eq_bot_of_localization_finitespan _ _ spn
   intro a
-  exact Eq.trans (LinearMap.localized'_ker_eq_ker_localizedMap _ _ _ _ f) (h a)
+  exact (LinearMap.localized'_ker_eq_ker_localizedMap _ _ _ _ f).trans (h a)
 
 lemma surjective_of_localization_finitespan (h : ∀ r : s, Function.Surjective
-    ((map (Submonoid.powers r.1) f).extendScalarsOfIsLocalization (Submonoid.powers r.1)
-    (Localization (Submonoid.powers r.1)))) :
+    (map' (Submonoid.powers r.1) f)) :
     Function.Surjective f := by
   simp only [← LinearMap.range_eq_top] at h ⊢
   apply submodule_eq_top_of_localization_finitespan _ _ spn
   intro a
-  exact Eq.trans (LinearMap.localized'_range_eq_range_localizedMap _ _ _ f) (h a)
+  exact (LinearMap.localized'_range_eq_range_localizedMap _ _ _ f).trans (h a)
 
 lemma bijective_of_localization_finitespan (h : ∀ r : s, Function.Bijective
-    ((map (Submonoid.powers r.1) f).extendScalarsOfIsLocalization (Submonoid.powers r.1)
-    (Localization (Submonoid.powers r.1)))) :
+    (map' (Submonoid.powers r.1) f)) :
     Function.Bijective f :=
   ⟨injective_of_localization_finitespan _ spn _ fun r => (h r).1,
   surjective_of_localization_finitespan _ spn _ fun r => (h r).2⟩
 
 noncomputable def linearEquivOfLocalizationFinitespan (h : ∀ r : s, Function.Bijective
-    ((map (Submonoid.powers r.1) f).extendScalarsOfIsLocalization (Submonoid.powers r.1)
-    (Localization (Submonoid.powers r.1)))) : M ≃ₗ[R] M' :=
+    (map' (Submonoid.powers r.1) f)) : M ≃ₗ[R] M' :=
   LinearEquiv.ofBijective f <| bijective_of_localization_finitespan _ spn _ h