chore(RingTheory): improve and generalize submodule localization API (#…

…19118)

In Algebra/Module/LocalizedModule/Submodule, we introduce `Submodule.localized₀`, which is localization of a submodule considered as a submodule over the base ring rather than the localization. This allows us to talk about the localization of a submodule without choosing a specific ring localization, just like what `IsLocalizedModule` allows us to do for localization of a module.

As applications, `Rₚ` and every hypothesis depending on it are completely removed from the statement of `Submodule.le_of_localization_maximal`, etc. in RingTheory/LocalProperties/Submodule. We also reorder lemmas in this file to make the development more natural and golf the proofs (making use of `Module.eqIdeal` introduced in RingTheory/Ideal/Defs; also add some trivial lemmas.

In RingTheory/LocalProperties/Projective, we fix a proof due to removed explicit argument `Rₚ` and remove some unnecessary lines.

Mathlib/Algebra/Module/LocalizedModule/Submodule.lean

@@ -28,49 +28,73 @@ Results about localizations of submodules and quotient modules are provided in t
 
 open nonZeroDivisors
 
-universe u u' v v' w w'
-
-variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'}
-variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N]
+variable {R S M N : Type*}
+variable (S) [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid N]
 variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N]
 variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f]
 variable (M' : Submodule R M)
 
-/-- Let `S` be the localization of `R` at `p` and `N` be the localization of `M` at `p`.
-This is the localization of an `R`-submodule of `M` viewed as an `S`-submodule of `N`. -/
-def Submodule.localized' : Submodule S N where
+namespace Submodule
+
+/-- Let `N` be a localization of an `R`-module `M` at `p`.
+This is the localization of an `R`-submodule of `M` viewed as an `R`-submodule of `N`. -/
+def localized₀ : Submodule R N where
   carrier := { x | ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x }
-  add_mem' := fun {x} {y} ⟨m, hm, s, hx⟩ ⟨n, hn, t, hy⟩ ↦ ⟨t • m + s • n, add_mem (M'.smul_mem t hm)
+  add_mem' := fun {x y} ⟨m, hm, s, hx⟩ ⟨n, hn, t, hy⟩ ↦ ⟨t • m + s • n, add_mem (M'.smul_mem t hm)
     (M'.smul_mem s hn), s * t, by rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']⟩
   zero_mem' := ⟨0, zero_mem _, 1, by simp⟩
-  smul_mem' := fun r x h ↦ by
-    have ⟨m, hm, s, hx⟩ := h
+  smul_mem' r x := by
+    rintro ⟨m, hm, s, hx⟩
+    exact ⟨r • m, smul_mem M' _ hm, s, by rw [IsLocalizedModule.mk'_smul, hx]⟩
+
+/-- Let `S` be the localization of `R` at `p` and `N` be a localization of `M` at `p`.
+This is the localization of an `R`-submodule of `M` viewed as an `S`-submodule of `N`. -/
+def localized' : Submodule S N where
+  __ := localized₀ p f M'
+  smul_mem' := fun r x ⟨m, hm, s, hx⟩ ↦ by
     have ⟨y, t, hyt⟩ := IsLocalization.mk'_surjective p r
     exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩
 
-lemma Submodule.mem_localized' (x : N) :
-    x ∈ Submodule.localized' S p f M' ↔ ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x :=
+lemma mem_localized₀ (x : N) :
+    x ∈ localized₀ p f M' ↔ ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x :=
+  Iff.rfl
+
+lemma mem_localized' (x : N) :
+    x ∈ localized' S p f M' ↔ ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x :=
   Iff.rfl
 
+/-- `localized₀` is the same as `localized'` considered as a submodule over the base ring. -/
+lemma restrictScalars_localized' :
+    (localized' S p f M').restrictScalars R = localized₀ p f M' :=
+  rfl
+
 /-- The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`. -/
-abbrev Submodule.localized : Submodule (Localization p) (LocalizedModule p M) :=
+abbrev localized : Submodule (Localization p) (LocalizedModule p M) :=
   M'.localized' (Localization p) p (LocalizedModule.mkLinearMap p M)
 
 @[simp]
-lemma Submodule.localized'_bot : (⊥ : Submodule R M).localized' S p f = ⊥ := by
+lemma localized₀_bot : (⊥ : Submodule R M).localized₀ p f = ⊥ := by
   rw [← le_bot_iff]
   rintro _ ⟨_, rfl, s, rfl⟩
   simp only [IsLocalizedModule.mk'_zero, mem_bot]
 
 @[simp]
-lemma Submodule.localized'_top : (⊤ : Submodule R M).localized' S p f = ⊤ := by
+lemma localized'_bot : (⊥ : Submodule R M).localized' S p f = ⊥ :=
+  SetLike.ext' (by apply SetLike.ext'_iff.mp <| Submodule.localized₀_bot p f)
+
+@[simp]
+lemma localized₀_top : (⊤ : Submodule R M).localized₀ p f = ⊤ := by
   rw [← top_le_iff]
   rintro x _
   obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x
   exact ⟨x, trivial, s, rfl⟩
 
 @[simp]
-lemma Submodule.localized'_span (s : Set M) : (span R s).localized' S p f = span S (f '' s) := by
+lemma localized'_top : (⊤ : Submodule R M).localized' S p f = ⊤ :=
+  SetLike.ext' (by apply SetLike.ext'_iff.mp <| Submodule.localized₀_top p f)
+
+@[simp]
+lemma localized'_span (s : Set M) : (span R s).localized' S p f = span S (f '' s) := by
   apply le_antisymm
   · rintro _ ⟨x, hx, t, rfl⟩
     have := IsLocalizedModule.mk'_smul_mk' S f 1 x t 1
@@ -87,29 +111,45 @@ lemma Submodule.localized'_span (s : Set M) : (span R s).localized' S p f = span
 
 /-- The localization map of a submodule. -/
 @[simps!]
-def Submodule.toLocalized' : M' →ₗ[R] M'.localized' S p f :=
-  f.restrict (q := (M'.localized' S p f).restrictScalars R) (fun x hx ↦ ⟨x, hx, 1, by simp⟩)
+def toLocalized₀ : M' →ₗ[R] M'.localized₀ p f := f.restrict fun x hx ↦ ⟨x, hx, 1, by simp⟩
 
 /-- The localization map of a submodule. -/
-abbrev Submodule.toLocalized : M' →ₗ[R] M'.localized p :=
+@[simps!]
+def toLocalized' : M' →ₗ[R] M'.localized' S p f := toLocalized₀ p f M'
+
+/-- The localization map of a submodule. -/
+abbrev toLocalized : M' →ₗ[R] M'.localized p :=
   M'.toLocalized' (Localization p) p (LocalizedModule.mkLinearMap p M)
 
-instance Submodule.isLocalizedModule : IsLocalizedModule p (M'.toLocalized' S p f) where
+instance : IsLocalizedModule p (M'.toLocalized₀ p f) where
   map_units x := by
     simp_rw [Module.End_isUnit_iff]
     constructor
     · exact fun _ _ e ↦ Subtype.ext
         (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))
-    · rintro m
-      use (IsLocalization.mk' S 1 x) • m
-      rw [Module.algebraMap_end_apply, ← smul_assoc, IsLocalization.smul_mk'_one,
-        IsLocalization.mk'_self', one_smul]
+    · rintro ⟨_, m, hm, s, rfl⟩
+      refine ⟨⟨IsLocalizedModule.mk' f m (s * x), ⟨_, hm, _, rfl⟩⟩, Subtype.ext ?_⟩
+      rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower,
+        ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right]
   surj' := by
     rintro ⟨y, x, hx, s, rfl⟩
     exact ⟨⟨⟨x, hx⟩, s⟩, by ext; simp⟩
   exists_of_eq e := by simpa [Subtype.ext_iff] using
       IsLocalizedModule.exists_of_eq (S := p) (f := f) (congr_arg Subtype.val e)
 
+instance isLocalizedModule : IsLocalizedModule p (M'.toLocalized' S p f) :=
+  inferInstanceAs (IsLocalizedModule p (M'.toLocalized₀ p f))
+
+end Submodule
+
+section Quotient
+
+variable {R S M N : Type*}
+variable (S) [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N]
+variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N]
+variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f]
+variable (M' : Submodule R M)
+
 /-- The localization map of a quotient module. -/
 def Submodule.toLocalizedQuotient' : M ⧸ M' →ₗ[R] N ⧸ M'.localized' S p f :=
   Submodule.mapQ M' ((M'.localized' S p f).restrictScalars R) f (fun x hx ↦ ⟨x, hx, 1, by simp⟩)
@@ -147,10 +187,12 @@ instance IsLocalizedModule.toLocalizedQuotient' (M' : Submodule R M) :
 instance (M' : Submodule R M) : IsLocalizedModule p (M'.toLocalizedQuotient p) :=
   IsLocalizedModule.toLocalizedQuotient' _ _ _ _
 
+end Quotient
+
 section LinearMap
 
-variable {P : Type w} [AddCommGroup P] [Module R P]
-variable {Q : Type w'} [AddCommGroup Q] [Module R Q] [Module S Q] [IsScalarTower R S Q]
+variable {P : Type*} [AddCommGroup P] [Module R P]
+variable {Q : Type*} [AddCommGroup Q] [Module R Q] [Module S Q] [IsScalarTower R S Q]
 variable (f' : P →ₗ[R] Q) [IsLocalizedModule p f']
 
 lemma LinearMap.localized'_ker_eq_ker_localizedMap (g : M →ₗ[R] P) :

Mathlib/RingTheory/Ideal/Defs.lean

@@ -68,6 +68,15 @@ theorem unit_mul_mem_iff_mem {x y : α} (hy : IsUnit y) : y * x ∈ I ↔ x ∈
 
 end Ideal
 
+/-- For two elements `m` and `m'` in an `R`-module `M`, the set of elements `r : R` with
+equal scalar product with `m` and `m'` is an ideal of `R`. If `M` is a group, this coincides
+with the kernel of `LinearMap.toSpanSingleton R M (m - m')`. -/
+def Module.eqIdeal (R) {M} [Semiring R] [AddCommMonoid M] [Module R M] (m m' : M) : Ideal R where
+  carrier := {r : R | r • m = r • m'}
+  add_mem' h h' := by simpa [add_smul] using congr($h + $h')
+  zero_mem' := by simp_rw [Set.mem_setOf, zero_smul]
+  smul_mem' _ _ h := by simpa [mul_smul] using congr(_ • $h)
+
 end Semiring
 
 section CommSemiring

Mathlib/RingTheory/LocalProperties/Projective.lean

@@ -31,8 +31,8 @@ variable [AddCommGroup N'] [Module R N'] (S : Submonoid R)
 theorem Module.projective_of_isLocalizedModule {Rₛ Mₛ} [AddCommGroup Mₛ] [Module R Mₛ]
     [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ]
     (S) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ] [IsLocalizedModule S f] [Module.Projective R M] :
-      Module.Projective Rₛ Mₛ :=
-    Projective.of_equiv (IsLocalizedModule.isBaseChange S Rₛ f).equiv
+    Module.Projective Rₛ Mₛ :=
+  Projective.of_equiv (IsLocalizedModule.isBaseChange S Rₛ f).equiv
 
 theorem LinearMap.split_surjective_of_localization_maximal
     (f : M →ₗ[R] N) [Module.FinitePresentation R N]
@@ -41,18 +41,8 @@ theorem LinearMap.split_surjective_of_localization_maximal
       (LocalizedModule.map I.primeCompl f).comp g = LinearMap.id) :
     ∃ (g : N →ₗ[R] M), f.comp g = LinearMap.id := by
   show LinearMap.id ∈ LinearMap.range (LinearMap.llcomp R N M N f)
-  have inst₁ (I : Ideal R) [I.IsMaximal] :
-    IsLocalizedModule I.primeCompl (LocalizedModule.map (M := N) (N := N) I.primeCompl) :=
-      inferInstance
-  have inst₂ (I : Ideal R) [I.IsMaximal] :
-    IsLocalizedModule I.primeCompl (LocalizedModule.map (M := N) (N := M) I.primeCompl) :=
-      inferInstance
-  apply
-    @Submodule.mem_of_localization_maximal R (N →ₗ[R] N) _ _ _
-      (fun P _ ↦ Localization.AtPrime P) _ _ _ _ _ _ _ _
-      (fun P _ ↦ LocalizedModule.map P.primeCompl)
-      (fun P _ ↦ inst₁ P)
-  intro I hI
+  refine Submodule.mem_of_localization_maximal _ (fun P _ ↦ LocalizedModule.map P.primeCompl) _ _
+    fun I hI ↦ ?_
   rw [LocalizedModule.map_id]
   have : LinearMap.id ∈ LinearMap.range (LinearMap.llcomp _
     (LocalizedModule I.primeCompl N) _ _ (LocalizedModule.map I.primeCompl f)) := H I hI

Mathlib/RingTheory/LocalProperties/Submodule.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, David Swinarski
 -/
 import Mathlib.Algebra.Module.LocalizedModule.Submodule
-import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.RingTheory.Localization.AtPrime
 
 /-!
@@ -15,87 +14,113 @@ In this file, we show that several conditions on submodules can be checked on st
 
 open scoped nonZeroDivisors
 
-variable {R A M} [CommRing R] [CommRing A] [AddCommGroup M] [Algebra R A] [Module R M] [Module A M]
+variable {R M M₁ : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
+  [AddCommMonoid M₁] [Module R M₁]
+
+section maximal
 
 variable
   (Rₚ : ∀ (P : Ideal R) [P.IsMaximal], Type*)
-  [∀ (P : Ideal R) [P.IsMaximal], CommRing (Rₚ P)]
+  [∀ (P : Ideal R) [P.IsMaximal], CommSemiring (Rₚ P)]
   [∀ (P : Ideal R) [P.IsMaximal], Algebra R (Rₚ P)]
   [∀ (P : Ideal R) [P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
   (Mₚ : ∀ (P : Ideal R) [P.IsMaximal], Type*)
-  [∀ (P : Ideal R) [P.IsMaximal], AddCommGroup (Mₚ P)]
+  [∀ (P : Ideal R) [P.IsMaximal], AddCommMonoid (Mₚ P)]
   [∀ (P : Ideal R) [P.IsMaximal], Module R (Mₚ P)]
   [∀ (P : Ideal R) [P.IsMaximal], Module (Rₚ P) (Mₚ P)]
   [∀ (P : Ideal R) [P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
   (f : ∀ (P : Ideal R) [P.IsMaximal], M →ₗ[R] Mₚ P)
-  [inst : ∀ (P : Ideal R) [P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
+  [∀ (P : Ideal R) [P.IsMaximal], IsLocalizedModule P.primeCompl (f P)]
+  (M₁ₚ : ∀ (P : Ideal R) [P.IsMaximal], Type*)
+  [∀ (P : Ideal R) [P.IsMaximal], AddCommMonoid (M₁ₚ P)]
+  [∀ (P : Ideal R) [P.IsMaximal], Module R (M₁ₚ P)]
+  (f₁ : ∀ (P : Ideal R) [P.IsMaximal], M₁ →ₗ[R] M₁ₚ P)
+  [∀ (P : Ideal R) [P.IsMaximal], IsLocalizedModule P.primeCompl (f₁ P)]
+
+theorem Submodule.mem_of_localization_maximal (m : M) (N : Submodule R M)
+    (h : ∀ (P : Ideal R) [P.IsMaximal], f P m ∈ N.localized₀ P.primeCompl (f P)) :
+    m ∈ N := by
+  let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)
+  suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
+  refine Not.imp_symm I.exists_le_maximal fun ⟨P, hP, le⟩ ↦ ?_
+  obtain ⟨a, ha, s, e⟩ := h P
+  rw [← IsLocalizedModule.mk'_one P.primeCompl, IsLocalizedModule.mk'_eq_mk'_iff] at e
+  obtain ⟨t, ht⟩ := e
+  simp_rw [smul_smul] at ht
+  exact (t * s).2 (le <| by apply ht ▸ smul_mem _ _ ha)
 
 /-- Let `N₁ N₂ : Submodule R M`. If the localization of `N₁` at each maximal ideal `P` is
 included in the localization of `N₂` at `P`, then `N₁ ≤ N₂`. -/
 theorem Submodule.le_of_localization_maximal {N₁ N₂ : Submodule R M}
     (h : ∀ (P : Ideal R) [P.IsMaximal],
-      N₁.localized' (Rₚ P) P.primeCompl (f P) ≤ N₂.localized' (Rₚ P) P.primeCompl (f P)) :
-    N₁ ≤ N₂ := by
-  intro x hx
-  suffices N₂.colon (Submodule.span R {x}) = ⊤ by
-    simpa using Submodule.mem_colon.mp
-      (show (1 : R) ∈ N₂.colon (Submodule.span R {x}) from this.symm ▸ Submodule.mem_top) x
-      (Submodule.mem_span_singleton_self x)
-  refine Not.imp_symm (N₂.colon (Submodule.span R {x})).exists_le_maximal ?_
-  push_neg
-  intro P hP le
-  obtain ⟨a, ha, s, e⟩ := h P ⟨x, hx, 1, rfl⟩
-  rw [IsLocalizedModule.mk'_eq_mk'_iff] at e
-  obtain ⟨t, ht⟩ := e
-  simp at ht
-  refine (t * s).2 (le (Submodule.mem_colon_singleton.mpr ?_))
-  simp only [Submonoid.coe_mul, mul_smul, ← Submonoid.smul_def, ht]
-  exact N₂.smul_mem _ ha
+      N₁.localized₀ P.primeCompl (f P) ≤ N₂.localized₀ P.primeCompl (f P)) :
+    N₁ ≤ N₂ :=
+  fun m hm ↦ mem_of_localization_maximal _ f _ _ fun P hP ↦ h P ⟨m, hm, 1, by simp⟩
 
 /-- Let `N₁ N₂ : Submodule R M`. If the localization of `N₁` at each maximal ideal `P` is equal to
 the localization of `N₂` at `P`, then `N₁ = N₂`. -/
-theorem Submodule.eq_of_localization_maximal {N₁ N₂ : Submodule R M}
+theorem Submodule.eq_of_localization₀_maximal {N₁ N₂ : Submodule R M}
     (h : ∀ (P : Ideal R) [P.IsMaximal],
-      N₁.localized' (Rₚ P) P.primeCompl (f P) = N₂.localized' (Rₚ P) P.primeCompl (f P)) :
+      N₁.localized₀ P.primeCompl (f P) = N₂.localized₀ P.primeCompl (f P)) :
     N₁ = N₂ :=
-  le_antisymm (Submodule.le_of_localization_maximal Rₚ Mₚ f fun P _ => (h P).le)
-    (Submodule.le_of_localization_maximal Rₚ Mₚ f fun P _ => (h P).ge)
+  le_antisymm (Submodule.le_of_localization_maximal Mₚ f fun P _ ↦ (h P).le)
+    (Submodule.le_of_localization_maximal Mₚ f fun P _ ↦ (h P).ge)
 
 /-- A submodule is trivial if its localization at every maximal ideal is trivial. -/
-theorem Submodule.eq_bot_of_localization_maximal (N₁ : Submodule R M)
+theorem Submodule.eq_bot_of_localization₀_maximal (N : Submodule R M)
+    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized₀ P.primeCompl (f P) = ⊥) :
+    N = ⊥ :=
+  Submodule.eq_of_localization₀_maximal Mₚ f fun P hP ↦ by simpa using h P
+
+theorem Submodule.eq_top_of_localization₀_maximal (N : Submodule R M)
+    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized₀ P.primeCompl (f P) = ⊤) :
+    N = ⊤ :=
+  Submodule.eq_of_localization₀_maximal Mₚ f fun P hP ↦ by simpa using h P
+
+theorem Module.eq_of_localization_maximal (m m' : M)
+    (h : ∀ (P : Ideal R) [P.IsMaximal], f P m = f P m') :
+    m = m' := by
+  by_contra! ne
+  rw [← one_smul R m, ← one_smul R m'] at ne
+  have ⟨P, mP, le⟩ := (eqIdeal R m m').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
+  have ⟨s, hs⟩ := (IsLocalizedModule.eq_iff_exists P.primeCompl _).mp (h P)
+  exact s.2 (le hs)
+
+theorem Module.eq_zero_of_localization_maximal (m : M)
+    (h : ∀ (P : Ideal R) [P.IsMaximal], f P m = 0) :
+    m = 0 :=
+  eq_of_localization_maximal _ f _ _ fun P _ ↦ by rw [h, map_zero]
+
+theorem LinearMap.eq_of_localization_maximal (g g' : M →ₗ[R] M₁)
     (h : ∀ (P : Ideal R) [P.IsMaximal],
-      N₁.localized' (Rₚ P) P.primeCompl (f P) = ⊥) :
-    N₁ = ⊥ :=
-  Submodule.eq_of_localization_maximal Rₚ Mₚ f fun P hP => by simpa using h P
-
-theorem Submodule.mem_of_localization_maximal (r : M) (N₁ : Submodule R M)
-    (h : ∀ (P : Ideal R) [P.IsMaximal], f P r ∈ N₁.localized' (Rₚ P) P.primeCompl (f P)) :
-    r ∈ N₁ := by
-  rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Submodule.span_le]
-  apply Submodule.le_of_localization_maximal Rₚ Mₚ f
-  intro N₂ hJ
-  rw [Submodule.localized'_span, Submodule.span_le, Set.image_subset_iff, Set.singleton_subset_iff]
-  exact h N₂
-
-include Rₚ in
-theorem Module.eq_zero_of_localization_maximal (r : M)
-    (h : ∀ (P : Ideal R) [P.IsMaximal], f P r = 0) :
-    r = 0 := by
-  rw [← Submodule.mem_bot (R := R)]
-  apply Submodule.mem_of_localization_maximal Rₚ Mₚ f r ⊥ (by simpa using h)
-
-include Rₚ in
-theorem Module.eq_of_localization_maximal (r s : M)
-    (h : ∀ (P : Ideal R) [P.IsMaximal], f P r = f P s) :
-    r = s := by
-  rw [← sub_eq_zero]
-  simp_rw [← @sub_eq_zero _ _ (f _ _), ← map_sub] at h
-  exact Module.eq_zero_of_localization_maximal Rₚ Mₚ f _ h
-
-include Rₚ f in
+      IsLocalizedModule.map P.primeCompl (f P) (f₁ P) g =
+      IsLocalizedModule.map P.primeCompl (f P) (f₁ P) g') :
+    g = g' :=
+  ext fun x ↦ Module.eq_of_localization_maximal _ f₁ _ _ fun P _ ↦ by
+    simpa only [IsLocalizedModule.map_apply] using DFunLike.congr_fun (h P) (f P x)
+
+include f in
 theorem Module.subsingleton_of_localization_maximal
     (h : ∀ (P : Ideal R) [P.IsMaximal], Subsingleton (Mₚ P)) :
     Subsingleton M := by
   rw [subsingleton_iff_forall_eq 0]
   intro x
-  exact Module.eq_of_localization_maximal Rₚ Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _
+  exact Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _
+
+theorem Submodule.eq_of_localization_maximal {N₁ N₂ : Submodule R M}
+    (h : ∀ (P : Ideal R) [P.IsMaximal],
+      N₁.localized' (Rₚ P) P.primeCompl (f P) = N₂.localized' (Rₚ P) P.primeCompl (f P)) :
+    N₁ = N₂ :=
+  eq_of_localization₀_maximal Mₚ f fun P _ ↦ congr(restrictScalars _ $(h P))
+
+theorem Submodule.eq_bot_of_localization_maximal (N : Submodule R M)
+    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized' (Rₚ P) P.primeCompl (f P) = ⊥) :
+    N = ⊥ :=
+  Submodule.eq_of_localization_maximal Rₚ Mₚ f fun P hP ↦ by simpa using h P
+
+theorem Submodule.eq_top_of_localization_maximal (N : Submodule R M)
+    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized' (Rₚ P) P.primeCompl (f P) = ⊤) :
+    N = ⊤ :=
+  Submodule.eq_of_localization_maximal Rₚ Mₚ f fun P hP ↦ by simpa using h P
+
+end maximal