Locally finite type over locally Noetherian is locally Noetherian

Proved

NoetherianScheme.isLocallyNoetherianScheme_of_locallyOfFiniteType

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

algebraic-geometrynoetherian

Let $f : X \to S$ be a morphism of schemes that is locally of finite type (for affine opens $V = \operatorname{Spec} B \subseteq S$ and $U = \operatorname{Spec} A \subseteq f^{-1}(V)$ , $A$ is a finitely generated $B$ -algebra). If $S$ is locally Noetherian, then $X$ is locally Noetherian.

Preamble

import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField

Formal statement

namespace NoetherianScheme

theorem isLocallyNoetherianScheme_of_locallyOfFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (hS : IsLocallyNoetherianScheme S) :
    IsLocallyNoetherianScheme 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", reference [5] = Stacks Project Lemma 29.15.6 (Tag 01T6): "Let f : X → S be a morphism. If S is locally Noetherian and f locally of finite type then X is locally Noetherian."

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