Local rings of a locally Noetherian scheme are Noetherian

Proved

NoetherianScheme.isNoetherianRing_stalk

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

algebraic-geometrynoetherian

Let $X$ be a locally Noetherian scheme and $x \in X$ a point. Then the local ring

\mathcal O_{X,x} = \varinjlim_{x \in V} \mathcal O_X(V)

(the stalk of the structure sheaf at $x$ ) is a Noetherian ring.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem isNoetherianRing_stalk (X : Scheme.{u}) (hX : IsLocallyNoetherianScheme X) (x : X) :
    IsNoetherianRing (X.presheaf.stalk x) := 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: "For a locally Noetherian scheme X, the local rings O_{X,x} are also Noetherian rings."

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