feat(RingTheory): Hopkins–Levitzki theorem (#21451)

**RingTheory/HopkinsLevitzki.lean** (new file): the Hopkins--Levitzki theorem says a module over a semiprimary ring is Noetherian iff it's Artinian (iff it's of finite length). As a consequence, a (left) Artinian ring is also (left) Noetherian, and a commutative ring is Artinian iff it's Noetherian and has Krull dimension 0.

**RingTheory/Jacobson/Semiprimary.lean** (new file): contains the definition of semiprimary rings, and connections between Jacobson radicals of modules and semisimplicity.

**RingTheory/Jacobson/Radical.lean** (new file): develop the theory of Jacobson radicals of modules, including versions of Nakayama's lemma over noncommutative rings.

**RingTheory/Artinian/Module.lean**: show an Artinian module or ring is semisimple iff it has trivial radical; show that an Artinian ring is semiprimary.

Author: alreadydone

Mathlib.lean

@@ -4636,6 +4636,7 @@ import Mathlib.RingTheory.HahnSeries.Summable
 import Mathlib.RingTheory.HahnSeries.Valuation
 import Mathlib.RingTheory.Henselian
 import Mathlib.RingTheory.HopfAlgebra
+import Mathlib.RingTheory.HopkinsLevitzki
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Ideal.Basis
@@ -4686,7 +4687,9 @@ import Mathlib.RingTheory.IsPrimary
 import Mathlib.RingTheory.IsTensorProduct
 import Mathlib.RingTheory.Jacobson.Ideal
 import Mathlib.RingTheory.Jacobson.Polynomial
+import Mathlib.RingTheory.Jacobson.Radical
 import Mathlib.RingTheory.Jacobson.Ring
+import Mathlib.RingTheory.Jacobson.Semiprimary
 import Mathlib.RingTheory.Kaehler.Basic
 import Mathlib.RingTheory.Kaehler.CotangentComplex
 import Mathlib.RingTheory.Kaehler.JacobiZariski

Mathlib/AlgebraicGeometry/Fiber.lean

@@ -101,7 +101,7 @@ instance (f : X ⟶ Y) (y : Y) [LocallyOfFiniteType f] : JacobsonSpace (f.fiber
 instance (f : X ⟶ Y) (y : Y) [IsFinite f] : Finite (f.fiber y) := by
   have H : IsFinite (f.fiberToSpecResidueField y) := MorphismProperty.pullback_snd _ _ inferInstance
   have : IsArtinianRing Γ(f.fiber y, ⊤) :=
-    @IsArtinianRing.of_finite (Y.residueField y) Γ(f.fiber y, ⊤) _ _ (show _ from _) _
+    @IsArtinianRing.of_finite (Y.residueField y) Γ(f.fiber y, ⊤) _ _ (show _ from _) _ _
       ((HasAffineProperty.iff_of_isAffine.mp H).2.comp (.of_surjective _ (Scheme.ΓSpecIso
         (Y.residueField y)).commRingCatIsoToRingEquiv.symm.surjective))
   exact .of_injective (β := PrimeSpectrum _) _ (f.fiber y).isoSpec.hom.homeomorph.injective

Mathlib/RingTheory/Artinian/Instances.lean

@@ -6,7 +6,6 @@ Authors: Junyan Xu
 import Mathlib.Algebra.Divisibility.Prod
 import Mathlib.Algebra.Polynomial.FieldDivision
 import Mathlib.RingTheory.Artinian.Module
-import Mathlib.RingTheory.SimpleModule.Basic
 
 /-!
 # Instances related to Artinian rings
@@ -26,6 +25,4 @@ instance : DecompositionMonoid R := MulEquiv.decompositionMonoid (equivPi R)
 instance : DecompositionMonoid (Polynomial R) :=
   MulEquiv.decompositionMonoid <| (Polynomial.mapEquiv <| equivPi R).trans (Polynomial.piEquiv _)
 
-theorem isSemisimpleRing_of_isReduced : IsSemisimpleRing R := (equivPi R).symm.isSemisimpleRing
-
 end IsArtinianRing

Mathlib/RingTheory/Artinian/Module.lean

@@ -7,6 +7,7 @@ import Mathlib.Data.SetLike.Fintype
 import Mathlib.Order.Filter.EventuallyConst
 import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient.Operations
+import Mathlib.RingTheory.Jacobson.Semiprimary
 import Mathlib.RingTheory.Nilpotent.Lemmas
 import Mathlib.RingTheory.Noetherian.Defs
 import Mathlib.RingTheory.Spectrum.Maximal.Basic
@@ -39,6 +40,11 @@ Let `R` be a ring and let `M` and `P` be `R`-modules. Let `N` be an `R`-submodul
   product of fields (and therefore is a semisimple ring and a decomposition monoid; moreover
   `R[X]` is also a decomposition monoid).
 
+* `IsArtinian.isSemisimpleModule_iff_jacobson`: an Artinian module is semisimple
+  iff its Jacobson radical is zero.
+
+* `instIsSemiprimaryRingOfIsArtinianRing`: an Artinian ring `R` is semiprimary, in particular
+  the Jacobson radical of `R` is a nilpotent ideal (`IsArtinianRing.isNilpotent_jacobson_bot`).
 
 ## References
 
@@ -68,6 +74,12 @@ variable {R M P N : Type*}
 variable [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid N]
 variable [Module R M] [Module R P] [Module R N]
 
+theorem LinearMap.isArtinian_iff_of_bijective {S P} [Ring S] [AddCommGroup P] [Module S P]
+    {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] P) (hl : Function.Bijective l) :
+    IsArtinian R M ↔ IsArtinian S P :=
+  let e := Submodule.orderIsoMapComapOfBijective l hl
+  ⟨fun _ ↦ e.symm.strictMono.wellFoundedLT, fun _ ↦ e.strictMono.wellFoundedLT⟩
+
 theorem isArtinian_of_injective (f : M →ₗ[R] P) (h : Function.Injective f) [IsArtinian R P] :
     IsArtinian R M :=
   ⟨Subrelation.wf
@@ -273,6 +285,18 @@ instance isArtinian_iSup :
   · intros; rw [iSup_of_empty]; infer_instance
   · intro _ _ ih _ _; rw [iSup_option]; infer_instance
 
+variable (R M) in
+theorem IsArtinian.isSemisimpleModule_iff_jacobson [IsArtinian R M] :
+    IsSemisimpleModule R M ↔ Module.jacobson R M = ⊥ :=
+  ⟨fun _ ↦ IsSemisimpleModule.jacobson_eq_bot R M, fun h ↦
+    have ⟨s, hs⟩ := Finset.exists_inf_le (Subtype.val (p := fun m : Submodule R M ↦ IsCoatom m))
+    have _ (m : s) : IsSimpleModule R (M ⧸ m.1.1) := isSimpleModule_iff_isCoatom.mpr m.1.2
+    let f : M →ₗ[R] ∀ m : s, M ⧸ m.1.1 := LinearMap.pi fun m ↦ m.1.1.mkQ
+    .of_injective f <| LinearMap.ker_eq_bot.mp <| le_bot_iff.mp fun x hx ↦ by
+      rw [← h, Module.jacobson, Submodule.mem_sInf]
+      exact fun m hm ↦ hs ⟨m, hm⟩ <| Submodule.mem_finset_inf.mpr fun i hi ↦
+        (Submodule.Quotient.mk_eq_zero i.1).mp <| congr_fun hx ⟨i, hi⟩⟩
+
 open Submodule Function
 
 namespace LinearMap
@@ -380,34 +404,21 @@ theorem Ring.isArtinian_of_zero_eq_one {R} [Semiring R] (h01 : (0 : R) = 1) : Is
   have := subsingleton_of_zero_eq_one h01
   inferInstance
 
-instance (R) [CommRing R] [IsArtinianRing R] (I : Ideal R) : IsArtinianRing (R ⧸ I) :=
+instance (R) [Ring R] [IsArtinianRing R] (I : Ideal R) [I.IsTwoSided] : IsArtinianRing (R ⧸ I) :=
   isArtinian_of_tower R inferInstance
 
 open Submodule Function
 
-theorem isArtinian_of_fg_of_artinian {R M} [Ring R] [AddCommGroup M] [Module R M]
-    (N : Submodule R M) [IsArtinianRing R] (hN : N.FG) : IsArtinian R N := by
-  let ⟨s, hs⟩ := hN
-  haveI := Classical.decEq M
-  haveI := Classical.decEq R
-  have : ∀ x ∈ s, x ∈ N := fun x hx => hs ▸ Submodule.subset_span hx
-  refine @isArtinian_of_surjective _ ((↑s : Set M) →₀ R) N _ _ _ _ _ ?_ ?_ isArtinian_finsupp
-  · exact Finsupp.linearCombination R (fun i => ⟨i, hs ▸ subset_span i.2⟩)
-  · rw [← LinearMap.range_eq_top, eq_top_iff,
-       ← map_le_map_iff_of_injective (show Injective (Submodule.subtype N)
-         from Subtype.val_injective), Submodule.map_top, range_subtype,
-         ← Submodule.map_top, ← Submodule.map_comp, Submodule.map_top]
-    subst N
-    refine span_le.2 (fun i hi => ?_)
-    use Finsupp.single ⟨i, hi⟩ 1
-    simp
-
 instance isArtinian_of_fg_of_artinian' {R M} [Ring R] [AddCommGroup M] [Module R M]
     [IsArtinianRing R] [Module.Finite R M] : IsArtinian R M :=
-  have : IsArtinian R (⊤ : Submodule R M) := isArtinian_of_fg_of_artinian _ Module.Finite.fg_top
-  isArtinian_of_linearEquiv (LinearEquiv.ofTop (⊤ : Submodule R M) rfl)
+  have ⟨_, _, h⟩ := Module.Finite.exists_fin' R M
+  isArtinian_of_surjective _ _ h
+
+theorem isArtinian_of_fg_of_artinian {R M} [Ring R] [AddCommGroup M] [Module R M]
+    (N : Submodule R M) [IsArtinianRing R] (hN : N.FG) : IsArtinian R N := by
+  rw [← Module.Finite.iff_fg] at hN; infer_instance
 
-theorem IsArtinianRing.of_finite (R S) [CommRing R] [Ring S] [Algebra R S]
+theorem IsArtinianRing.of_finite (R S) [Ring R] [Ring S] [Module R S] [IsScalarTower R S S]
     [IsArtinianRing R] [Module.Finite R S] : IsArtinianRing S :=
   isArtinian_of_tower R isArtinian_of_fg_of_artinian'
 
@@ -454,13 +465,9 @@ variable (R : Type*) [CommSemiring R] [IsArtinianRing R]
 
 @[stacks 00J7]
 lemma setOf_isMaximal_finite : {I : Ideal R | I.IsMaximal}.Finite := by
-  set Spec := {I : Ideal R | I.IsMaximal}
-  obtain ⟨_, ⟨s, rfl⟩, H⟩ := IsArtinian.set_has_minimal
-    (range (Finset.inf · Subtype.val : Finset Spec → Ideal R)) ⟨⊤, ∅, by simp⟩
+  have ⟨s, H⟩ := Finset.exists_inf_le (Subtype.val (p := fun I : Ideal R ↦ I.IsMaximal))
   refine Set.finite_def.2 ⟨s, fun p ↦ ?_⟩
-  classical
-  obtain ⟨q, hq1, hq2⟩ := p.2.isPrime.inf_le'.mp <| inf_eq_right.mp <|
-    inf_le_right.eq_of_not_lt (H (p ⊓ s.inf Subtype.val) ⟨insert p s, by simp⟩)
+  have ⟨q, hq1, hq2⟩ := p.2.isPrime.inf_le'.mp (H p)
   rwa [← Subtype.ext <| q.2.eq_of_le p.2.ne_top hq2]
 
 instance : Finite (MaximalSpectrum R) :=
@@ -469,6 +476,8 @@ instance : Finite (MaximalSpectrum R) :=
 
 end CommSemiring
 
+section CommRing
+
 variable {R : Type*} [CommRing R] [IsArtinianRing R]
 
 variable (R) in
@@ -546,4 +555,47 @@ noncomputable def equivPi [IsReduced R] : R ≃+* ∀ I : MaximalSpectrum R, R 
   .trans (.symm <| .quotientBot R) <| .trans
     (Ideal.quotEquivOfEq (nilradical_eq_zero R).symm) (quotNilradicalEquivPi R)
 
+theorem isSemisimpleRing_of_isReduced [IsReduced R] : IsSemisimpleRing R :=
+  (equivPi R).symm.isSemisimpleRing
+
+end CommRing
+
+section Ring
+
+variable {R : Type*} [Ring R] [IsArtinianRing R]
+
+theorem isSemisimpleRing_iff_jacobson : IsSemisimpleRing R ↔ Ring.jacobson R = ⊥ :=
+  IsArtinian.isSemisimpleModule_iff_jacobson R R
+
+instance : IsSemiprimaryRing R where
+  isSemisimpleRing :=
+    IsArtinianRing.isSemisimpleRing_iff_jacobson.mpr (Ring.jacobson_quotient_jacobson R)
+  isNilpotent := by
+    let Jac := Ring.jacobson R
+    have ⟨n, hn⟩ := IsArtinian.monotone_stabilizes ⟨(Jac ^ ·), @Ideal.pow_le_pow_right _ _ _⟩
+    have hn : Jac * Jac ^ n = Jac ^ n := by
+      rw [← Ideal.IsTwoSided.pow_succ]; exact (hn _ n.le_succ).symm
+    use n; by_contra ne
+    have ⟨N, ⟨eq, ne⟩, min⟩ := wellFounded_lt.has_min {N | Jac * N = N ∧ N ≠ ⊥} ⟨_, hn, ne⟩
+    have : Jac ^ n * N = N := n.rec (by rw [Jac.pow_zero, N.one_mul])
+      fun n hn ↦ by rwa [Jac.pow_succ, mul_assoc, eq]
+    let I x := Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
+    have hI x : I x ≤ Ideal.span {x} := by
+      rw [Ideal.span, LinearMap.span_singleton_eq_range]; exact LinearMap.map_le_range
+    have ⟨x, hx⟩ : ∃ x ∈ N, I x ≠ ⊥ := by
+      contrapose! ne
+      rw [← this, ← le_bot_iff, Ideal.mul_le]
+      refine fun ri hi rn hn ↦ ?_
+      rw [← ne rn hn]
+      exact ⟨ri, hi, rfl⟩
+    rw [← Ideal.span_singleton_le_iff_mem] at hx
+    have : I x = N := by
+      refine ((hI x).trans hx.1).eq_of_not_lt (min _ ⟨?_, hx.2⟩)
+      rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]
+    have : Ideal.span {x} = N := le_antisymm hx.1 (this.symm.trans_le <| hI x)
+    refine (this ▸ ne) ((Submodule.fg_span <| Set.finite_singleton x).eq_bot_of_le_jacobson_smul ?_)
+    rw [← Ideal.span, this, smul_eq_mul, eq]
+
+end Ring
+
 end IsArtinianRing

Mathlib/RingTheory/Artinian/Ring.lean

@@ -7,7 +7,6 @@ import Mathlib.Algebra.Field.Equiv
 import Mathlib.RingTheory.Artinian.Module
 import Mathlib.RingTheory.Localization.Defs
 import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
-import Mathlib.RingTheory.Nakayama
 
 /-!
 # Artinian rings
@@ -25,7 +24,7 @@ itself, or simply Artinian if it is both left and right Artinian.
   ring to any localization of itself is surjective.
 
 * `IsArtinianRing.isNilpotent_jacobson_bot`: the Jacobson radical of a commutative artinian ring
-  is a nilpotent ideal. (TODO: generalize to noncommutative rings.)
+  is a nilpotent ideal.
 
 ## Implementation Details
 
@@ -47,43 +46,12 @@ open Set Submodule IsArtinian
 
 namespace IsArtinianRing
 
-variable {R : Type*} [CommRing R] [IsArtinianRing R]
-
 @[stacks 00J8]
-theorem isNilpotent_jacobson_bot : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) := by
-  let Jac := Ideal.jacobson (⊥ : Ideal R)
-  let f : ℕ →o (Ideal R)ᵒᵈ := ⟨fun n => Jac ^ n, fun _ _ h => Ideal.pow_le_pow_right h⟩
-  obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → Jac ^ n = Jac ^ m := IsArtinian.monotone_stabilizes f
-  refine ⟨n, ?_⟩
-  let J : Ideal R := annihilator (Jac ^ n)
-  suffices J = ⊤ by
-    have hJ : J • Jac ^ n = ⊥ := annihilator_smul (Jac ^ n)
-    simpa only [this, top_smul, Ideal.zero_eq_bot] using hJ
-  by_contra hJ
-  change J ≠ ⊤ at hJ
-  rcases IsArtinian.set_has_minimal { J' : Ideal R | J < J' } ⟨⊤, hJ.lt_top⟩ with
-    ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → ¬I < J'⟩
-  rcases SetLike.exists_of_lt hJJ' with ⟨x, hxJ', hxJ⟩
-  obtain rfl : J ⊔ Ideal.span {x} = J' := by
-    apply eq_of_le_of_not_lt _ (hJ' (J ⊔ Ideal.span {x}) _)
-    · exact sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))
-    · rw [SetLike.lt_iff_le_and_exists]
-      exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩
-  have : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x} :=
-    sup_le_sup_left (smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _
-  have : Jac * Ideal.span {x} ≤ J := by -- Need version 4 of Nakayama's lemma on Stacks
-    by_contra H
-    refine H (Ideal.mul_le_left.trans (le_of_le_smul_of_le_jacobson_bot (fg_span_singleton _) le_rfl
-      (le_sup_right.trans_eq (this.eq_of_not_lt (hJ' _ ?_)).symm)))
-    exact lt_of_le_of_ne le_sup_left fun h => H <| h.symm ▸ le_sup_right
-  have : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥ := calc
-    Ideal.span {x} * Jac ^ (n + 1) = Ideal.span {x} * Jac * Jac ^ n := by
-      rw [pow_succ', ← mul_assoc]
-    _ ≤ J * Jac ^ n := mul_le_mul (by rwa [mul_comm]) le_rfl
-    _ = ⊥ := by simp [J]
-  refine hxJ (mem_annihilator.2 fun y hy => (mem_bot R).1 ?_)
-  refine this (mul_mem_mul (mem_span_singleton_self x) ?_)
-  rwa [← hn (n + 1) (Nat.le_succ _)]
+theorem isNilpotent_jacobson_bot {R} [Ring R] [IsArtinianRing R] :
+    IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) :=
+  Ideal.jacobson_bot (R := R) ▸ IsSemiprimaryRing.isNilpotent
+
+variable {R : Type*} [CommRing R] [IsArtinianRing R]
 
 lemma jacobson_eq_radical (I : Ideal R) : I.jacobson = I.radical := by
   simp_rw [Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal]

Mathlib/RingTheory/FiniteLength.lean

@@ -4,28 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
 import Mathlib.RingTheory.Artinian.Module
-import Mathlib.RingTheory.SimpleModule.Basic
 
 /-!
 # Modules of finite length
 
 We define modules of finite length (`IsFiniteLength`) to be finite iterated extensions of
 simple modules, and show that a module is of finite length iff it is both Noetherian and Artinian,
 iff it admits a composition series.
+
 We do not make `IsFiniteLength` a class, instead we use `[IsNoetherian R M] [IsArtinian R M]`.
 
-## Tag
+## Tags
 
 Finite length, Composition series
 -/
 
-universe u
-
 variable (R : Type*) [Ring R]
 
 /-- A module of finite length is either trivial or a simple extension of a module known
 to be of finite length. -/
-inductive IsFiniteLength : ∀ (M : Type u) [AddCommGroup M] [Module R M], Prop
+inductive IsFiniteLength : ∀ (M : Type*) [AddCommGroup M] [Module R M], Prop
   | of_subsingleton {M} [AddCommGroup M] [Module R M] [Subsingleton M] : IsFiniteLength M
   | of_simple_quotient {M} [AddCommGroup M] [Module R M] {N : Submodule R M}
       [IsSimpleModule R (M ⧸ N)] : IsFiniteLength N → IsFiniteLength M