Spec A is Noetherian iff A is Noetherian

Proved

NoetherianScheme.isNoetherianScheme_Spec_iff

by Lucas · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynoetherian

Let $A$ be a commutative ring. Then

\operatorname{Spec} A \text{ is a Noetherian scheme} \iff A \text{ is a Noetherian ring}.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem isNoetherianScheme_Spec_iff (A : Type u) [CommRing A] :
    IsNoetherianScheme (Spec (CommRingCat.of A)) ↔ IsNoetherianRing A := by sorry

end NoetherianScheme

Source

Wikipedia, "Noetherian scheme", revision 1372079294 (https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294), lead section, paragraph 2: "in particular, Spec A is a Noetherian scheme if and only if A is a Noetherian ring".

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph