English
An integral domain R is integrally closed if there exists a collection of prime localizations whose intersection recovers R and each localized ring is integrally closed.
Русский
Интегральная область R замкнута, если существует набор локализаций по пprime и их пересечение даёт R, причём каждая локализация интегрально замкнута.
LaTeX
$$$\\text{If } R \\text{ is a domain and there is a family } \\{R_p\\}_{p \\in \\mathcal P}\\text{ of localizations with } \\bigcap_p R_p = R \\text{ and each } R_p \\text{ integrally closed, then } R \\text{ is integrally closed.}$$$
Lean4
/-- An integral domain $R$ is integrally closed if there exists a set of prime ideals $S$ such that
$\bigcap_{\mathfrak{p} \in S} R_{\mathfrak{p}} = R$ and for every $\mathfrak{p} \in S$,
$R_{\mathfrak{p}}$ is integrally closed. -/
theorem of_localization [IsDomain R] (S : Set (PrimeSpectrum R))
(h : ∀ p ∈ S, IsIntegrallyClosed (Localization.AtPrime p.1))
(hs : ⨅ p ∈ S, (Localization.subalgebra (FractionRing R) p.1.primeCompl p.1.primeCompl_le_nonZeroDivisors) = ⊥) :
IsIntegrallyClosed R :=
by
apply
IsIntegrallyClosed.of_localization_submonoid (fun p : S ↦ p.1.1.primeCompl)
(fun p ↦ p.1.1.primeCompl_le_nonZeroDivisors) (fun p ↦ h p.1 p.2)
ext x
simp only [← hs, Algebra.mem_iInf, Subtype.forall]
