feat(algebraic_geometry): Prime spectrum is sober. (#10989)

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -8,6 +8,7 @@ import ring_theory.ideal.prod
 import ring_theory.ideal.over
 import linear_algebra.finsupp
 import algebra.punit_instances
+import topology.sober
 
 /-!
 # Prime spectrum of a commutative ring
@@ -357,6 +358,17 @@ lemma is_closed_iff_zero_locus (Z : set (prime_spectrum R)) :
   is_closed Z ↔ ∃ s, Z = zero_locus s :=
 by rw [← is_open_compl_iff, is_open_iff, compl_compl]
 
+lemma is_closed_iff_zero_locus_ideal (Z : set (prime_spectrum R)) :
+  is_closed Z ↔ ∃ (s : ideal R), Z = zero_locus s :=
+(is_closed_iff_zero_locus _).trans
+  ⟨λ x, ⟨_, x.some_spec.trans (zero_locus_span _).symm⟩, λ x, ⟨_, x.some_spec⟩⟩
+
+lemma is_closed_iff_zero_locus_radical_ideal (Z : set (prime_spectrum R)) :
+  is_closed Z ↔ ∃ (s : ideal R), s.radical = s ∧ Z = zero_locus s :=
+(is_closed_iff_zero_locus_ideal _).trans
+  ⟨λ x, ⟨_, ideal.radical_idem _, x.some_spec.trans (zero_locus_radical _).symm⟩,
+    λ x, ⟨_, x.some_spec.2⟩⟩
+
 lemma is_closed_zero_locus (s : set R) :
   is_closed (zero_locus s) :=
 by { rw [is_closed_iff_zero_locus], exact ⟨s, rfl⟩ }
@@ -407,6 +419,58 @@ begin
     { exact absurd h (ring.not_is_field_iff_exists_prime.2 ⟨x.as_ideal, ⟨hx, x.2⟩⟩) } }
 end
 
+local notation `Z(` a `)` := zero_locus (a : set R)
+
+lemma is_irreducible_zero_locus_iff_of_radical (I : ideal R) (hI : I.radical = I) :
+  is_irreducible (zero_locus (I : set R)) ↔ I.is_prime :=
+begin
+  rw [ideal.is_prime_iff, is_irreducible],
+  apply and_congr,
+  { rw [← set.ne_empty_iff_nonempty, ne.def, zero_locus_empty_iff_eq_top] },
+  { transitivity ∀ (x y : ideal R), Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y),
+    { simp_rw [is_preirreducible_iff_closed_union_closed, is_closed_iff_zero_locus_ideal],
+      split,
+      { rintros h x y, exact h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩ },
+      { rintros h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩, exact h x y } },
+    { simp_rw [← zero_locus_inf, subset_zero_locus_iff_le_vanishing_ideal,
+        vanishing_ideal_zero_locus_eq_radical, hI],
+      split,
+      { intros h x y h',
+        simp_rw [← set_like.mem_coe, ← set.singleton_subset_iff, ← ideal.span_le],
+        apply h,
+        rw [← hI, ← ideal.radical_le_radical_iff, ideal.radical_inf, ← ideal.radical_mul,
+          ideal.radical_le_radical_iff, hI, ideal.span_mul_span],
+        simpa [ideal.span_le] 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_idem
+
+instance [is_domain R] : irreducible_space (prime_spectrum R) :=
+begin
+  rw [irreducible_space_def, set.top_eq_univ, ← zero_locus_bot, is_irreducible_zero_locus_iff],
+  simpa using ideal.bot_prime
+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 ⟨s, hs, 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 [hs] using hxZ),
+  simp [hs]
+end
+
 section comap
 variables {S : Type v} [comm_ring S] {S' : Type*} [comm_ring S']
 

src/topology/sober.lean

@@ -167,6 +167,19 @@ begin
     rw set.image_singleton }
 end
 
+omit h
+
+lemma is_generic_point_iff_forall_closed {x : α} {S : set α} (hS : is_closed S) (hxS : x ∈ S) :
+  is_generic_point x S ↔ ∀ (Z : set α) (hZ : is_closed Z) (hxZ : x ∈ Z), S ⊆ Z :=
+begin
+  split,
+  { intros h Z hZ hxZ, exact (h.mem_closed_set_iff hZ).mp hxZ },
+  { intro h,
+    apply le_antisymm,
+    { rwa [set.le_eq_subset, hS.closure_subset_iff, set.singleton_subset_iff] },
+    { exact h _ is_closed_closure (subset_closure $ set.mem_singleton x) } }
+end
+
 end generic_point
 
 section sober

src/topology/subset_properties.lean

@@ -1401,6 +1401,11 @@ lemma irreducible_space.is_irreducible_univ (α : Type u) [topological_space α]
   [irreducible_space α] : is_irreducible (⊤ : set α) :=
 ⟨by simp, preirreducible_space.is_preirreducible_univ α⟩
 
+lemma irreducible_space_def (α : Type u) [topological_space α] :
+  irreducible_space α ↔ is_irreducible (⊤ : set α) :=
+⟨@@irreducible_space.is_irreducible_univ α _,
+  λ h, by { haveI : preirreducible_space α := ⟨h.2⟩, exact ⟨⟨h.1.some⟩⟩ }⟩
+
 theorem nonempty_preirreducible_inter [preirreducible_space α] {s t : set α} :
   is_open s → is_open t → s.nonempty → t.nonempty → (s ∩ t).nonempty :=
 by simpa only [univ_inter, univ_subset_iff] using