feat(ring_theory/ideal/local_ring): API for local rings. (#17185)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -446,7 +446,7 @@ begin
       (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 _ h.to_field) },
+    { letI := h.to_field, exact hx.symm ▸ ideal.bot_is_maximal },
     { exact absurd h (ring.not_is_field_iff_exists_prime.2 ⟨x.as_ideal, ⟨hx, x.2⟩⟩) } }
 end
 
@@ -822,6 +822,14 @@ order_embedding.of_map_le_iff nhds $ λ a b, (le_iff_specializes a b).symm
 
 instance : t0_space (prime_spectrum R) := ⟨nhds_order_embedding.injective⟩
 
+instance [is_domain R] : order_bot (prime_spectrum R) :=
+{ bot := ⟨⊥, ideal.bot_prime⟩,
+  bot_le := λ I, @bot_le _ _ _ I.as_ideal }
+
+instance {R : Type*} [field R] : unique (prime_spectrum R) :=
+{ default := ⊥,
+  uniq := λ x, ext _ _ ((is_simple_order.eq_bot_or_eq_top _).resolve_right x.2.ne_top) }
+
 end order
 
 /-- If `x` specializes to `y`, then there is a natural map from the localization of `y` to the
@@ -856,4 +864,24 @@ by { rw [(local_hom_tfae f).out 0 4, prime_spectrum.ext_iff], refl }
   [is_local_ring_hom f] : prime_spectrum.comap f (closed_point S) = closed_point R :=
 (is_local_ring_hom_iff_comap_closed_point f).mp infer_instance
 
+lemma specializes_closed_point (x : prime_spectrum R) :
+  x ⤳ closed_point R :=
+(prime_spectrum.le_iff_specializes _ _).mp (local_ring.le_maximal_ideal x.2.1)
+
+lemma closed_point_mem_iff (U : topological_space.opens $ prime_spectrum R) :
+  closed_point R ∈ U ↔ U = ⊤ :=
+begin
+  split,
+  { rw eq_top_iff, exact λ h x _, (specializes_closed_point x).mem_open U.2 h },
+  { rintro rfl, trivial }
+end
+
+@[simp] lemma _root_.prime_spectrum.comap_residue (x : prime_spectrum (residue_field R)) :
+  prime_spectrum.comap (residue R) x = closed_point R :=
+begin
+  rw subsingleton.elim x ⊥,
+  ext1,
+  exact ideal.mk_ker,
+end
+
 end local_ring

src/ring_theory/discrete_valuation_ring.lean

@@ -61,7 +61,7 @@ lemma not_a_field : maximal_ideal R ≠ ⊥ := not_a_field'
 
 /-- A discrete valuation ring `R` is not a field. -/
 lemma not_is_field : ¬ is_field R :=
-ring.not_is_field_iff_exists_prime.mpr ⟨_, not_a_field R, is_maximal.is_prime' (maximal_ideal R)⟩
+local_ring.is_field_iff_maximal_ideal_eq.not.mpr (not_a_field R)
 
 variable {R}
 

src/ring_theory/ideal/basic.lean

@@ -535,12 +535,12 @@ end ideal
 
 end ring
 
-section division_ring
-variables {K : Type u} [division_ring K] (I : ideal K)
+section division_semiring
+variables {K : Type u} [division_semiring K] (I : ideal K)
 
 namespace ideal
 
-/-- All ideals in a division ring are trivial. -/
+/-- All ideals in a division (semi)ring are trivial. -/
 lemma eq_bot_or_top : I = ⊥ ∨ I = ⊤ :=
 begin
   rw or_iff_not_imp_right,
@@ -553,8 +553,8 @@ begin
   simpa [H, h1] using I.mul_mem_left r⁻¹ hr,
 end
 
-/-- Ideals of a `division_ring` are a simple order. Thanks to the way abbreviations work, this
-automatically gives a `is_simple_module K` instance. -/
+/-- Ideals of a `division_semiring` are a simple order. Thanks to the way abbreviations work,
+this automatically gives a `is_simple_module K` instance. -/
 instance : is_simple_order (ideal K) := ⟨eq_bot_or_top⟩
 
 lemma eq_bot_of_prime [h : I.is_prime] : I = ⊥ :=
@@ -566,7 +566,7 @@ lemma bot_is_maximal : is_maximal (⊥ : ideal K) :=
 
 end ideal
 
-end division_ring
+end division_semiring
 
 section comm_ring
 
@@ -583,12 +583,11 @@ end ideal
 
 end comm_ring
 
+-- TODO: consider moving the lemmas below out of the `ring` namespace since they are
+-- about `comm_semiring`s.
 namespace ring
 
-variables {R : Type*} [comm_ring R]
-
-lemma not_is_field_of_subsingleton {R : Type*} [ring R] [subsingleton R] : ¬ is_field R :=
-λ ⟨⟨x, y, hxy⟩, _, _⟩, hxy (subsingleton.elim x y)
+variables {R : Type*} [comm_semiring R]
 
 lemma exists_not_is_unit_of_not_is_field [nontrivial R] (hf : ¬ is_field R) :
   ∃ x ≠ (0 : R), ¬ is_unit x :=
@@ -624,6 +623,22 @@ not_is_field_iff_exists_ideal_bot_lt_and_lt_top.trans
     ⟨p, bot_lt_iff_ne_bot.mp (lt_of_lt_of_le bot_lt le_p), hp.is_prime⟩,
    λ ⟨p, ne_bot, prime⟩, ⟨p, bot_lt_iff_ne_bot.mpr ne_bot, lt_top_iff_ne_top.mpr prime.1⟩⟩
 
+/-- Also see `ideal.is_simple_order` for the forward direction as an instance when `R` is a
+division (semi)ring. 
+
+This result actually holds for all division semirings, but we lack the predicate to state it. -/
+lemma is_field_iff_is_simple_order_ideal :
+  is_field R ↔ is_simple_order (ideal R) :=
+begin
+  casesI subsingleton_or_nontrivial R,
+  { exact ⟨λ h, (not_is_field_of_subsingleton _ h).elim,
+      λ h, by exactI (false_of_nontrivial_of_subsingleton $ ideal R).elim⟩ },
+  rw [← not_iff_not, ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top, ← not_iff_not],
+  push_neg,
+  simp_rw [lt_top_iff_ne_top, bot_lt_iff_ne_bot, ← or_iff_not_imp_left, not_ne_iff],
+  exact ⟨λ h, ⟨h⟩, λ h, h.2⟩
+end
+
 /-- When a ring is not a field, the maximal ideals are nontrivial. -/
 lemma ne_bot_of_is_maximal_of_not_is_field [nontrivial R] {M : ideal R} (max : M.is_maximal)
   (not_field : ¬ is_field R) : M ≠ ⊥ :=

src/ring_theory/ideal/local_ring.lean

@@ -130,6 +130,11 @@ end
 
 @[simp] lemma mem_maximal_ideal (x) : x ∈ maximal_ideal R ↔ x ∈ nonunits R := iff.rfl
 
+lemma is_field_iff_maximal_ideal_eq :
+  is_field R ↔ maximal_ideal R = ⊥ :=
+not_iff_not.mp ⟨ring.ne_bot_of_is_maximal_of_not_is_field infer_instance,
+  λ h, ring.not_is_field_iff_exists_prime.mpr ⟨_, h, ideal.is_maximal.is_prime' _⟩⟩
+
 end local_ring
 
 end comm_semiring
@@ -324,10 +329,28 @@ ideal.quotient.algebra _
 
 lemma residue_field.algebra_map_eq : algebra_map R (residue_field R) = residue R := rfl
 
+instance : is_local_ring_hom (local_ring.residue R) :=
+⟨λ a ha, not_not.mp (ideal.quotient.eq_zero_iff_mem.not.mp (is_unit_iff_ne_zero.mp ha))⟩
+
 variables {R}
 
 namespace residue_field
 
+/-- A local ring homomorphism into a field can be descended onto the residue field. -/
+def lift {R S : Type*} [comm_ring R] [local_ring R] [field S]
+  (f : R →+* S) [is_local_ring_hom f] : local_ring.residue_field R →+* S :=
+ideal.quotient.lift _ f (λ a ha,
+  classical.by_contradiction (λ h, ha (is_unit_of_map_unit f a (is_unit_iff_ne_zero.mpr h))))
+
+lemma lift_comp_residue {R S : Type*} [comm_ring R] [local_ring R] [field S] (f : R →+* S)
+  [is_local_ring_hom f] : (lift f).comp (residue R) = f :=
+ring_hom.ext (λ _, rfl)
+
+@[simp]
+lemma lift_residue_apply {R S : Type*} [comm_ring R] [local_ring R] [field S] (f : R →+* S)
+  [is_local_ring_hom f] (x) : lift f (residue R x) = f x :=
+rfl
+
 /-- The map on residue fields induced by a local homomorphism between local rings -/
 def map (f : R →+* S) [is_local_ring_hom f] : residue_field R →+* residue_field S :=
 ideal.quotient.lift (maximal_ideal R) ((ideal.quotient.mk _).comp f) $
@@ -433,3 +456,7 @@ local_ring.of_is_unit_or_is_unit_one_sub_self $ λ a,
   else or.inl $ is_unit.mk0 a h
 
 end field
+
+lemma local_ring.maximal_ideal_eq_bot {R : Type*} [field R] :
+  local_ring.maximal_ideal R = ⊥ :=
+local_ring.is_field_iff_maximal_ideal_eq.mp (field.to_is_field R)

src/ring_theory/ideal/operations.lean

@@ -1904,7 +1904,7 @@ end
   (⊥ : ideal (R ⧸ I)).is_maximal ↔ I.is_maximal :=
 ⟨λ hI, (@mk_ker _ _ I) ▸
   @comap_is_maximal_of_surjective _ _ _ _ _ _ (quotient.mk I) quotient.mk_surjective ⊥ hI,
- λ hI, @bot_is_maximal _ (@field.to_division_ring _ (@quotient.field _ _ I hI)) ⟩
+ λ hI, by { resetI, letI := quotient.field I, exact bot_is_maximal }⟩
 
 /-- See also `ideal.mem_quotient_iff_mem` in case `I ≤ J`. -/
 @[simp]

src/ring_theory/localization/at_prime.lean

@@ -139,6 +139,10 @@ not_iff_not.mp $ by
 simpa only [local_ring.mem_maximal_ideal, mem_nonunits_iff, not_not]
   using is_unit_to_map_iff S I x
 
+lemma comap_maximal_ideal (h : _root_.local_ring S := local_ring S I) :
+  (local_ring.maximal_ideal S).comap (algebra_map R S) = I :=
+ideal.ext $ λ x, by simpa only [ideal.mem_comap] using to_map_mem_maximal_iff _ I x
+
 lemma is_unit_mk'_iff (x : R) (y : I.prime_compl) :
   is_unit (mk' S x y) ↔ x ∈ I.prime_compl :=
 ⟨λ h hx, mk'_mem_iff.mpr ((to_map_mem_maximal_iff S I x).mpr hx) h,
@@ -168,8 +172,7 @@ variables {I}
 lemma at_prime.comap_maximal_ideal :
   ideal.comap (algebra_map R (localization.at_prime I))
     (local_ring.maximal_ideal (localization I.prime_compl)) = I :=
-ideal.ext $ λ x, by
-simpa only [ideal.mem_comap] using at_prime.to_map_mem_maximal_iff _ I x
+at_prime.comap_maximal_ideal _ _
 
 /-- The image of `I` in the localization at `I.prime_compl` is a maximal ideal, and in particular
 it is the unique maximal ideal given by the local ring structure `at_prime.local_ring` -/