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.induction (R₀ : Type u_1) (R : Type u_2) (M : Type u) [Ring R₀] [Ring R] [Module R₀ R] [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemiprimaryRing R] {P : (M : Type u) → [inst : AddCommGroup M] → [inst_1 : Module R₀ M] → [inst : Module R M] → Prop} (h0 : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M] [inst_4 : IsSemisimpleModule R M], Module.IsTorsionBySet R M ↑(Ring.jacobson R) → P M) (h1 : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R₀ M] [inst_2 : Module R M] [inst_3 : IsScalarTower R₀ R M], let N := Ring.jacobson R • ⊤; P ↥N → P (M ⧸ N) → P M) : P M

theorem IsSemiprimaryRing.finite_of_isNoetherian (R₀ : Type u_1) (R : Type u_2) (M : Type u) [Ring R₀] [Ring R] [Module R₀ R] [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemiprimaryRing R] [IsScalarTower R₀ R R] [Module.Finite R₀ (R ⧸ Ring.jacobson R)] [IsNoetherian R M] : Module.Finite R₀ M

theorem IsSemiprimaryRing.finite_of_isArtinian (R₀ : Type u_1) (R : Type u_2) (M : Type u) [Ring R₀] [Ring R] [Module R₀ R] [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemiprimaryRing R] [IsScalarTower R₀ R R] [Module.Finite R₀ (R ⧸ Ring.jacobson R)] [IsArtinian R M] : Module.Finite R₀ M

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

theorem IsArtinianRing.tfae (R : Type u_2) (M : Type u) [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_2) [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_2) [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) [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