of_isLocalization_maximal — Mathlib

English

A semilocal ring is Noetherian if all localizations at maximal ideals are Noetherian.

Русский

Полусемильное кольцо конечно, если все локализации по максимальным идеалам конечно порожденны.

LaTeX

$$$\\text{IsNoetherianRing}(R) \\Leftarrow \\forall P [P.IsMaximal], \\text{IsNoetherianRing}(R_p)$$$

Lean4

/-- A semilocal ring `R` is Noetherian if
its localization at every maximal ideal is a Noetherian ring. -/
theorem of_isLocalization_maximal (H : ∀ (P : Ideal R) [P.IsMaximal], IsNoetherianRing (Rₚ P)) : IsNoetherianRing R
    where
  noetherian
    N :=
    Submodule.fg_of_isLocalized_maximal Rₚ Rₚ (fun P _ => Algebra.linearMap R (Rₚ P)) N fun _ _ ↦
      IsNoetherian.noetherian _

Похожие утверждения