English
If there exists a family of submonoids S_i of R such that each localized algebra Localization(S_i) is integrally closed, and the infimum of the corresponding subalgebras equals the bottom, then R is integrally closed.
Русский
Пусть существует семейство подмоноидов S_i ⊆ R так, что локализации Localization(S_i) интегрально замкнуты, и соответствующий инфимум подалгебр равен нижнему пределу; тогда R интегрально замкнута.
LaTeX
$$$\\Big( \\forall i, IsIntegrallyClosed( Localization(S_i) ) \\Big) \\land \\big( \\inf_i Localization.subalgebra( FractionRing R ) (S_i) = ⊥ \\big) \\Rightarrow IsIntegrallyClosed(R).$$$
Lean4
theorem of_localization_submonoid [IsDomain R] {ι : Type*} (S : ι → Submonoid R) (h : ∀ i : ι, S i ≤ R⁰)
(hi : ∀ i : ι, IsIntegrallyClosed (Localization (S i)))
(hs : ⨅ i : ι, Localization.subalgebra (FractionRing R) (S i) (h i) = ⊥) : IsIntegrallyClosed R :=
IsIntegrallyClosed.of_iInf_eq_bot (fun i ↦ Localization.subalgebra (FractionRing R) (S i) (h i))
(fun i ↦ (hi i).of_equiv (IsLocalization.algEquiv (S i) (Localization (S i)) _).toRingEquiv) hs
