Affine opens of a locally Noetherian scheme have Noetherian sections

Proved

NoetherianScheme.isNoetherianRing_of_mem_affineOpens

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

algebraic-geometrynoetherian

Let $X$ be a locally Noetherian scheme and let $U \subseteq X$ be any open affine subset (so $U \cong \operatorname{Spec} A$ with $A = \Gamma(X,U)$ ). Then

A = \Gamma(X,U) \text{ is a Noetherian ring.}

The point is that $U$ need not be one of the affines in a cover witnessing local Noetherianity.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem isNoetherianRing_of_mem_affineOpens (X : Scheme.{u}) (hX : IsLocallyNoetherianScheme X)
    (U : X.Opens) (hU : U ∈ X.affineOpens) : IsNoetherianRing Γ(X, U) := 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 a locally Noetherian scheme, if Spec A ⊆ X is an open affine subset, then 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