English
If R is Noetherian and the Krull dimension satisfies KrullDimLE 0 over R, then R is Artinian.
Русский
Если R Noetherian и KrullDim≤0, то R Artinian.
LaTeX
$$$$\text{If } [\text{CommRing } R], [\text{IsNoetherianRing } R], \text{ and } \text{Ring.KrullDimLE } 0 R, \text{ then } \text{IsArtinianRing } R.$$$$
Lean4
theorem isArtinianRing_of_krullDimLE_zero {R} [CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 0 R] :
IsArtinianRing R :=
have eq := Ring.jacobson_eq_nilradical_of_krullDimLE_zero R
let Spec := {I : Ideal R | I.IsPrime}
have : Finite Spec := (minimalPrimes.finite_of_isNoetherianRing R).subset Ideal.mem_minimalPrimes_of_krullDimLE_zero
have (I : Spec) : I.1.IsPrime := I.2
have (I : Spec) : IsSemisimpleRing (R ⧸ I.1) :=
let _ := Ideal.Quotient.field I.1;
inferInstance
have : IsSemisimpleRing (R ⧸ Ring.jacobson R) :=
by
rw [eq, nilradical_eq_sInf, sInf_eq_iInf']
exact
(Ideal.quotientInfRingEquivPiQuotient _ fun I J ne ↦
Ideal.isCoprime_of_isMaximal <| Subtype.coe_ne_coe.mpr ne).symm.isSemisimpleRing
have : IsSemiprimaryRing R := ⟨this, eq ▸ IsNoetherianRing.isNilpotent_nilradical R⟩
IsSemiprimaryRing.isNoetherian_iff_isArtinian.mp ‹_›
