Finite type over a Noetherian base is Noetherian

Proved

NoetherianScheme.isNoetherianScheme_of_finiteType

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

algebraic-geometrynoetherian

Let $f : X \to S$ be a morphism of schemes of finite type (locally of finite type and quasi-compact). If $S$ is Noetherian, then $X$ is Noetherian.

This covers the families $X \to S$ discussed in the source: schemes of finite type over a Noetherian base are Noetherian.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem isNoetherianScheme_of_finiteType {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (hS : IsNoetherianScheme S) :
    IsNoetherianScheme X := by sorry

end NoetherianScheme

Source

Wikipedia, "Noetherian scheme", revision 1372079294 (https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294), section "Examples / Locally of finite type over a Noetherian base": "families of schemes X → S where the base S is Noetherian and X is of finite type over S"; Stacks Project Lemma 28.5.7 / 29.15.6.

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