Converse fails: Spec of a non-Noetherian valuation ring

Proved

NoetherianScheme.exists_valuationRing_noetherianSpace_not_isNoetherianScheme

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

algebraic-geometrynoetherian

There exists a valuation ring $R$ (an integral domain in which, for any two elements, one divides the other) such that

$R$ is not a Noetherian ring,
the underlying space of $\operatorname{Spec} R$ is a Noetherian topological space, and
$\operatorname{Spec} R$ is not a Noetherian scheme.

So the converse of "a Noetherian scheme is a Noetherian topological space" is false.

Formalization Note Not every non-Noetherian valuation ring works (a valuation ring of infinite rank has a non-Noetherian spectrum), so the source's "consider the spectrum of a non-Noetherian valuation ring" is encoded as an existence statement. The ring is taken in the lowest universe.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem exists_valuationRing_noetherianSpace_not_isNoetherianScheme :
    ∃ (R : Type) (_ : CommRing R) (_ : IsDomain R), ValuationRing R ∧ ¬ IsNoetherianRing R ∧
      TopologicalSpace.NoetherianSpace (Spec (CommRingCat.of R)) ∧
      ¬ IsNoetherianScheme (Spec (CommRingCat.of R)) := 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 3: "But the converse is false in general; consider, for example, the spectrum of a non-Noetherian valuation 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