From a5d04c838085d6c3554d59278c04126b62314757 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 20 Nov 2024 17:19:12 +0000 Subject: [PATCH] chore(RingTheory): improve and generalize submodule localization API (#19118) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .../Module/LocalizedModule/Submodule.lean | 94 ++++++++---- Mathlib/RingTheory/Ideal/Defs.lean | 9 ++ .../LocalProperties/Projective.lean | 18 +-- .../RingTheory/LocalProperties/Submodule.lean | 139 +++++++++++------- 4 files changed, 163 insertions(+), 97 deletions(-) diff --git a/Mathlib/Algebra/Module/LocalizedModule/Submodule.lean b/Mathlib/Algebra/Module/LocalizedModule/Submodule.lean index 786335636ddb0..650844736f7ca 100644 --- a/Mathlib/Algebra/Module/LocalizedModule/Submodule.lean +++ b/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) : diff --git a/Mathlib/RingTheory/Ideal/Defs.lean b/Mathlib/RingTheory/Ideal/Defs.lean index d2eb82b15fdd4..ba78f8a4b205b 100644 --- a/Mathlib/RingTheory/Ideal/Defs.lean +++ b/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 diff --git a/Mathlib/RingTheory/LocalProperties/Projective.lean b/Mathlib/RingTheory/LocalProperties/Projective.lean index d6a190e4ac15f..a2c4615a7942e 100644 --- a/Mathlib/RingTheory/LocalProperties/Projective.lean +++ b/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 diff --git a/Mathlib/RingTheory/LocalProperties/Submodule.lean b/Mathlib/RingTheory/LocalProperties/Submodule.lean index f4e9274c697bd..2ecaa20be887a 100644 --- a/Mathlib/RingTheory/LocalProperties/Submodule.lean +++ b/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