From f3b380e4f0c9bf09e911a91ba3acef89b0ed2393 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Thu, 23 Dec 2021 12:54:33 +0000 Subject: [PATCH] feat(algebraic_geometry): Prime spectrum is sober. (#10989) --- .../prime_spectrum/basic.lean | 64 +++++++++++++++++++ src/topology/sober.lean | 13 ++++ src/topology/subset_properties.lean | 5 ++ 3 files changed, 82 insertions(+) diff --git a/src/algebraic_geometry/prime_spectrum/basic.lean b/src/algebraic_geometry/prime_spectrum/basic.lean index 13949d5659f08..c238fc7276cf9 100644 --- a/src/algebraic_geometry/prime_spectrum/basic.lean +++ b/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'] diff --git a/src/topology/sober.lean b/src/topology/sober.lean index b3a5dd37bed61..e85dbbc3962c7 100644 --- a/src/topology/sober.lean +++ b/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 diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index 2a62ed32e88f9..6fc4cd8c0954e 100644 --- a/src/topology/subset_properties.lean +++ b/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