English
If a domain R is such that R localized at every maximal ideal is integrally closed, then R is integrally closed.
Русский
Если для любой максимальной идеальной локализации R, локализация R на мажорной идее интегрально замкнута, то сама R интегрально замкнута.
LaTeX
$$$(\\forall \\mathfrak m \\text{ maximal})\\ IsIntegrallyClosed( Localization.AtPrime( \\mathfrak m ) ) \\Rightarrow IsIntegrallyClosed(R).$$$
Lean4
/-- An integral domain `R` is integral closed if `Rₘ` is integral closed
for any maximal ideal `m` of `R`. -/
theorem of_localization_maximal [IsDomain R]
(h : ∀ p : Ideal R, p ≠ ⊥ → [p.IsMaximal] → IsIntegrallyClosed (Localization.AtPrime p)) : IsIntegrallyClosed R :=
by
by_cases hf : IsField R
· exact hf.toField.instIsIntegrallyClosed
refine of_localization (.range MaximalSpectrum.toPrimeSpectrum) (fun _ ↦ ?_) ?_
· rintro ⟨p, rfl⟩
exact h p.asIdeal (Ring.ne_bot_of_isMaximal_of_not_isField p.isMaximal hf)
· rw [iInf_range]
convert MaximalSpectrum.iInf_localization_eq_bot R (FractionRing R)
rw [subalgebra.ofField_eq, MaximalSpectrum.toPrimeSpectrum]
