feat(algebraic_geometry/prime_spectrum): prime spectrum of a ring is compact (#1987)

* wip

* wip

* wip

* wip

* WIP

* WIP

* Reset changes that belong to other PR

* Docstrings

* Add Heine--Borel to docstring

* Cantor's intersection theorem

* Cantor for sequences

* Revert "Reset changes that belong to other PR"

This reverts commit e6026b8.

* Move submodule lemmas to other file

* Fix build

* Update prime_spectrum.lean

* Docstring

* Update prime_spectrum.lean

* Slight improvement?

* Slightly improve structure of proof

* WIP

* Cleaning up proofs

* Final fixes

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

Author: jcommelin

src/algebraic_geometry/prime_spectrum.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin
 
 import topology.opens
 import ring_theory.ideal_operations
+import linear_algebra.finsupp
 
 /-!
 # Prime spectrum of a commutative ring
@@ -358,4 +359,25 @@ begin
     exact subset_zero_locus_vanishing_ideal t }
 end
 
+/-- The prime spectrum of a commutative ring is a compact topological space. -/
+instance : compact_space (prime_spectrum R) :=
+begin
+  apply compact_space_of_finite_subfamily_closed,
+  intros ι Z hZc hZ,
+  let I : ι → ideal R := λ i, vanishing_ideal (Z i),
+  have hI : ∀ i, Z i = zero_locus (I i),
+  { intro i,
+    rw [zero_locus_vanishing_ideal_eq_closure, closure_eq_of_is_closed],
+    exact hZc i },
+  have one_mem : (1:R) ∈ ⨆ (i : ι), I i,
+  { rw [← ideal.eq_top_iff_one, ← zero_locus_empty_iff_eq_top, zero_locus_supr],
+    simpa only [hI] using hZ },
+  obtain ⟨s, hs⟩ : ∃ s : finset ι, (1:R) ∈ ⨆ i ∈ s, I i :=
+    submodule.exists_finset_of_mem_supr I one_mem,
+  show ∃ t : finset ι, (⋂ i ∈ t, Z i) = ∅,
+  use s,
+  rw [← ideal.eq_top_iff_one, ←zero_locus_empty_iff_eq_top] at hs,
+  simpa only [zero_locus_supr, hI] using hs
+end
+
 end prime_spectrum

src/linear_algebra/basic.lean

@@ -745,6 +745,23 @@ lemma linear_eq_on (s : set M) {f g : M →ₗ[R] M₂} (H : ∀x∈s, f x = g x
   f x = g x :=
 by apply span_induction h H; simp {contextual := tt}
 
+lemma supr_eq_span {ι : Sort w} (p : ι → submodule R M) :
+  (⨆ (i : ι), p i) = submodule.span R (⋃ (i : ι), ↑(p i)) :=
+le_antisymm
+  (lattice.supr_le $ assume i, subset.trans (assume m hm, set.mem_Union.mpr ⟨i, hm⟩) subset_span)
+  (span_le.mpr $ Union_subset_iff.mpr $ assume i m hm, mem_supr_of_mem _ i hm)
+
+lemma span_singleton_le_iff_mem (m : M) (p : submodule R M) :
+  span R {m} ≤ p ↔ m ∈ p :=
+by rw [span_le, singleton_subset_iff, mem_coe]
+
+lemma mem_supr {ι : Sort w} (p : ι → submodule R M) {m : M} :
+  (m ∈ ⨆ i, p i) ↔ (∀ N, (∀ i, p i ≤ N) → m ∈ N) :=
+begin
+  rw [← span_singleton_le_iff_mem, le_supr_iff],
+  simp only [span_singleton_le_iff_mem],
+end
+
 /-- The product of two submodules is a submodule. -/
 def prod : submodule R (M × M₂) :=
 { carrier := set.prod p q,

src/linear_algebra/finsupp.lean

@@ -11,10 +11,10 @@ noncomputable theory
 
 open lattice set linear_map submodule
 
-namespace finsupp
-
 open_locale classical
 
+namespace finsupp
+
 variables {α : Type*} {M : Type*} {R : Type*}
 variables [ring R] [add_comm_group M] [module R M]
 
@@ -371,7 +371,7 @@ begin
     refine sum_mem _ _, simp [this] }
 end
 
-theorem mem_span_iff_total {s : set α} {x : M}:
+theorem mem_span_iff_total {s : set α} {x : M} :
   x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, finsupp.total α M R v l = x :=
 by rw span_eq_map_total; simp
 
@@ -423,8 +423,37 @@ end
 
 end finsupp
 
-lemma linear_map.map_finsupp_total {R : Type*} {β : Type*} {γ : Type*} [ring R]
-  [add_comm_group β] [module R β] [add_comm_group γ] [module R γ]
-  (f : β →ₗ[R] γ) {ι : Type*} [fintype ι] {g : ι → β} (l : ι →₀ R) :
-  f (finsupp.total ι β R g l) = finsupp.total ι γ R (f ∘ g) l :=
+variables {R : Type*} {M : Type*} {N : Type*}
+variables [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+
+lemma linear_map.map_finsupp_total
+  (f : M →ₗ[R] N) {ι : Type*} [fintype ι] {g : ι → M} (l : ι →₀ R) :
+  f (finsupp.total ι M R g l) = finsupp.total ι N R (f ∘ g) l :=
 by simp only [finsupp.total_apply, finsupp.total_apply, finsupp.sum, f.map_sum, f.map_smul]
+
+lemma submodule.exists_finset_of_mem_supr
+  {ι : Sort*} (p : ι → submodule R M) {m : M} (hm : m ∈ ⨆ i, p i) :
+  ∃ s : finset ι, m ∈ ⨆ i ∈ s, p i :=
+begin
+  obtain ⟨f, hf, rfl⟩ : ∃ f ∈ finsupp.supported R R (⋃ i, ↑(p i)), finsupp.total M M R id f = m,
+  { have aux : (id : M → M) '' (⋃ (i : ι), ↑(p i)) = (⋃ (i : ι), ↑(p i)) := set.image_id _,
+    rwa [supr_eq_span, ← aux, finsupp.mem_span_iff_total R] at hm },
+  let t : finset M := f.support,
+  have ht : ∀ x : {x // x ∈ t}, ∃ i, ↑x ∈ p i,
+  { intros x,
+    rw finsupp.mem_supported at hf,
+    specialize hf x.2,
+    rwa set.mem_Union at hf },
+  choose g hg using ht,
+  let s : finset ι := finset.univ.image g,
+  use s,
+  simp only [mem_supr, supr_le_iff],
+  assume N hN,
+  rw [finsupp.total_apply, finsupp.sum, ← submodule.mem_coe],
+  apply is_add_submonoid.finset_sum_mem,
+  assume x hx,
+  apply submodule.smul_mem,
+  let i : ι := g ⟨x, hx⟩,
+  have hi : i ∈ s, { rw finset.mem_image, exact ⟨⟨x, hx⟩, finset.mem_univ _, rfl⟩ },
+  exact hN i hi (hg _),
+end

src/order/complete_lattice.lean

@@ -266,6 +266,9 @@ supr_le $ le_supr _ ∘ h
 @[simp] theorem supr_le_iff : supr s ≤ a ↔ (∀i, s i ≤ a) :=
 ⟨assume : supr s ≤ a, assume i, le_trans (le_supr _ _) this, supr_le⟩
 
+lemma le_supr_iff : (a ≤ supr s) ↔ (∀ b, (∀ i, s i ≤ b) → a ≤ b) :=
+⟨λ h b hb, le_trans h (supr_le hb), λ h, h _ $ λ i, le_supr s i⟩
+
 -- TODO: finish doesn't do well here.
 @[congr] theorem supr_congr_Prop {α : Type u} [has_Sup α] {p q : Prop} {f₁ : p → α} {f₂ : q → α}
   (pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : supr f₁ = supr f₂ :=