feat(ring_theory/noetherian): The nilradical of a noetherian ring is …

…nilpotent (#16881)




Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/ring_theory/ideal/operations.lean

@@ -310,6 +310,8 @@ variables {R : Type u} [semiring R]
 @[simp] lemma add_eq_sup {I J : ideal R} : I + J = I ⊔ J := rfl
 @[simp] lemma zero_eq_bot : (0 : ideal R) = ⊥ := rfl
 
+@[simp] lemma sum_eq_sup {ι : Type*} (s : finset ι) (f : ι → ideal R) : s.sum f = s.sup f := rfl
+
 end add
 
 section mul_and_radical

src/ring_theory/noetherian.lean

@@ -7,7 +7,7 @@ import group_theory.finiteness
 import data.multiset.finset_ops
 import algebra.algebra.tower
 import order.order_iso_nat
-import ring_theory.ideal.operations
+import ring_theory.nilpotent
 import order.compactly_generated
 import linear_algebra.linear_independent
 import algebra.ring.idempotents
@@ -427,6 +427,25 @@ begin
   { rintro (rfl|rfl); simp [is_idempotent_elem] }
 end
 
+lemma exists_radical_pow_le_of_fg {R : Type*} [comm_semiring R] (I : ideal R) (h : I.radical.fg) :
+  ∃ n : ℕ, I.radical ^ n ≤ I :=
+begin
+  have := le_refl I.radical, revert this,
+  refine submodule.fg_induction _ _ (λ J, J ≤ I.radical → ∃ n : ℕ, J ^ n ≤ I) _ _ _ h,
+  { intros x hx, obtain ⟨n, hn⟩ := hx (subset_span (set.mem_singleton x)),
+    exact ⟨n, by rwa [← ideal.span, span_singleton_pow, span_le, set.singleton_subset_iff]⟩ },
+  { intros J K hJ hK hJK,
+    obtain ⟨n, hn⟩ := hJ (λ x hx, hJK $ ideal.mem_sup_left hx),
+    obtain ⟨m, hm⟩ := hK (λ x hx, hJK $ ideal.mem_sup_right hx),
+    use n + m,
+    rw [← ideal.add_eq_sup, add_pow, ideal.sum_eq_sup, finset.sup_le_iff],
+    refine λ i hi, ideal.mul_le_right.trans _,
+    obtain h | h := le_or_lt n i,
+    { exact ideal.mul_le_right.trans ((ideal.pow_le_pow h).trans hn) },
+    { refine ideal.mul_le_left.trans ((ideal.pow_le_pow _).trans hm),
+      rw [add_comm, nat.add_sub_assoc h.le], apply nat.le_add_right } },
+end
+
 end ideal
 
 /--
@@ -888,6 +907,13 @@ theorem is_noetherian_ring_of_ring_equiv (R) [ring R] {S} [ring S]
   (f : R ≃+* S) [is_noetherian_ring R] : is_noetherian_ring S :=
 is_noetherian_ring_of_surjective R S f.to_ring_hom f.to_equiv.surjective
 
+lemma is_noetherian_ring.is_nilpotent_nilradical (R : Type*) [comm_ring R] [is_noetherian_ring R] :
+  is_nilpotent (nilradical R) :=
+begin
+  obtain ⟨n, hn⟩ := ideal.exists_radical_pow_le_of_fg (⊥ : ideal R) (is_noetherian.noetherian _),
+  exact ⟨n, eq_bot_iff.mpr hn⟩
+end
+
 namespace submodule
 
 section map₂