feat(ring_theory/jacobson): definition of Jacobson rings (#3404)

src/data/equiv/ring.lean

@@ -162,6 +162,11 @@ variables [semiring R] [semiring S]
 def to_ring_hom (e : R ≃+* S) : R →+* S :=
 { .. e.to_mul_equiv.to_monoid_hom, .. e.to_add_equiv.to_add_monoid_hom }
 
+instance has_coe_to_ring_hom : has_coe (R ≃+* S) (R →+* S) := ⟨ring_equiv.to_ring_hom⟩
+
+@[norm_cast] lemma coe_ring_hom (f : R ≃+* S) (a : R) :
+  (f : R →+* S) a = f a := rfl
+
 /-- Reinterpret a ring equivalence as a monoid homomorphism. -/
 abbreviation to_monoid_hom (e : R ≃+* S) : R →* S := e.to_ring_hom.to_monoid_hom
 

src/ring_theory/ideal_operations.lean

@@ -616,13 +616,21 @@ submodule.span_induction H (λ _, id) ⟨0, I.zero_mem, f.map_zero⟩
 (λ y1 y2 ⟨x1, hx1i, hxy1⟩ ⟨x2, hx2i, hxy2⟩, ⟨x1 + x2, I.add_mem hx1i hx2i, hxy1 ▸ hxy2 ▸ f.map_add _ _⟩)
 (λ c y ⟨x, hxi, hxy⟩, let ⟨d, hdc⟩ := hf c in ⟨d • x, I.smul_mem _ hxi, hdc ▸ hxy ▸ f.map_mul _ _⟩)
 
+lemma mem_map_iff_of_surjective {I : ideal R} {y} :
+  y ∈ map f I ↔ ∃ x, x ∈ I ∧ f x = y :=
+⟨λ h, (set.mem_image _ _ _).2 (mem_image_of_mem_map_of_surjective f hf h),
+  λ ⟨x, hx⟩, hx.right ▸ (mem_map_of_mem hx.left)⟩
+
 theorem comap_map_of_surjective (I : ideal R) :
   comap f (map f I) = I ⊔ comap f ⊥ :=
 le_antisymm (assume r h, let ⟨s, hsi, hfsr⟩ := mem_image_of_mem_map_of_surjective f hf h in
   submodule.mem_sup.2 ⟨s, hsi, r - s, (submodule.mem_bot S).2 $ by rw [f.map_sub, hfsr, sub_self],
   add_sub_cancel'_right s r⟩)
 (sup_le (map_le_iff_le_comap.1 (le_refl _)) (comap_mono bot_le))
 
+lemma le_map_of_comap_le_of_surjective : comap f K ≤ I → K ≤ map f I :=
+λ h, (map_comap_of_surjective f hf K) ▸ map_mono h
+
 /-- Correspondence theorem -/
 def order_iso_of_surjective :
   ((≤) : ideal S → ideal S → Prop) ≃o
@@ -644,72 +652,74 @@ def lt_order_embedding_of_surjective :
   ((<) : ideal S → ideal S → Prop) ≼o ((<) : ideal R → ideal R → Prop) :=
 (le_order_embedding_of_surjective f hf).lt_embedding_of_le_embedding
 
+theorem map_eq_top_or_is_maximal_of_surjective (H : is_maximal I) :
+  (map f I) = ⊤ ∨ is_maximal (map f I) :=
+begin
+  refine classical.or_iff_not_imp_left.2 (λ ne_top, ⟨λ h, ne_top h, λ J hJ, _⟩),
+  { refine (order_iso_of_surjective f hf).injective
+      (subtype.ext_iff.2 (eq.trans (H.right (comap f J) (lt_of_le_of_ne _ _)) comap_top.symm)),
+    { exact (map_le_iff_le_comap).1 (le_of_lt hJ) },
+    { exact λ h, hJ.right (le_map_of_comap_le_of_surjective f hf (le_of_eq h.symm)) } }
+end
+
 end surjective
 
-end map_and_comap
+section injective
+variables (hf : function.injective f)
+include hf
 
-section jacobson
-variables {R : Type u} [comm_ring R]
+open function
 
-/-- The Jacobson radical of `I` is the infimum of all maximal ideals containing `I`. -/
-def jacobson (I : ideal R) : ideal R :=
-Inf {J : ideal R | I ≤ J ∧ is_maximal J}
-
-theorem jacobson_eq_top_iff {I : ideal R} : jacobson I = ⊤ ↔ I = ⊤ :=
-⟨λ H, classical.by_contradiction $ λ hi, let ⟨M, hm, him⟩ := exists_le_maximal I hi in
-  lt_top_iff_ne_top.1 (lt_of_le_of_lt (show jacobson I ≤ M, from Inf_le ⟨him, hm⟩) $ lt_top_iff_ne_top.2 hm.1) H,
-λ H, eq_top_iff.2 $ le_Inf $ λ J ⟨hij, hj⟩, H ▸ hij⟩
-
-theorem mem_jacobson_iff {I : ideal R} {x : R} :
-  x ∈ jacobson I ↔ ∀ y, ∃ z, x * y * z + z - 1 ∈ I :=
-⟨λ hx y, classical.by_cases
-  (assume hxy : I ⊔ span {x * y + 1} = ⊤,
-    let ⟨p, hpi, q, hq, hpq⟩ := submodule.mem_sup.1 ((eq_top_iff_one _).1 hxy) in
-    let ⟨r, hr⟩ := mem_span_singleton.1 hq in
-    ⟨r, by rw [← one_mul r, ← mul_assoc, ← add_mul, mul_one, ← hr, ← hpq, ← neg_sub, add_sub_cancel]; exact I.neg_mem hpi⟩)
-  (assume hxy : I ⊔ span {x * y + 1} ≠ ⊤,
-    let ⟨M, hm1, hm2⟩ := exists_le_maximal _ hxy in
-    suffices x ∉ M, from (this $ mem_Inf.1 hx ⟨le_trans le_sup_left hm2, hm1⟩).elim,
-    λ hxm, hm1.1 $ (eq_top_iff_one _).2 $ add_sub_cancel' (x * y) 1 ▸ M.sub_mem
-      (le_trans le_sup_right hm2 $ mem_span_singleton.2 $ dvd_refl _)
-      (M.mul_mem_right hxm)),
-λ hx, mem_Inf.2 $ λ M ⟨him, hm⟩, classical.by_contradiction $ λ hxm,
-  let ⟨y, hy⟩ := hm.exists_inv hxm, ⟨z, hz⟩ := hx (-y) in
-  hm.1 $ (eq_top_iff_one _).2 $ sub_sub_cancel (x * -y * z + z) 1 ▸ M.sub_mem
-    (by rw [← one_mul z, ← mul_assoc, ← add_mul, mul_one, mul_neg_eq_neg_mul_symm, neg_add_eq_sub, ← neg_sub,
-        neg_mul_eq_neg_mul_symm, neg_mul_eq_mul_neg, mul_comm x y]; exact M.mul_mem_right hy)
-    (him hz)⟩
-
-end jacobson
-
-section is_local
-variables {R : Type u} [comm_ring R]
+lemma comap_bot_le_of_injective : comap f ⊥ ≤ I :=
+begin
+  refine le_trans (λ x hx, _) bot_le,
+  rw [mem_comap, submodule.mem_bot, ← ring_hom.map_zero f] at hx,
+  exact eq.symm (hf hx) ▸ (submodule.zero_mem ⊥)
+end
 
-/-- An ideal `I` is local iff its Jacobson radical is maximal. -/
-@[class] def is_local (I : ideal R) : Prop :=
-is_maximal (jacobson I)
+end injective
 
-theorem is_local_of_is_maximal_radical {I : ideal R} (hi : is_maximal (radical I)) : is_local I :=
-have radical I = jacobson I,
-from le_antisymm (le_Inf $ λ M ⟨him, hm⟩, hm.is_prime.radical_le_iff.2 him)
-  (Inf_le ⟨le_radical, hi⟩),
-show is_maximal (jacobson I), from this ▸ hi
+section bijective
+variables (hf : function.bijective f)
+include hf
+
+open function
 
-theorem is_local.le_jacobson {I J : ideal R} (hi : is_local I) (hij : I ≤ J) (hj : J ≠ ⊤) : J ≤ jacobson I :=
-let ⟨M, hm, hjm⟩ := exists_le_maximal J hj in
-le_trans hjm $ le_of_eq $ eq.symm $ hi.eq_of_le hm.1 $ Inf_le ⟨le_trans hij hjm, hm⟩
+/-- Special case of the correspondence theorem for isomorphic rings -/
+def order_iso_of_bijective :
+  ((≤) : ideal S → ideal S → Prop) ≃o ((≤) : ideal R → ideal R → Prop):=
+{ to_fun := comap f,
+  inv_fun := map f,
+  left_inv := (order_iso_of_surjective f hf.right).left_inv,
+  right_inv := λ J, subtype.ext_iff.1
+    ((order_iso_of_surjective f hf.right).right_inv ⟨J, comap_bot_le_of_injective f hf.left⟩),
+  ord' := (order_iso_of_surjective f hf.right).ord' }
+
+lemma comap_le_iff_le_map : comap f K ≤ I ↔ K ≤ map f I :=
+⟨λ h, le_map_of_comap_le_of_surjective f hf.right h,
+ λ h, ((order_iso_of_bijective f hf).right_inv I) ▸ comap_mono h⟩
+
+theorem map.is_maximal (H : is_maximal I) : is_maximal (map f I) :=
+by refine classical.or_iff_not_imp_left.1
+  (map_eq_top_or_is_maximal_of_surjective f hf.right H) (λ h, H.left _);
+calc I = comap f (map f I) : ((order_iso_of_bijective f hf).right_inv I).symm
+   ... = comap f ⊤ : by rw h
+   ... = ⊤ : by rw comap_top
+
+theorem comap.is_maximal (H : is_maximal K) : is_maximal (comap f K) :=
+begin
+  refine ⟨λ h, H.left _, λ J hJ, _⟩,
+  { have : map f (comap f K) = ⊤ := eq.trans (congr_arg (map f) h) (map_top _),
+    rwa ← (order_iso_of_bijective f hf).left_inv K },
+  { refine (order_iso_of_bijective f hf).symm.injective
+      (eq.trans (H.right (map f J) (lt_of_le_of_ne _ _)) (map_top f).symm),
+    { exact (comap_le_iff_le_map f hf).1 (le_of_lt hJ) },
+    { exact λ h, hJ.right ((map_le_iff_le_comap).1 (le_of_eq h.symm)) } }
+end
 
-theorem is_local.mem_jacobson_or_exists_inv {I : ideal R} (hi : is_local I) (x : R) :
-  x ∈ jacobson I ∨ ∃ y, y * x - 1 ∈ I :=
-classical.by_cases
-  (assume h : I ⊔ span {x} = ⊤,
-    let ⟨p, hpi, q, hq, hpq⟩ := submodule.mem_sup.1 ((eq_top_iff_one _).1 h) in
-    let ⟨r, hr⟩ := mem_span_singleton.1 hq in
-    or.inr ⟨r, by rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel]; exact I.neg_mem hpi⟩)
-  (assume h : I ⊔ span {x} ≠ ⊤,
-    or.inl $ le_trans le_sup_right (hi.le_jacobson le_sup_left h) $ mem_span_singleton.2 $ dvd_refl x)
+end bijective
 
-end is_local
+end map_and_comap
 
 section is_primary
 variables {R : Type u} [comm_ring R]
@@ -742,16 +752,6 @@ begin
   { rw hij at hyi, exact or.inr hyi }
 end⟩
 
-theorem is_primary_of_is_maximal_radical {I : ideal R} (hi : is_maximal (radical I)) : is_primary I :=
-have radical I = jacobson I,
-from le_antisymm (le_Inf $ λ M ⟨him, hm⟩, hm.is_prime.radical_le_iff.2 him)
-  (Inf_le ⟨le_radical, hi⟩),
-⟨ne_top_of_lt $ lt_of_le_of_lt le_radical (lt_top_iff_ne_top.2 hi.1),
-λ x y hxy, ((is_local_of_is_maximal_radical hi).mem_jacobson_or_exists_inv y).symm.imp
-  (λ ⟨z, hz⟩, by rw [← mul_one x, ← sub_sub_cancel (z * y) 1, mul_sub, mul_left_comm]; exact
-    I.sub_mem (I.mul_mem_left hxy) (I.mul_mem_left hz))
-  (this ▸ id)⟩
-
 end is_primary
 
 end ideal
@@ -799,6 +799,38 @@ variables {R : Type*} {S : Type*} [comm_ring R] [comm_ring S]
 lemma map_eq_bot_iff_le_ker {I : ideal R} (f : R →+* S) : I.map f = ⊥ ↔ I ≤ f.ker :=
 by rw [ring_hom.ker, eq_bot_iff, map_le_iff_le_comap]
 
+lemma ker_le_comap {K : ideal S} (f : R →+* S) : f.ker ≤ comap f K :=
+λ x hx, mem_comap.2 (((ring_hom.mem_ker f).1 hx).symm ▸ K.zero_mem)
+
+lemma map_Inf {A : set (ideal R)} {f : R →+* S} (hf : function.surjective f) :
+  (∀ J ∈ A, ring_hom.ker f ≤ J) → map f (Inf A) = Inf (map f '' A) :=
+begin
+  refine λ h, le_antisymm (le_Inf _) _,
+  { intros j hj y hy,
+    cases (mem_map_iff_of_surjective f hf).1 hy with x hx,
+    cases (set.mem_image _ _ _).mp hj with J hJ,
+    rw [← hJ.right, ← hx.right],
+    exact mem_map_of_mem (Inf_le_of_le hJ.left (le_of_eq rfl) hx.left) },
+  {
+    intros y hy,
+    cases hf y with x hx,
+    rw ← hx,
+    refine mem_map_of_mem _,
+    rw Inf_eq_infi at ⊢ hy,
+    simp at ⊢ hy,
+    intros J hJ,
+    have : y ∈ map f J := hy (map f J) J hJ rfl,
+    cases (mem_map_iff_of_surjective f hf).1 this with x' hx',
+    have : x - x' ∈ J, {
+      apply h J hJ,
+      rw [ring_hom.mem_ker, ring_hom.map_sub, hx, hx'.right],
+      exact sub_self y
+    },
+    have := J.add_mem this hx'.left,
+    rwa [sub_add, sub_self, sub_zero] at this,
+  }
+end
+
 end ideal
 
 namespace submodule

src/ring_theory/ideals.lean

@@ -302,6 +302,10 @@ lemma eq_bot_of_prime {K : Type u} [field K] (I : ideal K) [h : I.is_prime] :
   I = ⊥ :=
 classical.or_iff_not_imp_right.mp I.eq_bot_or_top h.1
 
+lemma bot_is_maximal {K : Type u} [field K] : is_maximal (⊥ : ideal K) :=
+⟨λ h, absurd ((eq_top_iff_one (⊤ : ideal K)).mp rfl) (by rw ← h; simp),
+λ I hI, or_iff_not_imp_left.mp (eq_bot_or_top I) (ne_of_gt hI)⟩
+
 end ideal
 
 /-- The set of non-invertible elements of a monoid. -/

src/ring_theory/jacobson.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2020 Devon Tuma. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+import data.mv_polynomial
+import ring_theory.ideals
+import ring_theory.ideal_operations
+import ring_theory.jacobson_ideal
+
+/-!
+# Jacobson rings
+
+The following conditions are equivalent for a ring `R`:
+1. Every radical ideal `I` is equal to its jacobson radical
+2. Every radical ideal `I` can be written as an intersection of maximal ideals
+3. Every prime ideal `I` is equal to its jacobson radical
+
+Any ring satisfying any of these equivalent conditions is said to be Jacobson.
+
+## Main definitions
+
+Let `R` be a commutative ring. Jacobson Rings are defined using the first of the above conditions
+
+* `is_jacobson R` is the proposition that `R` is a Jacobson ring. It is a class,
+  implemented as the predicate that for any ideal, `I.radical = I` implies `I.jacobson = I`.
+
+## Main statements
+
+* `is_jacobson_iff_prime_eq` is the equivalence between conditions 1 and 3 above.
+
+* `is_jacobson_iff_Inf_maximal` is the equivalence between conditions 1 and 2 above.
+
+## Tags
+
+Jacobson, Jacobson Ring
+
+-/
+
+universes u v
+
+namespace ideal
+section is_jacobson
+variables {R : Type u} [comm_ring R] {I : ideal R}
+variables {S : Type v} [comm_ring S]
+
+/-- Definition of jacobson rings in terms of radical ideals -/
+@[class] def is_jacobson (R : Type u) [comm_ring R] :=
+    ∀ (I : ideal R), I.radical = I → I.jacobson = I
+
+/-- Defining jacobson rings in terms of prime ideals is completely equivalent -/
+lemma is_jacobson_iff_prime_eq : is_jacobson R ↔ ∀ P : ideal R, is_prime P → P.jacobson = P :=
+begin
+  split,
+  { exact λ h I hI, h I (is_prime.radical hI) },
+  { refine λ h I hI, le_antisymm (λ x hx, _) (λ x hx, mem_Inf.mpr (λ _ hJ, hJ.left hx)),
+    erw mem_Inf at hx,
+    rw [← hI, radical_eq_Inf I, mem_Inf],
+    intros P hP,
+    rw set.mem_set_of_eq at hP,
+    erw [← h P hP.right, mem_Inf],
+    exact λ J hJ, hx ⟨le_trans hP.left hJ.left, hJ.right⟩ }
+end
+
+/-- I equals its jacobson iff it can be written as an Inf of maximal ideals -/
+lemma is_jacobson_iff_Inf_maximal : is_jacobson R ↔
+    ∀ {I : ideal R}, I.radical = I → ∃ M ⊆ {J : ideal R | J.is_maximal ∨ J = ⊤}, I = Inf M :=
+begin
+  use λ H I h, ⟨{J : ideal R | I ≤ J ∧ J.is_maximal}, ⟨λ _ hJ, or.inl hJ.right, eq.symm (H _ h)⟩⟩,
+  intros H I hI,
+  rcases H hI with ⟨M, hM, hInf⟩,
+  refine le_antisymm _ le_jacobson,
+  intros x hx,
+  rw hInf,
+  erw mem_Inf at ⊢ hx,
+  intros I hI,
+  cases hM hI with is_max is_top,
+  { refine hx ⟨le_Inf_iff.1 (le_of_eq hInf) I hI, is_max⟩ },
+  { rw is_top, exact submodule.mem_top }
+end
+
+lemma radical_eq_jacobson (H : is_jacobson R) (I : ideal R) : I.radical = I.jacobson :=
+le_antisymm (le_Inf (λ J ⟨hJ, hJ_max⟩, (is_prime.radical_le_iff hJ_max.is_prime).mpr hJ))
+            ((H I.radical (radical_idem I)) ▸ (jacobson_mono le_radical))
+
+/-- Fields have only two ideals, and the condition holds for both of them -/
+@[priority 100]
+instance is_jacobson_field {K : Type u} [field K] : is_jacobson K :=
+λ I hI, or.rec_on (eq_bot_or_top I)
+(λ h, le_antisymm
+  (Inf_le ⟨le_of_eq rfl, (eq.symm h) ▸ bot_is_maximal⟩)
+  ((eq.symm h) ▸ bot_le))
+(λ h, by rw [h, jacobson_eq_top_iff])
+
+theorem is_jacobson_of_surjective [H : is_jacobson R] :
+  (∃ (f : R →+* S), function.surjective f) → is_jacobson S :=
+begin
+  rintros ⟨f, hf⟩,
+  rw is_jacobson_iff_Inf_maximal,
+  intros p hp,
+  use map f '' {J : ideal R | comap f p ≤ J ∧ J.is_maximal },
+  use λ j ⟨J, hJ, hmap⟩, hmap ▸ or.symm (map_eq_top_or_is_maximal_of_surjective f hf hJ.right),
+  have : p = map f ((comap f p).jacobson),
+  from (H (comap f p) (by rw [← comap_radical, hp])).symm ▸ (map_comap_of_surjective f hf p).symm,
+  exact eq.trans this (map_Inf hf (λ J ⟨hJ, _⟩, le_trans (ideal.ker_le_comap f) hJ)),
+end
+
+@[priority 100]
+instance is_jacobson_quotient [is_jacobson R] : is_jacobson (quotient I) :=
+is_jacobson_of_surjective ⟨quotient.mk I, (by rintro ⟨x⟩; use x; refl)⟩
+
+lemma is_jacobson_iso (e : R ≃+* S) : is_jacobson R ↔ is_jacobson S :=
+⟨λ h, @is_jacobson_of_surjective _ _ _ _ h ⟨(e : R →+* S), e.surjective⟩,
+  λ h, @is_jacobson_of_surjective _ _ _ _ h ⟨(e.symm : S →+* R), e.symm.surjective⟩⟩
+
+end is_jacobson
+
+end ideal