Morphisms from a Noetherian scheme are quasi-compact

Proved

NoetherianScheme.quasiCompact_of_isNoetherianScheme

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

algebraic-geometrynoetherian

Let $f : X \to S$ be any morphism of schemes with $X$ Noetherian. Then $f$ is quasi-compact: for every quasi-compact open $V \subseteq S$ , the preimage $f^{-1}(V)$ is quasi-compact.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem quasiCompact_of_isNoetherianScheme {X S : Scheme.{u}} (f : X ⟶ S)
    (hX : IsNoetherianScheme X) : QuasiCompact f := by sorry

end NoetherianScheme

Source

Wikipedia, "Noetherian scheme", revision 1372079294 (https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294), section "Properties and Noetherian hypotheses": "Every morphism from a Noetherian scheme X → S is quasi-compact." [2] = Stacks Project Lemma 28.5.8 (Tag 01P0).

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