Noetherian ⇔ locally Noetherian and quasi-compact

Proved

NoetherianScheme.isNoetherianScheme_iff_isLocallyNoetherianScheme_and_compactSpace

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

algebraic-geometrynoetherian

Let $X$ be a scheme. Then

X \text{ is Noetherian} \iff X \text{ is locally Noetherian and } X \text{ is (quasi-)compact}.

Here "Noetherian" means covered by finitely many open affines with Noetherian rings of sections, and "locally Noetherian" means covered by (possibly infinitely many) such open affines.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem isNoetherianScheme_iff_isLocallyNoetherianScheme_and_compactSpace (X : Scheme.{u}) :
    IsNoetherianScheme X ↔ IsLocallyNoetherianScheme X ∧ CompactSpace 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 1: "Thus, a scheme is Noetherian if and only if it is locally Noetherian and compact."

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