English
If X is locally Noetherian, then for every point x in X, the stalk O_{X,x} is a Noetherian ring.
Русский
Если X является локально Нётеровым, то для любой точки x схемы X локальная кольцо O_{X,x} является кольцом Нётерова.
LaTeX
$$$\\forall x\\in X\\,\\text{IsNoetherianRing}(\\mathcal{O}_{X,x})$$$
Lean4
instance [IsLocallyNoetherian X] {x : X} : IsNoetherianRing (X.presheaf.stalk x) :=
by
obtain ⟨U, hU, hU2, hU3⟩ := exists_isAffineOpen_mem_and_subset (U := ⊤) (x := x) (by aesop)
have := AlgebraicGeometry.IsAffineOpen.isLocalization_stalk hU ⟨x, hU2⟩
exact
@IsLocalization.isNoetherianRing _ _ (hU.primeIdealOf ⟨x, hU2⟩).asIdeal.primeCompl (X.presheaf.stalk x) _
(X.presheaf.algebra_section_stalk ⟨x, hU2⟩) this (IsLocallyNoetherian.component_noetherian ⟨U, hU⟩)
