From d7c689d247f6623595709af7d4e542e719aeebd7 Mon Sep 17 00:00:00 2001
From: Devon Tuma <tumax040@umn.edu>
Date: Wed, 27 Oct 2021 15:13:49 +0000
Subject: [PATCH] feat(algebraic_geometry/prime_spectrum): Closed points in
 prime spectrum (#9861)

This PR adds lemmas about the correspondence between closed points in `prime_spectrum R` and maximal ideals of `R`.

In order to import and talk about integral maps I had to move some lemmas from `noetherian.lean` to `prime_spectrum.lean` to prevent cyclic import dependencies.
---
 .../basic.lean}                               | 49 ++++++++++
 .../{ => prime_spectrum}/is_open_comap_C.lean |  2 +-
 .../prime_spectrum/noetherian.lean            | 93 +++++++++++++++++++
 src/algebraic_geometry/structure_sheaf.lean   |  2 +-
 src/ring_theory/dedekind_domain.lean          |  3 +-
 src/ring_theory/noetherian.lean               | 87 +----------------
 src/ring_theory/nullstellensatz.lean          |  2 +-
 7 files changed, 148 insertions(+), 90 deletions(-)
 rename src/algebraic_geometry/{prime_spectrum.lean => prime_spectrum/basic.lean} (88%)
 rename src/algebraic_geometry/{ => prime_spectrum}/is_open_comap_C.lean (98%)
 create mode 100644 src/algebraic_geometry/prime_spectrum/noetherian.lean

diff --git a/src/algebraic_geometry/prime_spectrum.lean b/src/algebraic_geometry/prime_spectrum/basic.lean
similarity index 88%
rename from src/algebraic_geometry/prime_spectrum.lean
rename to src/algebraic_geometry/prime_spectrum/basic.lean
index 859b28c709ea5..e586a206431f1 100644
--- a/src/algebraic_geometry/prime_spectrum.lean
+++ b/src/algebraic_geometry/prime_spectrum/basic.lean
@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 import topology.opens
 import ring_theory.ideal.prod
+import ring_theory.ideal.over
 import linear_algebra.finsupp
 import algebra.punit_instances
 
@@ -360,6 +361,21 @@ lemma is_closed_zero_locus (s : set R) :
   is_closed (zero_locus s) :=
 by { rw [is_closed_iff_zero_locus], exact ⟨s, rfl⟩ }
 
+lemma is_closed_singleton_iff_is_maximal (x : prime_spectrum R) :
+  is_closed ({x} : set (prime_spectrum R)) ↔ x.as_ideal.is_maximal :=
+begin
+  refine (is_closed_iff_zero_locus _).trans ⟨λ h, _, λ h, _⟩,
+  { obtain ⟨s, hs⟩ := h,
+    rw [eq_comm, set.eq_singleton_iff_unique_mem] at hs,
+    refine ⟨⟨x.2.1, λ I hI, not_not.1 (mt (ideal.exists_le_maximal I) $
+      not_exists.2 (λ J, not_and.2 $ λ hJ hIJ,_))⟩⟩,
+    exact ne_of_lt (lt_of_lt_of_le hI hIJ) (symm $ congr_arg prime_spectrum.as_ideal
+      (hs.2 ⟨J, hJ.is_prime⟩ (λ r hr, hIJ (le_of_lt hI $ hs.1 hr)))) },
+  { refine ⟨x.as_ideal.1, _⟩,
+    rw [eq_comm, set.eq_singleton_iff_unique_mem],
+    refine ⟨λ _ h, h, λ y hy, prime_spectrum.ext.2 (h.eq_of_le y.2.ne_top hy).symm⟩ }
+end
+
 lemma zero_locus_vanishing_ideal_eq_closure (t : set (prime_spectrum R)) :
   zero_locus (vanishing_ideal t : set R) = closure t :=
 begin
@@ -377,6 +393,20 @@ 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 t1_space_iff_is_field [is_domain R] :
+  t1_space (prime_spectrum R) ↔ is_field R :=
+begin
+  refine ⟨_, λ h, _⟩,
+  { introI h,
+    have hbot : ideal.is_prime (⊥ : ideal R) := ideal.bot_prime,
+    exact not_not.1 (mt (ring.ne_bot_of_is_maximal_of_not_is_field $
+      (is_closed_singleton_iff_is_maximal _).1 (t1_space.t1 ⟨⊥, hbot⟩)) (not_not.2 rfl)) },
+  { refine ⟨λ x, (is_closed_singleton_iff_is_maximal x).2 _⟩,
+    by_cases hx : x.as_ideal = ⊥,
+    { exact hx.symm ▸ @ideal.bot_is_maximal R (@field.to_division_ring _ $ is_field.to_field R h) },
+    { exact absurd h (ring.not_is_field_iff_exists_prime.2 ⟨x.as_ideal, ⟨hx, x.2⟩⟩) } }
+end
+
 section comap
 variables {S : Type v} [comm_ring S] {S' : Type*} [comm_ring S']
 
@@ -406,6 +436,11 @@ begin
   refl
 end
 
+lemma comap_injective_of_surjective (f : R →+* S) (hf : function.surjective f) :
+  function.injective (comap f) :=
+λ x y h, prime_spectrum.ext.2 (ideal.comap_injective_of_surjective f hf
+  (congr_arg prime_spectrum.as_ideal h : (comap f x).as_ideal = (comap f y).as_ideal))
+
 lemma comap_continuous (f : R →+* S) : continuous (comap f) :=
 begin
   rw continuous_iff_is_closed,
@@ -414,6 +449,20 @@ begin
   exact ⟨_, preimage_comap_zero_locus f s⟩
 end
 
+lemma comap_singleton_is_closed_of_surjective (f : R →+* S) (hf : function.surjective f)
+  (x : prime_spectrum S) (hx : is_closed ({x} : set (prime_spectrum S))) :
+  is_closed ({comap f x} : set (prime_spectrum R)) :=
+begin
+  haveI : x.as_ideal.is_maximal := (is_closed_singleton_iff_is_maximal x).1 hx,
+  exact (is_closed_singleton_iff_is_maximal _).2 (ideal.comap_is_maximal_of_surjective f hf)
+end
+
+lemma comap_singleton_is_closed_of_is_integral (f : R →+* S) (hf : f.is_integral)
+  (x : prime_spectrum S) (hx : is_closed ({x} : set (prime_spectrum S))) :
+  is_closed ({comap f x} : set (prime_spectrum R)) :=
+(is_closed_singleton_iff_is_maximal _).2 (ideal.is_maximal_comap_of_is_integral_of_is_maximal'
+  f hf x.as_ideal $ (is_closed_singleton_iff_is_maximal x).1 hx)
+
 end comap
 
 section basic_open
diff --git a/src/algebraic_geometry/is_open_comap_C.lean b/src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean
similarity index 98%
rename from src/algebraic_geometry/is_open_comap_C.lean
rename to src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean
index ec56600d25c4d..6df1e5afccdf6 100644
--- a/src/algebraic_geometry/is_open_comap_C.lean
+++ b/src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import algebraic_geometry.prime_spectrum
+import algebraic_geometry.prime_spectrum.basic
 import ring_theory.polynomial.basic
 /-!
 The morphism `Spec R[x] --> Spec R` induced by the natural inclusion `R --> R[x]` is an open map.
diff --git a/src/algebraic_geometry/prime_spectrum/noetherian.lean b/src/algebraic_geometry/prime_spectrum/noetherian.lean
new file mode 100644
index 0000000000000..c9abaabee3c72
--- /dev/null
+++ b/src/algebraic_geometry/prime_spectrum/noetherian.lean
@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2020 Filippo A. E. Nuccio. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Filippo A. E. Nuccio
+-/
+import algebraic_geometry.prime_spectrum.basic
+/-!
+This file proves additional properties of the prime spectrum a ring is Noetherian.
+-/
+
+universes u v
+
+namespace prime_spectrum
+
+open submodule
+
+variables (R : Type u) [comm_ring R] [is_noetherian_ring R]
+variables {A : Type u} [comm_ring A] [is_domain A] [is_noetherian_ring A]
+
+/--In a noetherian ring, every ideal contains a product of prime ideals
+([samuel, § 3.3, Lemma 3])-/
+lemma exists_prime_spectrum_prod_le (I : ideal R) :
+  ∃ (Z : multiset (prime_spectrum R)), multiset.prod (Z.map (coe : subtype _ → ideal R)) ≤ I :=
+begin
+  refine is_noetherian.induction (λ (M : ideal R) hgt, _) I,
+  by_cases h_prM : M.is_prime,
+  { use {⟨M, h_prM⟩},
+    rw [multiset.map_singleton, multiset.prod_singleton, subtype.coe_mk],
+    exact le_rfl },
+  by_cases htop : M = ⊤,
+  { rw htop,
+    exact ⟨0, le_top⟩ },
+  have lt_add : ∀ z ∉ M, M < M + span R {z},
+  { intros z hz,
+    refine lt_of_le_of_ne le_sup_left (λ m_eq, hz _),
+    rw m_eq,
+    exact ideal.mem_sup_right (mem_span_singleton_self z) },
+  obtain ⟨x, hx, y, hy, hxy⟩ := (ideal.not_is_prime_iff.mp h_prM).resolve_left htop,
+  obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx),
+  obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy),
+  use Wx + Wy,
+  rw [multiset.map_add, multiset.prod_add],
+  apply le_trans (submodule.mul_le_mul h_Wx h_Wy),
+  rw add_mul,
+  apply sup_le (show M * (M + span R {y}) ≤ M, from ideal.mul_le_right),
+  rw mul_add,
+  apply sup_le (show span R {x} * M ≤ M, from ideal.mul_le_left),
+  rwa [span_mul_span, set.singleton_mul_singleton, span_singleton_le_iff_mem],
+end
+
+/--In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero
+  product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as
+  product or prime ideals ([samuel, § 3.3, Lemma 3]) -/
+lemma exists_prime_spectrum_prod_le_and_ne_bot_of_domain
+  (h_fA : ¬ is_field A) {I : ideal A} (h_nzI: I ≠ ⊥) :
+  ∃ (Z : multiset (prime_spectrum A)), multiset.prod (Z.map (coe : subtype _ → ideal A)) ≤ I ∧
+    multiset.prod (Z.map (coe : subtype _ → ideal A)) ≠ ⊥ :=
+begin
+  revert h_nzI,
+  refine is_noetherian.induction (λ (M : ideal A) hgt, _) I,
+  intro h_nzM,
+  have hA_nont : nontrivial A,
+  apply is_domain.to_nontrivial A,
+  by_cases h_topM : M = ⊤,
+  { rcases h_topM with rfl,
+    obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ (p : ideal A), p ≠ ⊥ ∧ p.is_prime,
+    { apply ring.not_is_field_iff_exists_prime.mp h_fA },
+    use [({⟨p_id, h_pp⟩} : multiset (prime_spectrum A)), le_top],
+    rwa [multiset.map_singleton, multiset.prod_singleton, subtype.coe_mk] },
+  by_cases h_prM : M.is_prime,
+  { use ({⟨M, h_prM⟩} : multiset (prime_spectrum A)),
+    rw [multiset.map_singleton, multiset.prod_singleton, subtype.coe_mk],
+    exact ⟨le_rfl, h_nzM⟩ },
+  obtain ⟨x, hx, y, hy, h_xy⟩ := (ideal.not_is_prime_iff.mp h_prM).resolve_left h_topM,
+  have lt_add : ∀ z ∉ M, M < M + span A {z},
+  { intros z hz,
+    refine lt_of_le_of_ne le_sup_left (λ m_eq, hz _),
+    rw m_eq,
+    exact mem_sup_right (mem_span_singleton_self z) },
+  obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx)),
+  obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy)),
+  use Wx + Wy,
+  rw [multiset.map_add, multiset.prod_add],
+  refine ⟨le_trans (submodule.mul_le_mul h_Wx_le h_Wy_le) _, mt ideal.mul_eq_bot.mp _⟩,
+  { rw add_mul,
+    apply sup_le (show M * (M + span A {y}) ≤ M, from ideal.mul_le_right),
+    rw mul_add,
+    apply sup_le (show span A {x} * M ≤ M, from ideal.mul_le_left),
+    rwa [span_mul_span, set.singleton_mul_singleton, span_singleton_le_iff_mem] },
+  { rintro (hx | hy); contradiction },
+end
+
+end prime_spectrum
diff --git a/src/algebraic_geometry/structure_sheaf.lean b/src/algebraic_geometry/structure_sheaf.lean
index 02512367c633c..39b2648458233 100644
--- a/src/algebraic_geometry/structure_sheaf.lean
+++ b/src/algebraic_geometry/structure_sheaf.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Scott Morrison
 -/
-import algebraic_geometry.prime_spectrum
+import algebraic_geometry.prime_spectrum.basic
 import algebra.category.CommRing.colimits
 import algebra.category.CommRing.limits
 import topology.sheaves.local_predicate
diff --git a/src/ring_theory/dedekind_domain.lean b/src/ring_theory/dedekind_domain.lean
index 732a640b190c3..6f8aef637a01e 100644
--- a/src/ring_theory/dedekind_domain.lean
+++ b/src/ring_theory/dedekind_domain.lean
@@ -10,6 +10,7 @@ import ring_theory.integrally_closed
 import ring_theory.polynomial.rational_root
 import ring_theory.trace
 import algebra.associated
+import algebraic_geometry.prime_spectrum.noetherian
 
 /-!
 # Dedekind domains
@@ -406,7 +407,7 @@ lemma exists_multiset_prod_cons_le_and_prod_not_le [is_dedekind_domain A]
     ¬ (multiset.prod (Z.map prime_spectrum.as_ideal) ≤ I) :=
 begin
   -- Let `Z` be a minimal set of prime ideals such that their product is contained in `J`.
-  obtain ⟨Z₀, hZ₀⟩ := exists_prime_spectrum_prod_le_and_ne_bot_of_domain hNF hI0,
+  obtain ⟨Z₀, hZ₀⟩ := prime_spectrum.exists_prime_spectrum_prod_le_and_ne_bot_of_domain hNF hI0,
   obtain ⟨Z, ⟨hZI, hprodZ⟩, h_eraseZ⟩ := multiset.well_founded_lt.has_min
     (λ Z, (Z.map prime_spectrum.as_ideal).prod ≤ I ∧ (Z.map prime_spectrum.as_ideal).prod ≠ ⊥)
     ⟨Z₀, hZ₀⟩,
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 0570f41bdc4a7..3160927d2a976 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -3,13 +3,12 @@ Copyright (c) 2018 Mario Carneiro, Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kevin Buzzard
 -/
-import algebraic_geometry.prime_spectrum
 import data.multiset.finset_ops
 import group_theory.finiteness
 import linear_algebra.linear_independent
 import order.compactly_generated
 import order.order_iso_nat
-import ring_theory.ideal.quotient
+import ring_theory.ideal.operations
 
 /-!
 # Noetherian rings and modules
@@ -765,87 +764,3 @@ nat.rec_on n
 (λ n ih, by simpa [pow_succ] using fg_mul _ _ h ih)
 
 end submodule
-
-section primes
-
-variables {R : Type*} [comm_ring R] [is_noetherian_ring R]
-
-/--In a noetherian ring, every ideal contains a product of prime ideals
-([samuel, § 3.3, Lemma 3])-/
-
-lemma exists_prime_spectrum_prod_le (I : ideal R) :
-  ∃ (Z : multiset (prime_spectrum R)), multiset.prod (Z.map (coe : subtype _ → ideal R)) ≤ I :=
-begin
-  refine is_noetherian.induction (λ (M : ideal R) hgt, _) I,
-  by_cases h_prM : M.is_prime,
-  { use {⟨M, h_prM⟩},
-    rw [multiset.map_singleton, multiset.prod_singleton, subtype.coe_mk],
-    exact le_rfl },
-  by_cases htop : M = ⊤,
-  { rw htop,
-    exact ⟨0, le_top⟩ },
-  have lt_add : ∀ z ∉ M, M < M + span R {z},
-  { intros z hz,
-    refine lt_of_le_of_ne le_sup_left (λ m_eq, hz _),
-    rw m_eq,
-    exact mem_sup_right (mem_span_singleton_self z) },
-  obtain ⟨x, hx, y, hy, hxy⟩ := (ideal.not_is_prime_iff.mp h_prM).resolve_left htop,
-  obtain ⟨Wx, h_Wx⟩ := hgt (M + span R {x}) (lt_add _ hx),
-  obtain ⟨Wy, h_Wy⟩ := hgt (M + span R {y}) (lt_add _ hy),
-  use Wx + Wy,
-  rw [multiset.map_add, multiset.prod_add],
-  apply le_trans (submodule.mul_le_mul h_Wx h_Wy),
-  rw add_mul,
-  apply sup_le (show M * (M + span R {y}) ≤ M, from ideal.mul_le_right),
-  rw mul_add,
-  apply sup_le (show span R {x} * M ≤ M, from ideal.mul_le_left),
-  rwa [span_mul_span, singleton_mul_singleton, span_singleton_le_iff_mem],
-end
-
-variables {A : Type*} [comm_ring A] [is_domain A] [is_noetherian_ring A]
-
-/--In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero
-  product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as
-  product or prime ideals ([samuel, § 3.3, Lemma 3])
--/
-
-lemma exists_prime_spectrum_prod_le_and_ne_bot_of_domain (h_fA : ¬ is_field A) {I : ideal A}
-  (h_nzI: I ≠ ⊥) :
-  ∃ (Z : multiset (prime_spectrum A)), multiset.prod (Z.map (coe : subtype _ → ideal A)) ≤ I ∧
-    multiset.prod (Z.map (coe : subtype _ → ideal A)) ≠ ⊥ :=
-begin
-  revert h_nzI,
-  refine is_noetherian.induction (λ (M : ideal A) hgt, _) I,
-  intro h_nzM,
-  have hA_nont : nontrivial A,
-  apply is_domain.to_nontrivial,
-  by_cases h_topM : M = ⊤,
-  { rcases h_topM with rfl,
-    obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ (p : ideal A), p ≠ ⊥ ∧ p.is_prime,
-    { apply ring.not_is_field_iff_exists_prime.mp h_fA },
-    use [({⟨p_id, h_pp⟩} : multiset (prime_spectrum A)), le_top],
-    rwa [multiset.map_singleton, multiset.prod_singleton, subtype.coe_mk] },
-  by_cases h_prM : M.is_prime,
-  { use ({⟨M, h_prM⟩} : multiset (prime_spectrum A)),
-    rw [multiset.map_singleton, multiset.prod_singleton, subtype.coe_mk],
-    exact ⟨le_rfl, h_nzM⟩ },
-  obtain ⟨x, hx, y, hy, h_xy⟩ := (ideal.not_is_prime_iff.mp h_prM).resolve_left h_topM,
-  have lt_add : ∀ z ∉ M, M < M + span A {z},
-  { intros z hz,
-    refine lt_of_le_of_ne le_sup_left (λ m_eq, hz _),
-    rw m_eq,
-    exact mem_sup_right (mem_span_singleton_self z) },
-  obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx)),
-  obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy)),
-  use Wx + Wy,
-  rw [multiset.map_add, multiset.prod_add],
-  refine ⟨le_trans (submodule.mul_le_mul h_Wx_le h_Wy_le) _, mt ideal.mul_eq_bot.mp _⟩,
-  { rw add_mul,
-    apply sup_le (show M * (M + span A {y}) ≤ M, from ideal.mul_le_right),
-    rw mul_add,
-    apply sup_le (show span A {x} * M ≤ M, from ideal.mul_le_left),
-    rwa [span_mul_span, singleton_mul_singleton, span_singleton_le_iff_mem] },
-  { rintro (hx | hy); contradiction },
-end
-
-end primes
diff --git a/src/ring_theory/nullstellensatz.lean b/src/ring_theory/nullstellensatz.lean
index cc6e6adabe9b9..bce357fd533ed 100644
--- a/src/ring_theory/nullstellensatz.lean
+++ b/src/ring_theory/nullstellensatz.lean
@@ -6,7 +6,7 @@ Authors: Devon Tuma
 import ring_theory.jacobson
 import field_theory.is_alg_closed.basic
 import field_theory.mv_polynomial
-import algebraic_geometry.prime_spectrum
+import algebraic_geometry.prime_spectrum.basic
 
 /-!
 # Nullstellensatz