English
A scheme is locally Noetherian if it can be covered by affine opens whose rings of global sections are Noetherian and relate properly under localization.
Русский
Схема локально Ноетерова, если она покрыта афинными открытыми, для которых кольца глобальных секций являются Ноетериновыми и их локализации согласованы.
LaTeX
$$$[\text{LocallyNoetherian}(X)] \iff \, \text{cover by affine opens with Noetherian globals}.$$$
Lean4
/-- If a scheme `X` has a cover by affine opens whose sections are Noetherian rings,
then `X` is locally Noetherian. -/
theorem isLocallyNoetherian_of_affine_cover {ι} {S : ι → X.affineOpens} (hS : (⨆ i, S i : X.Opens) = ⊤)
(hS' : ∀ i, IsNoetherianRing Γ(X, S i)) : IsLocallyNoetherian X :=
by
refine ⟨fun U => ?_⟩
induction U using of_affine_open_cover S hS with
| basicOpen U f hN =>
have := U.prop.isLocalization_basicOpen f
exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN
| openCover U s _ hN =>
apply isNoetherianRing_of_away s ‹_›
intro ⟨f, hf⟩
have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩
have := U.prop.isLocalization_basicOpen f
have hEq := IsLocalization.algEquiv (.powers f) (Localization.Away f) Γ(X, X.basicOpen f)
exact isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv
| hU => exact hS' _
