feat(RingTheory): support of quotient module

Mathlib/Algebra/Module/LocalizedModule/Submodule.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.Algebra.Module.Submodule.Pointwise
+import Mathlib.Algebra.Algebra.Operations
 import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.Localization.Module
 
@@ -109,6 +110,19 @@ lemma localized'_span (s : Set M) : (span R s).localized' S p f = span S (f '' s
     intro x hx
     exact ⟨x, subset_span hx, 1, IsLocalizedModule.mk'_one _ _ _⟩
 
+lemma localized₀_smul (I : Submodule R R) : (I • M').localized₀ p f = I • M'.localized₀ p f := by
+  apply le_antisymm
+  · rintro _ ⟨a, ha, s, rfl⟩
+    refine Submodule.smul_induction_on ha ?_ ?_
+    · intro r hr n hn
+      rw [IsLocalizedModule.mk'_smul]
+      exact Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩
+    · simp +contextual only [IsLocalizedModule.mk'_add, add_mem, implies_true]
+  · refine Submodule.smul_le.mpr ?_
+    rintro r hr _ ⟨a, ha, s, rfl⟩
+    rw [← IsLocalizedModule.mk'_smul]
+    exact ⟨_, Submodule.smul_mem_smul hr ha, s, rfl⟩
+
 /-- The localization map of a submodule. -/
 @[simps!]
 def toLocalized₀ : M' →ₗ[R] M'.localized₀ p f := f.restrict fun x hx ↦ ⟨x, hx, 1, by simp⟩

Mathlib/RingTheory/Support.lean

@@ -5,8 +5,13 @@ Authors: Andrew Yang
 -/
 import Mathlib.RingTheory.PrimeSpectrum
 import Mathlib.RingTheory.Localization.AtPrime
+import Mathlib.RingTheory.Ideal.Colon
 import Mathlib.Algebra.Exact
 import Mathlib.Algebra.Module.LocalizedModule.Basic
+import Mathlib.Algebra.Module.LocalizedModule.Submodule
+import Mathlib.RingTheory.Localization.Module
+import Mathlib.RingTheory.Localization.Finiteness
+import Mathlib.RingTheory.Nakayama
 
 /-!
 
@@ -38,6 +43,7 @@ variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpec
 
 variable (R M) in
 /-- The support of a module, defined as the set of primes `p` such that `Mₚ ≠ 0`. -/
+@[stacks 00L1]
 def Module.support : Set (PrimeSpectrum R) :=
   { p | Nontrivial (LocalizedModule p.asIdeal.primeCompl M) }
 
@@ -128,30 +134,17 @@ lemma Module.support_of_noZeroSMulDivisors [NoZeroSMulDivisors R M] [Nontrivial
   obtain ⟨x, hx⟩ := exists_ne (0 : M)
   exact fun p ↦ ⟨x, fun r hr ↦ ⟨fun e ↦ hr (e ▸ p.asIdeal.zero_mem), hx⟩⟩
 
-lemma Module.mem_support_iff_of_finite [Module.Finite R M] :
-    p ∈ Module.support R M ↔ Module.annihilator R M ≤ p.asIdeal := by
-  classical
-  obtain ⟨s, hs⟩ := ‹Module.Finite R M›
-  refine ⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩
-  simp only [SetLike.le_def, Submodule.mem_annihilator_span_singleton] at H ⊢
-  contrapose! H
-  choose x hx hx' using Subtype.forall'.mp H
-  refine ⟨s.attach.prod x, ?_, ?_⟩
-  · rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]
-    intro m
-    obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)
-    rw [hk, mul_comm, mul_smul, hx, smul_zero]
-  · exact p.asIdeal.primeCompl.prod_mem (fun x _ ↦ hx' x)
-
 variable {N P : Type*} [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P]
 variable (f : M →ₗ[R] N) (g : N →ₗ[R] P)
 
+@[stacks 00L3 "(2)"]
 lemma Module.support_subset_of_injective (hf : Function.Injective f) :
     Module.support R M ⊆ Module.support R N := by
   simp_rw [Set.subset_def, mem_support_iff']
   rintro x ⟨m, hm⟩
   exact ⟨f m, fun r hr ↦ by simpa using hf.ne (hm r hr)⟩
 
+@[stacks 00L3 "(3)"]
 lemma Module.support_subset_of_surjective (hf : Function.Surjective f) :
     Module.support R N ⊆ Module.support R M := by
   simp_rw [Set.subset_def, mem_support_iff']
@@ -161,6 +154,7 @@ lemma Module.support_subset_of_surjective (hf : Function.Surjective f) :
 
 variable {f g} in
 /-- Given an exact sequence `0 → M → N → P → 0` of `R`-modules, `Supp N = Supp M ∪ Supp P`. -/
+@[stacks 00L3 "(4)"]
 lemma Module.support_of_exact (h : Function.Exact f g)
     (hf : Function.Injective f) (hg : Function.Surjective g) :
     Module.support R N = Module.support R M ∪ Module.support R P := by
@@ -183,14 +177,34 @@ lemma LinearEquiv.support_eq (e : M ≃ₗ[R] N) :
 
 section Finite
 
+variable [Module.Finite R M]
+
+open PrimeSpectrum
+
+lemma Module.mem_support_iff_of_finite :
+    p ∈ Module.support R M ↔ Module.annihilator R M ≤ p.asIdeal := by
+  classical
+  obtain ⟨s, hs⟩ := ‹Module.Finite R M›
+  refine ⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩
+  simp only [SetLike.le_def, Submodule.mem_annihilator_span_singleton] at H ⊢
+  contrapose! H
+  choose x hx hx' using Subtype.forall'.mp H
+  refine ⟨s.attach.prod x, ?_, ?_⟩
+  · rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]
+    intro m
+    obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)
+    rw [hk, mul_comm, mul_smul, hx, smul_zero]
+  · exact p.asIdeal.primeCompl.prod_mem (fun x _ ↦ hx' x)
+
 /-- If `M` is `R`-finite, then `Supp M = Z(Ann(M))`. -/
-lemma Module.support_eq_zeroLocus [Module.Finite R M] :
-    Module.support R M = PrimeSpectrum.zeroLocus (Module.annihilator R M) :=
+@[stacks 00L2]
+lemma Module.support_eq_zeroLocus :
+    Module.support R M = zeroLocus (Module.annihilator R M) :=
   Set.ext fun _ ↦ mem_support_iff_of_finite
 
 /-- If `M` is a finite module such that `Mₚ = 0` for some `p`,
 then `M[1/f] = 0` for some `p ∈ D(f)`. -/
-lemma LocalizedModule.exists_subsingleton_away [Module.Finite R M] (p : Ideal R) [p.IsPrime]
+lemma LocalizedModule.exists_subsingleton_away (p : Ideal R) [p.IsPrime]
     [Subsingleton (LocalizedModule p.primeCompl M)] :
     ∃ f ∉ p, Subsingleton (LocalizedModule (.powers f) M) := by
   have : ⟨p, inferInstance⟩ ∈ (Module.support R M)ᶜ := by
@@ -201,4 +215,53 @@ lemma LocalizedModule.exists_subsingleton_away [Module.Finite R M] (p : Ideal R)
   exact ⟨f, by simpa using hf', subsingleton_iff.mpr
     fun m ↦ ⟨f, Submonoid.mem_powers f, Module.mem_annihilator.mp hf _⟩⟩
 
+/-- `Supp(M/IM) = Supp(M) ∩ Z(I)`. -/
+@[stacks 00L3 "(1)"]
+theorem Module.support_quotient (I : Ideal R) :
+    support R (M ⧸ (I • ⊤ : Submodule R M)) = support R M ∩ zeroLocus I := by
+  apply subset_antisymm
+  · refine Set.subset_inter ?_ ?_
+    · exact Module.support_subset_of_surjective _ (Submodule.mkQ_surjective _)
+    · rw [support_eq_zeroLocus]
+      apply PrimeSpectrum.zeroLocus_anti_mono_ideal
+      rw [Submodule.annihilator_quotient]
+      exact fun x hx ↦ Submodule.mem_colon.mpr fun p ↦ Submodule.smul_mem_smul hx
+  · rintro p ⟨hp₁, hp₂⟩
+    rw [Module.mem_support_iff] at hp₁ ⊢
+    let Rₚ := Localization.AtPrime p.asIdeal
+    let Mₚ := LocalizedModule p.asIdeal.primeCompl M
+    let Mₚ' := LocalizedModule p.asIdeal.primeCompl (M ⧸ (I • ⊤ : Submodule R M))
+    let f : Mₚ →ₗ[R] Mₚ' := (LocalizedModule.map _ (Submodule.mkQ _)).restrictScalars R
+    have hf : LinearMap.ker f = I • ⊤ := by
+      refine (LinearMap.ker_localizedMap_eq_localized'_ker Rₚ ..).trans ?_
+      show Submodule.localized₀ _ _ _ = _
+      simp only [Submodule.ker_mkQ, Submodule.localized₀_smul, Submodule.localized₀_top]
+    let f' : (Mₚ ⧸ (I • ⊤ : Submodule R Mₚ)) ≃ₗ[R] Mₚ' :=
+      LinearEquiv.ofBijective (Submodule.liftQ _ f hf.ge) <| by
+        constructor
+        · rw [← LinearMap.ker_eq_bot, Submodule.ker_liftQ, hf,
+            ← le_bot_iff, Submodule.map_le_iff_le_comap, Submodule.comap_bot, Submodule.ker_mkQ]
+        · rw [← LinearMap.range_eq_top, Submodule.range_liftQ, LinearMap.range_eq_top]
+          exact (LocalizedModule.map_surjective _ _ (Submodule.mkQ_surjective _))
+    have : Module.Finite Rₚ Mₚ :=
+      Module.Finite.of_isLocalizedModule p.asIdeal.primeCompl
+        (LocalizedModule.mkLinearMap _ _)
+    have : Nontrivial (Mₚ ⧸ (I • ⊤ : Submodule R Mₚ)) := by
+      apply Submodule.Quotient.nontrivial_of_lt_top
+      rw [lt_top_iff_ne_top]
+      intro H
+      have : I.map (algebraMap R Rₚ) • (⊤ : Submodule Rₚ Mₚ) = ⊤ := by
+        rw [← top_le_iff]
+        show ⊤ ≤ (I.map (algebraMap R Rₚ) • (⊤ : Submodule Rₚ Mₚ)).restrictScalars R
+        rw [← H, Submodule.smul_le]
+        intro r hr n hn
+        rw [← algebraMap_smul Rₚ, Submodule.restrictScalars_mem]
+        exact Submodule.smul_mem_smul (Ideal.mem_map_of_mem _ hr) hn
+      have := Submodule.eq_bot_of_le_smul_of_le_jacobson_bot _ ⊤ Module.Finite.out this.ge
+        ((Ideal.map_mono hp₂).trans (by
+          rw [Localization.AtPrime.map_eq_maximalIdeal]
+          exact IsLocalRing.maximalIdeal_le_jacobson _))
+      exact top_ne_bot this
+    exact f'.symm.nontrivial
+
 end Finite