feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg (#22151)

A key fact used is `Module.FG.smul`: if `I` is a two-sided ideal of `R` that is f.g. as a left ideal and `N` is a f.g. `R`-module, then `I • M` is also a f.g. `R`-module.

Many lemmas about coprimality of ideals are also generalized to the noncommutative, two-sided setting.

Co-authored-by: Andrew Yang <the.erd.one@gmail.com>

Author: alreadydone

Mathlib/Algebra/Algebra/Operations.lean

@@ -95,6 +95,9 @@ theorem one_eq_span_one_set : (1 : Submodule R A) = span R 1 :=
 theorem one_le {P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P := by
   simp [one_eq_span]
 
+instance : AddCommMonoidWithOne (Submodule R A) where
+  add_comm := sup_comm
+
 variable {M : Type*} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
 
 instance : SMul (Submodule R A) (Submodule R M) where

Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

@@ -303,6 +303,7 @@ lemma XYIdeal_neg_mul {x y : F} (h : W.Nonsingular x y) :
     AdjoinRoot.mk_eq_mk.mpr ⟨1, Y_rw⟩, map_mul, span_insert, ← span_singleton_mul_span_singleton,
     ← Ideal.mul_sup, ← span_insert]
   convert mul_top (_ : Ideal W.CoordinateRing) using 2
+  on_goal 2 => infer_instance
   simp_rw [← Set.image_singleton (f := mk W), ← Set.image_insert_eq, ← map_span]
   convert map_top (R := F[X][Y]) (mk W) using 1
   apply congr_arg

Mathlib/NumberTheory/RamificationInertia/Basic.lean

@@ -242,8 +242,7 @@ lemma ramificationIdx_eq_one_iff
     (hp : P ≠ ⊥) (hpP : p.map (algebraMap R S) ≤ P) :
     ramificationIdx (algebraMap R S) p P = 1 ↔
       p.map (algebraMap R (Localization.AtPrime P)) = maximalIdeal (Localization.AtPrime P) := by
-  refine ⟨?_, ramificationIdx_eq_one_of_map_localization hpP hp
-    (primeCompl_le_nonZeroDivisors _)⟩
+  refine ⟨?_, ramificationIdx_eq_one_of_map_localization hpP hp (primeCompl_le_nonZeroDivisors _)⟩
   let Sₚ := Localization.AtPrime P
   rw [← not_ne_iff (b := 1), ramificationIdx_ne_one_iff hpP, pow_two]
   intro H₁
@@ -252,6 +251,7 @@ lemma ramificationIdx_eq_one_iff
   rw [IsScalarTower.algebraMap_eq _ S, ← Ideal.map_map, ha, Ideal.map_mul,
     Localization.AtPrime.map_eq_maximalIdeal]
   convert Ideal.mul_top _
+  on_goal 2 => infer_instance
   rw [← not_ne_iff, IsLocalization.map_algebraMap_ne_top_iff_disjoint P.primeCompl]
   simpa [primeCompl, Set.disjoint_compl_left_iff_subset]
 

Mathlib/RingTheory/Extension/Basic.lean

@@ -420,7 +420,7 @@ lemma Cotangent.finite (hP : P.ker.FG) :
   refine ⟨.of_restrictScalars (R := P.Ring) _ ?_⟩
   rw [Submodule.restrictScalars_top, ← LinearMap.range_eq_top.mpr Extension.Cotangent.mk_surjective,
     ← Submodule.map_top]
-  exact (P.ker.fg_top.mpr hP).map _
+  exact ((Submodule.fg_top P.ker).mpr hP).map _
 
 end Cotangent
 

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -264,8 +264,10 @@ theorem pi_iff {ι : Type*} {M : ι → Type*} [_root_.Finite ι] [∀ i, AddCom
 
 variable (R)
 
-instance self : Module.Finite R R :=
-  ⟨⟨{1}, by simpa only [Finset.coe_singleton] using Ideal.span_singleton_one⟩⟩
+theorem _root_.Ideal.fg_top : (⊤ : Ideal R).FG :=
+  ⟨{1}, by simpa only [Finset.coe_singleton] using Ideal.span_singleton_one⟩
+
+instance self : Module.Finite R R := ⟨Ideal.fg_top R⟩
 
 variable (M)
 

Mathlib/RingTheory/Finiteness/Ideal.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
+import Mathlib.Algebra.Group.Pointwise.Finset.Scalar
 import Mathlib.RingTheory.Finiteness.Finsupp
 import Mathlib.RingTheory.Ideal.Maps
 
@@ -86,4 +87,18 @@ lemma exists_pow_le_of_le_radical_of_fg {R : Type*} [CommSemiring R] {I J : Idea
     use n₁ + n₂
     exact Ideal.sup_pow_add_le_pow_sup_pow.trans (sup_le hn₁ hn₂)
 
+theorem _root_.Submodule.FG.smul {I : Ideal R} [I.IsTwoSided] {N : Submodule R M}
+    (hI : I.FG) (hN : N.FG) : (I • N).FG := by
+  obtain ⟨s, rfl⟩ := hI
+  obtain ⟨t, rfl⟩ := hN
+  classical rw [Submodule.span_smul_span, ← s.coe_smul]
+  exact ⟨_, rfl⟩
+
+theorem FG.mul {I J : Ideal R} [I.IsTwoSided] (hI : I.FG) (hJ : J.FG) : (I * J).FG :=
+  Submodule.FG.smul hI hJ
+
+theorem FG.pow {I : Ideal R} [I.IsTwoSided] {n : ℕ} (hI : I.FG) : (I ^ n).FG :=
+  n.rec (by rw [I.pow_zero, one_eq_top]; exact fg_top R) fun n ih ↦ by
+    rw [IsTwoSided.pow_succ]; exact hI.mul ih
+
 end Ideal

Mathlib/RingTheory/HopkinsLevitzki.lean

@@ -103,6 +103,18 @@ theorem isNoetherian_iff_isArtinian : IsNoetherian R M ↔ IsArtinian R M :=
     fun M _ _ _ _ h h' ↦ let N : Submodule R M := Ring.jacobson R • ⊤; by
       simp_rw [isNoetherian_iff_submodule_quotient N, isArtinian_iff_submodule_quotient N, N, h, h']
 
+theorem isNoetherian_iff_finite_of_jacobson_fg (fg : (Ring.jacobson R).FG) :
+    IsNoetherian R M ↔ Module.Finite R M :=
+  ⟨fun _ ↦ inferInstance, IsSemiprimaryRing.induction R R M
+    (P := fun M ↦ Module.Finite R M → IsNoetherian R M)
+    (fun M _ _ _ _ _ _ ↦ (IsSemisimpleModule.finite_tfae.out 0 1).mp)
+    fun M _ _ _ _ hs hq fin ↦ (isNoetherian_iff_submodule_quotient (Ring.jacobson R • ⊤)).mpr
+      ⟨hs (Module.Finite.iff_fg.mpr (.smul fg fin.1)), hq inferInstance⟩⟩
+
+theorem isNoetherianRing_iff_jacobson_fg : IsNoetherianRing R ↔ (Ring.jacobson R).FG :=
+  ⟨fun _ ↦ IsNoetherian.noetherian .., fun fg ↦
+    (IsSemiprimaryRing.isNoetherian_iff_finite_of_jacobson_fg fg).mpr inferInstance⟩
+
 end IsSemiprimaryRing
 
 theorem IsArtinianRing.tfae [IsArtinianRing R] :

Mathlib/RingTheory/Ideal/Maps.lean

@@ -608,11 +608,9 @@ protected theorem map_mul {R} [Semiring R] [FunLike F R S] [RingHomClass F R S]
       mul_le.2 fun r hri s hsj =>
         show (f (r * s)) ∈ map f I * map f J by
           rw [map_mul]; exact mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj))
-    (span_mul_span (↑f '' ↑I) (↑f '' ↑J) ▸ (span_le.2 <|
-      Set.iUnion₂_subset fun _ ⟨r, hri, hfri⟩ =>
-        Set.iUnion₂_subset fun _ ⟨s, hsj, hfsj⟩ =>
-          Set.singleton_subset_iff.2 <|
-            hfri ▸ hfsj ▸ by rw [← map_mul]; exact mem_map_of_mem f (mul_mem_mul hri hsj)))
+    (span_mul_span (↑f '' ↑I) (↑f '' ↑J) ▸ (span_le.2 <| by
+      rintro _ ⟨_, ⟨r, hri, rfl⟩, _, ⟨s, hsj, rfl⟩, rfl⟩
+      simp_rw [← map_mul]; exact mem_map_of_mem f (mul_mem_mul hri hsj)))
 
 /-- The pushforward `Ideal.map` as a (semi)ring homomorphism. -/
 @[simps]