The Hopkins–Levitzki theorem

Main results

• IsSemiprimaryRing.isNoetherian_iff_isArtinian: the Hopkins–Levitzki theorem, which states that for a module over a semiprimary ring (in particular, an Artinian ring), IsNoetherian is equivalent to IsArtinian (and therefore also to IsFiniteLength).

• In particular, for a module over an Artinian ring, Module.Finite, IsNoetherian, IsArtinian, and IsFiniteLength are all equivalent (IsArtinianRing.tfae), and a (left) Artinian ring is also (left) Noetherian.

• isArtinianRing_iff_isNoetherianRing_krullDimLE_zero: a commutative ring is Artinian iff it is Noetherian with Krull dimension at most 0.

Reference

• [F. Lorenz, Algebra: Volume II: Fields with Structure, Algebras and Advanced Topics][Lorenz2008]

theorem IsSemiprimaryRing.isNoetherian_iff_isArtinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] : IsNoetherian R M ↔ IsArtinian R M

theorem IsArtinianRing.tfae (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] : [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE

theorem isArtinianRing_iff_isFiniteLength (R : Type u_1) [Ring R] : IsArtinianRing R ↔ IsFiniteLength R R

Stacks Tag 00JB (A ring is Artinian if and only if it has finite length as a module over itself.)

instance instIsNoetherianRingOfIsArtinianRing (R : Type u_1) [Ring R] [IsArtinianRing R] : IsNoetherianRing R

Stacks Tag 00JB (A ring is Artinian if and only if it has finite length as a module over itself. Any such ring is both Artinian and Noetherian.)

theorem isNoetherian_of_finite_isArtinian (M : Type u_2) [AddCommGroup M] {R : Type u_3} [CommRing R] [Module R M] [Module.Finite R M] [IsArtinian R M] : IsNoetherian R M

A finitely generated Artinian module over a commutative ring is Noetherian. This is not necessarily the case over a noncommutative ring, see https://mathoverflow.net/a/61700.

theorem IsNoetherianRing.isArtinianRing_of_krullDimLE_zero {R : Type u_3} [CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 0 R] : IsArtinianRing R

theorem isArtinianRing_iff_isNoetherianRing_krullDimLE_zero {R : Type u_3} [CommRing R] : IsArtinianRing R ↔ IsNoetherianRing R ∧ Ring.KrullDimLE 0 R

Stacks Tag 00KH