English
For a local Noetherian ring R, Artinian is equivalent to the maximal ideal being nilpotent: IsArtinianRing R ⇔ IsNilpotent (IsLocalRing.maximalIdeal R).
Русский
Для локального кольца R, Noetherian, Artinian ⇔ максимальная идеал R нильпотентен.
LaTeX
$$$$\operatorname{IsArtinianRing} R \iff \operatorname{IsNilpotent}(\operatorname{IsLocalRing.maximalIdeal} R).$$$$
Lean4
theorem isArtinianRing_iff_isNilpotent_maximalIdeal (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] :
IsArtinianRing R ↔ IsNilpotent (IsLocalRing.maximalIdeal R) :=
by
rw [isArtinianRing_iff_krullDimLE_zero, Ideal.FG.isNilpotent_iff_le_nilradical (IsNoetherian.noetherian _), ←
and_iff_left (a := Ring.KrullDimLE 0 R) ‹IsLocalRing R›,
(Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 3 rfl rfl, IsLocalRing.isMaximal_iff, le_antisymm_iff,
and_iff_right]
exact IsLocalRing.le_maximalIdeal (by simp [nilradical, Ideal.radical_eq_top])
