of_isLocalization_maximal — Mathlib

English

Given a directed system of localized algebras indexed by maximal ideals, each integrally closed, the base ring is integrally closed.

Русский

Пусть дано семейство локализаций по максимальным идеалам, каждая интегрально замкнута; тогда основание замкнуто интегрально.

LaTeX

$$$\\forall P, IsIntegrallyClosed( R_p ) \\Rightarrow IsIntegrallyClosed(R).$$$

Lean4

theorem of_isLocalization_maximal [IsDomain R] (h : ∀ (P : Ideal R) [P.IsMaximal], IsIntegrallyClosed (Rₚ P)) :
    IsIntegrallyClosed R :=
  .of_localization_maximal
    (fun P _ _ ↦ .of_equiv <| ringEquivOfRingEquiv (Rₚ P) _ (RingEquiv.refl R) P.primeCompl.map_id)

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