feat(AlgebraicGeometry): prime spectrum of jacobson rings are jacobson spaces (#18353)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean

@@ -5,6 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian
 import Mathlib.RingTheory.Jacobson
+import Mathlib.Topology.JacobsonSpace
 
 /-!
 # The prime spectrum of a jacobson ring
@@ -22,11 +23,11 @@ import Mathlib.RingTheory.Jacobson
 
 open Ideal
 
-variable {R : Type*} [CommRing R] [IsJacobsonRing R]
+variable {R : Type*} [CommRing R]
 
 namespace PrimeSpectrum
 
-lemma exists_isClosed_singleton_of_isJacobsonRing
+lemma exists_isClosed_singleton_of_isJacobsonRing [IsJacobsonRing R]
     (s : (Set (PrimeSpectrum R))) (hs : IsOpen s) (hs' : s.Nonempty) :
     ∃ x ∈ s, IsClosed {x} := by
   simp_rw [isClosed_singleton_iff_isMaximal]
@@ -41,6 +42,30 @@ lemma exists_isClosed_singleton_of_isJacobsonRing
   rintro x ⟨-, hx⟩
   exact sInf_le ⟨this ⟨x, hx.isPrime⟩ hx, hx⟩
 
+instance [IsJacobsonRing R] : JacobsonSpace (PrimeSpectrum R) := by
+  rw [jacobsonSpace_iff_locallyClosed]
+  rintro S hS ⟨U, Z, hU, hZ, rfl⟩
+  simp only [← isClosed_compl_iff, isClosed_iff_zeroLocus_ideal, @compl_eq_comm _ U] at hU hZ
+  obtain ⟨⟨I, rfl⟩, ⟨J, rfl⟩⟩ := And.intro hU hZ
+  simp only [Set.nonempty_iff_ne_empty, ne_eq, Set.inter_assoc,
+    ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset,
+    zeroLocus_subset_zeroLocus_iff, Ideal.radical_eq_jacobson, Ideal.jacobson, le_sInf_iff] at hS ⊢
+  contrapose! hS
+  rintro x ⟨hJx, hx⟩
+  exact @hS ⟨x, hx.isPrime⟩ ⟨hJx, (isClosed_singleton_iff_isMaximal _).mpr hx⟩
+
+lemma isJacobsonRing_iff_jacobsonSpace :
+    IsJacobsonRing R ↔ JacobsonSpace (PrimeSpectrum R) := by
+  refine ⟨fun _ ↦ inferInstance, fun H ↦ ⟨fun I hI ↦ le_antisymm ?_ Ideal.le_jacobson⟩⟩
+  rw [← I.isRadical_jacobson.radical]
+  conv_rhs => rw [← hI.radical]
+  simp_rw [← vanishingIdeal_zeroLocus_eq_radical]
+  apply vanishingIdeal_anti_mono
+  rw [← H.1 (isClosed_zeroLocus I), (isClosed_zeroLocus _).closure_subset_iff]
+  rintro x ⟨hx : I ≤ x.asIdeal, hx'⟩
+  show jacobson I ≤ x.asIdeal
+  exact sInf_le ⟨hx, (isClosed_singleton_iff_isMaximal _).mp hx'⟩
+
 /--
 If `R` is both noetherian and jacobson, then the following are equivalent for `x : Spec R`:
 1. `{x}` is open (i.e. `x` is an isolated point)
@@ -49,7 +74,7 @@ If `R` is both noetherian and jacobson, then the following are equivalent for `x
   (i.e. `x` is both a minimal prime and a maximal ideal)
 -/
 lemma isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing
-    [IsNoetherianRing R] (x : PrimeSpectrum R) :
+    [IsNoetherianRing R] [IsJacobsonRing R] (x : PrimeSpectrum R) :
     List.TFAE [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}] := by
   tfae_have 1 → 2
   | h => by

Mathlib/RingTheory/Jacobson.lean

@@ -6,6 +6,7 @@ Authors: Devon Tuma
 import Mathlib.RingTheory.Localization.Away.Basic
 import Mathlib.RingTheory.Ideal.Over
 import Mathlib.RingTheory.JacobsonIdeal
+import Mathlib.RingTheory.Artinian
 
 /-!
 # Jacobson Rings
@@ -91,11 +92,9 @@ theorem Ideal.radical_eq_jacobson [H : IsJacobsonRing R] (I : Ideal R) : I.radic
   le_antisymm (le_sInf fun _J ⟨hJ, hJ_max⟩ => (IsPrime.radical_le_iff hJ_max.isPrime).mpr hJ)
     (H.out (radical_isRadical I) ▸ jacobson_mono le_radical)
 
-/-- Fields have only two ideals, and the condition holds for both of them. -/
-instance (priority := 100) isJacobsonRing_field {K : Type*} [Field K] : IsJacobsonRing K :=
-  ⟨fun I _ => Or.recOn (eq_bot_or_top I)
-    (fun h => le_antisymm (sInf_le ⟨le_rfl, h.symm ▸ bot_isMaximal⟩) (h.symm ▸ bot_le)) fun h =>
-      by rw [h, jacobson_eq_top_iff]⟩
+instance (priority := 100) [IsArtinianRing R] : IsJacobsonRing R :=
+  isJacobsonRing_iff_prime_eq.mpr fun P _ ↦
+    jacobson_eq_self_of_isMaximal (H := IsArtinianRing.isMaximal_of_isPrime P)
 
 theorem isJacobsonRing_of_surjective [H : IsJacobsonRing R] :
     (∃ f : R →+* S, Function.Surjective ↑f) → IsJacobsonRing S := by

Mathlib/RingTheory/JacobsonIdeal.lean

@@ -275,6 +275,9 @@ theorem radical_le_jacobson : radical I ≤ jacobson I :=
 theorem isRadical_of_eq_jacobson (h : jacobson I = I) : I.IsRadical :=
   radical_le_jacobson.trans h.le
 
+lemma isRadical_jacobson (I : Ideal R) : I.jacobson.IsRadical :=
+  isRadical_of_eq_jacobson jacobson_idem
+
 theorem isUnit_of_sub_one_mem_jacobson_bot (r : R) (h : r - 1 ∈ jacobson (⊥ : Ideal R)) :
     IsUnit r := by
   cases' exists_mul_sub_mem_of_sub_one_mem_jacobson r h with s hs

Mathlib/Topology/JacobsonSpace.lean

@@ -49,7 +49,7 @@ lemma IsClosedEmbedding.preimage_closedPoints (hf : IsClosedEmbedding f) :
   ext x
   simp [mem_closedPoints_iff, ← Set.image_singleton, hf.closed_iff_image_closed]
 
-lemma closedPoints_eq_univ [T2Space X] :
+lemma closedPoints_eq_univ [T1Space X] :
     closedPoints X = Set.univ :=
   Set.eq_univ_iff_forall.mpr fun _ ↦ isClosed_singleton
 
@@ -144,7 +144,7 @@ lemma JacobsonSpace.discreteTopology [JacobsonSpace X]
 instance (priority := 100) [Finite X] [JacobsonSpace X] : DiscreteTopology X :=
   JacobsonSpace.discreteTopology (Set.toFinite _)
 
-instance (priority := 100) [T2Space X] : JacobsonSpace X :=
+instance (priority := 100) [T1Space X] : JacobsonSpace X :=
   ⟨by simp [closedPoints_eq_univ, closure_eq_iff_isClosed]⟩
 
 open TopologicalSpace in