refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure (#16930)

Author: Multramate

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -5,10 +5,10 @@ Authors: Johan Commelin
 -/
 import algebra.punit_instances
 import linear_algebra.finsupp
-import ring_theory.nilpotent
-import ring_theory.localization.away
-import ring_theory.ideal.prod
 import ring_theory.ideal.over
+import ring_theory.ideal.prod
+import ring_theory.localization.away
+import ring_theory.nilpotent
 import topology.sets.closeds
 import topology.sober
 
@@ -37,79 +37,84 @@ whereas we denote subsets of prime spectra with `t`, `t'`, etc...
 
 ## Inspiration/contributors
 
-The contents of this file draw inspiration from
-<https://github.com/ramonfmir/lean-scheme>
+The contents of this file draw inspiration from <https://github.com/ramonfmir/lean-scheme>
 which has contributions from Ramon Fernandez Mir, Kevin Buzzard, Kenny Lau,
 and Chris Hughes (on an earlier repository).
-
 -/
 
 noncomputable theory
 open_locale classical
 
 universes u v
 
-variables (R : Type u) [comm_ring R]
+variables (R : Type u) (S : Type v) [comm_ring R] [comm_ring S]
 
-/-- The prime spectrum of a commutative ring `R`
-is the type of all prime ideals of `R`.
+/-- The prime spectrum of a commutative ring `R` is the type of all prime ideals of `R`.
 
 It is naturally endowed with a topology (the Zariski topology),
 and a sheaf of commutative rings (see `algebraic_geometry.structure_sheaf`).
 It is a fundamental building block in algebraic geometry. -/
-@[nolint has_nonempty_instance]
-def prime_spectrum := {I : ideal R // I.is_prime}
+@[ext] structure prime_spectrum :=
+(as_ideal : ideal R)
+(is_prime : as_ideal.is_prime)
 
-variable {R}
+attribute [instance] prime_spectrum.is_prime
 
 namespace prime_spectrum
 
-/-- A method to view a point in the prime spectrum of a commutative ring
-as an ideal of that ring. -/
-abbreviation as_ideal (x : prime_spectrum R) : ideal R := x.val
+variables {R S}
 
-instance is_prime (x : prime_spectrum R) :
-  x.as_ideal.is_prime := x.2
+instance [nontrivial R] : nonempty $ prime_spectrum R :=
+let ⟨I, hI⟩ := ideal.exists_maximal R in ⟨⟨I, hI.is_prime⟩⟩
 
-/--
-The prime spectrum of the zero ring is empty.
--/
+/-- The prime spectrum of the zero ring is empty. -/
 lemma punit (x : prime_spectrum punit) : false :=
 x.1.ne_top_iff_one.1 x.2.1 $ subsingleton.elim (0 : punit) 1 ▸ x.1.zero_mem
 
-section
-variables (R) (S : Type v) [comm_ring S]
+variables (R S)
+
+/-- The map from the direct sum of prime spectra to the prime spectrum of a direct product. -/
+@[simp] def prime_spectrum_prod_of_sum :
+  prime_spectrum R ⊕ prime_spectrum S → prime_spectrum (R × S)
+| (sum.inl ⟨I, hI⟩) := ⟨ideal.prod I ⊤, by exactI ideal.is_prime_ideal_prod_top⟩
+| (sum.inr ⟨J, hJ⟩) := ⟨ideal.prod ⊤ J, by exactI ideal.is_prime_ideal_prod_top'⟩
 
 /-- The prime spectrum of `R × S` is in bijection with the disjoint unions of the prime spectrum of
-    `R` and the prime spectrum of `S`. -/
+`R` and the prime spectrum of `S`. -/
 noncomputable def prime_spectrum_prod :
   prime_spectrum (R × S) ≃ prime_spectrum R ⊕ prime_spectrum S :=
-ideal.prime_ideals_equiv R S
+equiv.symm $ equiv.of_bijective (prime_spectrum_prod_of_sum R S)
+begin
+  split,
+  { rintro (⟨I, hI⟩|⟨J, hJ⟩) (⟨I', hI'⟩|⟨J', hJ'⟩) h;
+    simp only [ideal.prod.ext_iff, prime_spectrum_prod_of_sum] at h,
+    { simp only [h] },
+    { exact false.elim (hI.ne_top h.left) },
+    { exact false.elim (hJ.ne_top h.right) },
+    { simp only [h] } },
+  { rintro ⟨I, hI⟩,
+    rcases (ideal.ideal_prod_prime I).mp hI with (⟨p, ⟨hp, rfl⟩⟩|⟨p, ⟨hp, rfl⟩⟩),
+    { exact ⟨sum.inl ⟨p, hp⟩, rfl⟩ },
+    { exact ⟨sum.inr ⟨p, hp⟩, rfl⟩ } }
+end
 
 variables {R S}
 
 @[simp] lemma prime_spectrum_prod_symm_inl_as_ideal (x : prime_spectrum R) :
-  ((prime_spectrum_prod R S).symm (sum.inl x)).as_ideal = ideal.prod x.as_ideal ⊤ :=
+  ((prime_spectrum_prod R S).symm $ sum.inl x).as_ideal = ideal.prod x.as_ideal ⊤ :=
 by { cases x, refl }
+
 @[simp] lemma prime_spectrum_prod_symm_inr_as_ideal (x : prime_spectrum S) :
-  ((prime_spectrum_prod R S).symm (sum.inr x)).as_ideal = ideal.prod ⊤ x.as_ideal :=
+  ((prime_spectrum_prod R S).symm $ sum.inr x).as_ideal = ideal.prod ⊤ x.as_ideal :=
 by { cases x, refl }
 
-end
-
-@[ext] lemma ext {x y : prime_spectrum R} :
-  x = y ↔ x.as_ideal = y.as_ideal :=
-subtype.ext_iff_val
-
-/-- The zero locus of a set `s` of elements of a commutative ring `R`
-is the set of all prime ideals of the ring that contain the set `s`.
+/-- The zero locus of a set `s` of elements of a commutative ring `R` is the set of all prime ideals
+of the ring that contain the set `s`.
 
-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, `zero_locus s` is exactly the subset of `prime_spectrum R`
-where all "functions" in `s` vanish simultaneously.
+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, `zero_locus s` is exactly the subset of
+`prime_spectrum R` where all "functions" in `s` vanish simultaneously.
 -/
 def zero_locus (s : set R) : set (prime_spectrum R) :=
 {x | s ⊆ x.as_ideal}
@@ -121,15 +126,12 @@ def zero_locus (s : set R) : set (prime_spectrum 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`.
+/-- 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`
+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 :=
@@ -338,9 +340,8 @@ lemma mem_compl_zero_locus_iff_not_mem {f : R} {I : prime_spectrum R} :
   I ∈ (zero_locus {f} : set (prime_spectrum R))ᶜ ↔ f ∉ I.as_ideal :=
 by rw [set.mem_compl_iff, mem_zero_locus, set.singleton_subset_iff]; refl
 
-/-- The Zariski topology on the prime spectrum of a commutative ring
-is defined via the closed sets of the topology:
-they are exactly those sets that are the zero locus of a subset of the ring. -/
+/-- The Zariski topology on the prime spectrum of a commutative ring is defined via the closed sets
+of the topology: they are exactly those sets that are the zero locus of a subset of the ring. -/
 instance zariski_topology : topological_space (prime_spectrum R) :=
 topological_space.of_closed (set.range prime_spectrum.zero_locus)
   (⟨set.univ, by simp⟩)
@@ -387,7 +388,7 @@ begin
       (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⟩ }
+    refine ⟨λ _ h, h, λ y hy, prime_spectrum.ext _ _ (h.eq_of_le y.2.ne_top hy).symm⟩ }
 end
 
 lemma zero_locus_vanishing_ideal_eq_closure (t : set (prime_spectrum R)) :
@@ -496,7 +497,7 @@ instance : quasi_sober (prime_spectrum R) :=
  by rw [is_generic_point, closure_singleton, zero_locus_vanishing_ideal_eq_closure, h₂.closure_eq]⟩⟩
 
 section comap
-variables {S : Type v} [comm_ring S] {S' : Type*} [comm_ring S']
+variables {S' : Type*} [comm_ring S']
 
 lemma preimage_comap_zero_locus_aux (f : R →+* S) (s : set R) :
   (λ y, ⟨ideal.comap f y.as_ideal, infer_instance⟩ :
@@ -540,7 +541,7 @@ preimage_comap_zero_locus_aux f s
 
 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
+λ x y h, prime_spectrum.ext _ _ (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_singleton_is_closed_of_surjective (f : R →+* S) (hf : function.surjective f)
@@ -762,7 +763,7 @@ begin
   simp only [set.eq_univ_iff_forall, set.singleton_subset_iff,
     topological_space.opens.coe_bot, nilpotent_iff_mem_prime, set.compl_empty_iff, mem_zero_locus,
     set_like.mem_coe],
-  exact subtype.forall,
+  exact ⟨λ h I hI, h ⟨I, hI⟩, λ h ⟨I, hI⟩, h I hI⟩
 end
 
 lemma localization_away_comap_range (S : Type v) [comm_ring S] [algebra R S] (r : R)
@@ -795,20 +796,16 @@ section order
 /-!
 ## The specialization order
 
-We endow `prime_spectrum R` with a partial order,
-where `x ≤ y` if and only if `y ∈ closure {x}`.
+We endow `prime_spectrum R` with a partial order, where `x ≤ y` if and only if `y ∈ closure {x}`.
 -/
 
-instance : partial_order (prime_spectrum R) :=
-subtype.partial_order _
+instance : partial_order (prime_spectrum R) := partial_order.lift as_ideal ext
 
-@[simp] lemma as_ideal_le_as_ideal (x y : prime_spectrum R) :
-  x.as_ideal ≤ y.as_ideal ↔ x ≤ y :=
-subtype.coe_le_coe
+@[simp] lemma as_ideal_le_as_ideal (x y : prime_spectrum R) : x.as_ideal ≤ y.as_ideal ↔ x ≤ y :=
+iff.rfl
 
-@[simp] lemma as_ideal_lt_as_ideal (x y : prime_spectrum R) :
-  x.as_ideal < y.as_ideal ↔ x < y :=
-subtype.coe_lt_coe
+@[simp] lemma as_ideal_lt_as_ideal (x y : prime_spectrum R) : x.as_ideal < y.as_ideal ↔ x < y :=
+iff.rfl
 
 lemma le_iff_mem_closure (x y : prime_spectrum R) :
   x ≤ y ↔ y ∈ closure ({x} : set (prime_spectrum R)) :=
@@ -828,8 +825,8 @@ instance : t0_space (prime_spectrum R) := ⟨nhds_order_embedding.injective⟩
 
 end order
 
-/-- If `x` specializes to `y`, then there is a natural map from the localization of `y` to
-the localization of `x`. -/
+/-- If `x` specializes to `y`, then there is a natural map from the localization of `y` to the
+localization of `x`. -/
 def localization_map_of_specializes {x y : prime_spectrum R} (h : x ⤳ y) :
   localization.at_prime y.as_ideal →+* localization.at_prime x.as_ideal :=
 @is_localization.lift _ _ _ _ _ _ _ _
@@ -843,22 +840,18 @@ def localization_map_of_specializes {x y : prime_spectrum R} (h : x ⤳ y) :
 
 end prime_spectrum
 
-
 namespace local_ring
 
-variables (R) [local_ring R]
+variables [local_ring R]
 
-/--
-The closed point in the prime spectrum of a local ring.
--/
-def closed_point : prime_spectrum R :=
-⟨maximal_ideal R, (maximal_ideal.is_maximal R).is_prime⟩
+/-- The closed point in the prime spectrum of a local ring. -/
+def closed_point : prime_spectrum R := ⟨maximal_ideal R, (maximal_ideal.is_maximal R).is_prime⟩
 
 variable {R}
 
 lemma is_local_ring_hom_iff_comap_closed_point {S : Type v} [comm_ring S] [local_ring S]
   (f : R →+* S) : is_local_ring_hom f ↔ prime_spectrum.comap f (closed_point S) = closed_point R :=
-by { rw [(local_hom_tfae f).out 0 4, subtype.ext_iff], refl }
+by { rw [(local_hom_tfae f).out 0 4, prime_spectrum.ext_iff], refl }
 
 @[simp] lemma comap_closed_point {S : Type v} [comm_ring S] [local_ring S] (f : R →+* S)
   [is_local_ring_hom f] : prime_spectrum.comap f (closed_point S) = closed_point R :=

src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean

@@ -31,7 +31,7 @@ def image_of_Df (f) : set (prime_spectrum R) :=
 
 lemma is_open_image_of_Df : is_open (image_of_Df f) :=
 begin
-  rw [image_of_Df, set_of_exists (λ i (x : prime_spectrum R), coeff f i ∉ x.val)],
+  rw [image_of_Df, set_of_exists (λ i (x : prime_spectrum R), coeff f i ∉ x.as_ideal)],
   exact is_open_Union (λ i, is_open_basic_open),
 end
 
@@ -48,11 +48,13 @@ morphism `C⁺ : Spec R[x] → Spec R`. -/
 lemma image_of_Df_eq_comap_C_compl_zero_locus :
   image_of_Df f = prime_spectrum.comap (C : R →+* R[X]) '' (zero_locus {f})ᶜ :=
 begin
-  refine ext (λ x, ⟨λ hx, ⟨⟨map C x.val, (is_prime_map_C_of_is_prime x.property)⟩, ⟨_, _⟩⟩, _⟩),
+  ext x,
+  refine ⟨λ hx, ⟨⟨map C x.as_ideal, (is_prime_map_C_of_is_prime x.is_prime)⟩, ⟨_, _⟩⟩, _⟩,
   { rw [mem_compl_iff, mem_zero_locus, singleton_subset_iff],
     cases hx with i hi,
     exact λ a, hi (mem_map_C_iff.mp a i) },
-  { refine subtype.ext (ext (λ x, ⟨λ h, _, λ h, subset_span (mem_image_of_mem C.1 h)⟩)),
+  { ext x,
+    refine ⟨λ h, _, λ h, subset_span (mem_image_of_mem C.1 h)⟩,
     rw ← @coeff_C_zero R x _,
     exact mem_map_C_iff.mp h 0 },
   { rintro ⟨xli, complement, rfl⟩,

src/algebraic_geometry/prime_spectrum/maximal.lean

@@ -43,14 +43,14 @@ variable {R}
 namespace maximal_spectrum
 
 instance [nontrivial R] : nonempty $ maximal_spectrum R :=
-⟨⟨(ideal.exists_maximal R).some, (ideal.exists_maximal R).some_spec⟩⟩
+let ⟨I, hI⟩ := ideal.exists_maximal R in ⟨⟨I, hI⟩⟩
 
 /-- The natural inclusion from the maximal spectrum to the prime spectrum. -/
 def to_prime_spectrum (x : maximal_spectrum R) : prime_spectrum R :=
 ⟨x.as_ideal, x.is_maximal.is_prime⟩
 
 lemma to_prime_spectrum_injective : (@to_prime_spectrum R _).injective :=
-λ ⟨_, _⟩ ⟨_, _⟩ h, by simpa only [maximal_spectrum.mk.inj_eq] using subtype.mk.inj h
+λ ⟨_, _⟩ ⟨_, _⟩ h, by simpa only [mk.inj_eq] using (prime_spectrum.ext_iff _ _).mp h
 
 open prime_spectrum set
 

src/algebraic_geometry/prime_spectrum/noetherian.lean

@@ -21,12 +21,12 @@ 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 :=
+  ∃ (Z : multiset (prime_spectrum R)), multiset.prod (Z.map as_ideal) ≤ 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],
+    rw [multiset.map_singleton, multiset.prod_singleton],
     exact le_rfl },
   by_cases htop : M = ⊤,
   { rw htop,
@@ -54,8 +54,8 @@ end
   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)) ≠ ⊥ :=
+  ∃ (Z : multiset (prime_spectrum A)), multiset.prod (Z.map as_ideal) ≤ I ∧
+    multiset.prod (Z.map as_ideal) ≠ ⊥ :=
 begin
   revert h_nzI,
   refine is_noetherian.induction (λ (M : ideal A) hgt, _) I,
@@ -67,10 +67,10 @@ begin
     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] },
+    rwa [multiset.map_singleton, multiset.prod_singleton] },
   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],
+    rw [multiset.map_singleton, multiset.prod_singleton],
     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},

src/ring_theory/dedekind_domain/ideal.lean

@@ -342,8 +342,8 @@ begin
   obtain ⟨_, hPZ', hPM⟩ := (hM.is_prime.multiset_prod_le (mt multiset.map_eq_zero.mp hZ0)).mp hZM,
   -- Then in fact there is a `P ∈ Z` with `P ≤ M`.
   obtain ⟨P, hPZ, rfl⟩ := multiset.mem_map.mp hPZ',
-  letI := classical.dec_eq (ideal A),
-  have := multiset.map_erase prime_spectrum.as_ideal subtype.coe_injective P Z,
+  classical,
+  have := multiset.map_erase prime_spectrum.as_ideal prime_spectrum.ext P Z,
   obtain ⟨hP0, hZP0⟩ : P.as_ideal ≠ ⊥ ∧ ((Z.erase P).map prime_spectrum.as_ideal).prod ≠ ⊥,
   { rwa [ne.def, ← multiset.cons_erase hPZ', multiset.prod_cons, ideal.mul_eq_bot,
          not_or_distrib, ← this] at hprodZ },