feat: some golfing in AlgebraicGeometry.PrimeSpectrum.Basic (#7373)

Mathlib/AlgebraicGeometry/Limits.lean

@@ -85,7 +85,7 @@ instance : IsEmpty Scheme.empty.carrier :=
   show IsEmpty PEmpty by infer_instance
 
 instance spec_punit_isEmpty : IsEmpty (Scheme.Spec.obj (op <| CommRingCat.of PUnit)).carrier :=
-  ⟨PrimeSpectrum.punit⟩
+  inferInstanceAs <| IsEmpty (PrimeSpectrum PUnit)
 #align algebraic_geometry.Spec_punit_is_empty AlgebraicGeometry.spec_punit_isEmpty
 
 instance (priority := 100) isOpenImmersion_of_isEmpty {X Y : Scheme} (f : X ⟶ Y)

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -74,9 +74,9 @@ instance [Nontrivial R] : Nonempty <| PrimeSpectrum R :=
   ⟨⟨I, hI.isPrime⟩⟩
 
 /-- The prime spectrum of the zero ring is empty. -/
-theorem punit (x : PrimeSpectrum PUnit) : False :=
-  x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : PUnit)) x.1.zero_mem
-#align prime_spectrum.punit PrimeSpectrum.punit
+instance [Subsingleton R] : IsEmpty (PrimeSpectrum R) :=
+  ⟨fun x ↦ x.IsPrime.ne_top <| SetLike.ext' <| Subsingleton.eq_univ_of_nonempty x.asIdeal.nonempty⟩
+#noalign prime_spectrum.punit
 
 variable (R S)
 
@@ -248,12 +248,8 @@ theorem vanishingIdeal_anti_mono {s t : Set (PrimeSpectrum R)} (h : s ⊆ t) :
 #align prime_spectrum.vanishing_ideal_anti_mono PrimeSpectrum.vanishingIdeal_anti_mono
 
 theorem zeroLocus_subset_zeroLocus_iff (I J : Ideal R) :
-    zeroLocus (I : Set R) ⊆ zeroLocus (J : Set R) ↔ J ≤ I.radical :=
-  ⟨fun h =>
-    Ideal.radical_le_radical_iff.mp
-      (vanishingIdeal_zeroLocus_eq_radical I ▸
-        vanishingIdeal_zeroLocus_eq_radical J ▸ vanishingIdeal_anti_mono h),
-    fun h => zeroLocus_radical I ▸ zeroLocus_anti_mono_ideal h⟩
+    zeroLocus (I : Set R) ⊆ zeroLocus (J : Set R) ↔ J ≤ I.radical := by
+  rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]
 #align prime_spectrum.zero_locus_subset_zero_locus_iff PrimeSpectrum.zeroLocus_subset_zeroLocus_iff
 
 theorem zeroLocus_subset_zeroLocus_singleton_iff (f g : R) :
@@ -439,34 +435,13 @@ theorem isClosed_zeroLocus (s : Set R) : IsClosed (zeroLocus s) := by
   exact ⟨s, rfl⟩
 #align prime_spectrum.is_closed_zero_locus PrimeSpectrum.isClosed_zeroLocus
 
-theorem isClosed_singleton_iff_isMaximal (x : PrimeSpectrum R) :
-    IsClosed ({x} : Set (PrimeSpectrum R)) ↔ x.asIdeal.IsMaximal := by
-  refine' (isClosed_iff_zeroLocus _).trans ⟨fun h => _, fun h => _⟩
-  · obtain ⟨s, hs⟩ := h
-    rw [eq_comm, Set.eq_singleton_iff_unique_mem] at hs
-    refine'
-      ⟨⟨x.2.1, fun I hI =>
-          Classical.not_not.1
-            (mt (Ideal.exists_le_maximal I) <| not_exists.2 fun J => not_and.2 fun hJ hIJ => _)⟩⟩
-    exact
-      ne_of_lt (lt_of_lt_of_le hI hIJ)
-        (symm <|
-          congr_arg PrimeSpectrum.asIdeal
-            (hs.2 ⟨J, hJ.isPrime⟩ fun r hr => hIJ (le_of_lt hI <| hs.1 hr)))
-  · refine' ⟨x.asIdeal.1, _⟩
-    rw [eq_comm, Set.eq_singleton_iff_unique_mem]
-    refine' ⟨fun _ h => h, fun y hy => PrimeSpectrum.ext _ _ (h.eq_of_le y.2.ne_top hy).symm⟩
-#align prime_spectrum.is_closed_singleton_iff_is_maximal PrimeSpectrum.isClosed_singleton_iff_isMaximal
-
 theorem zeroLocus_vanishingIdeal_eq_closure (t : Set (PrimeSpectrum R)) :
     zeroLocus (vanishingIdeal t : Set R) = closure t := by
-  apply Set.Subset.antisymm
-  · rintro x hx t' ⟨ht', ht⟩
-    obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus s := by rwa [isClosed_iff_zeroLocus] at ht'
-    rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht
-    exact Set.Subset.trans ht hx
-  · rw [(isClosed_zeroLocus _).closure_subset_iff]
-    exact subset_zeroLocus_vanishingIdeal t
+  rcases isClosed_iff_zeroLocus (closure t) |>.mp isClosed_closure with ⟨I, hI⟩
+  rw [subset_antisymm_iff, (isClosed_zeroLocus _).closure_subset_iff, hI,
+      subset_zeroLocus_iff_subset_vanishingIdeal, (gc R).u_l_u_eq_u,
+      ← subset_zeroLocus_iff_subset_vanishingIdeal, ← hI]
+  exact ⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩
 #align prime_spectrum.zero_locus_vanishing_ideal_eq_closure PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
 
 theorem vanishingIdeal_closure (t : Set (PrimeSpectrum R)) :
@@ -478,6 +453,16 @@ theorem closure_singleton (x) : closure ({x} : Set (PrimeSpectrum R)) = zeroLocu
   rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]
 #align prime_spectrum.closure_singleton PrimeSpectrum.closure_singleton
 
+theorem isClosed_singleton_iff_isMaximal (x : PrimeSpectrum R) :
+    IsClosed ({x} : Set (PrimeSpectrum R)) ↔ x.asIdeal.IsMaximal := by
+  rw [← closure_subset_iff_isClosed, ← zeroLocus_vanishingIdeal_eq_closure,
+      vanishingIdeal_singleton]
+  constructor <;> intro H
+  · rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩
+    exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm
+  · exact fun p hp ↦ PrimeSpectrum.ext _ _ (H.eq_of_le p.2.1 hp).symm
+#align prime_spectrum.is_closed_singleton_iff_is_maximal PrimeSpectrum.isClosed_singleton_iff_isMaximal
+
 theorem isRadical_vanishingIdeal (s : Set (PrimeSpectrum R)) : (vanishingIdeal s).IsRadical := by
   rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure,
     vanishingIdeal_zeroLocus_eq_radical]
@@ -568,6 +553,13 @@ instance quasiSober : QuasiSober (PrimeSpectrum R) :=
     ⟨⟨_, isIrreducible_iff_vanishingIdeal_isPrime.1 h₁⟩, by
       rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]⟩⟩
 
+/-- The prime spectrum of a commutative ring is a compact topological space. -/
+instance compactSpace : CompactSpace (PrimeSpectrum R) := by
+  refine compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_
+  choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)
+  simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢
+  exact Ideal.isCompactElement_top.exists_finset_of_le_iSup _ _ S_empty
+
 section Comap
 
 variable {S' : Type*} [CommRing S']
@@ -834,33 +826,6 @@ theorem isBasis_basic_opens : TopologicalSpace.Opens.IsBasis (Set.range (@basicO
   rfl
 #align prime_spectrum.is_basis_basic_opens PrimeSpectrum.isBasis_basic_opens
 
-theorem isCompact_basicOpen (f : R) : IsCompact (basicOpen f : Set (PrimeSpectrum R)) :=
-  isCompact_of_finite_subfamily_closed fun {ι} Z hZc hZ => by
-    let I : ι → Ideal R := fun i => vanishingIdeal (Z i)
-    have hI : ∀ i, Z i = zeroLocus (I i) := fun i => by
-      simpa only [zeroLocus_vanishingIdeal_eq_closure] using (hZc i).closure_eq.symm
-    rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm, ← Set.diff_eq, Set.diff_eq_empty,
-      funext hI, ← zeroLocus_iSup] at hZ
-    obtain ⟨n, hn⟩ : f ∈ (⨆ i : ι, I i).radical := by
-      rw [← vanishingIdeal_zeroLocus_eq_radical]
-      apply vanishingIdeal_anti_mono hZ
-      exact subset_vanishingIdeal_zeroLocus {f} (Set.mem_singleton f)
-    rcases Submodule.exists_finset_of_mem_iSup I hn with ⟨s, hs⟩
-    use s
-    -- Using simp_rw here, because `hI` and `zeroLocus_iSup` need to be applied underneath binders
-    simp_rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm (zeroLocus {f})ᶜ, ← Set.diff_eq,
-      Set.diff_eq_empty]
-    rw [show (Set.iInter fun i => Set.iInter fun (_ : i ∈ s) => Z i) =
-      Set.iInter fun i => Set.iInter fun (_ : i ∈ s) => zeroLocus (I i) from congr_arg _
-        (funext fun i => congr_arg _ (funext fun _ => hI i))]
-    simp_rw [← zeroLocus_iSup]
-    rw [← zeroLocus_radical]
-    -- this one can't be in `simp_rw` because it would loop
-    apply zeroLocus_anti_mono
-    rw [Set.singleton_subset_iff]
-    exact ⟨n, hs⟩
-#align prime_spectrum.is_compact_basic_open PrimeSpectrum.isCompact_basicOpen
-
 @[simp]
 theorem basicOpen_eq_bot_iff (f : R) : basicOpen f = ⊥ ↔ IsNilpotent f := by
   rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]
@@ -890,13 +855,12 @@ theorem localization_away_openEmbedding (S : Type v) [CommRing S] [Algebra R S]
       exact isOpen_basicOpen }
 #align prime_spectrum.localization_away_open_embedding PrimeSpectrum.localization_away_openEmbedding
 
-end BasicOpen
+theorem isCompact_basicOpen (f : R) : IsCompact (basicOpen f : Set (PrimeSpectrum R)) := by
+  rw [← localization_away_comap_range (Localization (Submonoid.powers f))]
+  exact isCompact_range (map_continuous _)
+#align prime_spectrum.is_compact_basic_open PrimeSpectrum.isCompact_basicOpen
 
-/-- The prime spectrum of a commutative ring is a compact topological space. -/
-instance compactSpace : CompactSpace (PrimeSpectrum R) :=
-  { isCompact_univ := by
-      convert isCompact_basicOpen (1 : R)
-      rw [basicOpen_one, TopologicalSpace.Opens.coe_top] }
+end BasicOpen
 
 section Order
 

Mathlib/RingTheory/Ideal/Basic.lean

@@ -6,7 +6,6 @@ Authors: Kenny Lau, Chris Hughes, Mario Carneiro
 import Mathlib.Algebra.Associated
 import Mathlib.LinearAlgebra.Basic
 import Mathlib.Order.Atoms
-import Mathlib.Order.CompactlyGenerated
 import Mathlib.Tactic.Abel
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.LinearAlgebra.Finsupp
@@ -160,6 +159,9 @@ theorem span_singleton_one : span ({1} : Set α) = ⊤ :=
   (eq_top_iff_one _).2 <| subset_span <| mem_singleton _
 #align ideal.span_singleton_one Ideal.span_singleton_one
 
+theorem isCompactElement_top : CompleteLattice.IsCompactElement (⊤ : Ideal α) := by
+  simpa only [← span_singleton_one] using Submodule.singleton_span_isCompactElement 1
+
 theorem mem_span_insert {s : Set α} {x y} :
     x ∈ span (insert y s) ↔ ∃ a, ∃ z ∈ span s, x = a * y + z :=
   Submodule.mem_span_insert