feat(algebraic_geometry/prime_spectrum/basic): new lemmas + golf (#17289

)

Extract lemmas `closure_singleton`, `is_radical_vanishing_ideal`, and `is_irreducible_iff_vanishing_ideal_is_prime` to golf `prime_spectrum.quasi_sober`; also add a convenient but unused lemma `vanishing_ideal_eq_top_iff`.

- [x] depends on: #17254



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

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -268,6 +268,10 @@ end
   zero_locus (set.univ : set R) = ∅ :=
 zero_locus_empty_of_one_mem (set.mem_univ 1)
 
+lemma vanishing_ideal_eq_top_iff {s : set (prime_spectrum R)} : vanishing_ideal s = ⊤ ↔ s = ∅ :=
+by rw [← top_le_iff, ← subset_zero_locus_iff_le_vanishing_ideal,
+       submodule.top_coe, zero_locus_univ, set.subset_empty_iff]
+
 lemma zero_locus_sup (I J : ideal R) :
   zero_locus ((I ⊔ J : ideal R) : set R) = zero_locus I ∩ zero_locus J :=
 (gc R).l_sup
@@ -343,9 +347,8 @@ topological_space.of_closed (set.range prime_spectrum.zero_locus)
   begin
     intros Zs h,
     rw set.sInter_eq_Inter,
-    let f : Zs → set R := λ i, classical.some (h i.2),
-    have hf : ∀ i : Zs, ↑i = zero_locus (f i) := λ i, (classical.some_spec (h i.2)).symm,
-    simp only [hf],
+    choose f hf using λ i : Zs, h i.prop,
+    simp only [← hf],
     exact ⟨_, zero_locus_Union _⟩
   end
   (by { rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩, exact ⟨_, (union_zero_locus s t).symm⟩ })
@@ -404,6 +407,14 @@ lemma vanishing_ideal_closure (t : set (prime_spectrum R)) :
   vanishing_ideal (closure t) = vanishing_ideal t :=
 zero_locus_vanishing_ideal_eq_closure t ▸ (gc R).u_l_u_eq_u t
 
+lemma closure_singleton (x) : closure ({x} : set (prime_spectrum R)) = zero_locus x.as_ideal :=
+by rw [← zero_locus_vanishing_ideal_eq_closure, vanishing_ideal_singleton]
+
+lemma is_radical_vanishing_ideal (s : set (prime_spectrum R)) :
+  (vanishing_ideal s).is_radical :=
+by { rw [← vanishing_ideal_closure, ← zero_locus_vanishing_ideal_eq_closure,
+  vanishing_ideal_zero_locus_eq_radical], apply ideal.radical_is_radical }
+
 lemma vanishing_ideal_anti_mono_iff {s t : set (prime_spectrum R)}
   (ht : is_closed t) : s ⊆ t ↔ vanishing_ideal t ≤ vanishing_ideal s :=
 ⟨vanishing_ideal_anti_mono, λ h,
@@ -455,19 +466,24 @@ begin
     { simp_rw [← zero_locus_inf, subset_zero_locus_iff_le_vanishing_ideal,
         vanishing_ideal_zero_locus_eq_radical, hI.radical],
       split,
-      { intros h x y h',
-        simp_rw [← set_like.mem_coe, ← set.singleton_subset_iff, ← ideal.span_le],
-        apply h,
-        simpa [← hI.radical_le_iff, ideal.radical_inf, ← ideal.radical_mul,
-          hI.radical_le_iff, ideal.span_mul_span, ideal.span_le] using h' },
+      { simp_rw [← set_like.mem_coe, ← set.singleton_subset_iff,
+          ← ideal.span_le, ← ideal.span_singleton_mul_span_singleton],
+        refine λ h x y h', h _ _ _,
+        rw [← hI.radical_le_iff] at h' ⊢,
+        simpa only [ideal.radical_inf, ideal.radical_mul] using h' },
       { simp_rw [or_iff_not_imp_left, set_like.not_le_iff_exists],
         rintros h s t h' ⟨x, hx, hx'⟩ y hy,
         exact h (h' ⟨ideal.mul_mem_right _ _ hx, ideal.mul_mem_left _ _ hy⟩) hx' } } }
 end
 
 lemma is_irreducible_zero_locus_iff (I : ideal R) :
   is_irreducible (zero_locus (I : set R)) ↔ I.radical.is_prime :=
-(zero_locus_radical I) ▸ is_irreducible_zero_locus_iff_of_radical _ I.radical_is_radical
+zero_locus_radical I ▸ is_irreducible_zero_locus_iff_of_radical _ I.radical_is_radical
+
+lemma is_irreducible_iff_vanishing_ideal_is_prime {s : set (prime_spectrum R)} :
+  is_irreducible s ↔ (vanishing_ideal s).is_prime :=
+by rw [← is_irreducible_iff_closure, ← zero_locus_vanishing_ideal_eq_closure,
+  is_irreducible_zero_locus_iff_of_radical _ (is_radical_vanishing_ideal s)]
 
 instance [is_domain R] : irreducible_space (prime_spectrum R) :=
 begin
@@ -476,24 +492,12 @@ begin
 end
 
 instance : quasi_sober (prime_spectrum R) :=
-begin
-  constructor,
-  intros S h₁ h₂,
-  rw [← h₂.closure_eq, ← zero_locus_vanishing_ideal_eq_closure,
-    is_irreducible_zero_locus_iff] at h₁,
-  use ⟨_, h₁⟩,
-  obtain ⟨I, hI, rfl⟩ := (is_closed_iff_zero_locus_radical_ideal _).mp h₂,
-  rw is_generic_point_iff_forall_closed h₂,
-  intros Z hZ hxZ,
-  obtain ⟨t, rfl⟩ := (is_closed_iff_zero_locus_ideal _).mp hZ,
-  exact zero_locus_anti_mono (by simpa [hI.radical] using hxZ),
-  simp [hI.radical]
-end
+⟨λ S h₁ h₂, ⟨⟨_, is_irreducible_iff_vanishing_ideal_is_prime.1 h₁⟩,
+ by rw [is_generic_point, closure_singleton, zero_locus_vanishing_ideal_eq_closure, h₂.closure_eq]⟩⟩
 
 section comap
 variables {S : Type v} [comm_ring S] {S' : Type*} [comm_ring S']
 
-
 lemma preimage_comap_zero_locus_aux (f : R →+* S) (s : set R) :
   (λ y, ⟨ideal.comap f y.as_ideal, infer_instance⟩ :
     prime_spectrum S → prime_spectrum R) ⁻¹' (zero_locus s) = zero_locus (f '' s) :=