feat(algebraic_geometry/prime_spectrum): vanishing ideal (#1972)

* wip

* wip

* Remove stuff for next PR

* Update prime_spectrum.lean

* Process comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebraic_geometry/prime_spectrum.lean

@@ -17,6 +17,20 @@ It is naturally endowed with a topology: the Zariski topology.
 but that sheaf is not constructed in this file.
 It should be contributed to mathlib in future work.)
 
+## Main definitions
+
+* `prime_spectrum R`: The prime spectrum of a commutative ring `R`,
+  i.e., the set of all prime ideals of `R`.
+* `zero_locus s`: The zero locus of a subset `s` of `R`
+  is the subset of `prime_spectrum R` consisting of all prime ideals that contain `s`.
+* `vanishing_ideal t`: The vanishing ideal of a subset `t` of `prime_spectrum R`
+  is the intersection of points in `t` (viewed as prime ideals).
+
+## Conventions
+
+We denote subsets of rings with `s`, `s'`, etc...
+whereas we denote subsets of prime spectra with `t`, `t'`, etc...
+
 ## Inspiration/contributors
 
 The contents of this file draw inspiration from
@@ -26,6 +40,9 @@ and Chris Hughes (on an earlier repository).
 
 -/
 
+noncomputable theory
+open_locale classical
+
 universe variables u v
 
 variables (R : Type u) [comm_ring R]
@@ -69,6 +86,103 @@ def zero_locus (s : set R) : set (prime_spectrum R) :=
 @[simp] lemma mem_zero_locus (x : prime_spectrum R) (s : set R) :
   x ∈ zero_locus s ↔ s ⊆ x.as_ideal := iff.rfl
 
+@[simp] lemma zero_locus_span (s : set R) :
+  zero_locus (ideal.span s : set R) = zero_locus s :=
+by { ext x, exact (submodule.gi R R).gc s x.as_ideal }
+
+/-- The vanishing ideal of a set `t` of points
+of the prime spectrum of a commutative ring `R`
+is the intersection of all the prime ideals in the set `t`.
+
+An element `f` of `R` can be thought of as a dependent function
+on the prime spectrum of `R`.
+At a point `x` (a prime ideal)
+the function (i.e., element) `f` takes values in the quotient ring `R` modulo the prime ideal `x`.
+In this manner, `vanishing_ideal t` is exactly the ideal of `R`
+consisting of all "functions" that vanish on all of `t`.
+-/
+def vanishing_ideal (t : set (prime_spectrum R)) : ideal R :=
+⨅ (x : prime_spectrum R) (h : x ∈ t), x.as_ideal
+
+lemma coe_vanishing_ideal (t : set (prime_spectrum R)) :
+  (vanishing_ideal t : set R) = {f : R | ∀ x : prime_spectrum R, x ∈ t → f ∈ x.as_ideal} :=
+begin
+  ext f,
+  rw [vanishing_ideal, submodule.mem_coe, submodule.mem_infi],
+  apply forall_congr, intro x,
+  rw [submodule.mem_infi],
+end
+
+lemma mem_vanishing_ideal (t : set (prime_spectrum R)) (f : R) :
+  f ∈ vanishing_ideal t ↔ ∀ x : prime_spectrum R, x ∈ t → f ∈ x.as_ideal :=
+by rw [← submodule.mem_coe, coe_vanishing_ideal, set.mem_set_of_eq]
+
+lemma subset_zero_locus_iff_le_vanishing_ideal (t : set (prime_spectrum R)) (I : ideal R) :
+  t ⊆ zero_locus I ↔ I ≤ vanishing_ideal t :=
+begin
+  split; intro h,
+  { intros f hf,
+    rw [submodule.mem_coe, mem_vanishing_ideal],
+    intros x hx,
+    have hxI := h hx,
+    rw mem_zero_locus at hxI,
+    exact hxI hf },
+  { intros x hx,
+    rw mem_zero_locus,
+    refine set.subset.trans h _,
+    intros f hf,
+    rw [submodule.mem_coe, mem_vanishing_ideal] at hf,
+    exact hf x hx }
+end
+
+section gc
+variable (R)
+
+/-- `zero_locus` and `vanishing_ideal` form a galois connection. -/
+lemma gc : @galois_connection
+  (ideal R) (order_dual (set (prime_spectrum R))) _ _
+  (λ I, zero_locus I) (λ t, vanishing_ideal t) :=
+λ I t, subset_zero_locus_iff_le_vanishing_ideal t I
+
+/-- `zero_locus` and `vanishing_ideal` form a galois connection. -/
+lemma gc_set : @galois_connection
+  (set R) (order_dual (set (prime_spectrum R))) _ _
+  (λ s, zero_locus s) (λ t, vanishing_ideal t) :=
+have ideal_gc : galois_connection (ideal.span) coe := (submodule.gi R R).gc,
+by simpa [zero_locus_span, function.comp] using galois_connection.compose _ _ _ _ ideal_gc (gc R)
+
+lemma subset_zero_locus_iff_subset_vanishing_ideal (t : set (prime_spectrum R)) (s : set R) :
+  t ⊆ zero_locus s ↔ s ⊆ vanishing_ideal t :=
+(gc_set R) s t
+
+end gc
+
+-- TODO: we actually get the radical ideal,
+-- but I think that isn't in mathlib yet.
+lemma subset_vanishing_ideal_zero_locus (s : set R) :
+  s ⊆ vanishing_ideal (zero_locus s) :=
+(gc_set R).le_u_l s
+
+lemma le_vanishing_ideal_zero_locus (I : ideal R) :
+  I ≤ vanishing_ideal (zero_locus I) :=
+(gc R).le_u_l I
+
+lemma subset_zero_locus_vanishing_ideal (t : set (prime_spectrum R)) :
+  t ⊆ zero_locus (vanishing_ideal t) :=
+(gc R).l_u_le t
+
+@[simp] lemma zero_locus_bot :
+  zero_locus ((⊥ : ideal R) : set R) = set.univ :=
+(gc R).l_bot
+
+@[simp] lemma zero_locus_empty :
+  zero_locus (∅ : set R) = set.univ :=
+(gc_set R).l_bot
+
+@[simp] lemma vanishing_ideal_univ :
+  vanishing_ideal (∅ : set (prime_spectrum R)) = ⊤ :=
+by simpa using (gc R).u_top
+
 lemma zero_locus_empty_of_one_mem {s : set R} (h : (1:R) ∈ s) :
   zero_locus s = ∅ :=
 begin
@@ -80,30 +194,51 @@ begin
   apply x_prime.1 eq_top,
 end
 
+lemma zero_locus_empty_iff_eq_top {I : ideal R} :
+  zero_locus (I : set R) = ∅ ↔ I = ⊤ :=
+begin
+  split,
+  { contrapose!,
+    intro h,
+    apply set.ne_empty_iff_nonempty.mpr,
+    rcases ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩,
+    exact ⟨⟨M, hM.is_prime⟩, hIM⟩ },
+  { rintro rfl, apply zero_locus_empty_of_one_mem, trivial }
+end
+
 @[simp] lemma zero_locus_univ :
   zero_locus (set.univ : set R) = ∅ :=
 zero_locus_empty_of_one_mem (set.mem_univ 1)
 
-@[simp] lemma zero_locus_span (s : set R) :
-  zero_locus (ideal.span s : set R) = zero_locus s :=
-begin
-  ext x,
-  simp only [mem_zero_locus],
-  split,
-  { exact set.subset.trans ideal.subset_span },
-  { intro h, rwa ← ideal.span_le at h }
-end
+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
+
+lemma zero_locus_union (s s' : set R) :
+  zero_locus (s ∪ s') = zero_locus s ∩ zero_locus s' :=
+(gc_set R).l_sup
+
+lemma vanishing_ideal_union (t t' : set (prime_spectrum R)) :
+  vanishing_ideal (t ∪ t') = vanishing_ideal t ⊓ vanishing_ideal t' :=
+(gc R).u_inf
+
+lemma zero_locus_supr {ι : Sort*} (I : ι → ideal R) :
+  zero_locus ((⨆ i, I i : ideal R) : set R) = (⋂ i, zero_locus (I i)) :=
+(gc R).l_supr
+
+lemma zero_locus_Union {ι : Sort*} (s : ι → set R) :
+  zero_locus (⋃ i, s i) = (⋂ i, zero_locus (s i)) :=
+(gc_set R).l_supr
 
-lemma union_zero_locus_ideal (I J : ideal R) :
-  zero_locus (I : set R) ∪ zero_locus J = zero_locus (I ⊓ J : ideal R) :=
+lemma vanishing_ideal_Union {ι : Sort*} (t : ι → set (prime_spectrum R)) :
+  vanishing_ideal (⋃ i, t i) = (⨅ i, vanishing_ideal (t i)) :=
+(gc R).u_infi
+
+lemma zero_locus_inf (I J : ideal R) :
+  zero_locus ((I ⊓ J : ideal R) : set R) = zero_locus I ∪ zero_locus J :=
 begin
   ext x,
   split,
-  { rintro (h|h),
-    all_goals
-    { rw mem_zero_locus at h ⊢,
-      refine set.subset.trans _ h,
-      intros r hr, cases hr, assumption } },
   { rintro h,
     rw set.mem_union,
     simp only [mem_zero_locus] at h ⊢,
@@ -114,23 +249,29 @@ begin
     rcases hs with ⟨s, hs1, hs2⟩,
     apply (ideal.is_prime.mem_or_mem (by apply_instance) _).resolve_left hs2,
     apply h,
-    rw [submodule.mem_coe, submodule.mem_inf],
     split,
     { exact ideal.mul_mem_left _ hr },
-    { exact ideal.mul_mem_right _ hs1 } }
+    { exact ideal.mul_mem_right _ hs1 } },
+  { rintro (h|h),
+    all_goals
+    { rw mem_zero_locus at h ⊢,
+      refine set.subset.trans _ h,
+      intros r hr, cases hr, assumption } }
 end
 
-lemma union_zero_locus (s t : set R) :
-  zero_locus s ∪ zero_locus t = zero_locus ((ideal.span s) ⊓ (ideal.span t) : ideal R) :=
-by { rw ← union_zero_locus_ideal, simp }
-
-lemma zero_locus_Union {ι : Type*} (s : ι → set R) :
-  zero_locus (⋃ i, s i) = (⋂ i, zero_locus (s i)) :=
-by { ext x, simp only [mem_zero_locus, set.mem_Inter, set.Union_subset_iff] }
+lemma union_zero_locus (s s' : set R) :
+  zero_locus s ∪ zero_locus s' = zero_locus ((ideal.span s) ⊓ (ideal.span s') : ideal R) :=
+by { rw zero_locus_inf, simp }
 
-lemma Inter_zero_locus {ι : Type*} (s : ι → set R) :
-  (⋂ i, zero_locus (s i)) = zero_locus (⋃ i, s i) :=
-(zero_locus_Union s).symm
+lemma sup_vanishing_ideal_le (t t' : set (prime_spectrum R)) :
+  vanishing_ideal t ⊔ vanishing_ideal t' ≤ vanishing_ideal (t ∩ t') :=
+begin
+  intros r,
+  rw [submodule.mem_coe, submodule.mem_sup, submodule.mem_coe, mem_vanishing_ideal],
+  rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩,
+  rw mem_vanishing_ideal at hf hg,
+  apply submodule.add_mem; solve_by_elim
+end
 
 /-- The Zariski topology on the prime spectrum of a commutative ring
 is defined via the closed sets of the topology:
@@ -144,7 +285,7 @@ topological_space.of_closed (set.range prime_spectrum.zero_locus)
     let f : Zs → set R := λ i, classical.some (h i.2),
     have hf : ∀ i : Zs, i.1 = zero_locus (f i) := λ i, (classical.some_spec (h i.2)).symm,
     simp only [hf],
-    exact ⟨_, (Inter_zero_locus _).symm⟩
+    exact ⟨_, zero_locus_Union _⟩
   end
   (by { rintro _ _ ⟨s, rfl⟩ ⟨t, rfl⟩, exact ⟨_, (union_zero_locus s t).symm⟩ })
 
@@ -156,7 +297,7 @@ lemma is_closed_iff_zero_locus (Z : set (prime_spectrum R)) :
   is_closed Z ↔ ∃ s, Z = zero_locus s :=
 by rw [is_closed, is_open_iff, set.compl_compl]
 
-lemma zero_locus_is_closed (s : set R) :
+lemma is_closed_zero_locus (s : set R) :
   is_closed (zero_locus s) :=
 by { rw [is_closed_iff_zero_locus], exact ⟨s, rfl⟩ }
 
@@ -199,4 +340,18 @@ end
 
 end comap
 
+lemma zero_locus_vanishing_ideal_eq_closure (t : set (prime_spectrum R)) :
+  zero_locus (vanishing_ideal t : set R) = closure t :=
+begin
+  apply set.subset.antisymm,
+  { rintro x hx t' ⟨ht', ht⟩,
+    obtain ⟨fs, rfl⟩ : ∃ s, t' = zero_locus s,
+    by rwa [is_closed_iff_zero_locus] at ht',
+    rw [subset_zero_locus_iff_subset_vanishing_ideal] at ht,
+    calc fs ⊆ vanishing_ideal t : ht
+        ... ⊆ x.as_ideal        : hx },
+  { rw closure_subset_iff_subset_of_is_closed (is_closed_zero_locus _),
+    exact subset_zero_locus_vanishing_ideal t }
+end
+
 end prime_spectrum