feat(RingTheory/Localization): add facts about localization at minima…

…l prime ideals (#11201)

Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent.

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -963,6 +963,22 @@ protected def pointsEquivIrreducibleCloseds :
   map_rel_iff' {p q} :=
     (RelIso.symm irreducibleSetEquivPoints).map_rel_iff.trans (le_iff_specializes p q).symm
 
+section LocalizationAtMinimal
+
+variable {I : Ideal R} [hI : I.IsPrime]
+
+/--
+Localizations at minimal primes have single-point prime spectra.
+-/
+def primeSpectrum_unique_of_localization_at_minimal (h : I ∈ minimalPrimes R) :
+    Unique (PrimeSpectrum (Localization.AtPrime I)) where
+  default :=
+    ⟨LocalRing.maximalIdeal (Localization I.primeCompl),
+    (LocalRing.maximalIdeal.isMaximal _).isPrime⟩
+  uniq x := PrimeSpectrum.ext _ _ (Localization.AtPrime.prime_unique_of_minimal h x.asIdeal)
+
+end LocalizationAtMinimal
+
 end CommSemiRing
 
 end PrimeSpectrum

Mathlib/RingTheory/Ideal/MinimalPrime.lean

@@ -25,7 +25,8 @@ We provide various results concerning the minimal primes above an ideal
   preimage of some minimal prime over `I`.
 - `Ideal.minimalPrimes_eq_comap`: The minimal primes over `I` are precisely the preimages of
   minimal primes of `R ⧸ I`.
-
+- `Localization.AtPrime.prime_unique_of_minimal`: When localizing at a minimal prime ideal `I`,
+  the resulting ring only has a single prime ideal.
 
 -/
 
@@ -221,3 +222,31 @@ theorem Ideal.minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes =
 #align ideal.minimal_primes_eq_subsingleton_self Ideal.minimalPrimes_eq_subsingleton_self
 
 end
+
+namespace Localization.AtPrime
+
+variable {R : Type*} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] (hMin : I ∈ minimalPrimes R)
+
+theorem _root_.IsLocalization.AtPrime.prime_unique_of_minimal {S} [CommSemiring S] [Algebra R S]
+    [IsLocalization.AtPrime S I] {J K : Ideal S} [J.IsPrime] [K.IsPrime] : J = K :=
+  haveI : Subsingleton {i : Ideal R // i.IsPrime ∧ i ≤ I} := ⟨fun i₁ i₂ ↦ Subtype.ext <| by
+    rw [minimalPrimes_eq_minimals] at hMin
+    rw [← eq_of_mem_minimals hMin i₁.2.1 i₁.2.2, ← eq_of_mem_minimals hMin i₂.2.1 i₂.2.2]⟩
+  Subtype.ext_iff.mp <| (IsLocalization.AtPrime.orderIsoOfPrime S I).injective
+    (a₁ := ⟨J, ‹_›⟩) (a₂ := ⟨K, ‹_›⟩) (Subsingleton.elim _ _)
+
+theorem prime_unique_of_minimal (J : Ideal (Localization I.primeCompl)) [J.IsPrime] :
+    J = LocalRing.maximalIdeal (Localization I.primeCompl) :=
+  IsLocalization.AtPrime.prime_unique_of_minimal hMin
+
+theorem nilpotent_iff_mem_maximal_of_minimal {x : _} :
+    IsNilpotent x ↔ x ∈ LocalRing.maximalIdeal (Localization I.primeCompl) := by
+  rw [nilpotent_iff_mem_prime]
+  exact ⟨(· (LocalRing.maximalIdeal _) (Ideal.IsMaximal.isPrime' _)), fun _ J _ =>
+    by simpa [prime_unique_of_minimal hMin J]⟩
+
+theorem nilpotent_iff_not_unit_of_minimal {x : Localization I.primeCompl} :
+    IsNilpotent x ↔ x ∈ nonunits _ := by
+  simpa only [← LocalRing.mem_maximalIdeal] using nilpotent_iff_mem_maximal_of_minimal hMin
+
+end Localization.AtPrime

Mathlib/RingTheory/Localization/AtPrime.lean

@@ -132,6 +132,12 @@ namespace AtPrime
 
 variable (I : Ideal R) [hI : I.IsPrime] [IsLocalization.AtPrime S I]
 
+/-- The prime ideals in the localization of a commutative ring at a prime ideal I are in
+order-preserving bijection with the prime ideals contained in I. -/
+def orderIsoOfPrime : { p : Ideal S // p.IsPrime } ≃o { p : Ideal R // p.IsPrime ∧ p ≤ I } :=
+  (IsLocalization.orderIsoOfPrime I.primeCompl S).trans <| .setCongr _ _ <| show setOf _ = setOf _
+    by ext; simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left]
+
 theorem isUnit_to_map_iff (x : R) : IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl :=
   ⟨fun h hx =>
     (isPrime_of_isPrime_disjoint I.primeCompl S I hI disjoint_compl_left).ne_top <|